9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # Chapter 6 of Handbook of Theoretical Computer Science Volume B Formal Methods and Semantics

REWRITE SYSTEMS

Nachum Dershowitz and Jean-Pierre Jouannaud

Handbook of Theoretical Computer Science

Chapter 6 of

Volume B: Formal Methods and Semantics J. van Leeuwen, ed. pages 243 320 North-Holland Amsterdam, 1990

Equations are ubiquitous in mathematics and the sciences. Sometimes one tries to determine if an identity follows logically from given axioms; other times, one looks for solutions to a given equation. These reasoning abilities are also important in many computer applications, including symbolic algebraic computation, automated theorem proving, program speci cation and veri cation, and high-level programming languages and environments. Rewrite systems are directed equations used to compute by repeatedly replacing subterms of a given formula with equal terms until the simplest form possible is obtained. The idea of simplifying expressions has been around as long as algebra has. As a form of computer program, rewrite systems made their debut in Gorn, 1967 ; many modern programs for symbolic manipulation continue to use rewrite rules for simpli cation in an ad hoc manner. As a formalism, rewrite systems have the full power of Turing machines and may be thought of as non-deterministic Markov algorithms over terms, rather than strings. Regarding Markov algorithms, see, e.g. Tourlakis, 1984 . The theory of rewriting is in essence a theory of normal forms; to some extent it is an outgrowth of the study of Church's Lambda Calculus and Curry's Combinatory Logic. To introduce some of the central ideas in rewriting, we consider several variations on the Co ee Can Problem" attributed to Carel Scholten in Gries, 1981 . Imagine a can containing co ee beans of two varieties, white and black, arranged in some order. Representing the contents of the can as a sequence of bean colors, e.g. white white black black white white black black; the rules of our rst game are as follows: black white ! black white black ! black black black ! white This set of rules is an example of a rewrite system. Each rule describes a legal move: the rst two state that, at any stage of the game, the white bean of any adjacent pair of di erent beans may be discarded; the last rule states that two adjacent black beans may be replaced by one white one an unlimited supply of white beans is on hand. For example, the following is a possible sequence of moves the underlined beans participate in the current move: white white black black white white black black white white black black white black black white white white white black black white white white black black white white black black white black black black black white The object of this game is to end up with as few beans as possible. It is not hard to see that with an odd number of black beans the game will always end with one black bean, since the parity" of black beans is unchanging. Played right always keeping at least one black bean around, an even non-zero number of black beans leads to one white bean, but other pure-white results are also possible. For instance, applying the third rule right o to both pairs of black beans leaves six white beans. By adding an additional rule, the above game may be modi ed to always end in a single bean: black white ! black white black ! black black black ! white white white ! white 1

1 INTRODUCTION

What is di erent about this new game is that one of the rules applies to any can containing more than one bean. What is interesting is that the outcome of the game is completely independent of the choice of which move is made when. To establish this, an analysis of the di erent possible divergences helps. The order in which moves at non-overlapping locations are made is immaterial, since whichever moves were not taken can still be taken later. The critical cases occur when the possible moves overlap and making one precludes making the other. For example, from white black black, either black black or white white can result. The point is that these two situations can both lead to the same single-white state. The same is true for other overlapping divergences. With this independence in mind, it is a trivial matter to predict the deterministic outcome of any game, by picking a sequence amenable to a simple analysis. Indeed, any initial state with an even number of black beans must now end in one white one. The semantic" argument given in Gries, 1981 , based on the invarying parity of black beans, requires some insight, whereas the above analysis is entirely mechanical, as we will see later in this chapter. It is obvious that neither of the above games can go on forever, since the number of beans is reduced with each move. A potentially much longer, but still nite, game is: black white ! white white white black white black ! black black black ! white white white white white white ! white The new rules have the same end-e ect as the original ones: no matter how often a bean-increasing move is made, in the nal analysis the can must be emptied down to one bean. Finally, we consider a variant Gries' original problem in which the rules apply to any two not necessarily adjacent beans. The new rules are black : : : white ! black : : : white : : : black ! black : : : black : : : black ! white : : : white : : : white ! white : : : where the ellipsis on the right refers to the same beans as covered by its counterpart on the left. The new rules, in e ect, allow a player to shake" the can prior to making a move. Again, it can be shown that the outcome is uniquely determined by the initial setup and is, consequently, the same as that of the previous two games. The nal result of an unextendible sequence of rule applications is called a normal form." Rewrite systems de ning at most one normal form for any input term can serve as functional programs or as interpreters for equational programs O'Donnell, 1977a . When computations for equal terms always terminate in a unique normal form, a rewrite system may be used as a non-deterministic functional program GoguenTardo, 1979 . Such a system also serves as a procedure for deciding whether two terms are equal in the equational theory de ned by the rules, and, in particular, solves the word problem" for that theory. Knuth Knuth-Bendix, 1970 devised an e ective test based on critical overlaps to determine for any given terminating system if, in fact, all computations converge to a canonical form, regardless of the non-deterministic choices made. In that seminal paper, it was also demonstrated how failure of the test as transpires for the rst Co ee Can game often suggests additional rules that can be used to complete" a non-convergent system into a convergent one. The discovery Fay, 1979 that convergent rewrite systems can also be used to enumerate answers to satis ability questions for equational theories led to their application Dershowitz, 1984 within the logic programming paradigm. Rewriting methods have turned out to be among the more successful approaches to equational theorem proving. In this context, completion is used for forward reasoning," while rewriting is a form of backward reasoning." Completion utilizes an ordering on terms to provide strong guidance during forward reasoning and to direct the simpli cation of equations. Besides the use of convergent systems as decision procedures, Lankford 1975 proposed that completion-like methods supplant paramodulation for equational deduction 2

within resolution-based theorem provers; later, Hsiang 1982 showed how a variant of completion can be used in place of resolution for refutational theorem proving in rst-order predicate calculus. Although completion often generates an in nite number of additional rules, and|at the same time|deletes many old rules, Huet 1981 demonstrated that fairly" implemented completion serves as a semi-decision procedure for the equational theory de ned by the given equations when it does not abort something it might be forced to do on account of equations that cannot be directed without loss of termination. Lankford's procedure paramodulates to circumvent failure of completion. Rewriting techniques have also been applied Musser, 1980 to proving inductive theorems by showing that no contradiction can result from assuming the validity of the theorem in question. In the next two sections, we take a brief look at the syntax and semantics of equations from the algebraic, logical, and operational points of view. To use a rewrite system as a decision procedure, it must be convergent; this fundamental concept is studied in Section 4 as an abstract property of binary relations. To use a rewrite system for computation or as a decision procedure for validity of identities, the termination property is crucial; basic methods for proving termination are presented in Section 5. Section 6 is devoted to the question of satis ability of equations. Then, in Section 7, we return to the convergence property as applied to rewriting. The completion procedure, its extensions, re nements, and main uses, are examined in Section 8. Brief mention of variations on the rewriting theme is made in the nal section. Previous surveys of term rewriting include Huet-Oppen, 1980; Buchberger-Loos, 1982; Jouannaud-Lescanne, 1987; Klop, 1987 .

1.1 Further Reading

2 SYNTAX

Algebraic data types are an important application area for rewrite-based equational reasoning. In the abstract approach to data speci cation, data are treated as abstract objects and the semantics of functions operating on data are described by a set of constraints. When constraints are given in the form of equations, a speci cation is called algebraic Guttag, 1976 . In this section, we talk about the syntax of equations and of equational proofs. As we will see, by turning equations into left-to-right rules", a useful concept of direct" proof is obtained.

2.1 Terms

1

Suppose we wish to de ne the standard stack operations, top and pop, as well as an operation alternate that combines two stacks. Stacks of natural numbers can be represented by terms of the form pushs ; pushs ; : : :; pushsn; : : :, where is the empty stack and the si denote representations of natural numbers, 0, succ0, succsucc0, and so on. The precise syntax of these representations can be given in the following way: Zero = f0g Nat = Zero succNat Empty = fg Stack = Empty pushNat; Stack

2

The left sides of these equations name sets of di erent kinds of terms. An expression like succNat denotes the set of all terms succs, with s 2 Nat. The symbols 0, succ, , and push, used to build data, are called constructors;" any term built according to these rules is a constructor term. To specify the desired stack operations, we must also de ne the syntax of non-constructor terms:

3

top : Stack ! Nat pop : Stack ! Stack alternate : Stack Stack ! Stack Then we give semantics to the new functions by constraining them to satisfy the following set of equations: toppushx; y = x poppushx; y = y alternate ; z = z alternate pushx; y; z = pushx; alternate z; y where x, y, and z are variables ranging over all data of the appropriate type. Inverses of constructors, like top and pop, are called selectors. With these equations, it can be shown, for example, that alternate pushtoppush0; ; ; poppushsucc0; = push0; : A speci cation is said to be su ciently complete" if, according to the semantics, every term is equal to a term built only from constructors; the above operations are not well-de ned in this sense, since terms like pop are not equal to any constructor term. See Section 3.2. In general, given a denumerable set F = n Fn of function symbols|called a nitary vocabulary or signature |and a denumerable set X of variable symbols, the set of rst-order terms T F ; X over F and X is the smallest set containing X such that ft ; : : :; tn is in T F ; X whenever f 2 Fn and ti 2 T F ; X for i = 1; : : :; n. The stack example uses F = f0; g, F = ftop; pop; succg, F = fpush; alternate g, and X = fx; y; z g. The syntax of the stack example also di erentiates between terms of type Nat and of type Stack. Categorizing function symbols, variables, and terms into classes, called sorts, can be very helpful in practice; from now on, however, we will suppose that there is only one, all-inclusive sort. All concepts developed here can be carried over to the many-sorted case, as will be sketched in the Section 9. Each symbol f in F has an arity rank which is the index n of the set Fn to which it belongs. We will assume that the Fn are disjoint, though varyadic" vocabularies pose little problem. In a well-formed term, each symbol of arity n has n immediate subterms. Elements of arity zero are called constants, of which we will always make the sometimes critical assumption that there is at least one constant. Terms in T F F ; X are called monadic ; they are words" spelled with unary symbols from F and ending in a constant from F or variable from X . Variable-free terms are called ground or closed ; the set T F ; ; of ground terms will be denoted by G F . Note that G F is non-empty by the previous assumption. We will often use T to refer to a set of terms T F ; X , with F and X left unspeci ed, and G to refer to the corresponding set of ground terms. Occasionally, we use pre x or post x notation for F and in x for F . A term t in T F ; X may be viewed as a nite ordered tree, the leaves of which are labeled with variables from X or constants from F and the internal nodes of which are labeled with function symbols from F F of positive arity, with outdegree equal to the arity of the label. A position within a term may be represented|in Dewey decimal notation|as a sequence of positive integers, describing the path from the outermost, root" symbol to the head of the subterm at that position. By tjp , we denote the subterm of t rooted at position p. For example, if t = push0; poppushy; z, then tj : is the rst subterm of t's second subterm, which is pushy; z. Positions are often called occurrences ; we will use this latter denomination to refer, instead, to the subterm tjp. We write t s to mean that s is a subterm of t and also write t s to indicate that s occurs within t. We speak of position p as being above position q in some term t if p represented as a sequence of numbers is a pre x of q, i.e. if occurrence tjq is within tjp . A subterm of t is called proper if it is distinct from t. Reasoning with equations requires replacing subterms by other terms. The term t with its subterm tjp replaced by a term s is denoted by t s p . We refer to any term u that is the same as t everywhere except below p, i.e. such that u s p = t, as the context within which the replacement takes place; more precisely, a context is a term u with a distinguished position p. A substitution is a special kind of replacement operation, uniquely de ned by a mapping from variables to terms, and written out as fx 7! s ; : : :; xm 7! sm g when there are only nitely many variables xi not

0 1 0 1 2 0 1 1 0 1 2 0 1 2 2 1 1 1

4

mapped to themselves. Formally, a substitution is a function from X to T F ; X , extended to a function from T to itself also denoted and for which we use post x notation in such a way that ft ; : : :; tn = ft ; : : :; tn , for each f of arity n in F and for all terms ti 2 T . A term t matches a term s if s = t for some substitution ; in that case we write s t and also say that t is an instance of s or that s subsumes t. The relation is a quasi-ordering on terms, called subsumption. For example, fz fa, and fz ffa, since z is less speci c" than a or fa. On the other hand, fx and fz are equally general; we write fx = fz, where = is the equivalence relation associated with , called literal similarity -conversion in -calculus parlance; renaming, in other circles. Subsumption and the subterm ordering are special cases of the encompassment quasi-ordering, in which s t if a subterm of t is an instance of s. Encompassment is called containment" in Huet, 1981 . For example, fz gfa, since fa is an instance of fz. The composition of two substitutions, denoted by juxtaposition, is just the composition of the two functions; thus, if x = s for some variable x, then x = s . We say that substitution is at least as general as substitution , or that is an instance of if there exists a substitution such that = ; we use the same symbols to denote this quasi-ordering on substitutions, as we used for subsumption of terms. For example, fx 7! a; y 7! fag fx 7! y; y 7! fzg = fx 7! z; y 7! fxg. Here, and everywhere, we use the mirror image of a binary relation symbol like for its inverse. In this survey, we will mainly be dealing with binary relations on terms that possess the following fundamental properties: De nition 1. A binary relation ! over a set of terms T is a rewrite relation if it is closed both under context application the replacement" or monotonicity" property and under substitutions the fully invariant property". A transitive and irre exive rewrite relation will be called a rewrite ordering. In other words, ! is a rewrite relation if s ! t implies u s p ! u t p, for all terms s and t in T , contexts u, positions p, and substitutions . The inverse, symmetric closure, re exive closure, and transitive closure of any rewrite relation are also rewrite relations. To x nomenclature, the letters a through h will be used for function symbols; l, r, and s through w will denote arbitrary terms; x, y, and z will be reserved for variables; p and q, for positions; lower case Greek letters, for substitutions. Binary relations will frequently be denoted by arrows of one kind or another. If ! is a binary relation, then is its inverse, $ is its symmetric closure !, ! is its re exive closure ! =, ! is its re exive-transitive closure ! ! and ! is its transitive closure ! ! .

1 1 1 = +

2.2 Equations

1

Replacement leads to the important notion of congruence:" an equivalence relation on a set of terms is a congruence if fs ; : : :; sn ft ; : : :; tn whenever si ti for i = 1; : : :; n. In particular, the re exivesymmetric-transitive closure $ of any rewrite relation ! is a congruence. Note that rewrite relations and congruences form a complete lattice with respect to intersection. Our primary interest is in congruences generated by instances of equations. For our purposes, an equation is an unordered pair fs; tg of terms. For other purposes, it is preferable to regard equations as ordered pairs. Equations will be written in the form s = t. The two terms may contain variables; these are understood as being universally quanti ed. Given a nite or in nite set of equations E over a set of terms T , the equational theory of E, T hE, is the set of equations that can be obtained by taking re exivity, symmetry, transitivity, and context application or functional re exivity as inference rules and all instances of equations in E as axioms. Thus, if E is recursively-enumerable, so are its theorems T hE. We write E ` s = t if s = t 2 T hE.

1 2

1 A quasi-ordering _ is any re exive and transitive binary relation; the associated equivalence relation is the intersection of _ with its inverse; the associated strict" i.e. irre exive partial order is their di erence. 2 To avoid confusion, authors are frequently forced to use a di erent symbol in the syntax of equations, instead of the heavily overloaded equals sign"|a precaution we choose not to take in this survey.

5

A more compact inference system is based on the familiar notion of replacement of equals for equals" a.k.a. Leibniz's Law. We write s $E t, for terms s and t in T , if s has a subterm that is an instance of one side of an equation in E and t is the result of replacing that subterm with the corresponding instance of the other side of the equation. Formally, s $E t if s = u l p and t = u r p for some context u, position p in u, equation l = r or r = l in E, and substitution . It is folk knowledge that E ` s = t i s $ E t, where $ is the re exive-transitive closure of $E ; in other words, two terms are provably equal if one E may be obtained from the other by a nite number of replacements of equal subterms. The relation $E is the rewrite" closure of E, when the latter is viewed as a symmetric relation, and $ is the congruence E closure of $E , i.e. $ is the smallest congruence over T such that l $ r for all equations l = r in E E E and substitutions over T . We will write s E for the congruence class of a term s, and denote by T =E the set of all congruence classes, i.e. the quotient of the set T F ; X of terms and the provability relation $ . E A derivation in E is any sequence s $E s $E $E si $E of applications of equational axioms in E. A proof in E of an equation s = t is a justi ed" nite derivation s = s $E $E sn = t n 0, each step si $E si of which is justi ed by reference to an axiom l = r in E, a position pi in si , and a substitution i , such that si jpi = l i and si = si r i pi . Returning to our stack speci cation, and letting E be its axioms, the following is an example of a derivation: alternate pushtoppush0; z; z; $E alternate push0; z; $E alternate push0; poppushsuccy; z;

0 1 0 +1 +1

The rst step may be justi ed by the axiom toppushx; y = x, position 1:1, and substitution fx 7! 0; y 7! z g; the second step, by the axiom poppushx; y = y used from right to left, position 1:2, and substitution fx 7! succy; y 7! z g.

2.3 Rewrite Rules

The central idea of rewriting is to impose directionality on the use of equations in proofs. Unlike equations which are unordered, a rule over a set of terms T is an ordered pair hl; ri of terms, which we write as l ! r. Rules di er from equations by their use. Like equations, rules are used to replace instances of l by corresponding instances of r; unlike equations, rules are not used to replace instances of the right-hand side r. A nite or in nite set of rules R over T is called a rewrite system, or more speci cally a term-rewriting system. A system R may be thought of as a non-symmetric binary relation on T ; the rewrite closure !R of this relation describes the e ect of a left-to-right application of a rule in R. De nition 2. For given rewrite system R, a term s in T rewrites to a term t in T , written s !R t, if sjp = l and t = s r p , for some rule l ! r in R, position p in s, and substitution . This is the same as saying that s = u l p and t = u r p, for some context u and position p in u. A subterm sjp at which a rewrite can take place is called a redex ; we say that s is irreducible, or in normal form, if it has no redex, i.e. if there is no t in T such that s !R t. Systems of rules are used to compute by rewriting repeatedly, until, perhaps, a normal form is reached. A derivation in R is any nite or in nite sequence t !R t !R !R ti !R of applications of rewrite rules in R. The reducibility, or derivability, relation is the quasi-ordering ! , i.e. the re exive-transitive R closure of !R . We write s !R t if s ! t and t is irreducible, in which case we say that t is a normal form R of s. This normalizability relation !R is not a rewrite relation, since normalizing a subterm does not mean that its superterm is in normal form. One says that a rewrite system is normalizing if every term has at least one normal form. A ground rewriting-system is one all the rules of which are ground i.e. elements of G G ; an important early paper on ground rewriting is Rosen, 1973 . A string-rewriting system, or semi-Thue system, is one that has monadic words ending in the same variable i.e. strings of elements of T F ; fxg as left- and right-hand side terms; Book, 1987 is a survey of string rewriting. The rst three Co ee Can Games can

0 1 ! ! 1

6

be formulated as string-rewriting systems, with white and black as monadic symbols. A left-linear system is one in which no variable occurs more than once on any left-hand side. Ground- and string-rewriting systems are special cases of left-linear systems, with no variable and one variable per term, respectively. For our purposes, one of the most essential properties a rewrite system R can enjoy is unique normalization, by which is meant that every term t in T possesses exactly one normal form. The normalizability relation !R for uniquely-normalizing systems de nes a function, and we denote by Rt the value of that function for a term t in T . If all sequences of rewrites lead to a unique normal form, the system will be called convergent. A rewrite system R is said to be inter-reduced if, for each rule l ! r in R, the right-hand side r is irreducible under R and no term s less than l in the encompassment ordering is reducible. For convergent R, this is equivalent to the standard de nition Huet, 1981 which requires that the left-hand side l not be rewritable by any other rule. As we will see this, too, is a convenient property. We will reserve the adjective canonical for reduced convergent systems, though, in the literature, canonical" is usually synonymous with convergent". Orienting the equations of the stack example gives a canonical rewrite system R: toppushx; y ! x poppushx; y ! y alternate ; z ! z alternate pushx; y; z ! pushx; alternate z; y

!

That every term has at least one normal form will be shown in Section 5.3; that there can be no more than one normal form will be shown in Section 7.2. A derivation is any nite or in nite chain t !R t !R of rewrite steps. An example is: alternate pushtoppush0; z; z; !R alternate push0; z; !R push0; alternate ; z !R push0; z.

1 2

The rst step is an application of the top-push rule at the occurrence toppush0; z; the second is an application of the alternate -push rule, with 0 for x, z for y, and for z; the third, of alternate ; z ! z. Note that an alternative derivation is possible, leading to the same normal form: alternate pushtoppush0; z; z; !R pushtoppush0; z; alternate ; z !R pushtoppush0; z; z !R push0; z. Operationally, then, rewriting is a non-deterministic computation, with the choice of rule and position left open. For convergent systems, the choice among possible rewrites at each step does not a ect the normal form computed for any given input term. De nition 3. A binary relation ! on a set T is terminating if there exists no endless chain t ! t ! t ! of elements of T . Such relations have sometimes been called Noetherian in the term-rewriting literature|after the algebraicist, Emily Noether|though the adjective is ordinarily used to exclude in nite ascending chains. Termination is more than being normalizing, since the latter allows some derivations to be in nite. A partial irre exive ordering of a set T is well-founded if there exists no in nite descending chain t t of elements of T. Thus, a relation ! is terminating i its transitive closure ! is a well-founded ordering. The importance of terminating relations lies in the possibility of inductive proofs in which the hypothesis is assumed to hold for all elements t such that s ! t when proving it for arbitrary s. Induction on terminating relations, sometimes called Noetherian induction," is essentially well-founded induction i.e. trans nite induction extended to partial orderings; see, for example, Cohn, 1981 . We will have occasion to employ this technique in Sections 4.1 and 8.2. A rewrite system R is terminating for a set of terms T if the rewrite relation !R over T is terminating, i.e. if there are no in nite derivations t !R t !R of terms in T . When a system is terminating,

