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

Little work has been done on the machine verification of Buchberger's al-
gorithm. As we mentioned in the introduction, the most relevant is the work
of L. Thery [13] in Coq.T.CoquandandH.Persson[3]reportanincomplete
integrated development in Martin-Lof's type theory using Agda.Thereisalsoa
Mizar project [10] to formalize Grobner bases. The main difference between our
approach and these works is the underlying logic. All these logics are very differ-
ent from Acl2, which is more primitive, basically an untyped and quantifier-free
logic of total recursive functions, and makes no distinction between the program-
ming and the specification languages. In exchange, a high degree of automation
can be achieved and executability is obtained for free.
We think that an advantage of our approach is that the implementation
presented is compliant with Common Lisp, a real programming language, and
can be directly executed in Acl2 or in any compliant Common Lisp.Thisis
not the case of other systems, where the logic is not executable at all or the code
has to be extracted by unverified means. Taking into account that Lisp is the
language of choice for the implementation of CAS, like Macsyma and Axiom,
this is not just a matter of theoretical importance but also a practical one.
Our formal proof differs from Thery's. First, it is based on [1] instead of [4].
Second, we prove that Φ implies local-confluence instead of confluence: compare
this with the proof of SpolyImpConf in [13]. Differences extend also to defi-
nitions, e.g. ideals and confluence, mainly motivated by the lack of existential
quantification. Finally, [13] uses a non-constructive proof of Dickson's lemma by
L. Pottier 7 . Our termination argument uses a proof of Dickson's lemma obtained
by an ordinal embedding in 0 , the only well-founded structure known to Acl2.
We would like to remark that although polynomial properties seem trivial to
prove, this is not the case [8, 9]. It seems that this is not due to the simplicity
of the Acl2 logic. In [10] the authors recognize that it was challenging to prove
the associativity of polynomial multiplication in Mizar, a system devoted to the
formalization of mathematics. They were amazed by the fact that, in well-known
Algebra treatises, these properties are usually reduced to the univariate case or
their proofs are partially sketched and justified “by analogy”. In some cases,
the proofs are even left as an exercise. In the same way, the author of [13] had
to devote a greater effort to polynomials due to problems arising during their
formalization in Coq.
As for the user interaction required, we provided 169 definitions and 560
lemmas to develop a theory of polynomials (although this includes more than
the strictly needed here) and 109 definitions and 346 lemmas for the theory of
Grobner bases and Buchberger's algorithm. All these lemmas are proved almost
automatically. It is worth pointing out that of the 333 lemmas proved by induc-
tion, only 24 required a user-supplied induction scheme. Other lemmas needed a
hint about the convenience of using a given instance of another lemma or keep-
ing a function definition unexpanded. Only 9 functions required a hint for their
termination proofs. Thus, the main role of the user is to provide the suitable
sequence of definitions and lemmas to achieve the final correctness theorem.
7 A new proof of Dickson's lemma in Coq by H. Persson has been proposed later.