Information Technology Reference

In-Depth Information

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

Search WWH ::

Custom Search