1 2 3 1 2 + + 1 2

7

Figure 1: Joinability properties of relations. every term has at least one normal form. Note that a terminating system cannot have any rule, like alternate y; ! poppushx; y, with a variable on the right that is not also on the left since x could, for example, be topalternate y; , nor can a left-hand side be just a variable, like z ! alternate ; z. These two restrictions are often placed a priori on rewrite rules cf. Huet, 1980 , something we prefer not to do. Methods for establishing termination are described in Section 5. A valley, or rewrite, proof for a system R of an equation s = t takes the form s ! v t, in which R R the same term v is reached by rewriting s and t. Here is an example, using the above system: alternate pushtoppush0; z; z; alternate push0; poppushy; z; !R alternate push0; z; push0; alternate ; poppushy; z R !R push0; alternate ; z R With a terminating system of only a nite number of rules, the search space for rewrite proofs is nite. Of course, there is|in general|no guarantee that such a direct" proof exists for a particular consequence of the equations represented by R. When that is the case, i.e. when the relation $ is contained in ! , R R R the system is called Church-Rosser , after a property in Church-Rosser, 1936 . See Figure 1a. Equivalent properties are de ned in Section 4 and methods of establishing them are described in Section 7.

2.4 Decision Procedures

One of our main concerns is in decision procedures for equational theories; an early example of such a procedure for groups is Dehn, 1911 . Terminating, Church-Rosser rewrite systems are convergent and de ne unique normal forms. For a convergent system R to determine provability in its underlying equational theory treating its rules as equational axioms, it should have only a nite number of rules. Then, to decide if s = R t, one can test if computing the normal forms Rs and Rt results in the same term. The Church-Rosser property means that $ = ! ; termination ensures that ! = !R R ; niteness of R makes R R R R R !R decidable; and Church-Rosser implies that !R de nes a function R. Thus, a system R provides a decision procedure for the equational theory of a set of axioms E if R is a nite, b terminating, c Church-Rosser, and d sound and adequate for E. Here, soundness means that the rules of R are contained in the relation $ , and adequacy means that E is contained in $ ; together, they imply that $ = $ . E R E R

! ! ! !

8

In our stack example, R is sound and adequate for E; hence, R decides equality in E. In general, a system R with the properties a-d is said to be complete for E. Given a set of equations E, its word problem is the question whether an arbitrary equation s = t between two ground terms follows from E. The word problem is, thus, a special case of provability in E for arbitrary equations. If R is a convergent system for E, its word problem is decidable by reducing s and t to their R-normal form. Actually, it is enough if R is ground-convergent , that is, if every ground term has a unique normal form. Many rewriting-system decision procedures are known; perhaps the rst rewriting-based decision procedure for a word problem is the one in Evans, 1951 for loops". When a rewriting decision procedure exists, it can be very e ective. In Section 8, we will elaborate on systematic methods used to generate convergent systems from given equational axioms. Of course, not all equational theories can be decided by rewriting|for a variety of reasons. First, some theories classes of equations are not nitely based ; for such theories there exists no nite set of axioms from which all other equations in the theory follow. An example Taylor, 1979 is the intersection of the theories consequences of the following two semigroups abbreviating products by juxtaposition and exponentiation: xyz = xyz xyz = xyz xyz = x y z xy = yx xyzz = yxzz Nor are all nitely-based equational theories decidable, the rst counter-examples having been given by Markov 1947 and Post 1947 , in a slightly di erent context. See the interesting historical comments at the end of Tarski-Givant, 1985 . A prime example of an undecidable equational theory is Combinatory Logic with binary in x symbol " and constants S, K, and I:

2 2 2 2 3 3 3 3 3 3 2 1 3 2 3 3 2 1 3 2

I x = x K x y = x S x y z = x z y z see Curry-Feys, 1958 . Most disconcertingly, there are nitely-based, decidable theories for which there can be no rewriting-system decision procedure. For example, no nite system|even over an enlarged vocabulary|can rewrite any two terms, equal by commutativity, to the same term Dershowitz-etal, 1988 . In other words, no term-rewriting system can decide validity in the decidable theory de ned by the commutativity axiom, x y = y x, since that equation, oriented in either direction, gives a non-terminating rewrite system. Deciding word problems is a somewhat di erent question, since then one looks only at ground equations over a nite vocabulary. But this same example let F = f0; succ; g demonstrates that not all decidable word problems can be decided by a nite rewrite system over the same vocabulary; cf. Klop, 1987 . The following is one of the simple semigroup theories with an undecidable word problem given in Matijasevic, 1967 F = fa; bg, F = fg, and products are abbreviated as before:

0 2

xyz aba b a bab a aba b b a b a ba a b a ba

2 2 2 2 3 2 3 2 4 2 2 2 2

= = = = = =

xyz b a ba b a ba ab aba baba ba

2 2 2 3 2 3 2 2 4 2

2 4

2.5 Extensions

Happily, rewriting techniques can be adapted to handle some of the more important cases, in which any orientation of the axioms yields a non-terminating system. The simplest example of a structural" axiom requiring special treatment is commutativity: any system containing either x y ! y x or y x ! x y is 9

perforce non-terminating. We describe two techniques for dealing with such axioms, class rewriting" and ordered rewriting." A congruence- class-rewriting system comes in two parts: rules and equations. By R=S we denote the class system composed of a set R = fli ! ri g of rewrite rules and a set S = fui $ vi g of equations, the latter written with double-headed arrows to stress their symmetrical usage. Generalizing the notion of term rewriting, we say that s rewrites to t modulo S, denoted s !R=S t, if s $ u l p and u r p $ t, for S S some context u, position p in u, rule l ! r in R, and substitution . Thus, R is essentially computing in the quotient set T =S = f t S jt 2 T g of S-congruence classes more precisely, $ -congruence classes, rewriting a S term by rewriting any S-equivalent term. Class-rewriting systems were introduced in Lankford-Ballantyne, 1977a for permutative congruences, that is, congruences for which each congruence class is nite. Of great practical importance are associative-commutative AC rewrite systems, where S is an equational system consisting of associativity and commutativity axioms for a subset of the binary symbols in F . The last Co ee Can Game can be formulated as an AC system, by using an associative-commutative operator for adjacency with the four rules of the second game. Then, black white black can rewrite directly to black black or, via black black white, to white white. The notions of derivation and normal form extend naturally to class-rewriting systems. We say that R=S is terminating if !R=S is terminating and that it is Church-Rosser modulo S if $ is contained R=S in ! $ . More generally, any rewrite relation !T is Church-Rosser modulo S if $ T S S R=S R=S ! $ ; see Figure 1f. For instance, let BA=AC be the following class system over vocabulary F T S T = fand ; xor g and F = fF; T g:

2 2 0

BA

and x; T and x; F and x; x xor x; F xor x; x and xor x; y; z

AC

and x; y and x; and y; z xor x; y xor x; xor y; z

! ! ! ! ! !

x F x x F

xor and x; z; and y; z

$ $ $ $

and y; x and and x; y; z xor y; x xor xor x; y; z

This system is convergent, i.e. terminating and Church-Rosser modulo AC Hsiang, 1982 ; it computes normal forms of Boolean-ring expressions that are unique up to permutations under associativity and commutativity. The exclusive-or normal form is due to Zhegalkin, 1927; Stone, 1936 . The idea, then, is to put equations that cannot be handled by rewriting into S, placing in R only rules that preserve termination. If R=S is also Church-Rosser modulo S, then s $ S t i their normal forms are R S-equivalent. For this to work, there are two additional considerations: S-equivalence must be decidable, and R=S normal forms must be e ectively computable. The latter requirement does not, however, come automatically, even if R is nite and S-equivalence is decidable, since a rule in R is applicable to a term when any S-equivalent term contains an instance of a left-hand side, whereas S-equivalence classes need be neither nite nor computable. Note that a class system R=S cannot be terminating if R is non-empty and S contains an equation with a variable on one side not also on the other, or if it contains an axiom like idempotency, x x = x, with a lone variable on one side and more than one occurrence of it on the other. Even if S-equivalence classes are computable, they may be impractically large, making class-rewriting prohibitively expensive. These di culties with R=S are usually circumvented by using a weaker rewrite relation, introduced in Peterson-Stickel, 1981 . We denote this relation by !S nR others have used ,!R;S ; under it, a term is rewritten only if it has a subterm that is equivalent to an instance of a left-hand side. We call !S nR the extended" rewrite relation for R; our notation is meant to suggest that S-steps are not applied above the R-step. Formally: De nition 4. For given rewrite system R and congruence relation S, the S-extended rewrite relation !S nR is de ned by s !S nR t, for two terms s, t in T , i sjp $ l and t = s r p, for some rule l ! r in R, position S 10

p in s, and substitution . The notions of normal-form, etc., are analogous to the previous de nitions. We say that S nR is ChurchRosser modulo S if if !S nR is, i.e. any two terms, equal in R S, lead to S-equivalent terms via extended rewriting with S nR. S-extended rewriting avoids the need to compute S-congruence classes, requiring instead an S-matching algorithm: We say that a term t S-matches l, if there exists a substitution such that l $ t. MatchS ing algorithms are known for many theories, including associativity, commutativity, and associativity with commutativity; see Section 6.2. If R is nite and S-matching substitutions are computable, then !S nR is computable, too. The relation !S nR is a subset of !R=S , and hence does not necessarily render the same normal forms. For the above system BA=AC, we have and a; and a; b ,!BA=AC and a; b, but and a; and a; b 6,!BAnAC and a; b. However, it is often the case that by adding certain consequences as new rules, the two relations can be made to coincide, as shown in Peterson-Stickel, 1981 for AC, and in Jouannaud-Kirchner, 1986 for the general case. When R=S is terminating and S nR is Church-Rosser modulo S, the theory R S can be decided by computing S nR-normal forms and testing for S-equivalence. For example, if BA is augmented with the two rules, and x; and x; y ! and x; y and xor x; xor x; y ! y, then AC-extended rewriting su ces to compute the normal forms of BA=AC. In Section 4.2, conditions for equivalence of normal forms are discussed. An ordered-rewriting systems also comes in two parts: a set of equations and an ordering. Ordered rewriting does not require that a particular equation always be used from left-to-right. Instead, an equation may be used in whichever direction agrees with the given ordering on terms. Suppose, for example, that x y = y x is an equation and that a b is greater than b a in the ordering. Then, we would use commutativity to rewrite a b to the normal form b a, but not vice-versa. De nition 5. Given a set E of equations over a set of terms T and a rewrite ordering transitive and irre exive rewrite relation over T , a term s in T rewrites to a term t in T according to , denoted s !E t, or just s ! t, if s = u l p, t = u l p and l r , for some context u, position p in u, equation l = r in E, and substitution . This corresponds to considering each instance l = r of an equation as a rewrite rule going one way or the other. Thus, the ordered-rewriting relation ! , is contained in the rewrite relation obtained from the intersection of the two rewrite relations, $E and ; in particular, s t if s ! t. The relation ! is equivalent to the intersection when is total.

2.6 Further Reading

The standard work on the Lambda Calculus is Barendregt, 1984 ; its role in the semantics of functional programming is discussed in Barendregt, 1989 . Evans 1951 and Knuth Knuth-Bendix, 1970 pioneered the use of rewrite systems as decision procedures for validity in equational theories. Bledsoe 1977 was an early advocate of incorporating rewriting techniques in general-purpose theorem provers.

3 SEMANTICS

As is usual in logic, models give meaning to syntactic constructs. In our case, the models of equational theories are just algebras, that is, sets with operations on their elements, and provability by equational reasoning coincides with truth in all algebras. When a rewrite system has the unique normalization convergence property, a term's normal form can be its meaning". It turns out that the set of irreducible terms of a convergent system yields an algebra that is free" among all the algebras satisfying the axioms expressed by its rules. The free algebra is that model in which the only equalities are those that are valid in all models. 11

Let F = n Fn be a signature. An F -algebra A consists of a non-empty domain of values, called the universe or carrier, or underlying set , which we also denote A when feasible, we will use boldface for the algebra and italics for the corresponding universe, and a family FA of F -indexed nitary fundamental operations, such that for every symbol f of arity n in Fn , the corresponding operation fA in FA maps An to A. Since we presume the existence of at least one constant in F , universes will always be non-empty. Given an assignment : X ! A of values to each of the variables in X , the F -algebra A attaches a meaning to each term t of T F ; X , which is the result of applying the operations corresponding to each function symbol in t using the values assigned by for the variables. Let E be a set of equations; an algebra A is a model of E if, for every equation s = t in E, and for every assignment of values to variables in s and t, the meanings of s and t are identical. From now on, we generally omit reference to F and just speak of algebras". By ModE we denote the class of all models of E, each of which is an algebra. Consider the algebra A whose universe contains two elements, a black co ee bean and a white one: A = fblack; whiteg. The algebra has two operations: a unary operation invert" which turns a white bean into a black one and vice-versa, and a binary operation move" which takes two beans and returns a bean according to the rules of the second Co ee Can Game of Section 1. It is easy to see that this algebra is a model of the associative axiom x y z = x y z, interpreting " as move," since the result of a game does not depend upon the order of moves. However, interpreting the unary symbol , " as invert" and the identity constant 1 as white does not yield a group, since a black white move gives a black bean, and not the identity element. To obtain a group as might be preferred by some mathematicians, we must change the rules of the game slightly: black white ! black white black ! black black black ! white white white ! white This algebra is a model of all three group axioms. A class K of algebras is a variety if there exists a set E of equations such that K = ModE. For example, though groups are axiomatizable non-equationally by giving one associative operator " and a constant 1 satisfying 8x9yx y = 1, they may also be axiomatized in the following way:

0

3.1 Algebras

1x = x x, x = 1 x y z = x y z Groups are actually one-based," with the following axiom providing a basis: x=x=x=y=z=x=x=x=z = y Higman-Neumann, 1952 . Note that groups de ned in the latter way give a di erent variety than the previous axiomatization, since their signatures di er; nevertheless, the two equational theories are essentially the same, since the operations of one are de nable in terms of the other in particular, x=y = x y, and x y = x=x=x=y. Rings, commutative rings, and lattices are also varieties; elds are not. Tarski has endeavored to equationally axiomatize the foundations of mathematics; see Tarski-Givant, 1985 . Huet 1985 has shown that much of category theory is equational. A mapping is a homomorphism from algebra A to algebra B, if fA a ; : : :; an = fB a ; : : :; an , for all f 2 Fn and ai 2 A. An isomorphism is a bijective homomorphism. Any assignment : X ! B of values to variables extends in this way to a homomorphism : T ! B by letting ft ; : : :; tn = fB t ; : : :; tn . An equation s = t is valid or true in a speci c algebra B if, for all assignments of values in B to variables in s and t, s and t represent the same element of B. Satis ability" is the dual of validity: an equation is satis able in an algebra if it has a solution in that algebra, that is, if there is an assignment of values to

1 1 1 1

12

variables for which both sides yield the same value. Validity of an equation s = t that is, validity in all models is expressed as ModE j= s = t, or s =E t for short. Varieties are characterized in the following algebraic way Birkho , 1935 : A class of algebras K is a variety i it is closed under Cartesian products, subalgebras, and homomorphic images. That is, a class K of algebras is a variety if a for any A , : : :, An in K n 0, their product A An is also in K, where fA1 An : : : ha ; : : :; ani : : : = hfA1 : : :a : : :; : : :; fAn : : :an : : :i; b for any subset B of A for algebra A in K, the subalgebra obtained by restricting fA to B for each f in F is also in K; and c for any homomorphism : A ! B between universes, if A is in K, then so is the algebra B wherein fB : : : ai : : : = fA : : :ai : : :. This result of Birkho 's can be used to show that an operation is not equationally axiomatizable. For instance, the models of strict if then else are not closed under products, hence, no set of equations can characterize that operation. Still, it is remarkable that equational axioms E can be given for if then else such that an equation is valid for ModE i it is valid in the if-then-else" models Bloom-Tindell, 1983; Guessarian-Meseguer, 1987 . Let E be a set of equations. Clearly, replacement of equals for equals is sound, i.e. E ` s = t implies ModE j= s = t for all s and t. For the other direction, consider the quotient algebra T =E described in Section 2.2. It is one of the models of E. Since classes T =E are de ned by the congruence $ , which is E just replacement of equals, we have T =E j= s = t implies E ` s = t. Together, we get the following: Completeness Theorem Birkho -1935. For any set of equations E and terms s and t in T , ModE j= s = t i T =E j= s = t i E ` s = t. Accordingly, we may use the semantic notion =E and syntactic notion $ interchangeably. It follows that E a convergent rewrite system R decides validity for the models of its rules, since s $ t i Rs = Rt. R A substitution is a homomorphism from T to itself. If there exists a substitution : T ! T such that s and t are identical, then for any algebra B there exists a homomorphism : T ! B such that s = t. In other words, if an equation is satis able in the term algebra T , then it is satis able in all algebras. Similarly, any equation satis able in the quotient algebra T =E is satis able in all algebras in ModE. Satis ability in T is called uni ability ; satis ability in T =E is called E-uni ability. The uni cation problem is the subject of Section 6.

1 1 1 1 3

3.2 Initial Algebras

For many purposes, not all models are of equal interest. One generally asks whether an equation is valid in a speci c model. For example, one might ask whether the equation alternate y; = y is true for all stacks y. Of course, all equations are valid, let alone satis able, in a trivial algebra having only one element in its domain. For applications like abstract data types, attention is often focused on those standard" models that are nitely generated from the signature itself, in which every element of the domain is the interpretation of some term. An algebra A in a class K of algebras is free over a set X of variables if X is a subset of A and, for any algebra B 2 K and assignment : X ! B, there exists a unique homomorphism : A ! B such that and agree on X . A free algebra is unique up to isomorphism, whenever it exists. The free algebra over X among all algebras is just isomorphic to the term algebra T F ; X with the the symbol f 2 F itself as the operator fT . An algebra A in a class K of algebras is initial if, for any algebra B in K there exists a unique homomorphism : A ! B. The initial object among all F -algebras is isomorphic to the ground-term algebra G F , again with the function symbol itself as operator, and corresponds to the Herbrand universe over the symbols in F . The importance of the initial algebra lies in its uniqueness it is the free algebra for empty X , and in the fact that the class K consists of its homomorphic images, making it the most abstract" among them. Among all models of a set of equations E, the prototypical one is the initial algebra IE of E. Its universe consists of one element for each E-congruence class of ground terms. In other words, IE is isomorphic

3

An operation is strict, or naturally extended, if it yields the unde ned value whenever one of its arguments is unde ned.

13

to the quotient G =E of the ground-term algebra G and the congruence $ restricted to G . This algebra E can be realized if R is a ground-convergent rewrite system for E, since, then, E-equivalent ground terms have the same R-normal form. Accordingly, the normal-form algebra of R has the set of ground R-normal forms as its universe and operations fR de ned by fR t ; : : :; tn = Rft ; : : :; tn for all normal forms ti. This algebra is isomorphic to the initial algebra IR of the variety de ned by the rules in R considered as equations Goguen, 1980 . Thus, rewriting computes ground normal forms that are representatives of their congruence classes. It is in this sense that rewriting is a correct" implementation of initial-algebra semantics. Speci cation languages based on abstract data types, such as OBJ Futatsugi-etal, 1985 , follow this implementation scheme: equations are used as rewrite rules, and unique normalization is needed for the operational and initial algebra semantics to coincide. Exactly those variable-free equations that follow necessarily from E hold in the initial algebra. Thus, the word problem for E, i.e. deciding, for ground terms s and t, whether s = t holds in every model of E, is the same as determining if IE j= s = t. More generally, one may ask if an equation s = t possibly containing variables is valid in the initial algebra IE, which is the case i all of its ground instances hold for ModE. We will write s =I E t as an abbreviation for IE j= s = t and call the class I ndE of equations s = t valid in IE the inductive theory of E. It is easy to verify that the relation =I E is a congruence over T F ; X . Unlike equational theories, inductive theories are not necessarily recursively enumerable even for nite E. The inductive theory includes all the equations in the equational theory; on the other hand, an equation that holds in the initial model need not hold in all models, i.e. the inclusion T hE I ndE may be strict. Tarski 1968 dubbed !-complete those equational theories that coincide with the associated inductive theory, but !-completeness is not possible, in general Henkin, 1977 . Finally, note that if an equation s = t is not valid in IE, that means that some ground equation u = v which does not hold for ModE does hold for ModE fs = tg. For example, let F = f0; succ; ; push; alternateg and let E be alternate ; z = z alternate pushx; y; z = pushx; alternate z; y The equation alternate y; = y is valid in IE, since it is provable for all ground terms of the form pushs ; pushs ; : : :; pushsn; : : :, and all other ground terms entailing alternate are provably equal to one of this form. It is not, however, valid in a model A that, besides the usual stacks, includes stacks built on top of another empty-stack value, , and for which alternate A ; A = A . Thus, by Birkho 's Completeness Theorem, alternate y; = y is not an equational consequence of the given axioms. For a system R to correctly implement an algebraic speci cation E, it is enough that their inductive theories are the same, i.e. that I ndE = I ndR, when the rules of R are considered as equations. For example, the convergent three-rule system alternate ; z ! z alternate y; ! y alternate pushx; y; z ! pushx; alternate z; y is a correct implementation of the above speci cation E of alternate , since all equations in E are deductive theorems of R and all rules in R are inductive theorems of E. The notion of su cient completeness of function de nitions and its relation to software speci cation was introduced in Guttag, 1976 : De nition 6. Let the set F of function symbols be split into a set C of constructors and a set F , C of other symbols. Let E be a set of equations in T F ; X . The speci cation E is su ciently complete or has no junk" with respect to C , if every ground term t in G F is provably equal to a constructor term s in G C . De nition 7. Let C be a set of constructors and let E be a set of equations split into a set EC of equations in T C ; X and a set EF,C of other equations. The constructors C are said to be free when EC is empty. The

