Class Location/Time: SC1131 TR 11am - 12:15pm
Office Hours: SC 2108 TR 12:15pm - 1:15pm
Teaching Assistants: Stephen Skeirik (skeirik2) and Everett Hildenbrandt (hildenb2)
This is a classical paper on syntactic unification (solving equations in term algebras). It specifies the algorithm by very simple inference rules rules and gives a simple proof of correctness. It also discusses well computational complexity issues.
This is an excellent survey paper about unification modulo an equational theory (Σ, E), and also about various extensions such as order-sorted unification, combination of algorithms, and even narrowing. One key value is the adoption throughout of the Martelli-Montanari viewpoint: each algorithm is specified in a declarative way by a set of inference rules (i.e. rewrite rules). Although we will not go into the details of each unification algorithm (there are many), I strongly recommend each student to do ate least a general reading of this paper to get the "lay of the land" about unification.
This paper is one of the earliest and most cited ones about narrowing and about narrowing-based unification SEMI-algorithm for confluent and terminating equations by a then graduate student (you can also do stuff like that!) who was visiting SRI with his advisor (Gerard Huet) in my early times there. Some parts of the paper are unnecessary for the course. For example, previously basic narrowing was the best method to get narrowing to terminate (so it becomes an algorithm and satisfiability of QF+(Σ)-formulas in (Σ, TΣ(X)) is decidable), but basic narrowing terminates strictly less often than folding variant narrowing, which we will see later; so it is only of historical interest to look at the details of the basic narrowing strategy.
To obtain unification algorithms for theories whose equations are confluent MODULO axioms B, we need to understand two rewrite relations: →R/B and →R, B which can "simulate" efficiently →R/B. This has been a quite esoteric area with complicated and strange conditions and behaviors. This paper gives a much simpler notion of coherence assuming linear and regular axioms B. This will make the treatment of narrowing modulo B and of (E ∪ B)-unification easier. CS 476 lectures 4 and 5 are useful background for this paper. For the moment, you need only read Sections 1 and 2.
This paper contains the best results known up to now about how to get efficient narrowing modulo B unification algorithms. Some parts are not necessary for the course, and some of it is dated; but it is still the main reference available. In the lectures I will provide a simpler explanation of everything. Still, I would suggest taking a first look at the paper to get a high-level impression without getting bogged down in technical details. The coming lectures will make all this clearer.
These notes describe the relationship between the relations →R/B and →R, B, e.g. when properites such as confluence and termination are preserved. Proofs are included. Some initial lemmas on irreducibility are also presented. These notes complement the Strict Coherence of Rewriting Module Axioms paper.
These notes define what narrowing is, show how it corresponds to the rewrite relation →R, B, and show how it can be used to obtain a unification algorithm.
These notes define variants and variant narrowing and show how narrowing can be used to generate a complete set of variants.
The original paper introduing the notion of variants and the finite variant property.
This paper explores different notions of variant proposed in the literature and shows how they relate to one another---including notions of variants as only terms, as only substitutions, and as pairs of a term and a substitution.
These notes define the boundness property, show it is equivalent to the FVP, and also define folding variant narrowing, show its completeness, and finally show how it can be used as a semi-algorithm to determine when a theory satisfies the FVP.
These notes describe and prove correct a unification algorithm based on folding variant narrowing.
As shown in Lecture 9, variant unification provides a theory-generic decision procedure for checking the satisfiability of a POSITIVE QF formula in the initial algebra TΣ/E ∪ B of any theory having an FVP decomposition and a finitary B-unification algorithm. The class of FVP theories is infinite and contains many theories of interest. This raises the following intriguing question: could we somehow EXTEND such a theory-generic decision procedure to a similar theory-generic decision procedure for satisfiability of ANY QF formula in the initial algebra TΣ/E ∪ B under similar, but somewhat stronger, assumptions on (Σ, E ∪ B)? The answer is YES!, and is contained in this paper, which will be discussed in a few lectures, starting with Lecture 10.
These notes provide additional detail regarding the algorithms needed for variant satisfiability, including how to generate constructor variants and unifiers and how to check OS-compactness conditions.
Huet's paper on the correctness of KB completion algorithm is a classic. By computing critical pairs and orienting equations from left to right using a simplification order on terms one can, if successful, end up with a confluent and terminating set of equations equivalent to the original one given as input to the Knuth-Bendix algorithm. We are interested in the ground case of this algorithm to derive a correct-by-construction congruence closure algorithm.
Plaisted and Sattler-Klein's ground KB-completion algorithm adds a few simplifications/strategies and some data structure assumptions to the gound version of Huet's KB-completion algorithm to derive an O(n^2) conguence closure algorithm.
A review of the results of Huet and Plaisted & company plus proofs that decidability in the free models of empty theories is decidable.
Any Ground Associative-Commutative Theory Has a Finite Canonical System The paper by Narendran and Rusinowitz proves that a form of ground Knuth-Bendix completion modulo AC always terminates with a convergent set of ground rewrite rules equivalent to the original ground equations.
The paper by Barchmair et al. places "congruence closure" within an abstract, axiomatic setting as a set of inference rules. Basically, congruence closure is ground KB completion with the extra option of adding new constants besides those coming variables turned into constants; this can increase performance and decrease complexity from O(n^2) to O(n logn). What is nice about this paper is that:
different well-known algorithms are recovered as special cases based on different strategies to apply the inference rules;
they give also an AC congruence closure for the AC case.
The paper on order-sorted congruence closure proves a simple, yet surprising result: to do order-sorted congruence closure or order-sorted AC congruence closure you "don't have to do anything," that is, treating everything as unsorted yields correct decision procedures in both cases.
The paper by Rubio defines in detail the AC-RPO order, and proves that it defines a total order on AC congruence classes of ground terms. This order (or some similar order, but this is the best and simplest) is crucial to get AC congruence closure to work.
This paper by Derek Oppen gave a general notion of (non-cyclic) recursive data structures, with lists a la LISP is a paradigmatic example and prove decidable QF satisfiability of such structures. Oppen used an unsorted typing, which of course makes his theory, while seminal, messy and unsatisfactory.
This paper by Meseguer and Goguen gave a completely general solution to the problem of how to define selector functions that decompose into parts data elements built by free constructors for any recursive data structure. Although this paper was published a long time ago, the darkness of ignorance hangs like a plague over the topic of recursive data structures, which remains in the exact same conceptual mess as it was before this paper was published.