Computational Logic Group, CCIA, University of Seville, Spain
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.
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.
This book includes multiset.lisp and defines a macro named defmul to build (well-founded) multiset extensions induced by (well-founded) ACL2 relations.
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
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".
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).
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.
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.
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
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.
We define here several basic concepts about terms, lists of terms, substitutions and equations.
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.
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.
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.
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.
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.
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.
A particular unification algorithm is defined and verified, as a functional instance of the previously given.
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.
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.
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
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.
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
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.
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.
To certify the books, see the README file.
Some related papers