1 1 1 2 0 0

14

speci cation E is consistent or has no confusion" with respect to C , if for arbitrary ground constructor terms s and t in G C , s =E t i s =E t. This generalizes the standard notion of consistency, which is with respect to the Boolean values T and F. For example, the previous speci cation for stacks becomes inconsistent with respect to the free constructors f0; succ; ; pushg, if it is enriched" with the equation alternate y; = alternate y; y, since that implies push0; = push0; push0; . Adding an equation pushx; pushy; z = pushy; pushx; z to EC makes the constructors non-free and constructor terms represent unordered bags." When a set of equations is both consistent and su ciently complete, it is reasonable to consider it a speci cation" of the functions in F ,C . In this case, the algebra G F =E, considered as a C -algebra, is isomorphic to G C =EC . This allows one to build complex speci cations from simpler ones. Unfortunately, both properties are undecidable in general see Guttag, 1976 . As mentioned above, term-rewriting is used to compute in the initial algebra. More generally, if R=S is a ground-convergent class-rewriting or ordered-rewriting system, then the normal-form algebra, with universe RG = f Rt S jt 2 Gg and operations de ned by fR a ; : : :; an = Rfa ; : : :; an S for all ai 2 RG , is initial for the variety de ned by R S, and RG is isomorphic to IR S. In implementing a su ciently complete speci cation, one would want all ground normal forms to be constructor terms, i.e. that RG F G C . In certain cases, su cient completeness can be related to the following more tractable property: De nition 8. For any rewrite relation !T , a term s in T is ground T-reducible, if all its ground instances s 2 G are rewritable by !T . Suppose that a a ground-convergent class-rewriting system R=S is complete for an equational speci cation E, b the R=S-normal form of any ground constructor term in G C is a ground constructor term, and c S does not equate any ground constructor term with a ground non-constructor term in G F , G C . For a system R=S satisfying these properties, E is su ciently complete i all terms fx ; : : :; xn are ground R=Sreducible, when f is in F ,C and xi are distinct variables in X . The rationale is that, by ground reducibility, any non-constructor term t must contain a reducible subterm, and, since the system is terminating and sound for E, t must be equal to a constructor term. This connection between su cient completeness and ground reducibility is implicit in Plaisted, 1985 . If each left-hand side of a rule in R and each side of an equation in S contains a non-constructor symbol, then property b is ensured; cf. Huet-Hullot, 1980 . Ground reducibility is decidable for nite R and empty S Plaisted, 1985; Kapur-etal, 1987 . A faster decision method is obtained by reducing ground reducibility to the emptiness problem of the language produced by a conditional tree grammar" describing the system's ground normal forms Comon, 1989 . Testing for ground R-reducibility, however, requires exponential time, even for left-linear R Kapur-etal, 1987 . In the special case where all constructors are free, ground reducibility is more easily testable. This case had been considered in Nipkow-Weikum, 1982 for left-linear systems. The general case was considered in Dershowitz, 1985 and Kounalis, 1985 . The former de nes a test set" for ground-reducibility by instantiating fx ; : : :; xn in all possible ways up to a bound that depends on the maximal depth of a left-hand side; the latter constructs a smaller test set, computed by repeated uni cation of fx ; : : :; xn with left-hand sides, and improves on Thiel, 1984 . Ground R=S-reducibility is undecidable when S is a set of associative-commutative axioms Kapur-etal, 1987 , but is decidable when R is left-linear JouannaudKounalis, 1989 . For ground-convergent systems R, any equation between distinct R-normal forms is considered to be inconsistent with R considering all symbols in F as constructors. The observation that an equation s = t is valid in the initial algebra IR i no inconsistency follows from R fs = tg is the basis of the proof by consistency method of inductive theorem proving for proving theorems in I ndR, pioneered by Musser 1980 and so named in Kapur-Musser, 1987 . If there exists a ground-convergent system R0, with the same ground normal forms as R, and which presents the same equational theory as R fs = tg, then inconsistency is precluded Lankford, 1981 . It can readily be shown that RG R0G , for any two systems R and R0 , i every left-hand side of R0 is ground R-reducible Dershowitz, 1982b;

C

1 1 1 1 1

15

Jouannaud-Kounalis, 1989 . It follows that R and R0 have the same inductive theory if they are both ground convergent and every left-hand side of one system is ground reducible by the other. This method, relating validity in the initial algebra to ground-reducibility, extends to class-rewriting, with ground R=S-reducibility replacing its ordinary counterpart Goguen, 1980; Lankford, 1981; Jouannaud-Kounalis, 1989 . In Section 8, we will consider how to search for an appropriate R0. Note that the equation alternate y; = y is not an inductive theorem of the earlier stack speci cation, given at the beginning of Section 2.1, even though it holds for all stacks , pushs ; , etc. The problem is that the full vocabulary has a richer set of ground terms, involving top and pop, but their speci cation is not su ciently complete. In particular, the equation in question does not hold true for error" terms like pop: alternate pop; = pop does not follow from the axioms. Test-set based methods for proofs in the non-initial constructor model are described in Kapur-etal, 1986; Zhang, 1988 ; see also Kapur-Musser, 1987 .

1

3.3 Computable Algebras

When a system R is not terminating, rewriting will not necessarily compute a representative for the congruence class of a term. However, as long as R is Church-Rosser, one knows that if a normal form is obtained, it is unique. Of course, one can always turn a nite set of equations into a Church-Rosser system by turning each equation into a symmetric pair of rules, but then no term at all has a normal form. More interesting is the ability to code interpreters for functional languages as Church-Rosser systems that are normalizing for input programs that terminate for the given input values; see O'Donnell, 1977b . Furthermore, there are computational strategies that is, speci c choices of where to rewrite next, such as not forever ignoring an outermost" redex one that is not a subterm of another redex, that are guaranteed to result in a normal form whenever there is one O'Donnell, 1977a . An optimal strategy, i.e. one with normalizing derivations of minimal length, is not in general computable Huet-Levy, 1990 . Turing machine computations can be simulated by rewrite systems in at least two di erent ways: by systems of monadic rules that rewrite instantaneous descriptions according to the machine's transitions Huet-Lankford, 1978 , and by a non-monadic one-rule system in which the transitions appear as part of the terms Dauchet-1989 , re ning Dershowitz, 1987 . Thus, rewrite systems provide a fully general programming paradigm to the extent that Church's Thesis de nes fully general". These constructions also imply that most interesting properties, including convergence, are in general undecidable. On the other hand, equality the word problem is decidable in what are called computable" algebras Meseguer-Goguen, 1985 ; see Wirsing, 1989 . For a survey of equational logic, see Taylor, 1979 . A comprehensive multi-volume work on varieties is McKenzie-etal, 1987; Freese-etal, 1989 . Some relevant recent results are summarized in McNulty, 1989 . A detailed exposition of algebraic aspects of rewriting is Meseguer-Goguen, 1985 ; algebraic semantics are the subject of Wirsing, 1989 .

3.4 Further Reading

4 CHURCH-ROSSER PROPERTIES

Newman 1942 developed a general theory of sets of moves," that is, of arbitrary binary relations. It has since become customary to deal separately with properties of such abstract binary relations and with those of relations on terms. In our discussion of the Church-Rosser property, we continue in that tradition, putting o almost all mention of rewrite systems to later sections.

16

4.1 Con uence

In Section 2, we de ned the Church-Rosser property for rewrite systems. The analogous property can hold for any binary relation: De nition 9. A binary relation ! on any set T is Church-Rosser if its re exive-symmetric-transitive closure $ is contained in the joinability relation ! . See Figure 1a. This is equivalent to the following simpler property: De nition 10. A binary relation ! on any set T is con uent if the relation ! is contained in the joinability relation ! . Con uence says that no matter how one diverges from a common ancestor, there are paths joining at a common descendent. Sometimes the notation " is used for the common ancestor relation and for joinability common descendent; then con uence boils down to " . See Figure 1b. The equivalence with the Church-Rosser property Newman, 1942 , can be shown by a simple inductive argument on the number of divergences ! making up $ . For arbitrary !, de ne s ! t i s ! t and there is no u such that t ! u and call t the normal form of s. Con uence implies the impossibility of more than one normal form. A binary relation ! on a set is strongly con uent if any local divergence ! is contained in the immediate descendent relation ! , i.e. if for any peak s u ! t of elements s, t, and u, one of the following four cases holds: s = t, s t, s ! t, or s ! v t for some element v. See Figure 1c. A slightly weaker de nition is given in Huet, 1980 , namely ! ! , which also allows for circumstances like a ! b, a ! c, b ! d ! c, and c ! d ! b. Strong con uence implies con uence Newman, 1942 by a tiling" argument. Strong con uence is used in the classical proofs of the Church-Rosser property for the -calculus, since con uence of ! is exactly strong con uence of ! see Barendregt, 1984 . De nition 11. A binary relation ! on any set T is locally con uent if any local divergence ! is contained in the joinability relation ! . See Figure 1d. Local con uence does not generally imply con uence; see the counter-examples in Figure 2, due to Newman, 1942 and Hindley, 1964 . However:

! = = =

Diamond Lemma Newman, 1942 . A terminating relation is con uent i it is locally con uent.

! !

The name derives from the pictorial proof in Figure 3, due to Huet, 1980 , which uses induction with respect to the terminating relation. When ! is terminating, it follows from the above results that it is Church-Rosser i ! is contained in ! . Con uence is sometimes established by well-founded induction in the following way: Let be a wellfounded ordering on the elements and suppose that for every peak" s u ! t there exists an undirected path s = w $ w $ $ wn = t n 0 such that u w ; : : :; wn, . Then it can be shown by induction on multisets of elements; see Section 5.1 that ! is Church-Rosser Winkler-Buchberger, 1983 . See Figure 1e.

0 1 1 1

As preparation for the study, in the Section 7.3, of Church-Rosser properties of extended-rewriting with a congruence, we consider here abstract properties of combinations of an arbitrary binary relation !R and a symmetric binary relation $S , both on the same set. Let !T be a relation lying anywhere between !R and the quotient relation !R=S . Note that $ S = $ T . In what follows, we will also use R, S, T, and R=S R S to refer to the relations !R , $S , !T , and !R=S , respectively. At one extreme, T can be R, a case partially dealt with in Sethi, 1974; Huet, 1980 ; at the other extreme, T can be R=S; the general case|considered here|was rst studied in Jouannaud-Kirchner, 1986 . 17

4.2 Coherence

Figure 2: Two locally-con uent relations.

Figure 3: Proof of Diamond Lemma.

18

If one is going to compute normal forms with T instead of with R, the natural question to ask is if their normal forms are equivalent. That is, under what conditions is R !T contained in $ ? The relation T S is Church-Rosser modulo S if $ T is contained in ! $ ; see Figure 1f. When T is terminating S T S T and Church-Rosser modulo S, one can determine if s $R S t, by nding T -normal forms of s and t and testing them for S-equivalence. That is, $ S is equivalent to $ T which is contained in !T $ T ; R S S in particular, R=S- and T-normal forms must be equivalent. When R=S is terminating, the Church-Rosser property may be decomposed into two local ones: T is locally coherent modulo S with R if T !R is contained in ! $ ; T is locally coherent modulo S T S T with S if T $S is contained in ! $ . Compare Figures 2g and 2h with 2d. The concept of T S T coherence was developed by Jouannaud-Kirchner, 1986 and generalizes compatibility, as in Peterson-Stickel, 1981 . Coherence Lemma Jouannaud-Kirchner, 1986 . Let R T R=S. If R=S is terminating, then T is Church-Rosser modulo S i it is locally coherent modulo S with both R and S . One proves that $ S is contained in !T $ T by induction on the multiset of elements in a path R S t $R S t $R S $R S tn . The induction is with respect to the well-founded ordering on multisets see Section 5.1 induced by !R=S . It then follows that $ T is contained in ! $ . S T S T

! ! ! ! ! ! 0 1 +

Newman's 1942 paper Newman, 1942 de ned the basic notions. Huet 1980 introduced the use of Noetherian induction on terminating relations for studying these notions. Con uence the vanilla- avored kind and many related properties of relations are discussed in Klop, 1987 .

4.3 Further Reading

5 TERMINATION

2

Recall that a rewrite system R is terminating for a set of terms T if there are no in nite derivations t !R t !R of terms in T . The following is one example of a nonterminating system Toyama, 1987b : fa; b; x ! fx; x; x gx; y ! x gx; y ! y

1

The depth i.e. the maximum nesting of symbols of a term in any of its derivations is bounded by the depth of the initial term, but it has a cycling derivation starting from fga; b; ga; b; ga; b. If !R is contained in some well-founded partial ordering on T , then R is obviously terminating. The rule ffx ! fgfx, for instance, is terminating, since the number of adjacent f's is reduced with each application. In general, it is undecidable whether a system is terminating, even if both sides of all rules are monadic Huet-Lankford, 1978 or if it has only one left-linear rule Dauchet, 1989 . For ground systems, however, termination is decidable Huet-Lankford, 1978 . The decidability of termination of non-length-increasing string-rewriting systems is open.

5.1 Reduction Orderings

The above method of establishing termination requires one to reason about the global e ect of applying a rule at a subterm. To avoid consideration of the in nite number of possible contexts, one can use well-founded orderings on terms: De nition 12. A reduction ordering on a set of terms T is any well-founded rewrite ordering of T .

19

Termination is assured if each of the rules in R is contained in a reduction ordering; conversely, if R is terminating, then the relation !R itself is a reduction ordering. As suggested in Manna-Ness, 1970 , it is oftentimes convenient to separate reduction orderings into a homomorphism from the ground terms G F to an F -algebra W and a standard" well-founded ordering on W. The homomorphism and ordering are constrained to satisfy the following monotonicity condition: f : : :x : : : f : : :y : : : whenever x y, for all f in F and all x, y, etc. in W. Then, the ordering , under which s t if s t, for s and t in G , is well-founded. To compare free open terms s and t in T F ; X , variables are added to W , and variables in terms are mapped by to distinct variables in WX . Then, s t only if s t for all assignments of values in W to the variables in s and t. A system is terminating i such W, , and exist. For example, the system below, which computes the disjunctive normal form of formulae, can be shown terminating Filman, 1978 with an exponential mapping into the natural numbers: not not x ! x not or x; y ! and not x; not y not and x; y ! or not x; not y and x; or y; z ! or and x; y; and x; z and or y; z; x ! or and y; x; and z; x

+

The mapping : T ! f2; 3; : : :g is de ned by:

or a; b = a + b + 1 not a = 2a and a; b = a b c = 2

for all a and b in f2; 3; : : :g and constant c in F , with numbers compared under their natural ordering . The second rule, for instance, always decreases the interpretation of a term, since not or x; y = 2x y is greater than and not x; not y = 2x y , for all x and y. A class of exponential interpretations were used for termination arguments in Iturriaga, 1967 . The use, in particular, of polynomial interpretations was developed in Lankford, 1975; Lankford, 1979 . Here a multivariate integer polynomial f x ; : : :; xn of degree n is associated with each n-ary symbol f in Fn, for all n. The choice of coe cients must satisfy the monotonicity condition and ensure that terms are mapped into nonnegative integers only, as is the case, for example, when all coe cients are positive. Each rule must be shown to be reducing; that is, for each rule l ! r, the polynomial l , r must be positive for all values of variables greater than the minimal value of a ground term interprets variables in X as variables ranging over the naturals. To prove termination of an associative-commutative class-rewriting system, the interpretation of an associative-commutative operator ought to be an associative-commutative polynomial. In general, such polynomials must be of either the quadratic form f x; y = xy + x + y + , 1= 6= 0 or the linear form f x; y = x + y + where , , and are natural numbers BenCherifa-Lescanne, 1987 . For example, one can use the following polynomial interpretation to prove termination of the BA=AC system of Section 2: xor a; b = a + b + 1 and a; b = a b c = 2. Primitive-recursive interpretations cannot su ce for termination proofs in general, since they would place a bound on the length of computations Stickel, 1976 . In particular, integer polynomials place a double-exponential bound on the length of a derivation Lautemann, 1988 . The following system, based on the Battle of Hydra and Hercules" in Kirby-Paris, 1982 , is terminating, but not provably so in Peano Arithmetic:

0 + +1 + 1

20

hz; ex dz; g0; 0 dz; gx; y dcz; ggx; y; 0 gex; ey

0

! ! ! ! !

hcz; dz; x e0 gex; dz; y gdcz; gx; y; dz; gx; y egx; y

Think of gx; y as the ordinal !x + y, of dcn0; x as any of the kth predecessors of x k n, and of ex as x e is just a place marker. Trans nite - induction is required for a proof of termination. Nor do total reduction orderings su ce in termination arguments, as can be seen from the terminating system ffa ! fb; gb ! gag, for which a and b must be incomparable. Nevertheless, most of the orderings used in practice do extend to total reduction orderings. For a total rewrite ordering to be wellfounded, it is necessary that it contain the proper subterm relation , since if tjp t for some term t and position p, then there is an in nite descending sequence t t t p t t t p p . As we will see shortly, for nite vocabularies, this subterm" condition is also su cient for well-foundedness of a rewrite ordering. For termination of an ordered rewrite relation ! , the ordering according to which rewriting is performed must be a well-founded reduction ordering. Note that the variables occurring on the two sides of an equation need not coincide for termination, since the terms substituted for the variables must be such that the rewritten term is smaller vis-a-vis the reduction ordering. If the ordering is total on ground terms G , then each ground instance of an equation in E can be oriented one way or another. As we will see, such ground orderings do exist. Of course, no rewrite ordering can be total on T , since no two distinct variables x and y can be ordered were we to have x y, then we would have to have y x, as well, the latter being an instance of the former. Termination arguments are often facilitated by the observation that all rewrite orderings containing the subterm relation are well-founded when F is nite. To see why the subterm property su ces, we need rst to de ne a stronger notion than well-foundedness: De nition 13. A quasi-ordering _ on a set T is a well-quasi-ordered if every in nite sequence t , t , : : : of elements of T contains a pair of elements tj and tk , j k, such that tj _ tk . By the Pigeon-Hole Principle, an equivalence relation is a well-quasi-ordering i there are only a nite number of equivalence classes. The partial ordering associated with a quasi-ordering _ is well-founded i from some point on all elements in any in nite quasi-descending" chain t _ t _ t _ are equivalent. Thus, any well-quasiordered set is well-founded by the associated partial order, while a set is well-quasi-ordered if it is wellfounded and has only a nite number of pairwise incomparable elements the nite anti-chain property". It is also important to note that any extension of a well-quasi-ordering is a well-quasi-ordering and any restriction is well-founded though it need not be well-quasi-ordered. This is what makes well-quasi-orderings convenient. Our interest focuses on well-quasi-orderings of terms. Any well-quasi-ordering _ on a vocabulary F induces a well-quasi-ordering _emb on the terms T by means of the following set of schematic rules and equations: fs ; : : :; sn ! si 1in fs ; : : :; sn ! gs ; : : :; sn if f g fs ; : : :; sn ! gsi1 ; : : :; sik if f _g; 1 i ik n; k n fs ; : : :; sn $ gs ; : : :; sn if f g These schemata apply to all f and g of appropriate arity in F . The rst deletes context; the second decreases a function symbol; the third deletes subterms; the last replaces symbols with equivalents. The third rule, with its condition changed to k n, would subsume the second and fourth. As given, the termination of

1 2

5.2 Simpli cation Orderings

1

2

3

1 1 1

1

1

1

1

21

the one-way rules is more manifest. We write s _emb t if t is derivable from s using the above rules. The equivalence part of _emb is just renaming symbols with equivalents under . Viewing terms as ordered trees: s _emb t if there is a mapping from the nodes in t into the nodes in s such that the function symbol labeling a node in t is less than or equivalent to under _ the label of the corresponding node in s, and such that distinct edges in t map to disjoint paths of s. The following deep result is at the heart of our argument:

Tree Theorem Kruskal, 1960 . If

_ is a well-quasi-ordering of a vocabulary F , then the embedding relation _emb is a well-quasi-ordering of the terms T F .

