[ US ] [ CCIA ] [ Teaching ] [ SLC ] [e-mail]
Formalizing equational reasoning and rewriting (using ACL2)

UPDATED: July 17th, 2001.

We present here a formalization and mechanical proofs in the ACL2 system of some of the main properties of equational reasoning, mainly rewriting. You can see also an antecedent of this work, using NQTHM. The following is a exhaustive list of the books we have developed so far, with a brief description.

Multisets relations

• Multisets orderings: multiset.lisp

This book formalizes (in ACL2) Dershowitz and Manna's theorem about multiset orderings: every well-founded relation on a set can be "extended" to a well-founded relation on multisets (lists) of elements of the set. This kind of orderings is very useful in proving properties of equational reasoning.

• The defmul macro: defmul.lisp

This book includes multiset.lisp and defines a macro named defmul to build (well-founded) multiset extensions induced by (well-founded) ACL2 relations.

• Case studies of using defmul: mccarthy-91.lisp and ackermann.lisp.

Two examples given by Dershowitz and Manna, formalized in ACL2. We use defmul to prove termination of an iterative version of McCarthy's 91 function and termination of a tail-recursive version of Ackermann's function. But the main application of defmul is a mechanical proof of Newman's lemma, as shown below.

Abstract relations and abstract proofs

• Abstract proofs: abstract-proofs.lisp

We see here proofs from a very general point of view. Proofs are chains of r-steps, and r-steps are structures with four fields: elt1, elt2, direct and operator (every step "connect" elt1 and elt2 in the orientation given by direct,and by application of operator). Nothing more is assumed about an "abstract proof".

• Confuence and proofs: confluence.lisp

We define in this book the concept of confluent (Church-Rosser) and normalizing reduction relation, and prove that the reflexive-symmetric-transitive closure of a confluent and normalizing reduction relation is decidable (provided normal forms are computable). We treat proofs as manipulable objects, and we define some "operations" acting on proofs (an algebra of proofs).

• Newman's lemma: newman.lisp

We formalize in this book locally confluent and noetherian reduction relations, and prove Newman's lemma: local confluence of noetherian relations implies Church-Rosser property.

• Convergence: convergent.lisp

Using the results of confluence.lisp and newman.lisp and the encapsulate/functional-instanciation mechanism, we show decidability of the equivalence closure of every noetherian and locally confluent reduction relation.

• A case study, instantiating the abstract framework: perm.lisp

This is a naive example of how to instantiate the abstract framework in order to prove properties of a concrete reduction relation, whose equivalence closure is the "permutation of lists" relation. But the main instantiation of this abstract framework is the "term rewriting" reduction, as shown below.

The complete lattice of terms

• Some properties and previous basic results: basic.lisp

This book contains lemmas about lists, finite multisets, finite sets, and association lists needed for our proofs. This file is not intended to be a good formalization for that theory, but and ad hoc compilation of lemmas.

• Definitions and basic properties of first order terms: terms.lisp

We define here several basic concepts about terms, lists of terms, substitutions and equations.

• Definition and verification of rule-based matching algorithm: matching.lisp

Based in a set of rules that are applied non-deterministically to systems of equations, we define an "abstract" matching algorithm, a prove its correctness.

• Definition and verification of a concrete (and executable) subsumption algorithm: subsumption.lisp

As a particular case of the previous abstract matching algorithm, we define a concrete subsumption algorithm. This algorithm, given two terms, returns, whenever it exists, a substitution such that applied to the first term gives the second. Its verification is done using functional instantiation. Also it is shown that subsumption is a quasi-ordering and several additional properties. These properties are proved using only the soundness and completeness theorem of the defined algorithm.

• Renamings (definitions and properties): renamings.lisp

The concept of renaming substitution is defined and some properties are proved. Also, equivalence of terms (w.r.t subsumption) is defined. Finally, a particular kind of renaming is proved to be a renaming: number renaming. Renamings are important for some reasons: "standardization apart" and pretty printing of terms, for example.

