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

If we consider the sequence of terms consisting of the leader terms of the
polynomials added to the first argument, Dickson's lemma implies termination
of Buchberger's algorithm. This is because the polynomial added to the basis,
h , is not 0 and it cannot be reduced by F . Consequently, its leader term is not
divisible by any of the leader terms of the polynomials in F .
Dickson's lemma has been formalized in Acl2 in [7] and [12]. In both cases
it has been proved by providing an ordinal measure on finite sequences of terms
such that this measure decreases every time a new term not divisible by any of
the previous terms in the sequence is added.
We have defined a measure along these lines to prove the termination of
Buchberger's algorithm. In fact, our measure is defined on top of the measures
used to prove Dickson's lemma in [7, 12], lexicographically combined with the
length of the second argument. Although both proofs of Dickson's lemma are
based on totally different ideas, the results obtained can be used interchangeably
in our formalization.

6.2 Partial Correctness

In order to show that Buchberger computes a Grobner basis, and taking into ac-
count the results of the previous section, we just have to prove that p ∈F⇐⇒
p ∈ and that Buchberger ( F )satisfies Φ . The following Acl2

theorems establish these two properties:

Buchberger ( F )

(defthm |<Buchberger(F)> = <F>|
(implies (and (k-polynomialp p) (k-polynomialsp F))
(iff (in<> p (Buchberger F)) (in<> p F))))

(defthm |Phi(Buchberger(F))|
(let ((G (Buchberger F)) (proof (|Phi(Buchberger(F))|-proof p q F)))
(implies (and (k-polynomialp p) (k-polynomialp q) (k-polynomialsp F)
(in<> p G) (in<> q G))
(->* (s-poly p q) (|0|) proof G))))

The statement of this last theorem deserves some comments. Our Acl2 for-
mulation of Th. 1 defines the property Φ ( F ) as the existence of a function such
that for every s-polynomial of F , it computes a sequence of proof steps justi-
fying its reduction to (|0|) (assumption |Phi(F)| in the encapsulate of the
previous section). Thus, if we want to establish the property Φ for a particular
basis (the basis returned by Buchberger in this case), we must explicitly define
such function and prove that it returns the desired proofs for every s-polynomial
of the basis. In this case the function is called |Phi(Buchberger(F))|-proof .
For the sake of brevity, we omit the definition of this function, but it is very
interesting to point out that it is based in a recursion scheme very similar to
the recursive definition of Buchberger-aux . This function collects, every time a
new s-polynomial is examined, the corresponding proof justifying its reduction
to the zero polynomial.