It has a beautiful proof, due to Nash-Williams, 1963 : Proof. Note that, by the in nite version of Ramsey's Theorem, any in nite sequence of elements of a well-quasi-ordered set must contain a subsequence that constitutes an in nite quasi-ascending chain. Suppose, now, that the theorem were false. Then, there would exist by the Axiom of Choice a minimal counter-example" sequence t , t , : : :, ti , : : :, of which each element ti is chosen so that it is smallest in number of symbols among all sequences of terms beginning with t , t , : : :, ti, and having no embedding tj _emb tk for j k. By the minimality hypothesis, the set of proper subterms of the elements of the minimal counter-example must be well-quasi-ordered or else t , t , : : :, tl, , s , s , : : :would be a smaller counter-example, where s , s , : : :is a counter-example of subterms of tl , tl , : : :, such that s is a subterm of tl . Since F is well-quasi-ordered by _, there must exist an in nite subsequence ti1 , ti2 , : : :of the minimal counter-example such that their roots are a quasi-ascending chain. If any of these terms tij are elements of F , the original sequence could not have been a counter-example, because then tij _emb tij+1 . Consider, then, the immediate subterms wi1 , wi2 , : : :of that subsequence. For example, if tij is fga; b; gb, then wij is the word ga b gb. As noted above, the set of all these words must be well-quasi-ordered. Using an auxiliary minimalcounter-example argument, it can be shown that any in nite sequence of words over a well-quasi-ordered set contains a pair of words such that the rst is a not necessarily contiguous subword of the second. This result Higman, 1952 is known as Higman's Lemma." In our case, this means that the in nite sequence of words composed of the immediate subterms of ti1 , ti2 , : : :must contain a pair wij and wik k j such that wij is a subword of wik . That, however, would imply that tij _emb tik , a contradiction. The pure homeomorphic embedding relation ! is the special case of embedding, induced by simple equality of symbols for _. In other words, it is derivability using only the rst rule fs ; : : :; sn ! si of the previous system. It follows from the above theorem that any extension of homeomorphic embedding is a well-quasi-ordering of terms over a nite vocabulary. Since any rewrite ordering containing the subterm relation also contains homeomorphic embedding, the subterm condition su ces for well-foundedness of term orderings over nite vocabularies, as claimed. Such orderings are the main tool for proving termination of rewriting: De nition 14. A transitive and re exive rewrite relation _ is a simpli cation ordering if it contains the subterm ordering . Simpli cation orderings are quasi-orderings called quasi-simpli cation orderings" in Dershowitz, 1982a and are what Higman Higman, 1952 called divisibility orders." For nite R, only a nite number of function symbols can appear in any derivation t !R t !R . Thus, a nite R over T is terminating if there exists any simpli cation ordering _ of T such that R is contained in its strict part Dershowitz, 1982a . The existence of such a simpli cation ordering means that tj _ tk for all k j, which precludes any tj from being homeomorphically embedded in a subsequent tk , as would necessarily be the case for any in nite derivation. Virtually all the reduction orderings used in rewriting-system termination proofs are simpli cation orderings. For instance, integer polynomial interpretations with nonnegative coe cients are. One can even

1 2 1 2 1

1

2

1

1

2

1

2

+1

1

1

1

2

22

associate polynomials over the reals with function symbols and interpret terms as before Dershowitz, 1979 . For a given choice of real polynomials to de ne a simpli cation ordering, f : : :a : : : a must always hold and a b must always imply f : : :a : : : f : : :b : : :. For termination, l must be greater than r for each rule l ! r. All these inequalities need hold only when their variables are assigned values at least as large as the minimal interpretation of a constant, and are decidable Tarski, 1951 . In di cult termination proofs, it is frequently useful to build more complicated orderings on top of simpler ones. For example, if and are partial orderings of S and S , respectively, then we say that the pair hs ; s i is lexicographically greater than a pair hs0 ; s0 i for s ; s0 in S and s ; s0 in S , if s s0 , or else 0 and s 0 . If s =s s and are well-founded, then the lexicographic ordering of the cross-product S S is also well-founded. In the same way, well-founded lexicographic orderings are de ned on n-tuples of elements of well-founded sets. Lexicographic orderings work for tuples of xed length n. For collections of arbitrary size, another tool is needed. A nite multiset or bag is a nite unordered collection in which the number of occurrences of each element is signi cant. Formally, a multiset is a function from an element set S to the natural numbers, giving the multiplicity of each element. In general, if is a partial ordering on S, then the ordering mul on multisets of elements of S is de ned as the transitive closure of the replacement of an element with any nite number including zero of elements that are smaller under . If is well-founded, the induced ordering mul also is, as a consequence of Konig's Lemma for in nite trees Dershowitz-Manna, 1979 . As an example of the application of lexicographic and multiset orderings to termination proofs, consider the rule:

1 2 1 2 1 2 1 2 1 1 1 2 2 2 1 1 1 1 1 2 2 2 1 2 1 2

x y + z ! x y + x z We de ne a reduction ordering on terms as follows: Working our way from each innermost dot to the enclosing outermost dot, we construct a tuple of numbers, listing the size total number of symbols of the subterm headed by each dot encountered along the way. Each term is measured by the multiset of all its tuples one for each innermost dot, with multisets compared in the ordering induced by the lexicographic ordering on tuples. The term a b c d + e f, for example, is represented by fh3; 9; 11i, h3; 9; 11ig, while the term a b c d+b c e f after rewriting is represented by fh3; 5; 15i, h3; 7; 15i, h3; 7; 15ig. The latter multiset is smaller, since each of its elements is lexicographically smaller than h3; 9; 11i, which appears in the former multiset but not in the latter. Multiset orderings will play an important role in Section 8.1.

5.3 Path Orderings

The above termination proof of the single distributivity rule is a complicated way of capturing the intuition that " is, in some sense, the most signi cant function symbol. This suggests the possibility of constructing simpli cation orderings directly from well-founded orderings of vocabularies, or precedences. The idea Plaisted, 1978; Dershowitz, 1982a is that a term s should be bigger than any term that is built from terms smaller than s which are connected together by a structure of function symbols smaller, in the precedence, than the root of s. One such ordering is the multiset path ordering" introduced in Dershowitz, 1982a :

De nition 15. For any given precedence _, the multiset path ordering

the following schematic system mpo:

1 1 1

_mpo

is de ned as derivability using

fs ; : : :; sn ! si 1in fs ; : : :; sn ! gt ; : : :; tm if f g; fs ; : : :; sn !mpo t ; : : :; tm fs ; : : :; si; : : :; sn ! gs ; : : :; si, ; t ; : : :; tk ; si ; : : :; sn if f _g; si !mpo t ; : : :; si !mpo tk ; k 0 fs ; : : :; sn $ gs1 ; : : :; sn if f g; a permutation

1 + 1 1 1 1 1 +1 + 1 + 1

23

The second rule replaces a term with one having a smaller root symbol. The third replaces a subterm with any number of smaller ones; in particular, it allows deletion of subterms k = 0. Actually, the third rule must also permit any number of subterms to be replaced by smaller terms at the same time to avoid violating the arity of symbols in the vocabulary. The multiset path ordering contains the homeomorphic embedding relation and is, therefore, a simplication ordering. That !mpo is irre exive is true, but not self-evident. Moreover, if is a well-founded ordering of possibly in nite F , then mpo is a well-founded ordering of T . To see this Huet, 1980; Dershowitz, 1982a , note that by Zorn's Lemma a given precedence may be extended to an ordering such that the quasi-ordering , call it _, is a total well-quasi-ordering of F . By Kruskal's Tree Theorem, the induced embedding relation _emb well-quasi-orders T , as does the total multiset path ordering _mpo induced by the total precedence _. Thus, mpo is well-founded. Since the mapping from precedence _ to term ordering _mpo is incremental, in the sense that extending the precedence extends the corresponding ordering on terms, the smaller ordering mpo must also be well-founded. The multiset path ordering establishes termination of our stack and disjunctive normal form examples as well as the bean-increasing Co ee Can Game. For the four-rule stack system, take the precedence alternate push. The rst three rules are contained in mpo by the rst rule of mpo. For example, poppushx; y !mpo pushx; y !mpo y. For the remaining stack rule, we have alternate pushx; y; z mpo pushx; alternate z; y, since alternate push and alternate pushx; y; z !mpo x; alternate z; y, the latter since pushx; y !mpo y and alternate y; z $mpo alternate z; y. Termination of the disjunctive normal form system may be shown using the precedence not and or . One can think of the multiset path ordering as a functional mapping an ordering on function symbols the precedence to an ordering on terms, by recursively comparing the immediate subterms in the multiset extension of the term ordering. A related class of orderings Kamin-Levy, 1980 compares subterms lexicographically, instead.

+ +

_lpo is de ned as derivability by the following schematic system lpo: fs ; : : :; sn ! si 1in fs ; : : :; sn ! gt ; : : :; tm if f g; fs ; : : :; sn !lpo t ; : : :; tm fs ; : : :; si ; : : :; sn ! fs ; : : :; si, ; ti ; : : :; tn if si !lpo ti ; fs ; : : :; sn !lpo ti ; : : :; tn fs ; : : :; sn $ gs ; : : :; sn if f g As in the multiset path ordering, the precedence induces an ordering on terms, but, here, subterms of the same function symbol are compared left-to-right, lexicographically. They could just as well be compared right-to-left, or in any xed order. The following traditional example|for Ackermann's function|illustrates its use with a precedence ack succ: ack0; y ! succy acksuccx; 0 ! ackx; succ0 acksuccx; succy ! ackx; acksuccx; y

1 1 + 1 1 1 + 1 1 1 + 1 +1 1 1

De nition 16. For any given precedence _, the lexicographic path ordering

For example, the third rule is contained in lpo since x occurs in succx and acksuccx; succy is lexicographically greater than acksuccx; y. If the strict part of a precedence is of order type , then the multiset path ordering on the set of terms is of order type 0 in the notation of Feferman, 1968 . Combining multiset and lexicographic path orderings into one Kamin-Levy, 1980 , gives a more powerful ordering, which we call the recursive path ordering and which is related to Ackermann's ordinal notation Dershowitz-Okada, 1988a . The original recursive path ordering" Dershowitz, 1982a was of the multiset variety. Determining if a precedence exists that makes two terms comparable is NP-complete Krishnamoorthy-Narendran, 1984 . 24

These precedence-based orderings are syntactic", looking at function symbols one at a time. Similar semantically-oriented orderings have been devised; they replace the test f g by s t, where is now a well-founded quasi-ordering of terms, not function symbols. For example, the Knuth-Bendix ordering Knuth-Bendix, 1970 assigns a weight to a term which is the sum of the weights of its constituent function symbols. Terms of equal weight have their subterms compared lexicographically. Methods for choosing weights are described in Lankford, 1979; Martin, 1987 . None of these orderings, however, can prove termination of the rule ffx ! fgfx, since the righthand side is embedded in the left. To overcome this problem, Puel 1989 compares unavoidable patterns" instead of function symbols in the de nition of mpo . By unavoidable, we mean that any su ciently large term in T must be greater, under the encompassment ordering , than one of the unavoidable patterns. For example, any term constructed from a constant a and three or more f's and g's must contain an occurrence of one of the three patterns: ffx, fgx, or ggx. The well-foundedness of this pattern path ordering" is based on a powerful extension of Kruskal's Tree Theorem Puel, 1989 analogous to a similar theorem on strings in Ehrenfeucht-etal, 1983 . We saw above that polynomial orderings are applicable to associative-commutative systems, but are severely restrictive. The multiset path ordering, though compatible with commutativity axioms, is not well-founded when associativity is added as a bi-directional rule to mpo. For example, let the precedence be c b. Then, c + b + b !mpo c + b + b $S c + b + b, where S is associativity of +. To overcome this problem, the multiset path ordering has been adapted to handle associative-commutative operators by attening and also transforming terms distributing symbols that are bigger in the precedence over smaller ones before comparing Bachmair-Plaisted, 1985 , i.e. s is greater than t i the T-normal form Ts of s is greater under mpo than the T-normal form Tt of t, for some convergent transform" system T and precedence . The general use of rewrite systems as transforms and the formulation of abstract conditions of the resultant reduction ordering are explored in Bachmair-Dershowitz, 1986; Bellegarde-Lescanne, 1987 . Termination of the union of term- or class-rewriting systems can be reduced to the termination of each: Let R and S be two binary relations contained in well-founded orderings R and S , respectively. If S commutes over R , i.e. if R S is contained in S R , then the union R S is terminating. Actually, it su ces if S quasi-commutes over R , by which we mean that R S is contained in =R . For example, if R is any terminating rewrite system, then the union of !R with the proper S subterm relation is well-founded, since taking subterms is well-founded and if a subterm rewrites then so does the superterm. More generally, the union of any terminating rewrite relation with the proper encompassment ordering is also well-founded, since encompassment is just subsumption and or , both of which are well-founded, and any rewrite relation commutes over both. Similarly, if R is a binary relation contained in a well-founded ordering R , S is a symmetric binary relation contained in a congruence S , and R commutes over S , then the composite relation R S is terminating. To prove termination of a combined term-rewriting system R S, it is necessary and su cient that R and S be contained in reduction orderings that commute as above; to prove termination of a class-rewriting system R=S, it is necessary and su cient that R be contained in a reduction ordering that commutes over a symmetric and transitive rewrite relation that contains S. These ideas generalize results in Bachmair-Dershowitz, 1986; Jouannaud-Munoz, 1984 . Note that commutation of !R and !S is not ensured by R and S having disjoint vocabularies, the system at the beginning of this section being a counter-example Toyama, 1987b .

5.4 Combined Systems

5.5 Further Reading

Martin Gardner 1983 talks about multiset orderings and the Hydra battle. For a survey of the history and applications of well-quasi-orderings, see Kruskal, 1972 . For a comprehensive survey of termination, see Dershowitz, 1987 . The multiset and lexicographic path orderings, and their variants see Rusinowitch, 1987 , have been implemented in many rewriting-rule based theorem provers e.g. Lescanne, 1984 . Some 25

results on the complexity of derivations appear in Choppy-etal, 1987 .

We turn our attention now to the determination of satis ability. If an equation s = t is satis able in the free- term algebra T , that is, if s and t are identical for some substitution , then s and t are said to be uni able. The uni cation problem, per se, is to determine if two terms are uni able. More particularly, we are interested in determining the set of all unifying substitutions . Though uni able terms may have an in nite number of uni ers, there is|as we will see|a unique substitution unique up to literal similarity that is minimal with respect to the subsumption ordering on substitutions. More generally, we are interested in solving equations in the presence of equational axioms specifying properties of the operators. For a given equational theory E, we say that s and t are E -uni able if s = t is satis able in the free quotient algebra T =E, in which case it is satis able in all models of E. In general, there may be no minimal solution to a given E-uni cation problem.

6 SATISFIABILITY

6.1 Syntactic Uni cation

Let = be literal similarity of terms, under which two terms s and t are equivalent if each is an instance of the other. We show that the quotient T ==, ordered by the subsumption relation , is a lower semilattice, by showing that every pair of terms, s and t, has a greatest lower-bound, glbs; t, called their least general generalization Plotkin, 1972 . Note that T == is not an algebra, because literal similarity is not a congruence. Let LG be the following set of transformation" rules, operating on pairs P; w, where w is a term containing the partial solution, and P contains the pairs yet to be solved: Decompose: ffs ; : : :; sm ux ft ; : : :; tm g P ; w fs ux1 t ; : : :; sn uxn tng P ; w where is fx 7! fx ; : : :; xng and x ; : : :; xn are distinct new variable symbols Coalesce: fs ux t; s uy tg P ; w fs uy tg P ; w where is fx 7! yg

1 1 1 1 1 1

Each pair is written as s ux t, where x is a variable of w: Applying these rules to fs ux tg ; x, where x is not a variable of s or t, until none is applicable, results in fui u vi g ; glbs; t. To prove that repeated applications of LG always terminate, note that each application of a rule decreases the number of function symbols not including u in P . Since the system LG is actually Church-Rosser on T ==, least generalizations are unique up to literal similarity. For example, the least generalization of fga; gb; a and fgb; ga; b is fgx; gy; x. It follows from properties of well-founded lattices Birkho , 1948 that every pair of terms s and t that are bounded from above i.e., there exists a term that is an instance of both have a least i.e. most general upper-bound, denoted lubs; t. An equation s = t has a solution if s = t . Here, s and t may share variables and we demand that applying a single substitution mapping all occurrences of the same variable to the same term result in identical terms. The least solution with respect to subsumption, mgus; t, is called their most general uni er. For example, the most general common instance of alternate y0 ; and alternate pushx; y; z is alternate pushx; y; , or anything literally similar; the mgu of alternate y; and alternate ; z is fy 7! ; z 7! g; there is no solution to alternate z; = alternate pushx; y; z. Most general uni ers and least upper bounds of terms are closely related: by revising s and t so that the two terms have disjoint variables, we get lubs; t = s, where = mgus0 ; t0, for literally similar terms s0 and t0 of s and t, respectively; in the other direction, s and t are both equal to lubeqx; x; eqs; t, where = mgus; t, eq is any binary symbol, and x is any variable. As a consequence, the most general uni er is unique up to literal similarity, but need not always exist. This fundamental uniqueness result for rst-order terms does not hold true for higher-order languages with function variables Huet, 1976 . 26

Robinson 1965 was the rst to give an algorithm for nding most general uni ers. Following Herbrand, 1930; Martelli-Montanari, 1982 , we view uni cation as a step-by-step process of transforming multisets of equations, until a solved form" is obtained from which the most general uni er can be extracted. A solved form is any set of equations fx = s ; : : :; xn = sn g such that the xi are distinct and no xi is a variable in any sj . Then, the most general uni er is the substitution fx 7! s ; : : :; xn 7! sn g. Let jtj denote the size of the term t, that is the total number of its function symbols. The size of a variable is zero. Equations to be solved will be written in the form s = t. De ne a well-founded ordering on equations as follows: u = v s = t if i maxjuj; jvj maxjsj; jtj, or else maxjuj; jvj = maxjsj; jtj and maxjuj; jvj , minjuj; jvji is greater than maxjsj; jtj , minjsj; jtj. We also use a constant F to denote the absence of a solution, and make it smaller than any equation. Let MM be the following set of transformation rules operating on pairs P; S of sets of equations, with P containing the equations yet to be solved and S, the partial solution:

1 1 1 1 ? ? ?

Delete: fs = sg P; S P; S Decompose: ffs ; : : :; sm = ft ; : : :; tm g P; S fs = t ; : : :; sn = tn g P; S Fail: ffs ; : : :; sm = gt ; : : :; tng P; S ;; fF g if f 6= g Merge: fx = s; x = tg P; S fx = s; s = tg P; S if x 2 X and x = t s = t Coalesce: fx = yg P; S P ; S fx = yg if x; y 2 X and x 6= y, where = fx 7! yg Check: fx = sg P; S ;; fF g if x 2 X , x occurs in s, and x 6= s Eliminate: fx = sg P; S P ; S fx = sg if x 2 X , s 62 X , and x does not occur in s, where = fx 7! sg

? 1 ? 1 1 ? 1 ? 1 ? 1 ? ? ? ? ? ? ? ? ?

De nition 17. A syntactic uni cation procedure is any program that takes a nite set P of equations, and uses the above rules MM to generate a sequence of inferences from P ; ;. Starting with fs = tg; ; and using the uni cation rules repeatedly until none is applicable, results in ;; fF g i s = t has no solution, or else it results in a solved form ;; fx = s ; : : :; xn = sn g. The application of any of these rules does not change the set of solutions of P S. Hence, the former signi es failure, and in the latter case, = fx 7! s ; : : :; xn 7! sn g is a most general uni er of s and t. That is most general follows from the fact that the rules preserve all solutions. For example, the most general uni er of fx; x; a and fgy; ga; y is fx 7! ga; y 7! ag, since ffx; x; a = fgy; ga; yg; ; MM fx = gy; x = ga; a = yg; ; MM fx = gy; gy = ga; a = yg; ; MM fx = ga; ga = gag; fy = ag MM fx = gag; fy = ag MM ;; fx = ga; y = ag

0 0 ? ? 1 1 1 1 ? ? ? ? ? ? ? ? ? ?

On the other hand, fx; x; x and fgy; ga; y are not uni able, since ffx; x; x = fgy; ga; yg; ; MM fx = gy; x = ga; x = yg; ; MM fy = gy; y = gag; fx = yg MM ;; fF g on account of an occur check." To prove that repeated applications of MM always terminate, we can use a lexicographic combination of an ordering on numbers and the multiset extension of the ordering on equations. With each application of a rule, P; S MM P 0 ; S 0 , either the solved set S is enlarged, or the problem set P is reduced under mul . Since the solved set cannot increase without bound it can have at most one equation per variable, nor can the unsolved set decrease without limit since mul is well-founded, there can be no in nite MM -derivations. Uncontrolled use of eliminate leads to exponential time complexity. With appropriate data structures and control strategies, an e cient algorithm is obtained, which is quasi-linear in the worst case e.g. Baxter,

? ? ? ? ? ?

27

1976 ; more careful implementations provide for truly linear, but less practical, algorithms e.g PatersonWegman, 1978 . The coalesce rule allows us to avoid the use of multi-equations"; cf. Martelli-Montanari, 1982 . Eliminating the check rule produces solutions over the domain of in nite rational" trees Huet, 1976 , and has rami cations for the semantics of some Prolog implementations Colmerauer, 1984 .

6.2 Semantic Uni cation

