Verified Computer Algebra in ACL2 (Gröbner Bases Computation)

Verified Computer Algebra in ACL2 (Gr¨obner Bases Computation) I. Medina-Bulo1, F. Palomo-Lozano1, J.A. Alonso-Jim´enez2, and J.L. Ruiz-Reina2 1Depto. de Lenguajes y Sistemas Inform´aticos, Univ. de C´adiz E.S. de Ingenier´ıa de C´adiz, C/ Chile, s/n, 11003 C´adiz, Espa˜na {inmaculada.medina,francisco.palomo}@uca.es 2Depto. de Ciencias de la Computaci´on e Inteligencia Artificial, Univ. de Sevilla E.T.S. de Ingenier´ıa Inform´atica, Avda. Reina Mercedes, s/n, 41012 Sevilla, Espa˜na {jalonso,jruiz}@us.es Abstract. In this paper, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gr¨obner bases of polynomial ideals. This work is carried out in the Acl2 system and shows how verified Computer Algebra can be achieved in an executable logic. 1 Introduction Computer Algebra has experienced a great development in the last decade, as can be seen from the proliferation of Computer Algebra Systems (CAS). These systems are the culmination of theoretical results obtained in the last half century. One of the main achievements is due to B. Buchberger. In 1965 he devised an algorithm for computing Gr¨obner bases of multivariate polynomial ideals, thus solving the ideal membership problem for polynomial rings. Currently, his algorithm is available in most CAS and its theory, implementation and numerous applications are widely documented in the literature, e.g. [2, 4]. The aim of this paper is to describe the formal verification of a naive Common Lisp implementation of Buchberger’s algorithm. The implementation and formal proofs have been carried out in the Acl2 system, which consists of a programming language, a logic for stating and proving properties of the programs, and a theorem prover supporting mechanized reasoning in the logic. The importance of Buchberger’s algorithm in Computer Algebra justifies on its own the effort of obtaining a formal correctness proof with a theorem prover, and this is one of the motivations for this work. Nevertheless, this goal has already been achieved by L. Th´ery in [13], where he gives a formal proof using the Coq system and explains how an executable implementation in the Ocaml language is extracted from the algorithm defined in Coq. In contrast, in Acl2 we can reason directly about the Lisp program implementing the algorithm, i.e. about the very program which is executed by the underlying Lisp system. There is a price to pay: the logic of Acl2 is a quantifier-free fragment of first-order logic, less expressive1than the logic of Coq, which is based on type theory. We show how it is possible to formalize all the needed theory within the Acl2 logic. The formal proofs developed in Acl2 are mainly adapted from Chap. 8 of [1]. As the whole development consists of roughly one thousand Acl2 theorems and function definitions, we will only scratch its surface presenting the main results and a sketch of how the pieces fit together. We will necessarily omit many details that, we expect, can be inferred from the context. 2 The Acl2 System Acl2 formalizes an applicative subset of Common Lisp. In fact, the same language, based on prefix notation, is used for writing Lisp code and stating theorems about it2. The logic is a quantifier-free fragment of first-order logic with equality. It includes axioms for propositional logic and for a number of Lisp functions and data types. Inference rules include those for propositional calculus, equality and instantiation (variables in formulas are implicitly universally quantified). One important inference rule is the principle of induction,thatpermits proofs by well-founded induction on the ordinal 0(the logic provides a constructive definition of the ordinals up to 0). By the principle of definition new function definitions are admitted as axioms (using defun) only if its termination is proved by means of an ordinal measure in which the arguments of each recursive call, if any, decrease. In addition, the encapsulation principle allows the user to introduce new function symbols (using encapsulate) that are constrained to satisfy certain assumptions. To ensure that the constraints are satisfiable, the user must provide a witness function with the required properties. Within the scope of an encapsulate, properties stated as theorems need to be proved for the witnesses; outside, these theorems work as assumed axioms. Together, encapsulation and the derived inference rule, functional instantiation, provide a second-order aspect [5, 6]: theorems about constrained functions can be instantiated with function symbols if they are proved to have the same properties. The Acl2 theorem prover mechanizes the logic, being particularly well suited for obtaining automated proofs based on simplification and induction. Although the prover is automatic in the sense that once a proof attempt is started (with defthm) the user can no longer interact, nevertheless it is interactive in a deeper sense: usually, the role of the user is to lead the prover to a preconceived handproof, by proving a suitable collection of lemmas that are used as rewrite rules in subsequent proofs (these lemmas are usually discovered by the user after the inspection of failed proofs). We used this kind of interaction to obtain the formal proofs presented here. For a detailed description of Acl2, we refer the reader to the Acl2 book [5]. 1Nevertheless, the degree of automation of the Acl2 theorem prover is higher than in other systems with more expressive logics. 2Although we are aware that prefix notation may be inconvenient for people not used to Lisp, we will maintain it to emphasize the use of a real programming language. 3 Polynomial Rings and Ideals Let R=K[x1,...,x k] be a polynomial ring on an arbitrary commutative field K,wherek∈IN. The elements of Rare polynomials in the indeterminates x1,...,x kwith the coefficients in K. Polynomials are built from monomials of R, that is, power products like c·xa1 1···xak k,wherec∈Kis the coefficient, xa1 1···xak kis the term, and a1,...,a k∈IN . Therefore, there are several algebraic structures that it is necessary to formalize prior to the notion of polynomial. A computational theory of multivariate polynomials on a coefficient field was developed in [8, 9]. This Acl2 formalization includes common operations and fundamental properties establishing a ring structure. The aim was to develop a reusable library on polynomials. Regarding polynomial representation, we have used a sparse, normalized and uniform representation. That is, having fixed the number of variables, a canonical form can be associated to each polynomial. In this canonical representation all monomials are arranged in a strictly decreasing order, there are no null monomials and all of them have the same number of variables. The main advantage of this representation arises when deciding equality [9]. Monomial lists are used as the internal representation of polynomials. Monomials are also lists consisting of a coefficient and a term. Having selected a set of variables and an ordering on them, each term is uniquely represented by a list of natural numbers. Although most of the theory is done for an arbitrary field, via the encapsulation principle, we use polynomials over the field of rational numbers for our implementation of Buchberger’s algorithm. This alleviates some proofs at the cost of some generality, as Acl2 can use its built-in linear arithmetic decision procedure. In any case, the general theory has to be eventually instantiated to obtain an executable algorithm. The functions k-polynomialp and k-polynomialsp recognize polynomials and polynomial lists (with kvariables and rational coefficients). Analogously, +,*,-and |0| stand for polynomial addition, multiplication, negation and the zero polynomial. Let us now introduce the notion of ideal, along with the formalization of polynomial ideals in Acl2. Definition 1. I⊆Ris an ideal of Rif it is closed under addition and under the product by elements of R. Definition 2. The ideal generated by B⊆R, denoted as B,isthesetoflinear combinations of Bwith coefficients in R. We say that Bis a basis of I⊆Rif I=B. An ideal is finitely-generated if it has a finite basis. Hilbert’s Basis Theorem implies that every ideal in K[x1,...,x k] is finitelygenerated, if Kis a field. Polynomial ideals can be expressed in Acl2 by taking this into account. Let Cand Fbe lists of polynomials. The predicate p∈F can be restated as ∃Cp=lin-comb(C, F), where lin-comb is a recursive function computing the linear combination of the elements in Fwith coefficients in C. As Acl2 is a quantifier-free logic we use a common trick: we introduce a Skolem function assumed to return a list of coefficients witnessing the ideal membership. In Acl2 this can be expressed in the following way: (defun-sk<k> in<> (p F) (exists (C) (and (k-polynomialsp C) (equal p (lin-comb C F))))) The use of exists in this definition is just syntactic sugar. Roughly speaking, the above construction introduces a Skolem function in<>-witness,witharguments pand F, which is axiomatized to choose, if possible, a list Cof polynomial coefficients such that when linearly combined with the polynomials in F,pis obtained. Thus, Cis a witness of the membership of pto the ideal generated by F, and in<> is defined by means of in<>-witness. The following theorems establish that our definition of ideal in Acl2 meets the intended closure properties: (defthm |p in <F> & q in <F> => p + q in <F>| (implies (and (k-polynomialp p) (k-polynomialp q) (k-polynomialsp F)) (implies (and (in<> p F) (in<> q F)) (in<> (+ p q) F)))) (defthm |q in <F> => p * q in <F>| (implies (and (k-polynomialp p) (k-polynomialp q) (k-polynomialsp F)) (implies (in<> q F) (in<> (* p q) F)))) Whenever a theorem about in<> is proved we have to provide Acl2 with a hint to construct the necessary witness. For example, to prove that polynomial ideals are closed under addition we straightforwardly built an intermediate function computing the witness of p+q∈Ffrom those of p∈Fand q∈F. Definition 3. The congruence induced by an ideal I, written as ≡I, is defined by p≡Iq⇐⇒ p−q∈I. The definition of ≡Fin Acl2 is immediate3: (defun<k> =<> (p q F) (in<> (+ p (- q)) F)) Clearly, the ideal membership problem for an ideal Iis solvable if, and only if, its induced congruence ≡Iis decidable. Polynomial reductions will help us to design decision procedures for that congruence. 4 Polynomial Reductions Let <Mbe a well-founded ordering on monomials, p= 0 a polynomial and let lm(p) denote the leader monomial of pwith respect to <M. Definition 4. Let f=0be a polynomial. The reduction relation on polynomials induced by f, denoted as →f,isdefinedsuchthatp→fqif pcontains a monomial m=0such that there exists a monomial csuch that m=−c·lm(f) and q=p+c·f.IfF={f1,...,f k}is a finite set of polynomials, then the reduction relation induced by Fis defined as →F=k i=1 →fi. 3For the sake of readability, we use defun-sk<k> and defun<k>, instead of defun-sk and defun. These are just macros which add an extra parameter k(the number of variables) to a function definition, so we do not have to specify it in each function application. When kis not involved, defun is used. We have formalized polynomial reductions in the framework of abstract reductions developed in [11]. This approach will allow us to export, by functional instantiation, well-known properties of abstract reductions (for example, Newman’s lemma) to the case of polynomial reductions, avoiding the need to prove them from scratch. In [11], instead of defining reductions as binary relations, they are defined as the action of operators on elements, obtaining reduced elements. More precisely, the representation of a reduction relation requires defining three functions: 1. A unary predicate specifying the domain where the reduction is defined. In our case, polynomials, as defined by the function k-polynomialp. 2. A binary function, reduction, computing the application of an operator to a polynomial. In our case, operators are represented by structures m, c, f consisting of the monomials mand c, and the polynomial fappearing in the definition of the polynomial reduction relation (Def. 4). 3. A binary predicate checking whether the application of a given operator to a given object is valid. The application of an operator m, c, fto pis valid if pis a polynomial containing the monomial m,f= 0 is a polynomial in Fand c=−m/lm(f). Notice that the last requirement implies that lm(f) must divide m. This validity predicate is implemented by a function validp. These functions are just what we need to define in Acl2 all the concepts related to polynomial reductions. Let us begin defining ↔F(the symmetric closure of →F). We need the notion of proof step to represent the connection of two polynomials by the reduction relation, in either direction (direct or inverse). Each proof step is a structure consisting of four fields: a boolean field marking the step direction, the operator applied, and the elements connected (elt1, elt2). A proof step is valid if one of its elements is obtained by a valid application of its operator to the other element in the specified direction. The function valid-proof-stepp (omitted here), checks the validity of a proof step. The following function formalizes in Acl2 the relation ↔F. Note that due to the absence of existential quantification, the step argument is needed to explicitly introduce the proof step justifying that p↔Fq. (defun <-> (p q step F) (and (valid-proof-stepp step F) (equal p (elt1 step)) (equal q (elt2 step)))) Next, we define ∗ ↔F(the equivalence closure of →F). This can be described by means of a sequence of concatenated proof steps, which we call a proof 4.Note that again due to the absence of existential quantification, the proof argument explicitly introduces the proof steps justifying that p∗ ↔Fq. (defun <->* (p q proof F) (if (endp proof) 4Notice that the meaning of the word “proof” here is different than in the expression “Acl2 proof”. This proof is just a sequence of reduction steps. In fact, we are formalizing an algebraic proof system inside Acl2. (and (equal p q) (k-polynomialp p)) (and (k-polynomialp p) (<-> p (elt2 (first proof)) (first proof) F) (<->* (elt2 (first proof)) q (rest proof) F)))) Inthesameway,wedefinetherelation→∗ F(the transitive closure of →F), by a function called ->* (in this case, we also check that all proof steps are direct). The following theorems establish that the congruence ≡Fis equal to the equivalence closure ∗ ↔F. This result is crucial to connect the results about reduction relations to polynomial ideals. (defthm |p =<F> q => p <->F* q| (let ((proof (|p =<F> q => p <->F* q|-proof p q F))) (implies (and (k-polynomialp p) (k-polynomialp q) (k-polynomialsp F) (=<> p q F)) (<->* p q proof F))) (defthm |p <->F* q => p =<F> q| (implies (and (k-polynomialp p) (k-polynomialp q) (k-polynomialsp F) (<->* p q proof F)) (=<> p q F))) These two theorems establish that it is possible to obtain a sequence of proof steps justifying that p∗ ↔Fqfrom a list of coefficients justifying that p−q∈F, and vice versa. The expression (|p =<F> q => p <->F* q|-proof p q F) explicitly computes such proof, in a recursive way. This is typical in our development: in many subsequent Acl2 theorems, the proof argument in <->* or ->* will be locally-bound (through a let or let* form) to a function computing the necessary proof steps. As these functions are rather technical and it would take long to explain them, we will omit their definitions. But it is important to remark this constructive aspect of our formalization. Next, we proceed to prove the Noetherianity of the reduction relation. In the sequel, <represents the polynomial ordering whose well-foundedness was proved in [9]5. This ordering can be used to state the Noetherianity of the polynomial reduction. For this purpose, it suffices to prove that the application of a valid operator to a polynomial produces a smaller polynomial with respect to this well-founded relation: (defthm |validp(p, o, F) => reduction(p, o) < p| (implies (and (k-polynomialp p) (k-polynomialsp F)) (implies (validp p o F) (< (reduction p o) p)))) As a consequence of Noetherianity we can define the notion of normal form. Definition 5. A polynomial pis in normal form or is irreducible w.r.t. →Fif there is no qsuch that p→Fq.Otherwise,pis said to be reducible. A polynomial qis a normal form of pw.r.t. →Fif p→∗ Fqand qis irreducible w.r.t. →F. 5As it is customary in Acl2, this is proved by means of an ordinal embedding into 0. 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 pand 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 polynomials. This function is simple: it iteratively tests reducibility and applies valid operators until an irreducible polynomial is found. Note that termination is guaranteed 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→∗ Fnf F(p), we have to explicitly define a function |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 Fand red ∗ F: (defthm |nf(p, F) = red*(p, F)| (implies (and (k-polynomialp p) (k-polynomialsp F)) (equal (nf p F) (red* p F)))) With this result, we can translate all the properties proved about nf to red*. This is typical in our formalization: we use some functions for reasoning, and other functions for computing, translating the properties from one to another by proving equivalence theorems. For example, we proved the stability of the ideal with respect to red* using this technique. 5Gr¨obner Bases The computation of normal forms with respect to a given ideal can be seen as a generalized polynomial division algorithm, and the normal form computed as the “remainder” of that division. The ideal membership problem can be solved taking this into account: compute the normal form and check for the zero polynomial. Unfortunately, it is possible that, for a given basis F, a polynomial in Fcannot be reduced to the zero polynomial. This is where Gr¨obner bases come into play: Definition 6. Gis a Gr¨obner basis of the ideal generated by Fif G=F and p∈G⇐⇒p→∗ G0. The key point in Buchberger’s algorithm is that the property of being a Gr¨obner basis can be deduced by only checking that a finite number of polynomials (called s-polynomials) are reduced to zero: Definition 7. Let pand qbe polynomials. Let m,m1and m2be monomials such that m=lcm(lm(p),lm(q)) and m1·lm(p)=m=m2·lm(q). The s-polynomial induced by pand qis defined as s-poly(p, q)=m1·p−m2·q Theorem 1. Let Φ(F)≡∀p, q ∈Fs-poly(p, q)→∗ F0. The reduction induced by Fis locally confluent if Φ(F)is verified. That is: Φ(F)=⇒∀p, q, r (r→Fp∧r→Fq=⇒∃s(p→∗ Fs∧q→∗ Fs)) This theorem was the most difficult to formalize and prove in our work. First, note that it cannot be stated as a single theorem in the quantifier-free Acl2 logic, due to the universal quantifier in its hypothesis, Φ(F). For this reason, we state its hypothesis by the following encapsulate (we omit the local witnesses and some nonessential technical details): (encapsulate ((F () t) (s-polynomial-proof (p q) t)) ··· (defthm |Phi(F)| (let ((proof (s-polynomial-proof p q))) (and (k-polynomials (F)) (implies (and (in<> p (F)) (in<> q (F))) (->* (s-poly p q) (|0|) proof (F))))) The first line of this encapsulate presents the signature of the functions it introduces, and the theorem inside can be seen as an assumed property about these functions. In this case, we are assuming that we have a list of polynomials given by the 0-ary function F, with the property that every s-polynomial formed with pairs of elements of (F) is reduced to (|0|). This reduction is justified by a function s-polynomial-proof computing the corresponding sequence of proof steps representing the reduction to (|0|). We insist that Fand s-polynomial-proof are not completely defined: we are only assuming |Phi(F)| about them. Now, the conclusion of Th. 1 is established as follows: (defthm |Phi(F) => local-confluence(->F)| (let ((proof2 (transform-local-peak-F proof1))) (implies (and (k-polynomial p) (k-polynomial q) (<->* p q proof1 (F)) (local-peakp proof1)) (and (<->* p q proof2 (F)) (valleyp proof2))))) This theorem needs some explanation. Note that local confluence can be reformulated in terms of the “shape” of the involved proofs: a reduction is locally confluent if, and only if, for every local peak proof (that is, of the form p←r→q) there exists an equivalent valley proof (that is, of the form p∗ →s∗ ←q). It is easy to define in Acl2 the functions local-peakp and valleyp, checking those shapes of proofs. Note that again due to the absence of existential quantification, the valley proof in the above theorem is given by a function transform-local-peak-F, such that from a given local peak proof, it computes an equivalent valley proof. The definition of this function is very long and follows the same case distinction as in the classical proof of this result; only in one of its cases (the one dealing with “overlaps”), s-polynomial-proof is used as an auxiliary function, reflecting in this way where the assumption about Φ(F)is necessary. The last step in this section follows from general results of abstract reduction relations. In particular, if a reduction is locally confluent and Noetherian then its induced equivalence can be decided by checking if normal forms are equal. This has been proved in Acl2 [11] as a consequence of Newman’s lemma, also proved there. We can reuse this general result by functional instantiation and obtain an Acl2 proof of the fact that, if Φ(F), p∗ ↔Fq⇐⇒ nf F(p)=nf F(q). With this result, and using the equality between nf Fand red ∗ F,andthe equality between ≡Fand ∗ ↔F, it can be easily deduced that if Φ(F)thenFis aGr¨obner basis (of F). This is established by the following theorem (notice that (F) is still the list of polynomials assumed to have property Φby the above encapsulate): (defthm |Phi(F) => (p in <F> <=> red*(p, F) = 0)| (implies (k-polynomial p) (iff (in<> p (F)) (equal (red* p (F)) (|0|))))) 6 Buchberger’s Algorithm Buchberger’s algorithm obtains a Gr¨obner basis of a given finite set of polynomials Fby the following procedure: if there is a s-polynomial of Fsuch that its