Citation |

- Permanent Link:
- http://digital.auraria.edu/AA00004143/00001
## Material Information- Title:
- Term rewriting systems
- Creator:
- Sunshine, Todd Allan
- Publication Date:
- 1995
- Language:
- English
- Physical Description:
- iv, 96 leaves : illustrations ; 29 cm
## Subjects- Subjects / Keywords:
- Rewriting systems (Computer science) ( lcsh )
Rewriting systems (Computer science) ( fast ) - Genre:
- bibliography ( marcgt )
theses ( marcgt ) non-fiction ( marcgt )
## Notes- Bibliography:
- Includes bibliographical references (leaves 94-96).
- General Note:
- Submitted in partial fulfillment of the requirements for the degree, Master of Science, Computer Science.
- General Note:
- Department of Computer Science and Engineering
- Statement of Responsibility:
- by Todd Allan Sunshine.
## Record Information- Source Institution:
- |University of Colorado Denver
- Holding Location:
- |Auraria Library
- Rights Management:
- All applicable rights reserved by the source institution and holding location.
- Resource Identifier:
- 34088538 ( OCLC )
ocm34088538 - Classification:
- LD1190.E52 1995m .S86 ( lcc )
## Auraria Membership |

Full Text |

TERM REWRITING SYSTEMS
by Todd Allan Sunshine B.A., Cornell University, 1984 B.S., Cornell University, 1984 A thesis submitted to the Faculty of the Graduate School of the University of Colorado at Denver in partial fulfillment of the requirements for the degree of Master of Science Computer Science 1995 This thesis for the Master of Science degree by Todd Allan Sunshine has been approved for the Graduate School by Sunshine, Todd Allan (M.S., Computer Science) Term Rewriting Systems Thesis directed by Professor Jay Rothman ABSTRACT This thesis aims to provide an introduction to the concepts essential to a clear understanding of term rewriting systems. The thesis is composed of two primary elements; an introduction to the fundamental concepts underlying term rewriting systems as well as an actual implementation of a term rewriting system. The basis for understanding term rewriting systems is presented through a review of the fundamentals of binary relations and abstract reduction systems. Then, in the setting of abstract reduction systems, a detailed account of the Knuth-Bendix completion procedure is given. Relevant concepts pertaining to rewriting systems such as first-order unification, critical pairs, superposition, and term ordering are also discussed. Also presented is an introduction to recent developments in the arena of abstract completion. Based on the concepts introduced in the thesis a fully functional term rewriting system is then presented. The complete source listings of the term rewriting implementation are included. Of specific interest are the algorithms used to perform unification, superposition, normalization, and completion. Details of the programs use are demonstrated through annotated examples showing both the users input and resulting output. This abstract accurately represents the content of the candidates thesis. I recommend its publication. Signed Jay Rothman 111 CONTENTS Chapter 1. Introduction ............................................................ 1 2. Relations ............................................................... 2 2.1 Properties of Relations............................................. 3 2.2 Equivalence Relations............................................... 3 2.3 Closure of Relations ............................................... 4 2.4 Partial Orders...................................................... 4 3. Abstract Reduction Systems .............................................. 5 3.1 Terminating Reductions.............................................. 5 3.2 Confluence and the Church-Rosser Property........................... 6 3.3 Complete Reductions................................................. 8 3.4 Local Confluence ................................................... 9 3.5 Completion ........................................................ 11 4. Term Rewriting Systems.................................................. 12 4.1 Terms.............................................................. 12 4.2 Confluence of Term Rewriting Systems............................... 13 4.2.1 Unification................................................... 14 4.2.1.1 Syntactic Unification .................................. 14 4.2.1.2 Semantic Unification ................................... 16 4.2.2 Critical Pairs................................................ 18 4.2.2.1 Critical Pairs Completion .............................. 19 4.2.3 Knuth-Bendix Algorithm ....................................... 24 4.3 Termination of Term Rewriting Systems ............................. 26 4.3.1 Knuth-Bendix Ordering ..................................... 28 5. Abstract Completion .................................................... 30 6. Implementation of a TRS................................................. 33 6.1 Data Structures.................................................... 33 6.2 Unification........................................................ 34 6.3 Completion Procedure............................................... 35 6.4 Samples............................................................ 35 7. Conclusion.............................................................. 48 Appendix A................................................................. 49 References................................................................ 94 iv 1. Introduction When equations are interpreted as programs, they are used in one direction only, to rewrite an expression to a simpler one. A rewrite system is a set of such one-way rules. Equational programs based on rewrite systems are usually considered to be nondeterministic: an expression can be rewritten by any equation whose left-hand side matches any subterm of the expression. Knuth and Bendix [1970] proposed a procedure that attempts to construct a convergent rewrite system from a finite axiomatization of an equational theory. In their paper, they modestly state: The formal development in this paper is primarily a precise statement of what hundreds of mathematicians have been doing for many decades, so no great claims of originality are intended for most of the concepts or methods used. [p. 264] However, the overall viewpoint was indeed revolutionary, as it formalized the notion of a completion procedure in a concrete theoretical setting. Many rewrite systems satisfy the Church-Rosser, or "confluence," property: whenever two terms are equivalent, they can be rewritten to a common form. This guarantees that the "normal forms" (unrewritable terms) computed by a program are unique. Another important property is "termination": there are no infinite sequences of rewrites. Termination ensures that there is at least one normal form for every term. A system with both these properties is called "complete." A finite convergent system is a decision procedure for the free word problem of the underlying equational theory: an identity holds if and only if both its sides can be rewritten to the identical normal form. This "completion" procedure must be supplied with an ordering that is used to determine in which direction a derived equation s = t is to be oriented into a one- way rule, s - t or t > s. It deduces new equations by a process (involving unification) called "superposition". When the left-hand side of an instance of a rule can be rewritten by another rule, the two possible results of rewriting the left- hand side instance form what is called a "critical pair." These concepts will be presented formally, with precise definitions, as they arise. This paper is organized from the "ground up", such that each section is based on the preceding ones. In Section 2, a review of the basic properties of relations are reviewed. In Section 3, the relevant properties common to all reduction systems are introduced. In Section 4, the process of term rewriting as presented by Knuth and Bendix is formalized. In Section 5, recent developments in abstract completion are introduced. And finally, in Section 6, the concepts introduced in the paper are synthesized into a fully functional term rewriting system with samples of its execution. 1 2. Relations Before attempting to present the essential features of rewriting systems, it will first be necessary to review some fundamental background material. Therefore, in this section some more or less well-known properties of relations are summarized. First, let us recall some basic notions. A binary relation R on two sets A and B is a subset of the Cartesian product A x B. That is, a binary relation is a set of pairs. The first component of each pair is chosen from a set called the domain, and the second component of each pair is chosen from a (possibly different) set called the range. If R is a given binary relation, we shall often write xRy, instead of (x, y) e R, to indicate that an element jc is related via R to an element y. When we say that R is a binary relation on set A, we mean that R is a subset of A x A (that is, the domain and range are the same set A). There is the following possibility to picture a (finite) relation R on a set A. Each element of A is represented by a point and two points corresponding to elements x and y are connected by an arrow, x > y, whenever xRy holds. For example, if A = {w, x, y, z) and R = {(x, y), (x, w), (y, x), (z, y)}, then R is depicted in Figure 1. Because of this graphical representation, the preferred notation for an arbitrary relation is the arrow itself. 2 2.1 Properties of Relations We say a relation R on a set A is: (1) reflexive if, for all x e A, xRx. (2) symmetric if, for all x,y e A, xRy implies yRx. (3) transitive if, for all x,y,z e A, xRy and yRz imply xRz. (4) irreflexive if, for all x e A, xRx is false. (5) asymmetric if, for all x,y e A, xRy implies that yRx is false. (6) antisymmetric if, for all x,y e A, xRy and yRx imply x = y. Note that any asymmetric relation must also be irreflexive. 2.2 Equivalence Relations Mathematical abstractions are based on equivalence relations. If we want to ignore some inessential attributes of the objects in a certain set, then all objects with the same essential attributes have to be identified. Such an identification is a reflexive, symmetric, and transitive relation. This motivates the following definition. Definition 2.1 A relation R that is reflexive, symmetric, and transitive is said to be an equivalence relation. The following notation will be adopted. If R is an equivalence relation on a set A, then instead of xRy we will write x ~ y. When x ~ y, x is said to be equivalent to y modulo R. In order to formalize the abstraction processes mentioned above we have to decompose a given set into subsets. Let A be a set. A set P of pairwise disjoint nonempty subsets of A is called a partition of A whenever A uP. Obviously, each element of A belongs to exactly one subset. We may say that abstraction on a set A is formalized by the concept of partition. There is a one-to-one correspondence between partitions and equivalence relations. If P is a partition on A, an equivalence ~ is defined by the rule: x ~ y if and only if x and y are in the same class of the partition. Conversely, any equivalence relation on A induces a partition on A consisting of its equivalence classes. Hence, abstraction is based on equivalence relations. 3 2.3 Closure of Relations Suppose P is a set of properties of relations. The P-closure of a relation > is the smallest relation that includes all the pairs of and possesses the properties in P. Therefore, for an arbitrary relation -> on a set, let: = be the reflexive closure of - <-> be the symmetric closure of >+ be the transitive closure of - <->= be the reflexive and symmetric closure of > -V be the reflexive and transitive closure of - -+ be the symmetric and transitive closure of > <->* be the reflexive, symmetric, and transitive closure of 2.4 Partial Orders Partial orders, especially in regard to the ordering of terms, plays an important role in term rewriting systems. Therefore, while on the topic of relations let us review some basic definitions that we will need later. Definition 2.2 A reflexive, transitive, and antisymmetric relation on a set A is called a partial order on A. An example of a partial order is given by the set inclusion relation c over a collection of sets. A relation R on a set A is a total order if it is a partial order and for all x,y A, either xRy or yRx. A total order is often called a linear order because the elements of A can be laid out on a straight line such that x is to the left of y if and only if xRy. The integers under the relation < form a total order, as do the reals. Definition 2.3 A reflexive and transitive relation on a set A is called a preorder. 4 3. Abstract Reduction Systems It is frequently the case that when mathematical concepts are involved, it is easier to understand a concept in an abstract setting rather than a specific concrete setting. This is precisely the case when considering reduction systems. We therefore present the basic notions of reduction and replacement in an abstract theoretic sense. We introduce reduction systems in this setting in order to develop as far as possible the properties common to all reduction systems. Specifically, we consider reduction and replacement in terms of a set of objects and binary relations on that set. A pair (A, >) consisting of a set A and a relation on it is called an abstract reduction system. We say that a reduction system (A, ->) has a property (e.g., it is terminating, confluent, etc.) if the relation -> has the property. In this context, is called a reduction relation. 3.1 Terminating Reductions Termination is one of the basic concepts in theoretical computer science, which expresses in a certain way a finiteness condition. It should be intuitively clear that such conditions are necessary for any constructive proof method. To introduce terminating relations we need some more notions. Let > be an arbitrary relation on a set A. Given elements x and y of A, we say that x is reduced to y in one step if x - y, and y is called an (immediate) reduct of x. An element x of A is called reducible if x has any reduct. Otherwise, jc is called irreducible. Furthermore, we say that an element x of A has a terminating reduction if there are elements x^xxm e A such that x, - xi+I for i = 0,l,...,m-l and xm is irreducible. This will be written: X = x0 -> X, ... xm We say that an element x of A has a nonterminating reduction if there is an infinite sequence x^x,,... e A such that xj xi+I for all i > 0, which will be written: X = X0 > X, x2 > ... Which leads to the following definition: Definition 3.1 A relation - on a set A is called terminating if every element of A has only terminating reductions. That is, is 5 terminating if there is no infinite sequence x^x,,... e A such that Xj -> xj+I for all i > 0. Observe that a terminating relation - on a set A is necessarily acyclic, i.e., there is no element x of A such that x ->* x holds. Hence the relation: is not terminating since it is not acyclic. Even though every element of the relation depicted in Figure 2 has a terminating reduction, the relation itself is not terminating since it is not acyclic. 3.2 Confluence and the Church-Rosser Property One of the fundamental computing paradigms is that of reduction. Computing can be done by reducing an expression to a simpler one. Let (2 + 3) x (1 + 1) be a term to compute. A reduction of this term is (2 + 3) x (1 + 1) -> 5 x (1 + 1) 5 x 2 -> 10. Other reductions are possible, as in (2 + 3)x(l + l)->2x(l + l) + 3x(l + l)-2x2 + 3x2->4 + 6-10, which ends with the same term. This confluence of all the reductions flowing out of the same term is an essential property of this form of computing, as it guarantees the same result regardless of the reduction strategy. Formally, 6 Definition 3.2 A reduction system (A, ->) is confluent if for all w, x, y e A, w x and w ->* y imply that there exists a z e A, such that x -> z and y >* z. Confluence is depicted in Figure 3, where a complete line indicates a hypothesis (if...) and a dashed line indicates a conclusion (there exists Confluence says that no matter how one diverges from a common ancestor, there are paths joining at a common descendent. The implication is that confluence is a fundamental property of every model of computation using reduction, as it guarantees the independence of the result of a computation from the reductions taken. If -> is a reduction relation, then its generated equivalence <->* is called a convertibility relation. Definition 3.3 A reduction system (A, ) has the Church-Rosser Property if for all x, y e A, if jc <-* y, there exists az e A, such that x -* z and y * z. The Church-Rosser property is depicted in Figure 4. 7 Tigure 4 The conversion relation turns out to mean reducing to the same term: this is called the Church-Rosser property. Theorem 3.1 (Church-Rosser Theorem) A relation has the Church-Rosser property if and only if it is confluent [Church and Rosser, 1936] If a reduction system satisfies the Church-Rosser, or confluence, property, then whenever two terms are equivalent, they can be rewritten to a common form. This guarantees that the "normal forms" (unrewritable terms) computed by a program are unique. 3.3 Complete Reductions Now that we have defined both terminating and confluent reduction systems we are prepared for the following definition: Definition 3.4 A confluent and terminating reduction system is called complete. Consider the reduction system (A, ) given by A = {jc, y, z) and - as depicted in Figure 5. Then (A, >) is certainly terminating but is not confluent. 8 We are now going to characterize complete reduction systems. Let (A, >) be an arbitrary reduction system. An element x of A admits a normal form if there is an irreducible element, say y, in A such that x -* y. In Figure 5, y and z are normal forms of x. If (A, ) is a confluent reduction system, each element of A has at most one normal form. When (A, -) is a terminating reduction system, each element of A has at least one normal form. Hence, in a complete reduction system every element has exactly one normal form, often called the canonical normal form. The Church-Rosser Theorem is the basis of the confluence method explained below. Let - be a confluent and terminating relation on a set A. Given an element x of A, any reduction starting from x terminates after finitely many steps with an element, say x'. By the confluence of x' is uniquely determined. For if x were reducible to two irreducible elements y and z, then these elements would be convergent and, hence, equal. So x is always reducible to a unique element x', the canonical normal form of x 3.4 Local Confluence Related to the property of confluent reduction systems is the concept of locally confluent reduction systems. Definition 3.5 A reduction system (A, ->) is locally confluent if for all w, x, y e A, w > x and w > y imply that there exists a z e A, such that x -* z and y -* z. Local confluence is visualized in Figure 6. 9 Clearly, every confluent reduction system is locally confluent. The converse, however, is not true, as the following example indicates. The reduction system depicted in Figure 7 is locally confluent, but not confluent. Observe that the reduction system is not terminating. 10 3.5 Completion A completion procedure is aimed at constructing a confluent and terminating reduction system from a given reduction system. Unfortunately, both properties are undecidable in general. However, if the reduction itself is terminating, then there is a necessary and sufficient condition that is quite useful in building a completion procedure. Theorem 3.2 (Newmans Lemma) A terminating reduction system is confluent if and only if it is locally confluent [Newman, 1942]. As a corollary we get an important criterion for completeness. Corollary A reduction system is complete if and only if it is locally confluent and terminating. Given a reduction system (A, >), any equivalent complete reduction system is called a completion of (A, ->). Our main goal is an algorithmic construction of such a completion when it is possible. The idea of a possible algorithmic construction of a completion procedure is based on Theorem 3.2. Given a terminating reduction system (A, -) we try to construct a completion (A, =>) by locating all situations in which local confluence is injured. This suggests the following procedure. Start with the relation - and compute the set CP() of "critical pairs" of where (x, y) e A x A is called critical if there is an element z of A such that z -> x and z y, but jc and y are not convergent. If CP(-) is empty, the reduction relation > is locally confluent and hence confluent, which means that (A, -) is already complete. In case there exists at least one critical pair (x, y) we remedy the violation of local confluence by allowing that either x is reducible to y or, vice versa, y is reducible to x depending on the analysis where adjoining (x, y) or (y, x) to the reduction relation leaves the termination property untouched. When both possibilities destroy the termination property the procedure stops with "failure". After adjoining a critical pair to - we get a new relation. Again its critical pairs are computed and eventually added. If the procedure terminates with a relation =>, then there is no critical pair left. Consequently, (A, =>) is a completion of (A, ->). By construction, (A, =>) is a complete reduction system. But, it should also be clear that (A, =>) and (A, -) are equivalent. 11 4. Term Rewriting Systems Now that the groundwork has been laid, we can apply the general ideas derived in the framework of reduction systems to term reduction systems. But, first, we must establish some notational conventions. 4.1 Terms In this section we are concerned with the syntactic generation which yields the notion of a term. A signature is a set 2, whose elements are called operation symbols, together with a mapping arity: 2 - N, called the arity function, assigning to each operation symbol its finite arity. If/ e 2 and arityif) = n, / is of arity n, or / is n-ary. If n > 1,/is a functional symbol, and if n = 0, it is a constant symbol. Definition 4.1 Let 2 be a signature and V be a set of variables. The set of (first-order) terms over V is TÂ£(F) and is defined inductively as: (1) Ifv e V, then v e TÂ£(F). (2) If/e 2, and t...,tn e TZ(F) (n > 0), then e TÂ£(F). For convenience, we shall always assume that 2 and V are disjoint. Following convention, we shall agree to use the most readable notation for terms. This permits us to represent terms on an extended alphabet with parentheses and commas, which is closer to standard mathematical practice. Therefore, a term is either a variable symbol, a constant symbol, or a function symbol followed by a series of terms, separated by commas, and enclosed in parentheses. The finite set Var(t) of variables occurring in a term t is defined as follows: (1) Var(v) = {v}, if v e V. (2) Var= Var(/,) u...u Var(0, if/e 2 and if g TÂ£(F). We say that a term t is a ground term if Var(t) = 0. That is, a term that is variable-free is a ground term. The set of all ground terms is denoted by Tz and it is clear that Tz = Tz(0). 12 4.2 Confluence of Term Rewriting Systems Equational proofs of equational theorems are not easy to deduce. It is difficult to find a strategy for selecting and orienting axioms. A simple idea is always to apply the equalities in the same direction. Such a directed equality is called a rewrite rule, denoted by replacing the equal sign =, by an arrow Formally, if an equation is a pair (s, t) of terms s,t e TX(F) denoted by s = t, then s t is its associated rewrite rule. Definition 4.2 A term rewriting system (hereafter abbreviated TRS) is a set of reduction rules. Rewriting a term with a rewrite system R consists in replacing a subterm which matches a left-hand side of a rewrite rule by the right-hand side whose variables are bound to values computed by the matching algorithm. This relation is denoted by R. Iterating this process is called reducing. If two terms can be reduced to the same one, a special equational proof is obtained, called a rewrite proof. A term which cannot be rewritten is said to be in normal form. A property required for a rewrite system is the uniqueness of the normal form for any term. This is crucial for any application where computing normal forms must be independent of the strategy of rule application. Uniqueness of the normal form is implied by the property of confluence. A rewrite system is confluent when two rewrite sequences beginning from the same term can always be extended to end with the same term. Confluence, which has been shown to be an abstract property of relations, gives us a relation between equational proofs and rewrite proofs: given a confluent rewrite system, every equational theorem has a rewrite proof. Theorem 4.1 A rewriting system is locally confluent if and only if every critical pair is confluent. Combining Newmans lemma with the preceding theorem yields the key theorem from the Knuth-Bendix paper. Theorem 4.2 A terminating rewriting system is confluent if and only if every critical pair is confluent. The importance of Theorem 4.2 is that it shows that to test for local confluence it is sufficient to consider only the critical pairs. However, computing critical pairs is an application of unification. Therefore, before expounding further on how critical pairs are used to show confluence, we must digress into a somewhat detailed explanation of unification. 13 4.2.1 Unification In its essence, the unification problem in first-order logic can be expressed as follows: Given two terms containing some variables, find, if it exists, the simplest substitution (i.e., an assignment of some term to every variable) that will make the two terms identical. The nature of such unifying substitutions, as well as the means of computing them, makes up the study of unification. 4.2.1.1 Syntactic Unification A substitution is a function a: V - TÂ£(F), which is the identity function almost everywhere, i.e., except for a finite subset of V. Substitutions can be represented by a set of variable-term pairs ct = {jc; <- t ..., x < t} with x, tf. A substitution or in which ct(x) is g(h(a), a) and c(y) is h(a) would be written as: a = {x terms to terms. The application of a substitution a to a term t is also written Substitutions can be composed: ct0(/) denotes the term t after the application of the substitutions of 0 followed by the application of the substitutions of ct. The substitution ct0 is a new substitution built from old substitutions ct and 0 by (1) modifying 0 by applying a to its terms, then (2) adding variable-term pairs in ct not found in 0. Composition of substitutions is associative, that is, (a0)x(j) = ct(0x)(.s) but is not in general commutative, that is, ct0(^) Q substitution ct such that a(s) = t. If a term t can be formed from another term s by making substitutions for the variables of s, then we say that t is an instance of s or that s subsumes t. This forms the basis of a relation on terms called the subsumption ordering, written s < t. The subsumption relation is closely related to the ability to match one term to another: for only if there exists a substitution ct such that a(s) = t does it imply that sit. For example,/fx) 3 f(g(c)), since the substitution {x < g(c)} when applied to f(x) yields f(g(c)). If, for two terms s and t, s < t and t < s, then s is called a variant of t, written s ~ t (where ~ is the equivalence relation associated with *). It is easily shown that if s ~ t, then s and t can differ only by the names of their variables. Therefore 14 the equivalence relation ~ equates terms which are equal up to the renaming of variables. Thus the subsumption relation is in fact a preorder relation (i.e., it is a reflexive and transitive binary relation). However, the subsumption relation is not antisymmetric, so it is not an order relation. Consider, for example, if x and y are distinct variables, then x < y and y 3 x, but x y. In other words, the subsumption relation is only antisymmetric up to the renaming of variables. If neither s < t nor t 1 s, then s and t cannot be matched and are said to be unrelated. Let t* represent the set of all instances of a term t. In general, t* is an infinite set and can be represented diagrammatically as in Figure 8. The two sets of instances s* and t*, of terms s and t, respectively, may intersect as represented in Figure 9. Although s and t may themselves be unrelated, there will often be instances of each that are related. The set of terms that are instances of both s and t lie in the region s* n t*. 15 The unification of s and t is the process of finding elements of s* r\ t*. If s and t share variables, then their set of unified forms is, in general, a subset of, and not identical to, s* n t*. As an example of this, consider the two terms f(x, 2) and f(3, x): an instance of both is f(3, 2), but this is not a unified form. Definition 4.4 Two terms s and t are called unifiable if there exists a substitution c such that o(s) = a(t). In such a case, a is called a unifier of s and t, and g(s) is called a unification of s and t. As an example consider the two terms f(x, yj and f(g(y, a), h(a)). They are said to be unifiable, since the application of the substitution a = {x <- g(h(a), a), y 4- h(a)} will change both terms to f(g(h(a), a), h(a)). In his famous paper on the resolution principle for a machine-oriented logic, J.A. Robinson [1965] gave an algorithm to compute a substitution that unifies two terms. Furthermore, Robinson proved that if the unification of two first-order terms is possible, there exists a single, most general unified form, unique up to variable renaming. This most general unified form is the one that subsumes all other unified forms, and is the term r in Figure 9. Definition 4.5 A unifier a of terms s and t is called a most general unifier (MGU) of s and t if for any other unifier 0, there is a substitution x such that tct = 0. Consider, for example, the two terms f(x) and f(g(y)). The MGU is {x 4- g(y)}, but there are many non-MGU unifiers such as {x 4- g(a), y <- a). Intuitively, the MGU of two terms is the simplest of all their unifiers. 4.2.1.2 Semantic Unification In the previous section we presented the concepts involved in solving an equation s = t syntactically; this is a particular case of the problem of solving equations semantically, i.e. modulo some equational theory E (for this reason semantic unification is also called ^-unification). More precisely, in the presence of an equational theory E, and given an equation s = t, we want to find substitution a such that g(s) =e v(f). Therefore, syntactic unification is ^-unification with empty E. 16 A substitution ct is a solution in E to an equation s = t if a(X) =E a(t), in which case we say that ct is an ^-unifier of s and t; we say that t ^'-matches s if there exists a substitution ct such that ct(j) =e t. When more than one solution may exist for a theory E, we define a solution ct of s =Et to be more general than solution p if ct general unifier exists. Note that there are decidable theories with infinite sets of most general unifiers, and there are some for which there are solutions, but no most general one, as we shall see. Consider the two first order terms s and t s =f(x, g(a, b)) t =f(g(y, b), x) The decision problem for syntactic unification is whether or not there exist terms which can be substituted for the variables x and y in s and t so that the two terms thus obtained are identical. In this example g(a, b) and a are two such terms and we write 8 = {x <- g(a, b), y <- a} to represent this unifying substitution. We say that 8 is a unifier for s and t, since m = 8(0 =f(g(a, b), g(a, b)). Consider a variation of the above problem in the presence of an equational theory, which arises when we assume that the function /is commutative: (C) f(x, y) =f(y, x) Now 8 is still a unifier for s and t. However, ct = {y ctCO =f(x, g(a, b)) =c f(g(a, b), x) = ct(0 But ct is more general than 8, or put another way 8 is an instance of ct, since it is obtained as the composition of the substitutions 0ct where 0 = {x <- g(a, b)}. Hence a unification algorithm only needs to compute ct. Unlike syntactic unification, where there is at most one general unifying substitution, semantic unification can yield a number of most general unifiers. Under commutativity, for example, there are pairs of terms which have more than one most general unifier, but they always have at most finitely many. 17 The problem becomes entirely different if we assume that the function / is associative: (A) f(x, f(y, z)) =f(f(x, y), z) In this case 6 is still a unifying substitution, but t = {x f(g(a, b), g(a, b)), y <- a} is also a unifier, since =f(f(g(a, b), g(a, b)), g(a, b)) =A f(g(a, b), f(g(a, b), g(a, b))) = x{t) But t' = {x <- f(g(a, b), f(g(a, b), g(a, b))), y <-_a} is again a unifying substitution and it is not difficult to see, by an iteration of this process, that there are infinitely many unifiers, all of which are most general. Finally, if we assume that both axioms (A) and (C) hold for f, the situation changes yet again and for any pair of terms there are at most finitely many most general unifiers under (AC). 4.2.2 Critical Pairs We have shown that assuming termination, confluence is equivalent to local confluence, itself equivalent to the convergence of critical pairs. Yet it remains for us to formally construct the notion of critical pairs. In order to define critical pairs a few more notions are required. First, by t|p, we denote the subterm of t rooted at position p. Furthermore, reasoning with equations requires replacing subterms by other terms. Therefore, let the term t with its subterm 11 p replaced by a term s be denoted by t[s]p. Definition 4.6 Let s - s' and t > t' be two reduction rules of a given TRS R. We assume that the variables are renamed appropriately so that s and t share no variables. If p is the position of a nonvariable subterm of s and there exists a substitution a such that <*(s|p) = (0 then ct(j') along with a(s|/']p) is called a critical pair in R. Both components of a critical pair (a(sr), cr(.s|/']p)) are the two outcomes of reducing a(j) by s - s' and t - t\ respectively. 18 For example, consider the following reduction rules f(g(x), f(x, z)) z f(x, f(y, g(f(x, y)))) c Let us rename the variables of the first reduction rule so that we have -y =f(g(x), fix', z)) and t =f(x, f(y, g(f(x, y)))). Then, (1) j|p =f(x', z) is a nonvariable subterm of s; and (2) j|p and t are unifiable with a mgu a = {*' <- x, z < f(y, g(f(x, y)))}. Now we obtain <*(*') = a(z) =f(y, g(f(x, y))) cj(j[^p) = The critical pairs can be found by unifying each nonvariable subterm of the left-hand side of a rewrite rule with the left-hand side of another rule. This process is called the superposition algorithm. 4.2.2.1 Critical Pairs Completion We will now explain the essential features of the completion algorithm first by an informal, intuition-guided, completion of the equational specification of groups. Consider the group signature consisting of a binary operation Mult, a unary operation Inv, and a nullary operation e. We start by giving the axioms for groups a "sensible" orientation: (1) Mult(e, x) - x (2) Mult(Inv(x), x) > e (3) Mult(Mult(x, y), z) Mult(x, Mult(y, z)) Note that the TRS defined by these three reduction rules is terminating but not confluent. Termination will not be discussed here, but will be studied in the next section. Confluence is violated, as can be seen by the superposition of rules (2) 19 and (3), with result Mult(Mult(Inv(x), x), z). In a sense, Mult(Mult(Inv(x), x), z) is the most general term subject to the two possible reductions: Mult(Mult(Inv(x), x), z) >3 Mult(Inv(x), Mult(x, z)) Mult(Mult(Inv(x), x), z) 2 Mult(e, z) which yields the critical pair Mult(Inv(x), Mult(x, z)) and Mult(e, z). After applying the reduction Mult(e, x) - jc we have the problematic pair of terms Mult(Inv(x), Mult(x, z)) and z; problematic because their equality is derivable from the group axioms, but they are not convergent with respect to the reduction rules available so far. Therefore, we adopt the new reduction rule: (4) Mult(Inv(x), Mult(x, z)) z Continuing in this manner, we find that the superposition of rules (1) and (4): Mult(Inv(e), Mult(e, x)) Mult(Inv(e), x) Mult(Inv(e), Mult(e, x)) >4 x yields the critical pair Mult(Inv(e), x) and x. Therefore, adopt the reduction rule: (5) Mult(Inv(e), x) > x Superposition of rules (2) and (4): Mult(Inv(Inv(x)), Mult(Inv(x), x)) -2 Mult(Inv(Inv(x)), e) Mult(Inv(Inv(x)), Mult(Inv(x), x)) ->4 x yields the critical pair Mult(Inv(Inv(x)), e) and x. Therefore, adopt the new reduction rule: (6) Mult(Inv(Inv(x)), e) - x Superposition of rules (3) and (6): Mult(Mult(Inv(Inv(x)), e), y) >3 Mult(Inv(Inv(x)), Mult(e, y)) Mult(Mult(Inv(Inv(x)), e), y) 6 Mult(x, y) yields the critical pair Mult(Inv(Inv(x)), Mult(e, y)) and Mult(x, y). Therefore, after normalizing adopt the new reduction rule: (7) Mult(Inv(Inv(x)), y) -> Mult(x, y) 20 Superposition of rules (6) and (7): Mult(Inv(Inv(x)), e) 7 Mult(x, e) Mult(Inv(Inv(x)), e) 6 x yields the critical pair Mult(x, e) and x. Therefore, adopt the new reduction rule: (8) Mult(x, e) x Superposition of rules (6) and (8): Mult(Inv(Inv(x)), e) g Inv(Inv(x)) Mult(Inv(Inv(x)), e) ->6 jc yields the critical pair Inv(Inv(x)) and x. Therefore, adopt the new reduction rule: (9) Inv(Inv(x)) - x Notice that reduction rule (6) can be deleted due to rules (8) and (9) because: Mult(Inv(Inv(x)), e) ->6 x Mult(Inv(Inv(x)), e) -9 Mult(x, e) 8 x are convergent. Likewise reduction rule (7) can be deleted due to rule (9) because: Mult(Inv(Inv(x)), y) -7 Mult(x, y) Mult(Inv(Inv(x)), y) ->9 Mult(x, y) are convergent. Superposition of rules (5) and (8): Mult(Inv(e), e) -8 Inv(e) Mult(Inv(e), e) -5 e yields the critical pair Inv(e) and e. Therefore, adopt the new reduction rule: (10) Inv(e) e Notice that reduction rule (5) can be deleted due to rules (1) and (10) because: Mult(Inv(e), x) -5 x Mult(Inv(e), x) 10 Mult(e, x) x 21 are convergent. Superposition Rules (2) and (9): Mult(Inv(Inv(x)), Inv(x)) 9 Mult(x, Inv(x)) Mult(Inv(Inv(x)), Inv(x)) -2 e yields the critical pair Mult(x, Inv(x)) and e. Therefore, adopt the new reduction rule: (11) Mult(x, Inv(x)) e Superposition Rules (4) and (9): Mult(Inv(Inv(x)), Mult(Inv(x), z)) 9 Mult(x, Mult(Inv(x), z)) Mult(Inv(Inv(x)), Mult(Im(x), z)) >4 z yields the critical pair Mult(x, Mult(Inv(x), z)) and z. Therefore, adopt the new reduction rule: (12) Mult(x, Mult(Inv(x), z)) -> z Superposition Rules (3) and (11): Mult(Mult(x, y), Inv(Mult(x, y))) -3 Mult(x, Mult(y, Inv(Mult(x, y)))) Mult(Mult(x, y), Inv(Mult(x, y))) e yields the critical pair Mult(x, Mult(y, Inv(Mult(x, y)))) and e. Therefore, adopt the new reduction rule: (13) Mult(x, Mult(y, Inv(Mult(x, y)))) > e Superposition Rules (12) and (13): Mult(Inv(x), Mult(x, Mult(y, Inv(Mult(x, y))))) ->12 Mult(y, lnv(Mult(x, y))) Mult(Inv(x), Mult(x, Mult(y, Inv(Mult(x, y))))) 13 Mult(Inv(x), e) yields the critical pair Mult(y, Inv(Mult(x, y))) and Mult(Inv(x), e). Therefore, after normalizing adopt the new reduction rule: (14) Mult(y, Inv(Mult(x, y))) > Inv(x) Notice that reduction rule (13) can be deleted due to rules (11) and (14) because: 22 Mult(x, Mult(y, Inv(Mult(x, y)))) >13 e Mult(x, Mult(y, Inv(Mult(x, y)))) 14 Mult(x, Inv(x)) ->n e are convergent. Superposition Rules (4) and (14): Mult(Inv(y), Mult(y, Inv(Mult(x, y)))) 4 Inv(Mult(x, y)) Mult(Inv(y), Mult(y, Inv(Mult(x, y)))) ->14 Mult(Inv(y), Inv(x)) yields the critical pair Im(Mult(x, y)) and Mult(Inv(y), Inv(x)). Therefore, adopt the new reduction rule: (15) Inv(Mult(x, y)) Mult(Inv(y), Inv(x)) Notice that reduction rule (14) can be deleted due to rules (12) and (15) because: Mult(y, Inv(Mult(x, y))) -14 Inv(x) and Multfy, Inv(Mult(x, y))) ->I5 Multfy, Mult(Inv(y), Inv(x))) 12 Inv(x) are convergent. The TRS is now complete, and is composed of the following rewrite rules: (1) Mult(e, x) - x (2) Mult(Inv(x), x) -* e (3) Mult(Mult(x, y), z) - Mult(x, Multfy, z)) (4) Multflnvfx), Multfx, z)) -> z (5) Multfx, e) -> x (6) Invflnvfx)) > x (7) Invfe) -> e (8) Multfx, Invfx)) e (9) Multfx, Multflnvfx), z)) -> z (10) InvfMultfx, y)) > Multflnvfy), Invfx)) 23 4.2.3 Knuth-Bendix Algorithm A completion procedure is aimed at building a confluent and terminating rewrite system from a set of equalities. In what follows we shall explain a completion procedure based on Theorem 4.2 called the Knuth-Bendix Completion Procedure. The Knuth-Bendix procedure can be outlined roughly as follows: Input: An equational specification (E, E) and a reduction ordering > on TZ(F) (i.e., a program which computes >). Output: A complete TRS R. Method: A sequence (U J n e N) of finite TRSs is computed iteratively, if possible, as follows: R := 0; while (E t* 0) { Select an equation (s = t) e E; E := E {s = t}; Reduce s and t to respective normal forms s' and t1 with respect to R; if (s' t') { if (s' > t') a := s'; p = t'; else if (t1 > s') a := t'; P = s'; else failure CP := {P = Q | is a critical pair between the rules in R |