When it comes to E-uni cation, the situation is much more complex. A substitution is a solution in E to an equation s = t if s =E t , in which case we say that is an E -uni er of s and t; we say that t E -matches s if there exists a substitution such that s =E t. E-uni ability is undecidable whenever the word problem is, and in many other cases as well. For example, the solvability of Diophantine equations, that is, polynomial equations over the integers, is undecidable Matijasevic, 1970 , as is uni ability under associativity and distributivity alone Szabo, 1982 . Satis ability may be undecidable even even when congruence classes are nite as for associativity, commutativity, and distributivity Siekmann, 1984 . Second-order uni ability equivalence of function de nitions is also undecidable, in general Goldfarb, 1981 . On the brighter side, many other theories have decidable uni cation problems, including Presburger arithmetic Presburger, 1927; Shostak, 1979 , real closed elds Tarski, 1951; Collins, 1975 and monoids Makanin, 1978 . When more than one solution may exist for a theory E, we de ne a solution to be more general than a solution , if E in the E-subsumption ordering E , i.e. if there exists a substitution such that x =E x , for all variables x in X , but not vice-versa. An E-uni er is most general if no more general uni er exists. Note that E-subsumption is not well-founded for all E. There are decidable theories with in nite sets of most general uni ers an example is the set of solutions faiji 1g to x a = a x, where " is associative Plotkin, 1972 , and there are some for which there are solutions, but no most general one Fages-Huet, 1983 an example is associativity plus idempotence Baader, 1986 . We say that a set S of E-uni ers is complete if for every E-uni er there is one in S that is more general with respect to Esubsumption. For example, a complete uni cation algorithm exists for associativity and commutativity AC Stickel, 1981; Herold-Siekmann, 1987 ; alternative algorithms with better performance are Kirchner, 1989; Boudet, 1989 . Other theories for which algorithms are available that compute nite, complete sets of most general E-uni ers include commutativity, AC with identity and or idempotency see Fages, 1987 , as well as Boolean rings see Boudet-etal, 1988 . For many of these theories, uni cation is believed intractable from the time-complexity point of view Kapur-Narendran, 1986 . Of course, E-uni ability is semi-decidable for recursively-enumerable E. Paramodulation without the functional re exivity axioms Robinson-Wos, 1969 is one improvement over the obvious British-museum" method of interleaving the production of substitutions with the search for equational proofs. Paramodulation may be improved upon by a more goal-oriented process. The following set of rules, inspired by Gallier-Snyder, 1987; Hsiang-Jouannaud, 1988 , does the trick: Decompose: ffs ; : : :; sm $ ft ; : : :; tm g P; S fs $ t ; : : :; sn $ tn g P; S Eliminate: fx $ sg P; S P ; S fx = sg if x 2 X , and x does not occur in s, where = fx 7! sg Mutate: ffs ; : : :; sn $ tg P; S fs $ u ; : : :; sn $ un; r $ tg; S if fu ; : : :; un = r is literally similar to an equation in E but has no variables in common with S, P, t, or the si Splice: fs $ tg P; S fs $ x; r $ tg P; S if x = r is literally similar to an equation in E but has no variables in common with S, P, t, or the si Imitate: ffs ; : : :; sn $ yg P; S fs $ y ; : : :; sn $ yn ; y $ fy ; : : :; yng P ; S if y 2 X and the yi are new variables We call this set of rules EU. These rules non-deterministically compute solved forms, each of which represents an E-uni er.

1 ? 1 1 ? 1 ? ? 1 ? 1 ? 1 ? ? 1 ? ? ? 1 ? 1 ? 1 ? ? 1

28

To generate a complete set of uni ers may not require computing all possible sequences. In particular, the use of imitate can be severely restricted Hsiang-Jouannaud, 1988 . The set of rules EU can be improved for particular classes of equations. Two special cases have been investigated: i when E is strict" in the sense that for any valid equation s = t, there exists a proof with at most one proof step taking place at the top position Kirchner, 1986 ; and ii when there exists a ground-convergent set of rules complete for E. In the rst case, axioms of the form x = t, for variable x, are disallowed; hence splice is super uous. Moreover, decompose must always apply after mutate; hence, the two can be compiled into a single rule. For example, commutativity uses the following mutate and decompose" rule: ffs ; s = ft ; t g P; S fs = t ; s = t g P; S More complex cases, involving bounded applications of axioms in E prior to decomposition, can be treated similarly. Methods of combining uni cation algorithms for well-behaved theories that do not share symbols have been given in Yelick, 1987; Kirchner, 1989; Boudet-etal, 1988 ; The general case was solved in SchmidtSchauss, 1988 . Note that a uni cation algorithm that generates a complete set of most general uni ers for terms without free constants does not automatically work for matching one cannot just treat the variables of t as constants, since that changes the algebra and may introduce unsound solutions Burckert-etal, 1987 .

1 2 ? 1 2 1 ? 2 2 ? 1

De nition 18. An E-uni cation procedure is any non-deterministic program that takes a nite set P of equations, and uses the above rules EU to generate sequences of inferences from P ; ;.

0 0

Even when a convergent system R exists for a theory E, E-uni cation problem remains only semi-decidable. For example, the system x+0 ! x x + succy ! succx + y x + predy ! predx + y x,0 ! x x , succy ! predx , y x , predy ! succx , y x0 ! 0 x succy ! x y + y x predy ! x y , y succpredx ! x predsuccx ! x for addition and multiplication of integers is canonical, but were R-uni cation or R-matching decidable, then the existence of integer solutions to Diophantine equations, such as x x + y y , succsuccsucc0 = 0; would also be decidable. The latter is Hilbert's Tenth Problem, shown to be undecidable in Matijasevic, 1970 . Cf. Bockmayr, 1987; Heilbrunner-Holldobler, 1987 . When a convergent R is available, a one-way sort of paramodulation su ces, due to the existence of a rewrite proof for an arbitrary valid equation Dershowitz-etal, 1987b; Martelli-etal, 1989 . The following set of rules, RU, restricts uses of equations to left-hand sides of rules: Decompose: ffs ; : : :; sm ! ft ; : : :; tm g P; S fs ! t ; : : :; sn ! tn g P; S Eliminate: fx ! sg P; S P ; S fx = sg if x 2 X , and x does not occur in s, where = fx 7! sg Mutate: ffs ; : : :; sn ! tg P; S fs ! u ; : : :; sn ! un; r ! tg; S if fu ; : : :; un ! r is literally similar to a rule in R but has no variables in common with S, P, t, or the si Imitate: ffs ; : : :; sn ! yg P ; S fs ! y ; : : :; sn ! yn ; y ! fy ; : : :; yng P ; S if y 2 X and the yi are new variables

1 ? 1 1 ? 1 ? ? 1 ? 1 ? 1 ? ? 1 1 ? 1 ? 1 ? ? 1

6.3 Narrowing

This set of rules subsumes narrowing", as used for this purpose in Fay, 1979 : 29

De nition 19. A term s narrows in one step to a term t, via substitution , symbolized s ;R t, if t is s r p , for some non-variable position p in s, rule l ! r in R the variables of which have been renamed so that they are distinct from those in s, and most general uni er of sjp and l.

The verb narrow" perhaps carries the wrong connotation: it is the set of R-congruence classes of instances of the term that is being narrowed. It is easy to see that RU mimics narrowing by using decompose, imitate, and mutate. For example, if R is ffx; x ! cx; a ! bg, then the problem ffa; y ! z; fy; b ! z g mutates to fa ! x; y ! x; cx ! z; fy; b ! z g. Then a is imitated by x, and x and y are eliminated, by substituting a for them: fca ! z; fa; b ! z g. This corresponds to narrowing of fa; y to ca by instantiating y 7! a, and eventually yields the solution fy 7! a; z 7! cbg. Narrowing has the following property: Narrowing Lemma. If R is a convergent rewrite system and s ! t, then there exist terms u and v such R that s ; u, t ! v, and v u. R R If is irreducible that is, if x is irreducible for all variables x, then t = v, and the lemma holds even for non-convergent R Hullot, 1980 . Without convergence, reducible solutions are lost. For example, if R is ffa; b ! c; a ! bg or ffx; gx ! c; a ! gag, then fy; y cannot be narrowed, and fy; y ! c fails to lead to a solved form, despite the fact that there is a solution fy 7! ag. Variations on narrowing include: normal narrowing Fay, 1979 in which terms are normalized via !R before narrowing, basic narrowing Hullot, 1980 in which the substitution part of prior narrowings is not subsequently narrowed, and their combination Rety-etal, 198? , all of which are semi-complete for convergent R. Class-rewriting yields similar results Jouannaud-etal, 1983 .

? ? ? ? ? ? ? ? ? !

6.4 Further Reading

For a survey regarding syntactic uni cation, see Lassez-etal, 1988 ; for uni cation in general, see Huet, 1976 . For a survey of theory and applications of syntactic and semantic uni cation, see Knight, 1989 . Questions of decidability of uni cation in equational theories are summarized in Siekmann, 1984 ; a summary of complexity results for some of the decidable cases is Kapur-Narendran, 1987 . A popular exposition on the undecidability of the existence of solutions to Diophantine equations is Davis-Hersh, 1973 . For a comprehensive treatment of narrowing and E-uni cation, see Kirchner, 1985 . For the satis ability problem of arbitrary rst-order formulae with equality as the only predicate, see Maher, 1988 ,Comon-Lescanne-1989.

In this section, we continue our study of the Church-Rosser property for rewrite systems. In particular, we will see that con uence is decidable for nite, terminating systems. Con uence, in general, is undecidable Huet, 1980 , even if all rules are monadic Book-etal, 1981 . For nite ground systems|even if they are nonterminating|decision procedures exist see Dauchet-etal, 1987; Oyamaguchi, 1987 . Ground con uence, on the other hand, is undecidable, even if the system is terminating Kapur-etal, 1987 . Even for convergent systems R, the questions whether congruence classes de ned by $ are nite in number, or are all nite in R size, are undecidable, unless R is ground Raoult, 1981 .

7 CRITICAL PAIRS

7.1 Term Rewriting

Let l ! r and s ! t be two rules. We say that the left-hand side l overlaps the left-hand side s if there is a nonvariable subterm sjp of s such that l and sjp have a common upper bound with respect to subsumption. To determine overlap, the variables in the two not necessarily distinct rules are renamed, if necessary, so that they are disjoint. Then, l overlaps s if there exists a unifying substitution such that l = s jp . When there is an overlap, the overlapped term s can be rewritten to either t or s r p . The two-step proof t R s l p !R s r p is called a critical peak. 30

Figure 4: Proof of Critical Pair Lemma.

De nition 20. If l ! r and s ! t are two rewrite rules with distinct variables, p is the position of a nonvariable subterm of s, and is a most general uni er of sjp and l, then the equation t = s r p is a

critical pair formed from those rules.

Thus, a critical pair is the equation arising from a most general nonvariable overlap between two left-hand sides. For example, pushx; alternate ; y = pushx; y is the critical pair obtained from alternate pushx; y; z ! pushx; alternate z; y and alternate y; ! y. Let cpR denote the set of all critical pairs between not necessarily distinct, but perhaps renamed rules in R and let $cp R denote its symmetric rewrite closure. Critical Pair Lemma Knuth-Bendix, 1970 . For any rewrite system R and peak s R u !R t, there either exists a rewrite proof s ! v t or a critical-pair proof s $cp R t. R R The proof Knuth-Bendix, 1970 , depicted in Figure 4, considers all relative positions of the two redexes. As stressed in Huet, 1980 , no assumption of termination is necessary for this lemma. It follows from this and the Diamond Lemma, that a terminating system R is con uent i cpR, regarded as a relation, is a subset of the joinability relation ! . This holds, for instance, for the stack interleaving example of R R Section 3.2. Since nite systems have a nite number of critical pairs, their con uence is decidable, provided they are terminating. This criterion for con uence is called the superposition test Knuth-Bendix, 1970 . Without termination, a system may have no critical pairs hence be locally con uent, and still be noncon uent. A system sans critical pairs except trivial ones of the form t = t is called non-overlapping , or non-ambiguous . The following example of a non-overlapping, but non-con uent system Huet, 1980 , is based on the ladder" in Figure 2b:

fx; x ! a fx; gx ! b c ! gc The term c has no normal form, but fc; c has two, a and b. This example can be modi ed so that the system is normalizing Sivakumar, 1986 : 31

fx; x ! gx fx; gx ! b hc; y ! fhy; c; hy; y The Critical Pair Lemma can be weakened so that not all pairs need be considered. Various such critical pair criteria have been investigated, all revolving around the case of a critical peak that is rewritable in additional ways, making it possible to replace the peak with an alternate proof that is in some sense smaller. The connectedness criterion is based on the well-founded method of establishing local con uence mentioned in Section 4.1 and ignores any critical pair s = t derived from an overlap s R u !R t such that there exists another proof s $ t, each term of which is derivable from u by !R Winkler-Buchberger, 1983 ; the R compositeness criterion ignores critical pairs for which the overlapped term can be rewritten at a position strictly below the point of overlap Kapur-etal, 1988 .

+

7.2 Regular Systems

By enforcing strong restrictions on the form of left-hand sides, con uence can be ensured even for nonterminating systems. De nition 21. A rewrite system that is both left-linear no multiple occurrences of a variable on the left and non-overlapping no non-trivial critical pairs is called regular. Examples of regular systems are the stack and Combinatory Logic systems of Sections 2.3 and 2.4, respectively. Mutually recursive function de nitions, with one equation employing if then else per de ned function, are regular. Regular systems are always con uent, by the following result: Parallel Moves Lemma Huet, 1980 . If R is regular, then !k is strongly con uent. R

The symbol !k denotes one parallel" application of rules in R at disjoint redexes. For the name R and inspiration of this lemma, cf. Curry-Feys, 1958 . The con uence of regular systems establishes the consistency of the operational semantics of recursive programming languages; see Raoult-Vuillemin, 1980 . The above lemma may be weakened to allow critical pairs that join in one parallel step Huet, 1980 ; the ground case was considered in Rosen, 1973 . For regular systems, normal forms can be computed by a parallel-outermost" redex evaluation scheme O'Donnell, 1977a , but not by a leftmost-outermost" scheme Huet-Levy, 1990 ; with additional sequentiality" requirements, one can e ciently compute normal forms, without lookahead Ho mann-O'Donnell, 1979; Huet-Levy, 1990 . How to avoid all unnecessary rewrites and obtain an optimal strategy is, however, an undecidable problem, in general Huet-Levy, 1990 . For modularity of programming with rewrite systems, one would have wished that the union of two convergent systems over disjoint vocabularies be convergent. Unfortunately, though the union of two con uent systems sharing no function symbols is con uent Toyama, 1987a , the termination property as we saw in Section 5.4 is not preserved under disjoint union. This is true even for con uent systems Toyama, 1987b . If, however, the two convergent systems are also left-linear, then their union is convergent Toyama-etal, 1989 . Critical pairs also provide a necessary and su cient condition for a left-linear terminating system R to be Church-Rosser modulo a congruence S. That is, if cpR S is a subset of !R $ R , then $ S S R is also contained therein Huet, 1980 . Then, R-normal forms may be used to decide validity, provided Sequivalence is decidable. For example, if S is commutativity and R includes all commutativity variants of its rules, then R-normal forms are unique up to permutations of operands. To handle rewriting modulo a congruence in the presence of non-left-linear rules, Peterson-Stickel, 1981 suggested using the extended rewrite relation S nR to compute normal forms. The set of critical peaks of the

! !

7.3 Class Rewriting

32

form t S nR s !S nR s r p is in general in nite, so the Critical Pair Lemma is of little practical help. Instead, we consider peaks t R s !S nR s r p and cli s t $S s !S nR s r p separately. De nition 22. Let S be an set of equations. If s ! t and l ! r are two rewrite rules with distinct variables, p is the position of a nonvariable subterm of s, and is a most general substitution most general, with respect to subsumption modulo S such that sjp =S l, then t = s r p is an S-critical pair of the two rules. If s $ t is an equation in S, l ! r is a rewrite rule renamed as necessary, p is the position of a nonvariable proper subterm of s, and is a most general substitution such that sjp =S l, then t ! s r p is an S-extended rule of l ! r. In the set cpS R, we include all critical pairs obtained by overlapping S-variants of rules in R on renamed rules in R. We also need the set exS R of extended rules obtained by overlapping variants of rules in R on renamed equations in S. Extended Critical Pair Lemma Jouannaud, 1983 . For any rewrite system R, equational system S , and peak s R !S nR t, there exists a rewrite proof s ! nR $ nR t, or a critical-pair proof S S S s $ $cpS R $ t which may involve S -steps within the critical pair's variable part only. Similarly, S S for any cli s $S !S nR t, there exists a rewrite proof s ! nR $ nR t, or an extended-rule S S S proof s $ , exS R $ t which may involve S -steps within the extended rule's variable part only. ! S S The point is that in the absence of a rewrite proof, there must be a proof that is an application of an S-instance" of a critical pair. The possible need for S-steps in the variable part is illustrated by the equation a $ b and rules fx ! gx and fx ! hx. A critical peak ga R fa $S fb !R hb lends itself to the critical pair proof ga $S gb $cp R hb. Using this lemma, it can be shown that if R=S is terminating and the subterm relation modulo S is wellfounded, then S nR is Church-Rosser modulo S i cpS R and exS R are contained in !S nR $ S nR S Jouannaud-Kirchner, 1986 . If these conditions are satis ed, and an S-matching procedure is available, then validity in R S can be decided. Note that subterm modulo S is well-founded when S-congruence classes are nite. It is possible to combine the above results by partitioning rules into left-linear and not necessarily leftlinear subsets. The critical pair condition can then be tailored to the di erent kinds of rules, with term rewriting used for the left-linear subset and extended rewriting for the rest Jouannaud-Kirchner, 1986 . Additional improvements are provided by critical pair criteria for extended rewriting, as described in BachmairDershowitz, 1987a .

! !

7.4 Ordered Rewriting

Ordered rewriting systems enjoy a similar critical pair condition for con uence, but only for certain classes of orderings and only for ground terms. An ordering is called a complete simpli cation ordering if it is a simpli cation ordering that is total on G , i.e. for any two distinct ground terms u and v, either u v or v u. For example, if a precedence is total, it is easy to show that the induced lexicographic path ordering lpo is a complete simpli cation ordering a property not shared by the multiset path ordering. De nition 23. Let l = r and s = t be two equations in E with disjoint variables such that l overlaps s at non-variable position p with most general uni er . The equation t = s r p is a critical pair if the participating steps t $E s $E s r p can form a peak; in other words, if t E s !E s r p , for some substitution . Let cp E denote the set of all such critical pairs between equations in E. Ordered Critical Pair Lemma Lankford, 1975 . For any set of equations E , complete simpli cation ordering , and peak s E u !E t between ground terms s; t; u, there either exists an ordered-rewrite proof s ! t or a critical-pair proof s $cp E t. E E

33

The di erence between the proof of this and the original Critical Pair Lemma is only that the bottom step in Figure 4b may go one way or the other, depending on whether s t or vice-versa. If s = t, the rewrite proof is trivial. It is to ensure that s and t are comparable, that we require to be total on ground terms. It may seem that local con uence is not guaranteed by the critical pair condition, when equations in E have variables on one side that do not appear on the other. For example, with E = fx + gy = x + fzg, and the lexicographic path ordering induced by the precedence g f b a, there is a peak a+ fb E a + ga !E a + fa, whereas there is no rewrite proof a + fb !E a + fa. But, in fact, there is a critical pair hidden here: overlapping the left-hand side of the equation on a literally similar instance x + gy0 = x + fz 0 gives the pair x + fz = x + fz 0 . Thus, a + fb ,!cp E a + fa. With local con uence established, we have a ground convergent rewrite relation !E . Such an orderedrewriting system|when nite|may be used to decide validity: if s = t is valid for ground convergent E, then by Skolemizing the variables in s and t, that is by treating those variables as constants, and extending the ordering to include them, both s and t will have the same normal form. For example, if E is the commutativity axiom x y = y x and z y x in a lexicographic path ordering, then y x z and z y x have the same normal form, x y z. As a more interesting example, consider the following system for entropic groupoids Hsiang-Rusinowitch, 1987 : x y x ! x x y z ! x z x y y z ! x z x y z $ x y z and suppose we wish to decide validity of an equation s = t. First, the variables x , : : :, xn appearing in s and t are replaced by Skolem constants c , : : :, cn. Then, a lexicographic path ordering is used with a precedence in which " is larger than the constants, and the constants are linearly ordered: cn : : : c . The equation is used to rewrite any product of the form x y z to the same term with the occurrence of y replaced by the smallest term viz. c under lpo .

1 2 1 2 1 1 1 1 1 1

7.5 Reduced Systems

By reducing right-hand sides and deleting rules with rewritable left-hand sides, a convergent system can always be converted into a canonical, i.e. reduced and convergent, one see, e.g., Metivier, 1983 . One of the nice things about reduced systems is that, for any given equational theory, there can be only one nite or in nite canonical system contained in a particular reduction ordering Butler-Lankford, 1980; Metivier, 1983 . This uniqueness result is up to literal similarity. Uniqueness does not, however, hold for arbitrary canonical class-rewriting systems Dershowitz-etal, 1988 , but does for associative-commutative systems Lankford-Ballantyne, 1983 .

7.6 Further Reading

A detailed study of the Church-Rosser property of non-overlapping systems is Klop, 1980 . Computing with regular systems is the subject of O'Donnell, 1977a .

8 COMPLETION

In the previous section, we saw that con uence of nite terminating systems can be decided using the superposition test. Suppose a given system fails that test because some critical pair has no rewrite proof. Building on ideas of Evans 1951 , Knuth and Bendix 1970 , suggested extending such a system with a new rule tailored to cover the o ending critical pair. Of course, new rules mean new critical pairs, some of 34

which may also not pass the test. But, often enough, repeating this process eventually leads to a convergent system, with all critical pairs having rewrite proofs. This procedure is called completion. Interestingly, the critical pairs generated along the way are frequently the kind of lemmata a mathematician would come up with Knuth-Bendix, 1970 . Starting with a nite set of equations and a reduction ordering on terms, the completion procedure attempts to nd a nite canonical system for the theory presented by the equations by generating critical pairs and orienting them as necessary. If reducing the two sides of a critical pair s = t yields an equation u = v, where u and v are not identical, then adding a new rule u ! v or v ! u supplies a rewrite proof for s = t. To decide between the two orientations, the given reduction ordering is employed: if u v then u ! v is added, while if v u then v ! u is chosen. The new rule, u ! v or v ! u, is then used to form new critical pairs. Running the procedure can have one of three outcomes: success in nding a canonical system, failure in nding anything, or looping and generating an in nite number of rules forming an in nite canonical system. Completion has recently been put in a more abstract framework Bachmair-etal, 1986 , an approach we adopt here. As in traditional proof theory cf. Takeuti, 1987 , proofs are reduced, in some well-founded sense, by replacing locally maximal subproofs with smaller ones, until a normal-form proof is obtained. In completion, the axioms used are in a constant state of ux; these changes are expressed as inference rules, which add a dynamic character to establishing the existence of reducible subproofs. This view of completion, then, has two main components: an inference system, used in the completion process to generate new rewrite rules, and a rewrite relation that shows how any proof can be normalized, as long as the appropriate rules have been generated. An inference rule for our purposes is a binary relation between pairs E; R, where E is a set of equations and R is a set of rewrite rules. Rules or equations that di er only in the names of their variable are, for all intents and purposes, treated as identical. Let be a reduction ordering, and _ the well-founded ordering on rules de ned as follows: s ! t _ l ! r if i s l under the encompassment ordering, or else ii s = l s and l are literally similar and t r. We de ne the following set KB of six inference rules:

