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

6.3 Deciding Ideal Membership

Finally, we can compile the results above to define a decision procedure for ideal
membership. This procedure just checks whether a given polynomial reduces to
0 with respect to the Grobner basis returned by Buchberger's algorithm.

(defun<k> imdp (p F)
(equal (red* p (Buchberger F)) (|0|)))

red ∗ G Theorem 2. G = Buchberger ( F )= ⇒ ( p ∈F⇐⇒ ( p )=0) .

The Acl2 theorem stating the soundness and completeness of the decision
procedure follows, as an easy consequence of the correctness of Buchberger and
the theorem |Phi(F) => (p in <F> <=> red*(p, F) = 0)| in Sect. 5.

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

In this context, the theorem |Phi(F) => (p in <F> <=> red*(p, F) = 0)|
is used by functional instantiation, replacing F by (lambda () (Buchberger F))
and s-polynomial-proof by |Phi(Buchberger(F))|-proof .
Note that all the functions used in the definition of the decision procedure are
executable and therefore the procedure is also executable. Note also that we do
not mention operators or proofs, neither when defining the decision procedure
nor when stating its correctness. These are only intermediate concepts, which
make reasoning more convenient.

7 Conclusions

We have shown how it is possible to use the Acl2 system in the formal develop-
ment of Computer Algebra algorithms by presenting a verified implementation
of Buchberger's algorithm and a verified decision procedure for the ideal mem-
bership problem. It is interesting to point out that all the theory needed to prove
the correctness of the algorithm has been developed in the Acl2 logic, in spite
of its (apparently) limited expressiveness.
We have benefited from work previously done in the system. In particular,
all the results about abstract reductions were originally developed for a formal-
ization of rewriting systems [11]. We believe that this is a good example of how
seemingly unrelated formalizations can be reused in other projects, provided the
system offers a minimal support for it. However, we feel that Acl2 could be
improved to provide more comfortable mechanisms for functional instantiation
and for abstraction in general. Encapsulation provides a good abstraction mech-
anism but functionally instantiating each encapsulated theorem is a tedious and
error-prone task. Recently, several proposals have been formulated (e.g. poly-
morphism and abstract data types) to cope with this problem in Acl2 6 .A
graphical interface to visualize proof trees would be helpful too.

6 A similar modularity issue has been reported in the Coq system too [13].