• Well-foundedness of subsumption between terms: subsumption-well-founded.lisp

An ordinal measure is given to justify that there is no infinite strictly decreasing chain of subsumed terms. That property is proved using only the soundness and completeness theorem of the defined subsumption algorithm.

• Definition and properties of subsumption between substitutions: subsumption-subst.lisp

A suitable definition of subsumption between substitutions is given, avoiding some restrictions imposed by the ACL2 logic and our representation of substitutions. The definition is shown to verify the intended properties.

• Definition and verification of a rule-based unification algorithm: unification-pattern.lisp

An "abstract" unification algorithm is defined and verified. This unification algorithm is defined as a set of transformations rules acting on sets of equations, based on the ones given by Martelli and Montanari. These rules are non-deterministically applied until a solution (or unsolvability) is detected. A partially defined selection function is used to formalize non-determinism.

• Definition and verification of a concrete (and executable) unification algorithm: unification.lisp

A particular unification algorithm is defined and verified, as a functional instance of the previously given.

• Definition and verification of an anti-unification algorithm: anti-unification.lisp

An anti-unification algorithm is defined and verified. This anti-unification algorithm, given two terms, returns a common generalization, subsumed by any other common generalization. Thus, we proved the existence of a least upper bound of two given terms, with respect to subsumption.

• Definition and verification of a most general instance algorithm: mg-instance.lisp

An "most general instance" algorithm is defined and verified. This algorithm, given two terms, returns a common instance, that subsumes any other common instance. Thus, we proved the existence of a greatest lower bound of two given terms, with respect to subsumption.

• The complete lattice of terms: lattice-of-terms.lisp

Just for mathematical recreation (and as a compilation of the previous books) we proved that the set of first-order term in a signature (with an additional top term) is a well-founded lattice.

Equational theories and rewriting

• Definition of the equational theory given by a set of equational axioms: equational-theories.lisp

We define here several concepts about equational deduction: equational operators and equational proofs. We also extend the algebra of proofs with the operations of instantiation and context. Using this approach, we prove that equational equivalence is the least equivalence relation defined in the set of terms, in a given signature, closed under instantiation and inclusion in contexts, and containing the equational axioms.

• Definitions and basic properties of rewrite systems: rewriting.lisp

Equations can be seen as reduction rules in rewrite systems. The concept of reducibility is defined and a reducibility algorithm is proved to implement the concept. Noetherian rewrite systems are also defined by means of reduction orderings, and in this case the reduced terms are proved to decrease with respect to a well founded relation. Finally, a naive algorithm to compute a normal form w.r.t. a noetherian term rewriting system is defined and verified.

Decidability of equational theories given by complete term rewriting systems

• Critical pair lemma: critical-pairs.lisp

The concept of critical pair between two rules is defined and Knuth-Bendix critical pair lemma is proved: A rewrite system is locally confluent if all its critical pairs are joinable. Additionally, we define and verify a function to compute all the critical pairs of a term rewriting system.

• Decidability of confluent and terminating rewrite systems: kb-decidability.lisp

Using the books critical-pairs.lisp and convergent.lisp, we prove that if all the critical pairs of a noetherian term rewriting system R have common normal forms, then the equational theory described by R is decidable.

All the books are tared and gziped in acl2-equational.tgz.

To certify the books, see the README file.

Some related papers

• Mechanical verification of a rule based unification algorithm in the Boyer-Moore theorem prover, presented at AGP'99. And also the slides.
• Multiset relations: a tool for proving termination, presented at ACL2 Workshop 2000. Here are the slides.
• A Theory About First-order Terms in ACL2, presented at ACL2 Workshop 2002, with the slides.
• Formalizing rewriting in the ACL2 theorem prover Springer-Verlag ), presented at AISC 2000, and the slides
• A mechanical proof of Knuth-Bendix critical pair theorem (using ACL2), presented at FTP 2000. Here are the slides.

e-mail
Dpto. de Ciencias de la Computación e Inteligencia Artificial