8.1 Abstract Completion

Delete: Compose: Simplify: Orient: Collapse: Deduce:

E fs = sg; R E; R fs ! tg E fs = tg; R E fs = tg; R E; R fs ! tg

E; R E; R fs ! ug if t !R u E fs = ug; R if t !R u E; R fs ! tg if s t E fu = tg; R if s !R u by l ! r with s ! t _ l ! r E; R ` E fs = tg; R if s = t 2 cpR

` ` ` ` `

KB . Delete removes a trivial equation s = s. Compose rewrites the right-hand side t of a rule s ! t,

We write E; R `KB E 0 ; R0 if the latter may be obtained from the former by one application of a rule in if possible. Simplify rewrites either side of an equation s = t. Orient turns an equation s = t that is orientable s t or t s into a rewriting rule. Collapse rewrites the left-hand side of a rule s ! t and turns the result into an equation u = t, but only when the rule l ! r being applied to s is smaller than the rule being removed under the rule ordering. Deduce adds equational consequences to E, but only those that follow from critical overlaps s R u !R t. De nition 24. A standard completion procedure is any program that takes a nite set E of equations and a reduction ordering , and uses the above rules KB to generate a sequence of inferences from E ; ;. In practice, the completion rules are usually applied in the given order, saving space by preserving only reduced rules and equations. The results of a nite completion sequence E ; ; `KB E ; R `KB `KB En; Rn are En and Rn; more generally, the limit of a possibly in nite completion sequence E ; ; `KB

0 0 0 1 1 0

35

E ; R `KB is the pair E1 ; R1, where E1 is the set i j i Ej of persisting equations and R1 is the set i j i Rj of persisting rules. We say that a completion sequence is successful, if E1 is empty and R1 is canonical. If success occurs after a nite number of steps, then the resultant system R1 is a decision procedure for E . But the completion may loop", producing an in nitely large set of persisting rules. A simple example Ardis, 1980 of looping is provided by the equation fgfx = gfx. Oriented the only way possible, the rule fgfx ! gfx overlaps itself, generating the critical pair gfgfx = fggfx, which simpli es to ggfx = fggfx. Continuing in the same manner, an in nite set of rules ffgi fx ! gi fxji 1g is produced. The rules in KB are evidently sound, in that the class of provable theorems is unchanged by an inference step. Furthermore, only rules contained in are added. We are thus assured that the limit R1 of any nite or in nite successful completion sequence is terminating and presents the same equational theory as did E . Figure 5 shows an example of a successful completion sequence. Starting with the three axioms x1 = x 1x = x x, x y = y

1 1 0 0 0 0

over a vocabulary containing a constant 1, post x unary symbol , ", and in x binary symbol ", it generates the eight-rule canonical system 1x ! x x1 ! x x, x ! 1 x x, ! 1 1, ! 1 x, , ! x , x y ! y x x, y ! y x using size as the reduction ordering. For a given reduction ordering , a not necessarily nite convergent system R contained in exists for an equational theory E, i each E-congruence class of terms has a unique minimal element vis-a-vis Avenhaus, 1985 . Nonetheless, completion may fail to nd R, even when given !R as the reduction ordering Dershowitz-etal, 1988 . For example, despite the existence of ffa ! a; c ! a; b ! ag, no successful sequence exists for ffb = a; fc = c; b = cg, as long as b and c are incomparable under the given ordering. In fact, on account of the partialness of the ordering, some sequences may fail while others may succeed Avenhaus, 1985; Dershowitz-etal, 1988 . For example, let be a recursive path ordering with precedence f d c a and d b a but b and c are incomparable, and let E = ffc = c; b = d; c = d; fd = ag. There is a successful sequence:

+ 0

E ; ; KB fb = d; fd = ag; fd ! c; fc ! cg KB ;; ffa ! a; b ! a; c ! a; d ! ag ` `

+ + 0

as well as a failing one: E ; ; KB fc = d; fd = ag; fd ! b; fc ! cg KB fb = cg; ffb ! a; d ! b; fc ! cg ` `

+ + 0

The latter sequence cannot be extended further. As pointed out already in Knuth-Bendix, 1970 , such failures can be circumvented by incorporating an inference rule that adds s ! kx ; : : :; xn and t ! kx ; : : :; xn to Ri if s = t is an unorientable equation in Ei, where k is a new function symbol not in the original vocabulary and x ; : : :; xn are those variables appearing in s and t. Though this inference is not sound it constitutes a conservative extension, it results in a decision procedure if ultimately successful. In the above failing example, replacing b = c with b ! k and c ! k leads directly to fa ! k; b ! k; c ! k; d ! k; fk ! kg. Two terms s and t in T fa; b; c; d; f g are equal in the original theory i they have the same normal form in this system. Unfortunately, this process can, in

1 1 1

36

i 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23

Ri x1 ! x R 1x R x, x y R x, x R 1, R x, , y 1, y R 1, y R R x, , R 1, y x, , R x x, y R x x,

1

! x ! y ! 1 ! 1 ! xy ! 1y ! y

Ei 1x x1 x, x y 1x x, x y x, x y

= = = = = =

x x y x y y

inference orient orient

2

3

5

7

9

orient deduce 1,3 orient 1, = 1 deduce 1,5 orient x, , y = x y deduce 3,3 orient 1, y = 1 y deduce 7,9 orient compose 11,2 x, x = 1 1y = y y = y x, , = x collapse 12,7 simplify 2 delete deduce 1,9 orient

9

9

! x ! y ! x ! y ! 1

7

18

21

x y = x y collapse 9,17 delete x x, y = y deduce 3,17 orient x x, = 1 deduce 1,21 orient

Table 1: A successful completion sequence for a fragment of group theory. 37

general, degenerate into unsuccessful sequences that add in nitely many new symbols. As we will see below, completion has been extended in various ways, in particular to handle the associative-commutative axioms, which cannot be handled as rules. Completion can also be used as a mechanical theorem prover. The idea is that, even when the procedure loops, any valid theorem should eventually have a rewrite proof using the rules already on hand. This is not actually the case, since a procedure might abort when no equation is orientable. But for implementations that are fair in their choice of inferences, one can show that|barring abortion|all provable equations eventually lend themselves to a direct proof by rewriting. This perspective on completion was taken by Huet Huet, 1981 , and in Lankford, 1975 from the refutational point of view. The di cult part is the need to show that deleting simpli able rules does not|in the long run|shrink the class of equations having rewrite proofs. Once we have established that completion acts as a semi-decision procedure for validity when it loops, we will be ready to apply it to theorem-proving in inductive theories and in rst-order predicate calculus. A proof in E R is a sequence of E-steps and R-steps. By applying the above inference rules, it may be possible to simplify a given proof, replacing some steps with alternate ones from E 0 R0, whenever E; R ` E 0 ; R0. By a proof pattern we intend a schema describing a class of subproofs; e.g. to characterize KB rewrite proofs, we use the pattern s ! v t, where s, t, and v denote arbitrary terms. If a proof contains R R no peaks s R u !R t nor applications s $E t of equations, it must be a rewrite proof. Let E be the set of all equations deducible from E and R be the orientable subset of E that intersects with the reduction ordering . The following set C of proof-pattern rules captures the elimination of the undesirable patterns and the simpli cation of proofs that takes place during completion: s $E s s s !R t s !R v R t where s !R t by l ! r and s !R v by l0 ! r0 and l ! r _ l0 ! r0 s $E t s !R v $E t s $E t s !R t s !R t s !R v $E t where s !R t by l ! r and s !R v by l0 ! r0 and l ! r _ l0 ! r0 s R u !R t s $E t s R u !R t s ! v t R R Symmetric rules, with the proof patterns on both sides of inverted, are also needed. Note how these rules correspond exactly to the e ect of the inference rules: Any proof step involving a deleted equation can be omitted; when a rule is replaced with a new composed rule, any rewrite step using it can be replaced by a two-step valley; when an equation is simpli ed, its use in a proof is replaced by a rewrite step and a smaller equational step; when an equation is oriented, the corresponding proof step becomes a rewrite step; when a rule is collapsed into an equation, a combination of a rewrite and equational steps may be used instead; when a critical pair is deduced, the corresponding critical peak in a proof may be replaced by a new equational step. The last proof-pattern rule corresponds to a non-critical peak, which can always be converted into a valley. We assume that the ordering is such that for any equation s = t in E there is a term v for which s ! R v t. With a reduction ordering that does not satisfy this condition there is no chance of a successful R completion. Then, at least one of the rules of C can be applied to any non-rewrite proof or to any proof employing a non-reduced rule. Thus, C-normal forms are R -rewrite proofs that use only reduced rules. Furthermore, we can apply the techniques of Section 5 and show that the proof-normalization relation C is terminating: Consider the ordering c which compares proofs by comparing multisets containing the pair hfsg; l ! ri for each application s !R t of a rule l ! r and hfs; tg; l ! ri for each application s $E t of an equation l = r. Pairs are compared lexicographically, using the multiset ordering mul induced by the given reduction ordering for the rst component, and the ordering _ on rules for the second. Multisets of pairs, measuring the complexity of proofs, are compared by c , the multiset ordering induced by this lexicographic ordering. Since and _ are both well-founded, c is a reduction ordering on proofs. Since it can be veri ed that C is contained in c , the former is terminating. Note how this proof ordering considers the justi cation of a proof and not just the terms in it. For further details, consult Bachmair, 1989b .

0

38

For any given completion sequence E ; ; `KB E ; R `KB , let $ stand for $ i Ri , that is, for a i E proof at the ith stage, using rewriting with Ri in either direction or equational steps with Ei. The proof normalization relation C mirrors the inference system KB in that for any completion sequence and for any proof s $ t at stage i there exists a proof s $ t at each subsequent stage j such that s $ t s $ i j i j C t. In this way, inference rules are used to generate rules needed for proofs to be C-reducible. A possibly in nite sequence E ; ; `KB E ; R `KB is deemed fair if for any proof s $ t that is C-reducible, i there exists a step j, such that s $ t C s $ t. Imposing fairness, we have: i j Proof Normalization Theorem Huet, 1981 . If a completion sequence E ; ; `KB E ; R `KB is fair, then for any proof s $ t there exists a proof s ! v t using reduced rules only. i R R Huet introduced the notion of fairness of completion and proved this theorem for a speci c fair implementation; the following proof Bachmair-etal, 1986 builds on the above development and holds for any implementation of the inference system KB : Proof. The proof is by induction with respect to C . Suppose that s $ t is not a rewrite proof i s ! t. Then it must contain a peak that is reducible by C. Similarly, if s $ t involves a i R R nonpersistent step, then it is C-reducible. By fairness, s $ t C s $ t for some step j and by induction i j there is a proof s ! t with only reduced rules. R R By the Critical Pair Lemma, non-critical peaks are C-reducible. Thus, it can be shown that a completion sequence is fair if all persistent critical pairs are accounted for cpR1 is a subset of Ei, no simpli able rule persists R1 is reduced, and no equation persists E1 is empty. Practically speaking, fairness means that critical pairs are generated for all new rules, and need eventually to be simpli ed or oriented, unless the new rule itself is later simpli ed. A marking scheme is generally used to keep track of which rules still need to be overlapped with which; see, for instance, Huet, 1981 . By generating the remaining critical pairs and then eliminating them, Figure 5 becomes fair. We say that an n-step completion sequence E ; ; `KB E ; R `KB `KB En ; Rn succeeds if En is empty, Rn is reduced, and each of the latter's critical pairs already appeared in some Ei. The sequence fails if no fair sequence has it as a pre x; in that case there is little point continuing. A completion procedure is considered correct if it only generates fair, successful sequences|when it does not abort. Assuming the procedure never discriminates against any critical pair or simpli able rule or equation, the only good reason to abort and produce a failing sequence is if all equations are unorientable. The critical pair criteria mentioned in the Section 7.1 may be used to improve on the above requirements for fairness, by necessitating consideration of fewer critical pairs; see Bachmair-Dershowitz, 1988 . It follows from the above theorem that the limit R1 of a fair sequence is canonical. Furthermore, since $ = $ , completion, correctly implemented, provides a semi-decision procedure for validity, or else aborts. 1 That is, if ModE j= s = t, and if completion does not give up in the middle, then, at some step k, it will be possible to check that s !Rk Rk t. Note that two successful derivations, given the same starting set E and reduction ordering , must output the same canonical systems, be they nite or in nite, since there can be but one reduced, canonical system up to literal similarity contained in see Section 7.5. Thus, if there exists a canonical system R for E contained in , then a correct procedure, given E and , cannot succeed with any system but R|though it may abort without nding it. Furthermore, if R is nite, then an in nite, looping completion sequence is likewise impossible, since R1 must be of the same size as R.

0 1 1 0 1 1 + 0 1 1

8.2 Fairness

1

1

1

1

+

1

1

0

1

1

0

0

!

!

0

0

0

Before we consider other theorem-proving applications of completion, we adapt it to handle extended rewriting. Let S be an equational system and a reduction ordering such that commutes over S. Rules are compared using the following ordering: s ! t _ l ! r if s s0 =S l, for some s0 i.e. if s properly encompasses

8.3 Extended Completion

39

As before, we write E; R `KB =S E 0 ; R0 if the latter may be obtained from the former by one application of a rule in KB =S. With this inference system, delete removes an equation between S-equivalent terms; collapse simpli es left-hand sides; extend adds extended rules; deduce generates extended critical pairs. Extended rewriting requires S-matching; S-completion requires S-uni cation to generate critical pairs and extended rules. The set S is unchanging throughout. De nition 25. An S -completion procedure is any program that takes a nite set E of equations, an Suni cation procedure, and a reduction ordering that commutes over S, and uses the above rules KB =S to generate a sequence of inferences from E ; ;. The most important case, in practice, is when S is a set of commutativity C or associativitycommutativity AC axioms for some binary function symbols Lankford-Ballantyne, 1977b; Peterson-Stickel, 1981 . For the purposes of AC-completion, rules are commonly attened by removing nested occurrences of associative-commutative symbols. An associative-commutative uni cation algorithm is employed|in place of the standard syntactic uni cation algorithm|to generate the critical pairs in cpAC Ri , and associativecommutativematching is used to apply rules. For each rule fs; t ! r headed by an associative-commutative symbol f, an extended rule fs; ft; z ! fr; z is added and attened out to fs; t; z ! fr; z; extensions of AC-extended rules are redundant. For example, consider the same set E as in Figure 5, along with the following set S of AC axioms: xy $ y x x y z $ x y z

0 0 0

a term that is S-equivalent to l, or else s = l and t r. We de ne the following set KB =S of inference rules: Delete: E fs = tg; R ` E; R if s $ t S Compose: E; R fs ! tg ` E; R fs ! vg if t !R=S v Simplify: E fs = tg; R ` E fu = tg; R if s !R=S u Orient: E fs = tg; R ` E; R fs ! tg if s t Collapse: E; R fs ! tg ` E fv = tg; R if s !R=S v by l ! r with s ! t _ l ! r Extend: E; R ` E; R fs ! tg if s ! t 2 exS R Deduce: E; R ` E fs = tg; R if s = t 2 cpS R

Extend uses associativity to create two extended rules, 1 x z ! x z and x, x z ! 1 z, the rst of which collapses away, and the second of which composes to yield an existing rule. Deduce generates x y, x ! y, from an S-overlap of x, x y ! y on itself at position 2. The resultant rule is extended to x y, x z ! y, z, which forms an S-critical pair with x, x ! 1 and generates x, y, !x y, .

Extending as necessary, cleaning up, and 1, ! x x, ! x, , ! x y, x ! x, y, ! attening products, the 1 x1 1 x x, z x x y, , y, x y, x z y x, x, y, z nal result is: ! x ! z ! x, y ! y, z ! y x, z

A better choice of ordering, one that would make y x, greater than x, y, , would result in the following neater system G=AC for Abelian commutative groups: 1, ! 1 x1 ! x x x, ! 1 x x, z ! z x, , ! x y x, ! x, y, 40

A proof in S E R is a sequence of S-steps, E-steps, and R-steps. Analogous to the standard case, a relation C=S can be de ned that describes the simplifying e ect of S-completion at the proof level. Using the Extended Critical Pair Lemma, it can then be shown that a completion sequence is fair with respect to C=S if all persistent critical pairs are accounted for cpS R1 is a subset of the S-variants of Ei, all persistent extended rules are accounted for exS R1 is a subset of the S-variants of Ri, and no equation persists E1 is empty. With fairness, we get that an extended-rewrite proof s ! nR $ nR t will S S S eventually be generated if s $S E0 t Jouannaud-Kirchner, 1986 . However, the limit S nR1 need not be reduced. Additional aspects of completion modulo equational theories have been considered: Huet, 1980 deals with the left-linear case; Jouannaud-Kirchner, 1986 analyze exactly which critical pairs are necessary when some rules are left-linear and others are not; Bachmair-Dershowitz, 1987a take the inference rule approach and generalize previous results.

1 1

We have seen that completion can have any one of three outcomes: it may succeed in nding a decision procedure for validity after a nite number of steps; it may loop and generate more and more rules until|at some point|any particular valid equation has a rewrite proof; or it may abort with unorientable equations before nding any proof. Since there are total reduction orderings for any set of ground terms the lexicographic path ordering with total precedence is one such, completion of ground terms|given such an ordering|will not abort. Moreover, ground completion need never apply the deduce inference rule, since the collapse rule always applies to one of the rules contributing to a critical pair. And without deduce, completion will not loop. Thus, for any nite set of ground equations, completion is sure to generate a decision procedure Lankford, 1975 , which is not surprising, since all such theories are decidable Ackermann, 1954 . In fact, various On lg n congruence-closure algorithms exist for the purpose e.g. Downey-etal, 1980 ; see also Snyder, 1989 . More interesting are those cases where there are non-ground rules for which a canonical rewrite system is available, and all critical pairs between a ground rule and a non-ground one are either ground or simplify to a trivial rule. By supplying completion with a complete simpli cation ordering, these critical pairs can always be oriented. The complete ordering must be compatible with the canonical system for the non-ground rules. For example, AC-completion can be used in this way to generate decision procedures for nitely-presented Abelian groups starting from G=AC Lankford-etal, 1984 . We now turn our attention to completion of ordered rewriting systems, and call the process ordered" or unfailing" completion. Ordered completion either returns a nite ordered rewriting system in nite time, or else loops and generates an in nite system. With a nite system, validity can be decided by ordered rewriting; an in nite system can only serve as a semi-decision procedure. Since all orientable instances of equations are used to rewrite, there will be no need to explicitly distinguish between rewrite rules and other equations in the inference rules. Let be a reduction ordering that can be extended to a complete simpli cation ordering, and let be the encompassment ordering. Consider the following set OC of inference rules, operating on set of equations E cf. Bachmair-etal, 1989 : Delete: E fs = sg ` E Simplify: E fs = tg ` E fs = ug if t ! u and s u Collapse: E fs = tg ` E fs = ug if t ! u by l = r and t l Deduce: E ` E fs = tg if s = t 2 cp E We write E `OC E 0 if the latter may be obtained from the former by one application of a rule in OC. With this inference system, deduce generates ordered critical pairs, and the other rules simplify them. De nition 26. An ordered completion procedure is any program that takes a nite set E of equations and a reduction ordering that can be extended to a complete simpli cation ordering, and uses the above rules OC to generate a sequence of inferences from E .

0 0

8.4 Ordered Completion

41

For example, consider the following axioms for entropic groupoids: x y x = x x y z y = x z y y

1 2 1 2

The second equation is permutative and cannot be oriented by any reduction ordering. Completion will therefore fail. Ordered completion, on the other hand, yields the ground-convergent ordered-rewriting system shown in Section 7.4. Analogous to the standard case, a relation OC can be de ned that describes the simplifying e ect of ordered completion at the proof level. Fairness is de ned accordingly. Using the Ordered Critical Pair Lemma, it can then be shown that a completion sequence is fair with respect to OC if all persistent critical pairs are accounted for, i.e. if cp E1 is a subset of Ei. With fairness, we get that a rewrite proof between two ground terms s and t will eventually be generated i s $ 0 t Hsiang-Rusinowitch, 1987 . E Thus, the word problem in arbitrary equational theories can always be semi-decided by ordered completion. See Boudet-etal, 1988 for an interesting application. It is not hard to see that OC can mimic KB for any given equational theory E and reduction ordering not necessarily total on G . The natural question is whether ordered completion must succeed in generating a canonical set of rules whenever one exists for the given reduction ordering . The answer is a rmative Bachmair-etal, 1989 , provided can be extended to a complete reduction ordering. For example, if b and c are incomparable, ordered completion infers fb = cg; ffb ! a; d ! b; fc ! cg OC fb = c; fc = ag; ffb ! a; d ! b; fc ! cg ` With the recursive path ordering in which f c a, this sequence continues until success:

` fb = c; c = ag; ffb ! a; d ! b; fc ! c; fc ! ag OC ;; ffa ! a; b ! a; c ! a; d ! ag ` OC

+ +

Ordered completion can also be modi ed to act as a refutationally complete inference system for validity in equational theories. To prove s = t, its Skolemized negation eqs0 ; t0 = F is added to the initial set E feqx; x = T g of equations. With a completable reduction ordering the Skolem constants are added to the algebra, hence must be comparable, the outcome T = F characterizes validity of s = t in the theory of E Hsiang-Rusinowitch, 1987 .

8.5 Inductive Theorem Proving

