Verified Computer Algebra in ACL2 - Artificial Intelligence and Symbolic Computation - page 171

Verified Computer Algebra in A CL 2
(Grobner Bases Computation)

I. Medina-Bulo 1 , F. Palomo-Lozano 1 ,
J.A. Alonso-Jimenez 2 , and J.L. Ruiz-Reina 2

1 Depto. de Lenguajes y Sistemas Informaticos, Univ. de Cadiz
E.S. de Ingenierıa de Cadiz, C/ Chile, s/n, 11003 Cadiz, Espana
{ inmaculada.medina,francisco.palomo } @uca.es
2 Depto. de Ciencias de la Computacion e Inteligencia Artificial, Univ. de Sevilla
E.T.S. de Ingenierıa Informatica, Avda. Reina Mercedes, s/n, 41012 Sevilla, Espana
{ jalonso,jruiz } @us.es

Abstract. In this paper, we present the formal verification of a Com-
mon Lisp implementation of Buchberger's algorithm for computing
Grobner bases of polynomial ideals. This work is carried out in the Acl2
system and shows how verified Computer Algebra can be achieved in an
executable logic.

1 Introduction

Computer Algebra has experienced a great development in the last decade, as
can be seen from the proliferation of Computer Algebra Systems (CAS). These
systems are the culmination of theoretical results obtained in the last half cen-
tury. One of the main achievements is due to B. Buchberger. In 1965 he devised
an algorithm for computing Grobner bases of multivariate polynomial ideals,
thus solving the ideal membership problem for polynomial rings. Currently, his
algorithm is available in most CAS and its theory, implementation and numerous
applications are widely documented in the literature, e.g. [2, 4].
The aim of this paper is to describe the formal verification of a naive Com-
mon Lisp implementation of Buchberger's algorithm. The implementation and
formal proofs have been carried out in the Acl2 system, which consists of a pro-
gramming language, a logic for stating and proving properties of the programs,
and a theorem prover supporting mechanized reasoning in the logic.
The importance of Buchberger's algorithm in Computer Algebra justifies on
its own the effort of obtaining a formal correctness proof with a theorem prover,
and this is one of the motivations for this work. Nevertheless, this goal has
already been achieved by L. Thery in [13], where he gives a formal proof using
the Coq system and explains how an executable implementation in the Ocaml
language is extracted from the algorithm defined in Coq. In contrast, in Acl2
we can reason directly about the Lisp program implementing the algorithm, i.e.
about the very program which is executed by the underlying Lisp system. There
is a price to pay: the logic of Acl2 is a quantifier-free fragment of first-order