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

The notion of normal form of a polynomial can be easily defined in our
framework. First, we define a function reducible , implementing a reducibility
test: when applied to a polynomial p and to a list of polynomials F , it returns
a valid operator, whenever it exists, or nil otherwise. The following theorems
state the main properties of reducible :

(defthm |reducible(p, F) => validp(p, reducible(p, F), F)|
(implies (reducible p F)
(validp p (reducible p F) F)))

(defthm |~reducible(p, F) => ~validp(p, o, F)|
(implies (not (reducible p F))
(not (validp p o F))))

Now it is easy to define a function nf that computes a normal form of a given
polynomial with respect to the reduction relation induced by a given list of poly-
nomials. This function is simple: it iteratively tests reducibility and applies valid
operators until an irreducible polynomial is found. Note that termination is guar-
anteed by the Noetherianity of the reduction relation and the well-foundedness
of the polynomial ordering.

(defun<k> nf (p F)
(if (and (k-polynomialp p) (k-polynomialsp F))
(let ((red (reducible p F)))
(if red (nf (reduction p red) F) p))

p))

The following theorems establish that, in fact, nf computes normal forms.
Again, in order to prove that p → F nf F ( p ), we have to explicitly define a func-
tion |p ->F* nf(p, F)|-proof which construct a proof justifying this. This
function is easily defined by collecting the operators returned by reducible .

(defthm |p ->F* nf(p, F)|
(let ((proof (|p ->F* nf(p, F)|-proof p F)))
(implies (and (k-polynomialp p) (k-polynomialsp F))
(->* p (nf p F) proof F))))

(defthm |nf(p, F) irreducible|
(implies (and (k-polynomialp p) (k-polynomialsp F))
(not (validp (nf p F) o F))))

Although nf is suitable for reasoning about normal form computation, it is
not suitable for being used by an implementation of Buchberger's algorithm: for
example, nf explicitly deals with operators, which are a concept of theoretical
nature. At this point, we talk about the polynomial reduction function red F
used in Buchberger's algorithm. This function (whose definition we omit) do not
make any use of operators but is modeled from the closure of the set extension
of another function, red , which takes two polynomials as its input and returns
the result of reducing the first polynomial with respect to the second one. The
following theorem shows the equivalence between nf and red F :

F