An inductive theorem-proving method based on completion was rst proposed in Musser, 1980 . Recall from Section 3.2 that an inductive theorem s =I E t holds i there is no equation u = v between ground terms that follows from E fs = tg, but not from E alone. Let H be a set of equational hypotheses. Given a ground-convergent system R for E, we aim to nd a ground-convergent system R0 for E H with the same ground normal forms. If R0 is the result of a successful completion sequence starting from H; R and using an ordering containing R, then, by the nature of completion, R0 is convergent and every term reducible by R is reducible by R0 . To check that every ground term reducible by R0 is also R-reducible, it is necessary and su cient that every left-hand side of R0 be ground R-reducible. If R0 passes this test, then the two systems have the same ground normal forms and s =I R t for each s = t in H Dershowitz, 1982b; JouannaudKounalis, 1989 . If, on the other hand, s 6=I R t, then fair completion will uncover an inconsistency, if it does not fail. This approach is also valid when extended-completion or ordered-completion is used Goguen, 1980 . For example, let F be f; push; alternateg and R be the following canonical system for interleaving stacks: alternate ; z ! z alternate pushx; y; z ! pushx; alternate z; y

42

and suppose we wish to prove that alternate y; = y is an inductive theorem. This equation can be oriented from left to right. Since the critical pairs = and pushx; y = pushx; alternate ; y are provable by rewriting, completion ends with the system R0 = R falternate y; ! yg. Since the left-hand side alternate y; of the new rule is ground R-reducible, for all ground terms y in G f; push; alternate g, the theorem is valid in IR. In more complicated cases, additional lemmata may be generated along the way. Finding an R0 that is complete for H R as completion does is actually much more than needed to preclude inconsistency. One need only show that some R0 provides a valley proof for all ground consequences of H R and that RG R0 G . Thus, for each inference step Hi ; Ri `OC Hi ; Ri , the equational hypotheses in Hi should be inductive consequences of Hi Ri, and the rules in Ri should be inductive consequences of Ri Bachmair, 1988 . Then, at each stage n, H R follows from Hn R ; the original hypotheses H are proved as soon as an empty Hn su ces. Assuming Ri is always the original R, it is enough if any ground cli v R u $Hi w can be reduced to a smaller proof in Hi R smaller, in some well-founded sense, and no instance of a hypothesis in Hi is itself an inconsistency that is, an equation between two distinct ground R-normal forms. Consequently, there is no need though it may help to generate critical pairs between two rules derived from H ; it su ces to consider critical pairs obtained by narrowing with R at a set of covering" positions in Hi Fribourg, 1986 . When, and if, these pairs all simplify away, the inductive theorems are proven. On the other hand, if any of the hypotheses are false, a contradiction must eventually surface in a fair derivation. The use of critical pair criteria in this connection is explored in Gobel, 1987; Kuchlin, 1989 . How to handle inductive equations that cannot be oriented is discussed in Bachmair, 1989b; Jouannaud-Kounalis, 1989 .

+1 +1 +1 +1 0 0 0 0 +1 0

8.6 First-Order Theorem Proving

Rewriting techniques have been applied to rst-order theorem proving in two ways. One approach is to use resolution for non-equality literals together with some kind of superposition of left-hand sides of equality literals within clauses Lankford-Ballantyne, 1979; Peterson, 1983; Hsiang-Rusinowitch, 1986; Bachmair, 1989a . An alternative approach Hsiang-Dershowitz, 1983 is to use the Boolean ring system BA of Section 2 and treat logical connectives equationally. Let R be BA, S be AC for xor and and , and E = fs = T g, where s is a logically unsatis able Boolean formula. It follows from Herbrand's Theorem Herbrand, 1930 that a nite conjunction of instances s i has normal form F under BA=AC. Thus, AC-completion, starting with R and E, will reduce the proof T BA and : : : and T; T ; : : :; T $ and : : : and s ; s ; : : :; s n ,! BA=AC F E

1 2

to a critical pair T = F, if it does not fail. As with resolution theorem-proving, one can prove validity of a closed formula in rst-order predicate calculus by deriving a contradiction from its Skolemized negation. There are several problems with such an approach: a AC-uni cation is required to compute critical pairs; b failure is possible unless the more expensive ordered procedure is used; and c critical pairs with the distributivity axiom in BA are very costly. Hsiang 1985 showed that if each equation in E is of the form xor s; T = F, where s is the exclusive-or normal form of a clause, then only a subset of the critical pairs with BA must be computed. See Muller-Socher-Ambrosius, 1988 for clari cations regarding the need for factoring" if terms are simpli ed via BA. This approach allows the integration of convergent systems for relevant equational theories, when such are available. A di erent completion-like procedure for rst-order theorem proving, incorporating simpli cation, has been proved correct by Bachmair-Dershowitz, 1987b . A rst-order method, using Boolean rings and based on polynomial ideals, is Kapur-Narendran, 1985 .

8.7 Further Reading

A survey of completion and its manifold applications may be found in Dershowitz, 1989 . For a book focusing on the abstract view of completion and its variants, see Bachmair, 1989b . The relationship 43

between completion and algorithms for nding canonical bases of polynomial ideals is discussed in Loos, 1981 and Buchberger, 1987 . Reve Lescanne, 1983 , Formel Fages, 1984 , Kads Stickel, 1986 , and Rrl Kapur-Zhang, 1988 are four current implementations of AC-completion. Rewrite-based decision procedures for semigroups, monoids, and groups are investigated in Benninghofen-etal, 1987 ; experiments with the completion of nitely-presented algebras are described in Lankford-etal, 1984; LeChenadec, 1985 ; some new classes of decidable monadic word problems were found in Pedersen, 1989 . The use of completion and its relation to Dehn's method for deciding word problems and small cancellation theory is explored in LeChenadec, 1987 . Early forerunners of ordered completion were Lankford, 1975; Brown, 1975 . Ordered completion modulo a congruence has been implemented by Anantharaman-etal, 1989 . One of the rst implementations of inductive theorem proving by completion was Huet-Hullot, 1980 . A recent book on using rewrite techniques for theorem proving in rst-order predicate calculus with equality is Rusinowitch, 1989 .

9 EXTENSIONS

In this section, we brie y consider four variations of the rewriting theme: order-sorted rewriting," conditional rewriting," priority rewriting," and graph rewriting." In ordered rewriting, replacement is constrained to make terms smaller in a given ordering; more syntactic means of limiting rewriting are obtained by taxonomies of term types. For example, some data may be of type Boolean, some may represent natural numbers, others, stacks of reals. The appropriate semantic notion in this case is the many-sorted heterogeneous algebra. Under reasonable assumptions, virtually everything we have said extends to the multisorted case. Sorted i.e. typed rewriting has been dealt with, for example, in Huet-Oppen, 1980; Goguen-Meseguer, 1985 . Order-sorted algebras, introduced in Goguen, 1978 and developed in Gogolla, 1983; Dick-Cunningham, 1985; Goguen-etal, 1985; Goguen-Meseguer, 1987; Smolka-etal, 1989 , and others, extend sorted algebras by imposing a partial ordering on the sorts, intended to capture the subset relation between them. For example, one can distinguish between stacks, in general, and non-empty stacks by declaring NonEmptyStack to be a subsort of Stack and specifying their operations to have the following types: : ! Stack push : Nat Stack ! NonEmptyStack top : NonEmptyStack ! Nat pop : NonEmptyStack ! Stack The main advantage is that de nitions can be su ciently complete without introducing error elements for functions applied outside their intended domains like top. Free algebras can be constructed in the order-sorted case Goguen-Meseguer, 1987 , but the algebra obtained is, in general, an amalgamation of the term algebra. To avoid this complication, a syntactic regularity" condition namely, that every term has a least sort may be imposed on the signature GoguenMeseguer, 1987 . Subsorts also require run-time checking for syntactic validity. For example, the term poppushe; pushe; has sort Stack, so its top cannot be taken, yet that term is equal to the nonempty stack pushe; . Fortunately, the run-time checks require no additional overhead Goguen-etal, 1985 . Deduction in order-sorted algebras also presents some di culties. For example, suppose that a sort S 0 contains two constants a and b, and S is the supersort S 0 fcg. Let E consist of two identities: a = c and b = c, and consider the equation fa = fb, where f is of type S 0 ! S. Clearly, the equation holds in all models, but this cannot be shown by replacement of equals, since fc is not well-formed. Additional problems are caused when a sort is allowed to be empty, as pointed out in Huet-Oppen, 1980 . A sound and complete set of inference rules for order-sorted equality is given in Goguen-Meseguer, 1987 . 44

9.1 Order-Sorted Rewriting

For order-sorted rewriting, con uence does not imply that every theorem has a rewrite proof. Consider the same example as in the previous paragraph. The system fa ! c; b ! cg is con uent, but there is no rewrite proof for a = b, since a term is not rewritten outside its sort. One way to preclude such anomalies is to insist that rules be sort decreasing," i.e. that any instance of a right-hand side have a sort no larger than that of the corresponding left-hand side Goguen-etal, 1985 . Order-sorted uni cation is investigated in Walther, 1988; Meseguer-etal, 1989 and order-sorted completion, in Kirchner, 1987 . Another way to restrict applicability of equations is to add enabling conditions. A conditional equation is an equational implication u = v ^ ^ un = vn s = t, for n 0 that is, a universal Horn clause with equality literals only. An example of a conditional equation with only one premiss is empty?x = no pushtopx; popx = x. Initial algebras exist for classes of algebras presented by conditional equations. A conditional rule is an equational implication in which the equation in the conclusion is oriented, for which we use the format u = v ^ ^ un = vn j l ! r. The following is an example of a system of both conditional and unconditional rules: toppushx; y ! x poppushx; y ! y empty? ! yes empty?pushx; y ! no empty?x = no j pushtopx; popx ! x To give operational semantics to conditional systems, the conditions under which a rewrite may be performed need to be made precise. In the above example, is a term pushtops; pops rewritten whenever the subterm s is such that the condition empty?s = no can be proved, whenever a rewrite proof exists, or only when empty?s rewrites to no? The rami cations of various choices are discussed in Brand-etal, 1978; Bergstra-Klop, 1986; Dershowitz-etal, 1988 . The most popular convention is that each condition admit a rewrite proof; in other words, for a given system R, a rule u = v ^ ^ un = vn j l ! r is applied to a term t l if ui ! vi , for each condition ui = vi , in which case t l !R t r . Recent proposals for logic R R programming languages, incorporating equality, have been based on conditional rewriting and narrowing e.g. Dershowitz-Plaisted, 1985; Goguen-Meseguer, 1986 ; see Reddy, 1986 . For the above recursive de nition of !R to yield a decidable relation, restrictions must be made on the rules. The most general well-behaved proposal are decreasing systems, terminating systems with conditions that are smaller in a well-de ned sense than left-hand sides Dershowitz-etal, 1988 ; hence, recursively evaluating the conditions always terminates. More precisely, a rule u = v ^ ^ un = vn j l ! r is decreasing if there exists a well-founded extension of the proper subterm ordering such that contains !R and l ui ; vi for i = 1; : : :; n. Decreasing systems generalize the concept of hierarchy" in the work of Remy, 1982 , and are slightly more general than the systems considered in Kaplan, 1987; JouannaudWaldmann, 1986 ; they have been extended in Dershowitz-Okada, 1988b to cover systems important in logic programming with variables in conditions that do not also appear in the left-hand side, e.g. gx = z j fx ! hz. The rewrite relation !R for decreasing systems is terminating, and|when there are only a nite number of rules|is decidable. For con uence, a suitable notion of conditional critical pair," which is just the conditional equation derived from overlapping left-hand sides, is de ned. The Critical Pair Lemma holds for decreasing systems R Kaplan, 1987 : a decreasing system R is locally con uent and hence convergent i there is a rewrite proof s ! t for each critical pair u = v ^ ^ un = vn s = t and substitution R R such that ui = R vi for i = 1; : : :; n. Nevertheless, con uence is only semi-decidable, on account of the semi-decidability of satis ability of the conditions ui = vi . For non-decreasing systems, even ones for which the rewrite relation is terminating, the rewrite relation may be undecidable Kaplan, 1987 , and the Critical Pair Lemma does not hold, though terminating systems having no critical pairs are con uent see Dershowitz-etal, 1987a . To handle more general systems of conditional rules, rules must be overlapped on

1 1 1 1 1 1 1 1 1 1

9.2 Conditional Rewriting

45

conditions, extending ordered completion to what has been called oriented paramodulation" Ganzinger, 1987; Dershowitz, 1988; Kounalis-Rusinowitch, 1988 .

9.3 Priority Rewriting

In priority rewriting, the choice among several possible redexes is constrained to meet, a priori, given priorities on the rules. Priorities, then, are just a partial ordering of rules. The original Markov algorithms were priority string rewriting systems, in which the written order of the rules determined their priority. The following de nition of subtraction of natural numbers and divisibility of integers by naturals illustrates the conciseness made possible by using subsorts and priorities: Zero = f0g P os = succZero succPos Nat = Zero Pos Neg = negPos Int = Nat Neg ,: Nat Nat ! Int j: Nat Int ! fT; F; errorg x,0 ! x 0 , y ! negy succx , succy ! x , y 0jx ! error z jx : Neg ! F z j0 ! T z jx ! z jx , z Note how priority systems with a total priority ordering can have no critical" overlaps between two left-hand sides at the top. Priority term-rewriting systems were rst formally studied in Baeten-etal, 1984 . Their de nition is subtle, since an outermost redex is rewritten only if no possible derivation of its proper subterms enables a higher-priority rule at the outermost position. A condition is given under which this de nition of rewriting is computable. Priority systems cannot, in general, be expressed as term-rewriting systems. Rewriting has also been generalized to apply to graphs, instead of terms. In fact, the idea of rewriting all kinds of objects is already in Thue, 1914 . In graph rewriting, subgraphs are replaced according to rules, containing variables, themselves referring to subgraphs. For example, a rule fgx ! hx, when applied to a directed acyclic graph kga; fga, where ga is shared by k's two subterms, should rewrite the graph to kga; ha, with the a still shared. Unlike trees, graphs do not have a simple structure lending itself to inductive de nitions and proofs, for which reason, the graph-rewriting de nitions, as introduced in Ehrig, 1977 and simpli ed in Raoult, 1984 , have a global avor. A categorical framework is used to precisely de ne matching and replacement; a rewriting is then a pushout in a suitable category. Though the categorical apparatus leads to apparently complicated de nitions, many proofs, e.g. the Critical Pair Lemma, become nothing more than commutativity of diagrams. A completely di erent approach to graph rewriting is taken in Bauderon-Courcelle, 1987 , where nite graphs are treated as algebraic expressions. Finitely-oriented labeled hypergraphs are considered as a set of hyperedges glued together by means of vertices. This generalizes the situation of words, with hyperedge labels as the constants, gluing for concatenation, and a set S of equational laws de ning equivalence of expressions instead of associativity. Class-rewriting in R=S is, then, tantamount to graph-rewriting with a system R. 46

9.4 Graph Rewriting

We thank Leo Bachmair, Hubert Comon, Kokichi Futatsugi, Steve Garland, Rob Hasker, Jieh Hsiang, G
rard e Huet, St
phane Kaplan, Deepak Kapur, Pierre Lescanne, Joseph Loyall, George McNulty, Jos
Meseguer, e e Mike Mitchell, Paul Purdom, and Hantao Zhang for their help with aspects of this survey. It goes without saying that our work in this eld would not have been possible without the collaboration of many other colleagues and students over the years. The rst author's research was supported in part by the National Science Foundation under Grant DCR 85-13417, by the Center for Advanced Study of the University of Illinois at Urbana-Champaign, and by Hebrew University at Jerusalem. The second author's research was supported in part by the Greco Programmation du Centre National de la Recherche Scienti que, the ESPRIT project METEOR, and a CNRS NSF grant.

ACKNOWLEDGEMENTS

References

Ackermann, 1954 W. Ackermann, Solvable Cases of the Decision Problem, North-Holland, Amsterdam 1954. Anantharaman-etal, 1989 S. Anantharaman, J. Hsiang and J. Mzali, SbReve2: A term rewriting laboratory with AC-unfailing completion, Proc. of the Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, pp. 533-537, N. Dershowitz, ed. Available as Vol. 355 Lecture Notes in Computer Science, Springer, Berlin April 1989. Ardis, 1980 M. A. Ardis, Data abstraction transformations, Report TR-925, Ph.D. thesis, Department of Computer Science, University of Maryland. August 1980. Avenhaus, 1985 J. Avenhaus, On the termination of the Knuth-Bendix completion algorithm, Report 120 84, Universitat Kaiserslautern, Kaiserslautern, West Germany 1985. Baader, 1986 F. Baader, Uni cation in idempotent semigroups is of type zero, J. Automated Reasoning 2 3 1986. Bachmair-Dershowitz, 1986 L. Bachmair and N. Dershowitz, Commutation, transformation, and termination, Proc. of the Eighth International Conference on Automated Deduction, J. H. Siekmann, ed., Oxford, England, pp. 5-20. Available as Vol. 230, Lecture Notes in Computer Science, Springer, Berlin July 1986. Bachmair-Dershowitz, 1987a L. Bachmair and N. Dershowitz, Completion for rewriting modulo a congruence, Proc. of the Second International Conference on Rewriting Techniques and Applications, P. Lescanne, ed., Bordeaux, France, pp. 192-203. Available as Vol. 256, Lecture Notes in Computer Science, Springer, Berlin; revised version to appear in Theoretical Computer Science 1988 May 1987. Bachmair-Dershowitz, 1987b L. Bachmair and N. Dershowitz, Inference rules for rewrite-based rstorder theorem proving, Proc. of the Second Symposium on Logic in Computer Science, Ithaca, NY, pp. 331-337 June 1987. Bachmair-Dershowitz, 1988 L. Bachmair and N. Dershowitz, Critical pair criteria for completion, J. of Symbolic Computation 6 1, pp. 1-18 1988. Bachmair-Plaisted, 1985 L. Bachmair and D. A. Plaisted, Associative path ordering, J. of Symbolic Computation 1 4, pp. 329-349 December 1985. Bachmair, 1988 L. Bachmair, Proof by consistency in equational theories, Proc. of the Third IEEE Symposium on Logic in Computer Science, Edinburgh, Scotland, pp. 228-233 July 1988. 47

Bachmair, 1989a L. Bachmair, Proof normalization for resolution and paramodulation, Proc. of the Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, N. Dershowitz, ed. Available as Vol. 355 Lecture Notes in Computer Science, Springer, Berlin, pp. 15-28 April 1989. Bachmair, 1989b L. Bachmair, Canonical Equational Proofs, Pitman-Wiley, London. To appear 1989. Bachmair-etal, 1986 L. Bachmair, N. Dershowitz and J. Hsiang, Orderings for equational proofs, Proc. of the Symposium on Logic in Computer Science, Cambridge, MA, pp. 346-357 June 1986. Bachmair-etal, 1989 L. Bachmair, N. Dershowitz and D. A. Plaisted, Completion without failure, in: Resolution of Equations in Algebraic Structures, H. Ait-Kaci, M. Nivat, ed., II: Rewriting Techniques, Academic Press, New York, pp. 1-30 1989. Baeten-etal, 1984 J. C. M. Baeten, J. A. Bergstra and J. W. Klop, Priority rewrite systems, Report CS-R8407, Math Centrum, Amsterdam 1984. Barendregt, 1984 H. P. Barendregt, The Lambda Calculus, its Syntax and Semantics, North-Holland, Amsterdam. Second edition 1984. Barendregt, 1989 H. Barendregt, Functional programming and lambda calculus, in: Handbook of Theoretical Computer Science, J. van Leeuwen, ed., North-Holland, Amsterdam 1989. Bauderon-Courcelle, 1987 M. Bauderon and B. Courcelle, Graph expressions and graph rewritings, Mathematical Systems Theory 20, pp. 83-127 1987. Baxter, 1976 L. D. Baxter, A practically linear uni cation algorithm, Report CS-76-13, University of Waterloo, Waterloo, Canada 1976. Bellegarde-Lescanne, 1987 F. Bellegarde and P. Lescanne, Transformation orderings, Proc. of the Twelfth Colloquium on Trees in Algebra and Programming 1987. BenCherifa-Lescanne, 1987 A. Ben Cherifa and P. Lescanne, Termination of rewriting systems by polynomial interpretations and its implementation, Science of Computer Programming 9 2, pp. 137159 October 1987. Benninghofen-etal, 1987 B. Benninghofen, S. Kemmerich and M. M. Richter, Systems of Reductions, Lecture Notes in Computer Science 277, Springer, Berlin 1987. Bergstra-Klop, 1986 J. A. Bergstra and J. W. Klop, Conditional rewrite rules: Con uency and termination, J. of Computer and System Sciences 32, pp. 323-362 1986. Birkho , 1935 G. Birkhoff, On the structure of abstract algebras, Proc. of the Cambridge Philosophical Society 31, pp. 433-454 1935. Birkho , 1948 G. Birkhoff, Lattice Theory, American Mathematical Society, New York. Revised edition 1948. Bledsoe, 1977 W. Bledsoe, Non-resolution theorem proving, Arti cial Intelligence 9, pp. 1-35 1977. Bockmayr, 1987 A. Bockmayr, A note on a canonical theory with undecidable uni cation and matching problem, J. of Automated Reasoning 3, pp. 379-381 1987. Book, 1987 R. V. Book, Thue systems as rewriting systems, J. of Symbolic Computation 3 1&2, pp. 39-68 February April 1987. Book-etal, 1981 R. V. Book, M. Jantzen and C. Wrathan, Monadic Thue systems, Theoretical Computer Science 19 3, pp. 231-251 1981. 48

Bloom-Tindell, 1983 S. L. Bloom and R. Tindell, Varieties of `if-then-else', SIAM J. on Computing 12 4, pp. 677-707 November 1983. Boudet, 1989 A. Boudet, AC-uni cation is easy, Report, Laboratoire de Recherche en Informatique, Universite Paris-Sud, Orsay, France April 1989. Boudet-etal, 1988 A. Boudet, J.-P. Jouannaud and M. Schmidt-Schau, Uni cation in free extensions of Boolean rings and Abelian groups, Proc. of the Third Symposium on Logic in Computer Science, Edinburgh, Scotland, pp. 121-130. To appear in J. of Symbolic Computation July 1988. Brand-etal, 1978 D. Brand, J. A. Darringer and W. J. Joyner, Jr., Completeness of conditional reductions, Report RC 7404, IBM Thomas J. Watson Research Center, Yorktown Heights, NY December 1978. Brown, 1975 T. C. Brown, Jr., A structured design-method for specialized proof procedures, Ph.D. thesis, California Institute of Technology, Pasadena, CA 1975. Burckert-etal, 1987 H.-J. J. Burckert, A. Herold and M. Schmidt-Schau, On equational theories, uni cation and decidability, Proc. of the Second International Conference on Rewriting Techniques and Applications, P. Lescanne, ed., Bordeaux, France, pp. 204-215. Available as Vol. 256, Lecture Notes in Computer Science, Springer, Berlin May 1987. Buchberger-Loos, 1982 B. Buchberger and R. Loos, Algebraic simpli cation, in: Computer Algebra, Springer, Berlin, pp. 11-43 1982. Buchberger, 1987 B. Buchberger, History and basic features of the critical-pair completion procedure, J. of Symbolic Computation 3 1&2, pp. 3-38 February April 1987. Butler-Lankford, 1980 G. Butler and D. S. Lankford, Experiments with computer implementations of procedures which often derive decision algorithms for the word problem in abstract algebras, Memo MTP-7, Department of Mathematics, Louisiana Tech. University, Ruston, LA August 1980. Choppy-etal, 1987 C. Choppy, S. Kaplan and M. Soria, Algorithmic complexity of term rewriting systems, Proc. of the Second International Conference on Rewriting Techniques and Applications, P. Lescanne, ed., Bordeaux, France, pp. 256-285. Available as Vol. 256, Lecture Notes in Computer Science, Springer, Berlin May 1987. Church-Rosser, 1936 A. Church and J. B. Rosser, Some properties of conversion, Transactions of the American Mathematical Society 39, pp. 472-482 1936. Cohn, 1981 P. M. Cohn, Universal Algebra, D. Reidel, Dordrecht, Holland. Second edition 1981. Collins, 1975 G. Collins, Quanti er elimination for real closed elds by cylindrical algebraic decomposition, Proc. Second GI Conference on Automata Theory and Formal Languages, pp. 134-183. Available as Vol. 33, Lecture Notes in Computer Science, Springer, Berlin 1975. Colmerauer, 1984 A. Colmerauer, Equations and inequations on nite and in nite trees, Proc. of the Second International Conference on Fifth Generation Computer Systems, Tokyo, Japan, pp. 85-99 1984. Comon-Lescanne, 1989 H. Comon and P. Lescanne, Equational problems and disuni cation, J. of Symbolic Computation. To appear 1989. Comon, 1989 H. Comon, Disuni cation and inductive proofs, J. of Computer Systems and Sciences. To appear 1989. Curry-Feys, 1958 H. B. Curry and R. Feys, Combinatory Logic, 1, North-Holland, Amsterdam 1958. 49

