Information Technology Reference

In-Depth Information

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.

Search WWH ::

Custom Search