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

normal form is not zero, then this normal form can be added to the basis. This
makes it reducible to zero (without changing the ideal), but new s-polynomials
are introduced that have to be checked. This completion processisiterateduntil
all the s-polynomials of the current basis are reducible to zero.
In order to formalize an executable implementation of Buchberger's algorithm
in Acl2, several helper functions are needed. The function initial-pairs re-
turns all the ordered pairs from the elements of a list. The main function com-
putes the initial pairs from a basis and starts the real computation process.

(defun Buchberger (F)
(Buchberger-aux F (initial-pairs F)))

Next, the function that computes a Grobner basis from an initial basis is
defined. This function takes the initial basis and a list of pairs as its input. The
function pairs returns the ordered pairs built from its first argument and every
element in its second argument. As all Acl2 functions must be total and we
need to deal with polynomials with a fixed set of variables to ensure termination
of the function, we have to explicitly check that the arguments remain in the
correct domain. We will comment more about these “type conditions” in Sect. 7.

(defun<k> Buchberger-aux (F C)
(if (and (naturalp k) (k-polynomialsp F) (k-polynomial-pairsp C))
(if (endp C)
F
(let* ((p (first (first C))) (q (second (first C)))
(h (red* (s-poly p q) F)))
(if (equal h (|0|))
(Buchberger-aux F (rest C))
(Buchberger-aux (cons h F) (append (pairs h F) (rest C))))))

F))

A measure has to be supplied to prove the termination of the above function,
so that it can be admitted by the principle of definition. The following section
explains this issue.

6.1 Termination

Termination of Buchberger's algorithm can be proved using a lexicographic mea-
sure on its arguments. This is justified by the following observations:

1. In the first recursive branch, the first argument keeps unmodified while the
second argument structurally decreases since one of its elements is removed.
2. In the second recursive branch, the first argument decreases in a certain
well-founded sense despite of the inclusion of a new polynomial. This is a
consequence of Dickson's lemma.

Lemma 1 (Dickson). Let k ∈ IN and m 1 ,m 2 ,... an infinite sequence of mono-

mials with k variables. Then, there exist indices i<j such that m i divides m j .