Dauchet, 1989 M. Dauchet, Simulation of Turing machines by a left-linear rewrite rule, Proc. of the Third International Conference on Rewriting Techniques and Applications, Chapel Hill, NC, N. Dershowitz, ed. Available as Vol. 355 Lecture Notes in Computer Science, Springer, Berlin, pp. 109-120 April 1989. Dauchet-etal, 1987 M. Dauchet, S. Tison, T. Heuillard and P. Lescanne, Decidability of the con uence of ground term rewriting systems, Proc. of the Second Symposium on Logic in Computer Science, Ithaca, NY, pp. 353-359 June 1987. Davis-Hersh, 1973 M. Davis and R. Hersh, Hilbert's 10th problem, Scienti c American 229 5, pp. 84-91 November 1973. Dehn, 1911 M. Dehn, Uber unendliche diskontinuierliche Gruppen, Mathematische Ann. 71, pp. 116-144 1911. Dershowitz-Manna, 1979 N. Dershowitz and Z. Manna, Proving termination with multiset orderings, Communications of the ACM 22 8, pp. 465-476 August 1979. Dershowitz-Okada, 1988a N. Dershowitz and M. Okada, Proof-theoretic techniques and the theory of rewriting, Proc. of the Third Symposium on Logic in Computer Science, Edinburgh, Scotland, pp. 104-111 July 1988. Dershowitz-Okada, 1988b N. Dershowitz and M. Okada, Conditional equational programming and the theory of conditional term rewriting, Proc. of the International Conference on Fifth Generation Computer Systems, Tokyo, Japan November 1988. Dershowitz-Plaisted, 1985 N. Dershowitz and D. A. Plaisted, Logic programming cum applicative programming, Proc. of the IEEE Symposium on Logic Programming, Boston, MA, pp. 54-66 July 1985. Dershowitz, 1979 N. Dershowitz, A note on simpli cation orderings, Information Processing Letters 9 5, pp. 212-215 November 1979. Dershowitz, 1982a N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science 17 3, pp. 279-301 March 1982. Dershowitz, 1982b N. Dershowitz, Applications of the Knuth-Bendix completion procedure, Proc. of the Seminaire d'Informatique Theorique, Paris, France, pp. 95-111 December 1982. Dershowitz, 1984 N. Dershowitz, Equations as programming language, Proc. of the Fourth Jerusalem Conference on Information Technology, IEEE Computer Society, pp. 114-123, pp. 114-124 May 1984. Dershowitz, 1985 N. Dershowitz, Computing with rewrite systems, Information and Control 64 2 3, pp. 122-157 May June 1985. Dershowitz, 1987 N. Dershowitz, Termination of rewriting, J. of Symbolic Computation 3 1&2, pp. 69-115. Corrigendum December 1987 , Vol. 4, No. 3, pp. 409-410 February April 1987. Dershowitz, 1988 N. Dershowitz, Proving equational Horn clauses, . Submitted 1988. Dershowitz, 1989 N. Dershowitz, Completion and its applications, in: Resolution of Equations in Algebraic Structures, H. Ait-Kaci, M. Nivat, ed., II: Rewriting Techniques, Academic Press, New York, pp. 31-86 1989. Dershowitz-etal, 1987a N. Dershowitz, M. Okada and G. Sivakumar, Con uence of conditional rewrite systems, Proc. of the First International Workshop on Conditional Term Rewriting Systems, S. Kaplan, J.-P. Jouannaud, ed., Orsay, France. Available as Vol. 308, Lecture Notes in Computer Science, Springer, Berlin 1988 , pp. 31-44 July 1987. 50

Dershowitz-etal, 1987b N. Dershowitz and G. Sivakumar, Solving goals in equational languages, Proc. of the First International Workshop on Conditional Term Rewriting Systems, S. Kaplan, J.-P. Jouannaud, ed., Orsay, France. Available as Vol. 308, Lecture Notes in Computer Science, Springer, Berlin 1988 , pp. 45-55 July 1987. Dershowitz-etal, 1988 N. Dershowitz, L. Marcus and A. Tarlecki, Existence, uniqueness, and construction of rewrite systems, SIAM J. on Computing 17 4, pp. 629-639 August 1988. Dershowitz-etal, 1988 N. Dershowitz, M. Okada and G. Sivakumar, Canonical conditional rewrite systems, Proc. of the Ninth Conference on Automated Deduction, Argonne, IL, pp. 538-549. Available as Vol. 310, Lecture Notes in Computer Science, Springer, Berlin May 1988. Dick-Cunningham, 1985 R. J. Cunningham and A. J. J. Dick, Rewrite systems on a lattice of types, Acta Informatica 22, pp. 149-169 1985. Downey-etal, 1980 P. J. Downey, R. Sethi and R. E. Tarjan, Variations on the common subexpressions problem, J. of the Association for Computing Machinery 27 4, pp. 758-771 1980. Ehrenfeucht-etal, 1983 A. Ehrenfeucht, D. Haussler and G. Rozenberg, On regularity of contextfree languages, Theoretical Computer Science 27 3, pp. 311-332 December 1983. Ehrig, 1977 H. Ehrig, Introduction to the algebraic theory of graph grammars, Proc. of the International Conferenece on the Fundamentals of Complexity Theory, Pozn
n-K
rnik, Poland, pp. 245-255. a o Available as Vol. 56, Lecture Notes in Computer Science, Springer, Berlin 1977. Evans, 1951 T. Evans, On multiplicative systems de ned by generators and relations, I, Proc. of the Cambridge Philosophical Society 47, pp. 637-649 1951. Fages-Huet, 1983 F. Fages and G. Huet, Uni cation and matching in equational theories, Proc. of the Eighth Colloquium on Trees in Algebra and Programming, l'Aquilla, Italy, pp. 205-220. Available as Vol. 159, Lecture Notes in Computer Science, Springer, Berlin 1983. Fages, 1984 F. Fages, Le systme KB: manuel de r
f
rence: pr
sentation et bibliographie, mise en oeuvre, e ee e Report R. G. 10.84, Greco de Programmation, Bordeaux, France 1984. Fages, 1987 F. Fages, Associative-commutative uni cation, J. of Symbolic Computation 3 3, pp. 257-275 June 1987. Fay, 1979 M. Fay, First-order uni cation in an equational theory, Proc. of the Fourth Workshop on Automated Deduction, Austin, TX, pp. 161-167 February 1979. Feferman, 1968 S. Feferman, Systems of predicative analysis II: Representation of ordinals, J. of Symbolic Logic 33 2, pp. 193-220 June 1968. Filman, 1978 R. E. Filman, Personal communication 1978. Freese-etal, 1989 R. Freese, R. McKenzie, G. F. McNulty and W. Taylor, Algebras, Lattices, Varieties, II, Wadsworth, Monterey, CA. To appear 1989. Fribourg, 1986 L. Fribourg, A strong restriction of the inductive completion procedure, Proc. of the Thirteenth EATCS International Conference on Automata, Languages and Programming, L. Kott, ed., Rennes, France, pp. 105-115. Available as Vol. 226, Lecture Notes in Computer Science, Springer, Berlin; to appear in J. Symbolic Computation July 1986. Futatsugi-etal, 1985 K. Futatsugi, J. A. Goguen, J.-P. Jouannaud and J. Meseguer, Principles of OBJ2, Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, New Orleans, LA, pp. 52-66 January 1985. 51

Gallier-Snyder, 1987 J. H. Gallier and W. Snyder, A general complete E-uni cation procedure, Proc. of the Second International Conference on Rewriting Techniques and Applications, P. Lescanne, ed., Bordeaux, France, pp. 192-203. Available as Vol. 256, Lecture Notes in Computer Science, Springer, Berlin May 1987. Ganzinger, 1987 H. Ganzinger, A completion procedure for conditional equations, Proc. of the First International Workshop on Conditional Term Rewriting Systems, S. Kaplan, J.-P. Jouannaud, ed., Orsay, France. Available as Vol. 308, Lecture Notes in Computer Science, Springer, Berlin 1988 , pp. 62-83 July 1987. Gardner, 1983 M. Gardner, Mathematical games: Tasks you cannot help nishing no matter how hard you try to block nishing them, Scienti c American 24 2, pp. 12-21 August 1983. Gobel, 1987 R. Gobel, Ground con uence, Proc. of the Second International Conference on Rewriting Techniques and Applications, P. Lescanne, ed., Bordeaux, France, pp. 156-167. Available as Vol. 256, Lecture Notes in Computer Science, Springer, Berlin May 1987. Gogolla, 1983 M. Gogolla, Algebraic speci cations with partially ordered sets and declarations, Forschungsbericht Informatik 169, Universitat Dortmund, Dortmund, West Germany 1983. Goguen-Meseguer, 1985 J. A. Goguen and J. Meseguer, Completeness of many sorted equational deduction, Houston J. of Mathematics 11 3, pp. 307-334 1985. Goguen-Meseguer, 1986 J. A. Goguen and J. Meseguer Eqlog: Equality, types, and generic modules for logic programming, in: Logic Programming: Functions, Relations, and Equations, D. DeGroot, G. Lindstrom, ed., Prentice-Hall, Englewood Cli s, NJ, pp. 295-363 1986. Goguen-Meseguer, 1987 J. A. Goguen and J. Meseguer, Order-sorted algebra I: Partial and overloaded operators, errors and inheritance, Unpublished report, SRI International, Menlo Park, CA 1987. Goguen-Tardo, 1979 J. A. Goguen and J. J. Tardo, An introduction to OBJ: A language for writing and testing formal algebraic speci cations, Proc. of the Speci cation of Reliable Software Conference, pp. 170-189 April 1979. Goguen, 1978 J. A. Goguen, Exception and error sorts, coercion and overloading operators, Research Report, Stanford Research Institute 1978. Goguen, 1980 J. A. Goguen, How to prove algebraic inductive hypotheses without induction, with applications to the correctness of data type implementations, Proc. of the Fifth International Conference on Automated Deduction, Les Arcs, France, pp. 356-373. Available as Vol. 87, Lecture Notes in Computer Science, Springer, Berlin, W. Bibel, ed., R. Kowalski, ed. July 1980. Goguen-etal, 1985 J. A. Goguen, J.-P. Jouannaud and J. Meseguer, Operational semantics of ordersorted algebra, Proc. of the EATCS International Conference on Automata, Languages and Programming, pp. 221-231. Available as Vol. 194, Lecture Notes in Computer Science, Springer, Berlin 1985. Goldfarb, 1981 W. D. Goldfarb, Note on the undecidability of the second-order uni cation problem, Theoretical Computer Science, pp. 225-230 1981. Gorn, 1967 S. Gorn, Explicit de nitions and linguistic dominoes, in: Systems and Computer Science, J. Hart, S. Takasu, ed., University of Toronto Press, pp. 77-115 1967. Gries, 1981 D. Gries, The Science of Programming, Springer, New York 1981. Guessarian-Meseguer, 1987 I. Guessarian and J. Meseguer, On the axiomatization of `if-then-else', SIAM J. on Computing 16 2, pp. 332-357 April 1987. 52

Guttag, 1976 J. V. Guttag, Abstract data types and the development of data structures, Communications of the ACM 20 6, pp. 396-404 July 1976. Heilbrunner-Holldobler, 1987 S. Heilbrunner and S. Holldobler, The undecidability of the uni cation and matching problem for canonical theories, Acta Informatica 24 2, pp. 157-171 April 1987. Henkin, 1977 L. Henkin, The logic of equality, American Mathematical Monthly 84 8, pp. 597-612 October 1977. Herbrand, 1930 J. Herbrand, Recherches sur la th
orie de la d
monstration, Thse de doctorat, Univere e e sit
de Paris, Paris, France 1930. e Herold-Siekmann, 1987 A. Herold and J. Siekmann, Uni cation in Abelian semigroups, J. of Automated Reasoning 3 3, pp. 247-283 1987. Higman-Neumann, 1952 G. Higman and B. H. Neumann, Groups as groupoids with one law, Publ. Math. Debrecen 2, pp. 215-221 1952. Higman, 1952 G. Higman, Ordering by divisibility in abstract algebras, Proc. of the London Mathematical Society 3 2 7, pp. 326-336 September 1952. Hindley, 1964 J. R. Hindley, The Church-Rosser property and a result in combinatory logic, Ph.D. thesis, University of Newcastle-upon-Tyne 1964. Ho mann-O'Donnell, 1979 C. M. Hoffmann and M. J. O'Donnell, Interpreter generation using tree pattern matching, Proc. of the Sixth ACM Symposium on Principles of Pr

- Theoretical Computer Science,
- DRAFT Chapter for the CRC Handbook of Computer Science
- and Theoretical Computer Science Computational Power of Gene Rearrangement
- 2 Theoretical Computer Science--- Results
- Theoretical Computer Science Cheat Sheet
- (Express), volume 128 of Electronic Notes in Theoretical Computer Science,
- Original in Formal Syntax and Semantics of Java, LNCS volume 1523
- Chicago Journal of Theoretical Computer Science MIT Press Volume 1995, Article 1
- Chicago Journal of Theoretical Computer Science MIT Press Volume 1995, Article 2
- What is Theoretical Computer Science (Preliminary Version)

更多相关文章：
**
***Chapter* *6* *Formal* School Statuses and Rolesppt课件_图文.ppt

*Chapter* *6* *Formal* School Statuses and Rolesppt课件_基础医学_医药卫生_专业资料。*Chapter* *6* *Formal* School Statuses and Rolesppt ...**
[化学课件]有机化学英文课件***chapter*1_图文.ppt

[化学课件]有机化学英文课件*chapter*1_理学_高等教育...halogens have 1 bond and 3 lone pairs *Formal* ...F *B* : *6* electrons in the valence shells *of* ...**
北京航空航天大学 离散数学课件 ***Chapter*0_图文.ppt

北京航空航天大学 离散数学课件*Chapter*0_理学_高等... 罗森著,袁崇义等译,离散数学及其应用(原书第*6*版 ...*Computer* *Science*: *Computer* Architecture, Data ...**
***Chapter* *6* *Formal* School Statuses and Roles_图文.ppt

*Chapter* *6* *Formal* School Statuses and Roles_英语...http://video.sina.com.cn/v/*b*/167310 24-...Participate in professional development on *methods* ...**
商务交际英语(1) ***Chapter6*_图文.ppt

商务交际英语(1)*Chapter6*_英语学习_外语学习_教育...? *B*. Here at ABC Company, we sincerely ...6.3 Writing *Formal* Reports 撰写正式报告 ? 正式...**
***Chapter* 3_students slides_图文.ppt

27人阅读|*6*次下载 *Chapter* 3_students slides_...A *formal* collection *of* people and other resources...Burry, President *B*. Wong, VP Accounting C.Rod...**
重庆大学算法导论英文课件***Chapter*_22_Elementary_Graph_图文.pdf

重庆大学算法导论英文课件*Chapter*_22_Elementary_Graph...*of*?*Computer*?*Science*?and?Engineering,?CQU Algorithm...Example (Parenthesis Theorem) y 3/*6* *B* 4/5 x...**
***chapter* 7 *formal* and informal style_图文.ppt

*chapter* 7 *formal* and informal style_英语考试_外语...A *Handbook* *of* Writing Unit Seven *Formal* and ...IV. 介绍一些典型的对偶句 *6*.There are no ugly ...**
***chapter* *6* *formal* approaches to sla_图文.ppt

*chapter* *6* *formal* approaches to sla_专业资料。...(*b*) attribute the results to methodological ... *theoretical* paradigms provide regarding the old ...**
...- On Teaching ***Theoretical* Foundations *of* *Computer* *Science* ....pdf

*chapter* and s u *b* s t i t u t e *6* with...*Chapter* : *Theoretical* *Computer* *Science* *formalism*s ...*of* Programming "*Formal* languages Wesley, and their...**
***Chapter* *6* Memo_Writing_图文.ppt

no prior*computer* knowledge or any *formal* course work in *computer* *science*. ... BE Writing *Chapter* *6* *B*... 3页 1下载券 *Chapter*_*6*-1_Writing_Bu.....**
***Chapter* *6* Thought Patterns and Language_图文.ppt

*Chapter* *6* Thought Patterns and Language_英语学习_...*Formal* Logicalfocus Thinking Mode ? The Chinese ...precision is conducive to *theoretical* construction. ...**
英文版国际金融练习题***Chapter*_*6*.doc

英文版国际金融练习题*Chapter*_*6*_经济学_高等教育_教育专区。国际金融 ...A. percentage change *B*. settle C. open interest D. estimated *volume* 10....**
国际经济学第八版***Chapter* *6*_图文.ppt

国际经济学第八版*Chapter* *6*_经济学_高等教育_教育...6.4 C *Formal* Model *of* Intra-Industry Trade (...*6*.5 *B* Illustration *of* the product cycle model ...**
***Chapter* *6* (II) Official Letters_图文.ppt

*Chapter* *6* (II) Letters ---- Official Letters Outline ? ? ? ? ? The ...*b*) ?Yours faithfully? (for an unacquainted receiver; *formal* British style)...**
The Mathematics ***of* Language.pdf

*theoretical* *computer* *science* (complexity classes, language hierarchies, *formal* ...The last *chapter*, *chapter* *6* - The Model Theory *of* Linguistic Structure - ...**
...1 Logic and the Challenge ***of* *Computer* *Science*_免....pdf

35页 免费*of* the *Computer* *Science* ... 暂无评价 8页 免费 *Chapter* *6* *of* *Handbook* *of*... 暂无评价 65页 免费喜欢此文档的还喜欢...**
***Chapter* *6*-2 Quantity *of*__ Goods_图文.ppt

*Chapter* *6* Terms *of* Commodity Part 2: Quantity *of* Commodity Quantity *of* ...*theoretical* weight 箩、令、打等计量单位一般用于( ) A.SALE BY QUANTITY *B*....**
***Computer* *Science* Overview Brookshear PPT Chap 06_图文.ppt

*Chapter* *6*: Programming Languages *Computer* *Science*: ...*Formal* versus Actual Parameters ? Passing parameters...Cylinder*Volume* written in the programming language ...**
跨文化***chapter6*_图文.ppt

voice qualities*volume* tempo articulation nasality ... polychronic cultures have a much less *formal* ...*Chapter* *6* Nonverbal Intercultural Communication *b*. ... 更多相关标签：

[化学课件]有机化学英文课件

北京航空航天大学 离散数学课件

商务交际英语(1)

27人阅读|

重庆大学算法导论英文课件

no prior

英文版国际金融练习题

国际经济学第八版

35页 免费

voice qualities