Unique Normal Forms and Confluence of Rewrite Systems: Persistence

1 Introduction

Two of the most challenging and important problems in rewriting are proving the Unique-Normal-Form and Church-Rosser (also called confluence) properties for non-l~ft-linear (nonlinear, for short) systems, particu­ larly m the absence of termination. There is consid­ erable progress on proving Church-Rosser theorems for left-linear systems (systems in which the left-hand sides (lhs's) of the rules contain at most one occurrence of any variable) [Church and Rosser, 1936; Rosen, 1973; O'Donnell, 1977; Huet, 1980]. In contrast, for nonlinear systems there are only a handful of general results and almost all of them require termination [Newman, 1942; Knuth and Bendix, 1970· Huet, 1980; Middeldorp and Toyama, 1991; Rao, 1993i. We know of only four works that do not require termination [Klop, 1980; Chew, 1981;

Toyama, 1987; Oyamaguchi and Ohta, 1992].

In 1980, Klop proved the Church-Rosser property for the disjoint sum of an orthogonal (i.e., left-linear and nonoverlapping; see next section for precise defini­ tions) combinatory reduction system and a single non­ linear rule of various specific forms (e.g., D ( x, x) -+ x and D(x,x) -+ E(x)). In 1987, Toyama proved that the disjoint-sum of two Church-Rosser rewrite sys­ tems is Church-Rosser. In 1992, Oyamaguchi and Ohta showed the Church-Rosser property for non-E­ overlapping right-ground (i.e., right-hand sides con­ tain no variables) rewrite systems. A weaker result than Church-Rosser, viz., uniqueness of normal forms for strongly nonoverlapping, 1 compatible systems was shown by Chew in the 1981 STOC [1981] (see also [Klop and de Vrijer, 1989] for some unique-normal-form results for ..X-calculus + specific rules). A strongly nonoverlap­ ping system is one that remains nonoverlapping even when the variables in the lhs's are renamed to make the rules left-linear. The non-E-overlapping requirement is stronger than Chew's strongly nonoverlapping require­ ment and is in a sense the strongest version of nonover­ lapping requirement possible.

·Research supported in part by NSF grant CCR-9303011.

In this paper, we attack these two fundamental prob­ lems and prove the following results:

• Every persistent system has the unique normal form property. Roughly speaking, persistence means that no rule can be applied inside the template (non-variable part) of an lhs. Persistence is a substantially weaker requirement than the strong-nonoverlap requirement, hence this result is a substantial generalization of Chew's result [Chew, 1981]. (To keep the technical details un­ derstandable we do not permit root overlaps. This gen­ eralization will be discussed in detail in the full version.) The approach used in proving .this result is also novel and should be outlined.

We introduce the idea of constraints and their sat­ isfiability in a rewrite system. We then characterize nonoverlaps and persistence as certain kinds of unsat­ isfiable constraints. We then prove that these kinds of constraints remain unsatisfiable even when certain kinds of rules are added to a persistent system and exploit this fact to first prove a slightly weaker uniquely nor­ malization property and then the unique normal form property (UN). This stepwise approach makes for eas­ ier understandability. Our approach also yields a neces-

1 Chew allows root overlaps provided they are compatible, e.g., x + 0 -+ x and 0 + x -+ x root overlap in 0 + 0.

&ary and sufficient condition for persistence for the first time, which we then use to give several syntactically­ checkable sufficient conditions for persistence. Some of these classes are new, not known previously to be per­ sistent. These results are significant generalizations of some of the results in [Verma, 1991], where a sufficient condition for persistence, based on proving unique nor­ malization (plus other technical conditions), was given. Our results are interesting from another viewpoint also. Persistence was introduced by us in a different context [Verma, 1991], viz., for generalizing to nonlinear systems the congruence-closure normalization algorithm of Chew [Chew, 1980], which in turn generalizes the congruence­ closure algorithm of [Downey et al., 1980; Kozen, 1977; Nelson and Oppen, 1980] to rules containing variables. Recently, we showed that persistence also plays a cen­ tral role in transforming certain kinds of rewrite systems into constructor-based rewrite systems [Thatte, 1988; Verma, 1995]. Therefore, our results in this paper pro­ vide substantial new evidence for the fundamental role of persistence in rewriting.

• We prove that the union (generalization of disjoint sum, function symbols can be shared) of a system R2 with a left-linear system R1 is confluent provided that the union is semi-terminating (no sequence containing infinite R2 reductions), persistent and rhs's of rules in R1 do not share any function symbols with lhs's of rules in R2. We are not aware of any confluence result which allows this much function sharing. The closest result is that of Klop's on CRS's. However, Klop's proof cannot be used directly since it uses postponement of certain kinds of reductions, which does not hold for us. More­ over, Klop gets persistence for free because of the speci­ ficity of rules in R2. Note that Toyama's proof technique cannot be used since it uses the non-increasing nature of ranks of terms, which does not hold for non-disjoint sums. Recently, Rao [Rao, 1993] generalizing a result of [Middeldorp and Toyama, 1991] proved a confluence resul.t for terminating systems that allows some sharing proVided that the union is a hierarchical combination and constructor-based. In particular, no sharing of de­ fined symbols is allowed in the lhs's and only construc­ tors can be shared between lhs of the higher system with rhs's of the lower. We note that Rao's proof is somewhat easier since his conditions ensure that the union is also terminating and persistent. The full proof of our result is fairly long. We sketch the important details here and leave the rest to the full version. We then give several s~cient conditions that can be checked syntactically, which ensure that the union has the properties we need.

· Finally, we consider the confluence of one-rule sys­ tems. The motivation for studying properties of one rule systems is Dauchet 's interesting result: every ( determin­ istic) turing machine can be simulated by a single left­ linear, nonoverlapping rule [Dauchet, 1992]. We show that there is a single nonoverlapping rule that is not per­ sistent and not confluent. The smallest previous example known to us contains 3 rules. We also state a confluence theorem for single rule persistent systems (proof omitted for space).

2 Preliminaries

To save space, we assume familiarity with basic no­ tions of rewriting (see [Dershowitz and Jouannaud, 1990; Klop, 1992] for excellent surveys). Let V be a countable set of elements called variables and E be a countable set of function symbols with E n V = 0. 7 is the set of all terms of a first-order language constructed from V and E. It is convenient to think of terms as or­ dered rooted trees. T(S) denotes that the terms are constructed from function symbols in S (the set V of variables is implicit). The root symbol of a term is: root(t) = / if t = /{tt, ... , tn), and root(t) =tift E V. Consider an extra constant 0 called a hole and the set T' = /(E U {D} ). ThenCE 7' is called a context on E. We use the notation C[, ... , ] for the context contatining n holes (n ~ 0). A is a subterm of B if B = C[A] for some context C.

The notion of a path or occurrence is used to refer to subterms in a term as follows. A path is either the empty string A that reaches the root or o.i ( o is a path and i an integer) which reaches the ith argument of the root of the subterm reached by o. tfo refers to the subterm oft reached by o and t[o +- s] denotes the term obtained by replacing the subterm tfo by s. o ~ q whenever 3p o.p = q; if p ¥= A also, then o < q. For any term t its set of occurrences is denoted O(t).

A substitution maps variables to terms. An instance (also called a redex) u(s) of a terms is obtained by sub­ stituting u(x) for every variable x ins. A rule is a pair of terms l ~ r, such that l rl. V and every variable oc­ curring in r also appears in l (the variables in a rule are implicitly universally quantified). A system R is a finite set of rules. By substituting different terms for the variables, we can produce many different rule instances from the same rule. We say that a rule A ~ B is a rule instance of the rule l ~ r if we can substitute terms for the variables in l ~ r to get A ~ B. As the variables of each rule are universally quantified we shall assume hereafter that any two distinct rules do not share any variable. Terms s and t are unifiable if and only if there exists a ground term C which is an instance of both s and t. We say s overlaps t if and only if a non-variable subterm u (proper subterm, if s = t) of one of the two terms unifies with the other term. (When checking for overlaps it is best to relabel the variables in s and t so that they do not share any variables.) A set S ~ 7 is nonoverlapping if and only iffor all s, t E S, not(s over­ laps t). (Since s and t could be equal, the definition of nonoverlapping does not allow self-overlapping rules like associativity.) We say that s and t root overlap if and only if they are left-hand sides of two distinct rules in the system and they can be instantiated to the same term. A system R is nonoverlapping if and only if the set of lhs's is nonoverlapping and there are no root overlaps.

Definition 1 (rewrite relation) We use~ to denote rewrite relations, where s ~ R t {read s reduces to t) if and only if 3 a 1'Ule l ~ r, an occurrence o E O(s), and a substitution u such that the subterm sfo = u(l) and t = s[o +- u(r)].

Notation. The letters a,b,c, etc., denote constants, v, x, y, z denote variables, and /, g, h, etc., denote func­ tion symbols of nonzero arity. We use = R to represent the least equivalence relation containing ~ R· When the set of rules R is clear from the context, we drop the subscripts from ~. The reflexive-transitive closure of ~ is denoted by ~ (i.e., a sequence of zero or more reductions). We use p: A~ B to give the name p to the sequence of reductions from A to B (!PI denotes its length). The transitive closure of~ is denoted by ~ (i.e., a sequence of one or more reductions). We use 4 to indicate root reduction (i.e., reduction of the entire term) and ~ to indicate nonroot reduction (i.e., reduction at a proper subterm). Similarly, ~ repre­ sents a sequence of zero or more nonroot reductions, etc. For every natural number n, [n] denotes {1, 2, ... , n }, [OJ =0.

Lemma 2 {[Newman, 1942]) A noetherian relation is locally confluent (LCR) if and only if it is confluent. (We say that relation ~ is locally confluent if and only if 'VA, B, C A ~ B and A ~ C implies 3 D such that B ~ D and C ~D. We say that relation ~ is con­ fluent (CR} if and only if'VA,B,C A~ Band A~ C implies 3D such that B ~ D and C ~D.)

Definition 3 Let R be a rewrite system. A term t is a normal form if there is no term u such that t ~ u. A term t has a normal form if there is a normal form u such that t ~ u. R (or ~R) is uniquely normalizing (is UN-+} if for all terms A, B, C such that A ~ B and A ~ C and B, C are normal forms we have B = C. R (or ~R) has unique normal forms (is UN) if for all normal forms A, B with A =R B we have A= B. R is terminating if there are no infinite reduction sequences to~ t1 ~ ....

The relation between the various properties CR, UN, and UN-+ is given in the next lemma.

Lemma 4 The following implications hold for every system R: C R =} UN =} UN-+. The reverse impli­ cations generally do not hold.

Proof: The proofs of both statements are standard (see, for example [Klop, 1980]). We include examples to show that the reverse implications do not hold always since they are useful in grasping some of the implications of our results.

UN-+ =/1- UN. Let R = {a~ b,a ~ c,c ~ c,d ~ c,d ~ e}. R is UN-+, but not UN since b =R e and b, e are distinct normal forms.

UN =/1- CR. Let R ={a~ b,b ~ b,a ~ c,c ~ c}. R is UN (a, b and c are not normal forms) but R is not CR since b and c do not have a common reduct. 0

Two rewrite systems Rt and R2 (see [Toyama, 1987] for formal definitions) are disjoint if no function symbol appears in a rule from R1 and a rule from R2· The dis­ joint sum is obtained by taking the union of two disjoint systems. Note that this disjoint sum is different from Klop's [Klop, 1980]. The disjoint sum of combinatory reduction systems (in which terms are written in "com­ binator notation") is defined as the union of two systems with disjoint constant symbols, but with the same appli­ cation function symbol. Klop pointed out that this sum does not preserve confluence.

3 Persistence

In this section we first define persistence and then give a necessary and sufficient condition for it. From the necessary and sufficient condition, we derive several syntactically-checked sufficient conditions for it. Finally, we use our characterization of persistence to prove that every persistent system is UN. Intuitively, persistence requires that the template of the lhs in a redex is un­ touched by nonroot reductions, and any root reduction after a sequence of nonroot reductions starting from a redex of l (l ~ r E R) can only be applied with the same rule. Hence all the terms in the sequence of non­ root reductions are instances of the template of l. (This property is the inspiration for the term persistence.)

Definition 5 R (or ~ R } is persistent if for every term A such that (i) A 4R B via l ~ r E R, (ii) A ~R A', and (iii) A' ~R B' vial'~ r' E R applied at o E O(A'), either {1} A' 4R B' and l' ~ r' = l ~ r, or (2} there is a u E 0(1), u ~ o, and l ju is a variable.

Note that persistence implies that the system must be nonoverlapping, but the converse is false, e.g., let R = {f(x,x) ~ a,f(x,g(x)) ~ a,b ~ g(b)}. The above definition of persistence is a slight modification of the definition in [Verma, 1991] to avoid root overlaps.

3.1 Necessary and Sufficient Conditions

We begin with some definitions.

Definition 6 An equation is a pair of terms ( s, t) with implicitly universally quantified variables. We say that an equation (s, t) is provable in a system R if sand tare joinable (reduce to a common term) in R.

A constraint is a pair of terms ( s, t) with implicitly ex­ istentially quantified variables. We say that a constraint ( s, t) is satisfiable in a system R, if there is a substitution u such that (u(s),u(t)) is provable in R. Substitution u is then called a satisfying substitution. A constraint ( s, t) is left-reducible if there is a substitution u such that u(s) ~ u(t). We say that u(s) is a solution in this case.

We extend these definitions to sets of equations and sets of constraints. In general, each constraint/equation may be separately existentially/universally quantified, but here we only need sets of constraints that are quan­ tified at the top level (i.e., a set of variable sharing con­ straints, so the substitution must be consistent for differ­ ent occurrences of the same variable).

Let R be a rewrite system and let l ~ r, l' ~ r' be two rules (not necessarily distinct) in R. Assume, for simplic­ ity, that distinct rules do not share any variables. Let U ni f denote the (ordinary) unification algorithm and Uni/ 00 denote the unification algorithm "without the occurs-check" (for concreteness, let these algorithms be the ones in [Dwork et al., 1984]). We say that a nonover­ lap of l with a non-variable subterm u of l' (proper sub­ term, if the two rules are the same) is due to occurs-check ( 0-nonoverlap) if l and u unify with U ni / 00 (but not with Unif). We say that a nonoverlap is due to inhomo­ geneity (!-nonoverlap), if land u do not unify even with Unif 00 · For an 0-nonoverlap of land u, Unif(l, u) gen­ erates a set of n > 0 constraints, where each constraint e; is of the form (z;, C;[z;, ... , z;]) (if one of the terms in a constraint is a variable, in this paper we adopt the con­ vention of listing it first) with some nonempty context C; not containing z; and whose template is (properly) included in the template of one of the terms (the z; 's are not necessarily distinct). We say that such a set of n > 0 constraints is left-unreducible in R iff there is no substitution u such that u(z;) ~R u(C;[z;, . . . ,z;]) for all i E [n]. In other words, the set of constraints is not left-reducible simultaneously.

Example. The nonoverlap of f(x,g(x)) and f(x,x) at the root is due to the occurs-check, whereas all the non­ overlaps of h(z,g(z), a) and h(x, x, b) are due to inhomo­ geneity.

Theorem 7 A rewrite system R is persistent if and only if the following conditions hold: {i) R is nonoverlapping, and (ii) For each 0-nonoverlap in R, the corresponding .set of constraints is left-unreducible in R .

Proof (sketch}: Necessity is obvious. For sufficiency, a direct proof that the stated conditions imply persistence is quite difficult. We prove the following stronger claim that implies persistence. Let L(R) denote the set of dis­ tinct (distinct means distinct even after variable renam­ ing) lhs's of rules in R and let SL(R) denote the set of all distinct non-variable subterms of the terms in L(R). (Note that since R is nonoverlapping the lhs's of two different rules must be distinct, but proper subterms of lhs's may not be.)

Claim 8 There is no term A such that p : A ~ B = u(l) and q: A~ C = u'(l') for distinct 1,1' in SL(R), unless l and l' overlap.

The proof is omitted to save space. Obviously persis­ tence follows from the claim, since the set of lhs's con­ tains neither root nor nonroot .overlaps. 0

Remark. In general, checking the second condition of Theorem 7 is easily seen to be undecidable even for a certain fixed rewrite system. However, below are some easily-checked syntactic conditions that imply the above condition.

• Corollary 9 1. Any nonoverlapping rewrite system in which all nonoverlaps are due to inhomogeneity is persistent.
• Any strongly nonoverlapping system (see [Chew, 1981]} is persistent.
• Any nonoverlapping rewrite system in which no function symbol appearing in the lhs of any nonlin­ ear rule appears on the rhs of any rule is persistent.
• ·. Any nonoverlapping quasi-terminating (see [Der­ showitz, 1987] for definition) is persistent.
• Any left-linear nonoverlapping system is persistent.

Proof: Straightforward.

0

Remarks. Note that except for quasi-termination all the other conditions can be easily checked syntactically given a rewrite system. The classes ( 1) and ( 4) of the corollary are new classes for which persistence was not known earlier. Note further that these applications are not meant to be exhaustive. They are included because of their utility and because some of them have appeared in the earlier literature in various contexts.

Examples. We give some simple examples to illustrate these classes.

For 1. Let R = {f(x,x)-+ a,f(a,b)-+ b}. R has only

I-nonoverlaps and R is not strongly nonoverlapping. For 2. Let R = {f(x,x) -+ e,g(x) -+ f(x,g(x)),c-+ g(c)} ([Klop, 1980J). Note that R is strongly nonover­ lapping and persistent (trivially) since every proper sub­ term (if it exists) of every lhs is a variable and the root symbols of alllhs's are different. Note also that R is not confluent since g( c) ~ g( e) and g( c) ~ e but g( e) and e are not joinable. Note however that R is UN.

For 3. Let R = {f(x,x)-+ a,f(x,g(x))-+ b,c-+ h(c)}. Note that if we change the third rule to c -+ g(c) the resulting system is not persistent and not confluent also. For 4. Let R = {f(x,x)-+ f(a,a),f(x,g(x))-+ b}.

For 5. Let R = {f(x,y) -+ e,g(x) -+ f(x,g(x)),c-+ g(c)}. Note that this is the left-linear version of the Example for 2. R is persistent and, of course, confluent.

We now prove the following important consequence of persistence: every persistent system R has the unique normal form property.

3.2 Unique Normal Form Property

Lemma 10 R is persistent iff R' = R U {h(x,x) -+ a,h(Nt,N2) -+ b} is persistent, where N1, N2 are two distinct normal forms with respect to R, and h, a, b are new function symbols not in the signature of R and not in N1 or N2 .

Proof: Clearly, R' persistent implies R persistent. Now suppose R is persistent. We note that R' is also nonover­ lapping and that the new rules only have I-nonoverlaps with R and with each other ( N1 and N2 are distinct terms and both contain no h's). So it suffices to show that every set of constraints corresponding to an 0nonoverlap that is left-unreducible in R is also left­ unreducible in R'. Suppose that there is a set of con­ straints that is left-reducible in R' but left-unreducible in R. Consider the case of one constraint z = C[z, ... , z]. Note that Cis some nonempty context and all the func­ tion symbols of C appear in the lhs's of some rules in R. In particular, h, a and b do not appear in C. Let u be the substitution such that p: u(z) =A ~R' C[A, ... ,A]. If A contains no h's, then the constraint is also left­ reducible in R since the rhs's of rules in R cannot intro­ duce any h in the term being reduced and hence the two extra rules in R' can never be applied in p. So suppose that A contains some h-preredexes. (terms h( ... )).

Therefore, let A = C'[At. ... , An] where the con­ text C' does not contain any symbols in { h, a, b} and root(A;) E {h,a,b} for i E [n]. Clearly, C' cannot be empty. Also, note that the C' can be modified, but it cannot be completely erased. Formally, every term t in the reduction sequence p must be of the form Ct[· .. ] for a nonempty context Ct not containing any symbols in { h, a, b}. We call a reduction in p an ex­ ternal reduction if it occurs outside every subterm of the form h( .. . ), and internal otherwise. Define a trans­ formation Ton terms in 7{FU {h,a,b}, V) to T(F, V) as follows: if t = C[to, ... , tn] {n ~ 0) where C is a (possibly empty) context not containing any symbols in {h,a,b} and root(t,) E {h,a,b} for i E [n], then T(t) = C[u, ... , u], where u E Vis a fixed variable.

Claim: A--+ R' B implies T(A) ~ R T(B).

Proof of claim. If the reduction from A to B is an inter­ nal step, then by the construction of R', T(A) = T(B), which is very important in the sequel. If the reduction step is external, then A = C[At, . .. An], where C is a nonempty context not containing { h, a, b} and there is an occurrence o E O{C) such that C/o :f. o, A/o = u(l) for some substitution u and rule l --+ r in R (note Rand not R'). Also, B = A[o +-- u(r )] = C'[Aiw .. , A,J, where ij E [n] and C' is a possibly empty context not containing symbols in {h,a,b}. Now the template of l must be contained in C since rules in R do not contain any function symbols from { h, a, b}, and vari­ ables in l cover subterms of the form A, {if any are dominated by occurrence o ). Now T(A) = C[u, ... , u]. Clearly, T(A)/o = u'(l), where u'(x) = T(u(x)) and T(A)[o +-- u'(r)] = C'[u, ... , u] = T(B) and we are done. 0

By the above claim and a simple induction we have the following claim: T(A) ~ R C[T(A), ... , T(A)] via the external reductions in p. But, this contradicts the assumption that the constraint was left-unreducible in R and the proof is complete. 0

Theorem 11 Every persistent system R is uniquely normalizing UN-+.

Proof: Suppose that R is not uniquely normalizing. Then, 3 A such that A~ Band A~ C, where B,C are distinct normal forms. Let R' = R U {h(x,x) --+ a,h(B,C) --+ b}, where h,a,b are new function sym­ bols not in the signature of R and not in B, C. Now h(A,A) ~R' h(B,C) so R' is not persistent. There­ fore, by Lemma 10, R is not persistent, which contradicts the assumption. 0

Theorem 12 Every persistent system R has the unique normal form property {UN).

Proof: Suppose that R is persistent but does not have the unique normal form property. Then, there are distinct R-normal forms A and B such that A = R B. Consider a shortest proof of A =R B. It is of the form q : At = A =R A2 =R ... =R B =An for some n > 1, where each = R step is either --+ R or +--R· Since A and B are R­ normal forms the first step in q is +-- and the last step in q is--+. Call a term A, in q a peak if Aa-t +--A,--+ Ai+t in q. Call a term Ai in q a valley if Aa-t --+ A, +­ Ai+t· Because the arrows at the ends are in opposite directions and towards A and B, there is at least one peak in q. Let A,,, ... , A,,. be all the peaks in q; and let At = Ah, . .. , Aj,.+ 1 = An be all the valleys in q. Here m > 0 and 1 =it <it <h ... < im < im+t = n. Note that the terms at both ends are also considered valleys. Therefore, we can write q as:

Let h2m be a new function symbol of arity 2m and a, b be two new constants not in the signature of R and not in A or B. Consider the system

By a similar argument as in the proof of Lemma 10, we have that R' is also persistent since R is persistent. But, consider the term H = h2m(Aa 11 A, 11 ··· , A,,., A,,.). Clearly, H is an instance of the second new rule. Now, by the reductions in q, we have H ~R H' = h2m(A,Ah,Ah,····Ai,.,Aj,.,B). But, since H' is an instance of the first new rule in R', we have that R' is not persistent. This contradicts our assumption that R is persistent and the proof is complete. D

As a consequence of Theorem 12 we have that all the classes of Corollary 9 are UN.

4 The Church-Rosser property of the Union

Let Rt be any left-linear system. Let R2 be any system such that every function symbol appearing in the lhs of any rule in R2 does not appear on the rhs of any rule in Rt (we call this lr-disjoint; similarly one can define ll-disjoint, etc). Further, assume that R = Rt U R2 is persistent and satisfies the following finiteness condition called semi-termination.

{F) There is no sequence of R-reductions from any term t containing an infinite number of R2 reduction steps.

Note that (F) immediately implies that R2 is termi­ nating, but termination of R2 is not sufficient for semi­ termination of R as shown below.

Example. Let Rt = {a --+ b}, R2 = {h(x,x) -+ h(a,b)}. Now Rt and R2 are both terminating {in fact, simply terminating, i.e., their termination can be estab­ lished by simplification orderings; see [Dershowitz, 1987] for a definition), but R has the following cyclic deriva­ tion: h(a,b) -+R h(b,b)--+ h(a,b). The example can be · easily modified so that R is not even quasiterminating. Note that all conditions except (F) are satisfied.

We now prove that R is confluent and then give suf­ ficient conditions that ensure J>ersistence and finiteness · of R. Observe that Toyama's lToyama, 1987] technique cannot be used since it depends on the non-increasing property of ranks w.r.t. reductions, which does not hold for us. We need the following lemmas for the proof of confluence.

Lemma 13 For all A,B,C such that A ~R1 B and A ~ R C, there exists D, E such that C ~ R 1 D and B~RD.

Proof {sketch): An easy argument using the confluence of Rt shows that it issufficient to prove the following: for all A, B, C such that A ~ R 1 B and A --+ R 2 C, there exists D such that C ~ R, D and B ~ R D (actually we show something stronger, viz., B ~R1 · ~R2 D). 0

We classify the set of function symbols that appear in R into linear and nonlinear as follows: if a function symbol f appears in the lhs of any rule in R2, then f is nonlinear and linear otherwise. For the next lemma, we need the following definition of the norm of a term.

Definition 14 ([Klop, 1980]) The nonlinear height of a term t (notation ltln) is the maximum number of non­ linear symbols on any path from the root of t to a leaf. The norm oft, denoted II t II = max{luln I t ~ R u }.

Lemma 15 {1} II t II is finite for every t. (2} t ~ u implies II t II ~ II u II· (9} If u is a subterm oft, then II u II ~ II t II· In particular, if root(t) is nonlinear and u is a proper subterm, then II (llu) <II (lit).

Proof: Part (1) Follows from the lr-disjoint and finite­ ness (F) conditions. Part (2) follows from the definition of norm and transitivity of ~ . Part (3) is straightfor­ ward. 0

Lemma 16 If A -+R2 B, A ~R1 C' and C' -+R2 C, then there is aD such that B ~R D and C ~RD.

Proof (sketch}: By induction on the norm. By Lemma 13 we have D' and E such that C' ~ R, D', D' ~ R 2 E and B !t R, E. Also, all the reduction steps from C' to D' are covered by the steps from D' to E. We consider three cases: ( i) the reduction step Rs from C' to C is independent of all the steps from D' to E, ( ii) Rs is covered by a step from D' toE, and (iii) Rs covers some (possibly all) of the reductions steps from D' to E. Case (i) is easy. For cases (ii) and (iii) we use persistence and the induction hypothesis to find the desired term D. 0

We now define the nonlinear derivation height (nota­ tion DHn) of a term.

Definition 17 DHn(t) = max{n I 3u,t ~R u with n R2-reductions }.

Lemma 18 {1} DHn(t) is finite for every t. {2} lft-+ R u, then DHn(t) ~ DHn(u). lft -+R2 u, then DHn(t) > DHn(u).

Proof: Use the definition of DHn, transitivity of ~ , and the lr-disjoint and finiteness (F) conditions. 0

Theorem 19 If R1 is left-linear, R = R1 U R2 is lr-disjoint, persistent and semi-terminating, then R is Church-Rosser.

Proof: We prove that CR(A) by induction on DHn(A). The base case is DHn(A) = 0. In this case, the only derivations possible from A consist solely of R1reductions. Since R is persistent so is R1 and since ev­ ery left-linear persistent system is confluent [O'Donnell, 1977; Rosen, 1973; Huet, 1980], the claim holds for the base case. Assume CR(A) for DHn(A) < m (m > 0). We show the following claim:

Claim. A -+ R2 B, A ~ R 1 C', and C' ~ R2 C implies there is aD such that B ~R D and C ~R D for the case DHn(A) ~ m.

Proof of claim: If there are zero reductions from C' to C, then we use Lemma 13 to get the desired term D. Otherwise, let C' -+ R 2 C" be the first R2-reduction step. By Lemma 16 we have aD' such that B ~ D' and C" !t D'. Now, DHn(C") < DHn(C') ~ DHn(A) by Lemma 18, therefore by the induction hypothesis for the theorem, i.e., CR(C"), we have aD such that D' ~ D andC~ D. o Induction Step: We now prove CR(A) when DHn(A) = m. So suppose that A ~ R B and A ~ R C. If all the reductions in either A ~ R B or A ~ R C are R1reductions, then we are done by Lemma 13. Otherwise we have the following situation: A ~ R 1 C' -+ R 2 C" ~ C and A ~ B' B' -+ B" and B" ~ B --r ' Rt ' R2 --r ' where C' -+ C" and B' -+ B" are the first reductions from R2 on the respective derivations. Now, we have the following derivations. By confluence of R1 (see base case) we have aD' such that B' ~R1 D' and C' ~ R, D'. By Lemma 13 we have a D" such that D' ~ . · ~ D" and C" ~ D" By the above --r R1 --r R2 --r R1 · claim, we have an E such that B" !t R E and D" ~ R E. By Lemma 18, DHn(B") < DHn(B') ~ DHn(A) and DHn(C") < DHn(C') ~ DHn(A). Therefore, by the induction hypothesis of the theorem, i.e., CR(B") and CR(C"), we have aD such that B ~R D and C ~R D and the proof is complete. 0

Remarks. The above result can be generalized in sev­ eral different ways, we 01nit proofs of the generalizations for lack of space. First, the definition of nonlinear sym­ bols can be narrowed to exactly the symbols in lhs's of nonlinear rules of R2. Second, we can drop the finiteness requirement and prove CR( A) for only those terms A for which DHn(A) and II A II are both finite. Third, we do not really need full persistence of R, a slightly weaker form is sufficient. This is important because it permits some kinds of harmless root and nonroot overlaps in R. Finally, note that this proof shows some similarities to Klop's proof. However, as noted earlier Klop's proof cannot be used since it uses postponement of nonlinear reductions, which does not hold for us and also persis­ tence is immediate there.

We now give sufficient conditions that ensure persis­ tence and semitermination of the union. First, we note that nonoverlapping and semitermination imply persis­ tence.

Lemma 20 If the lr-disjoint union R of a left-linear system R1 and any system R2 is nonoverlapping and semi-terminating, then R is persistent.

Proof: A left-linear rule can have only /-nonoverlap with another (not necessarily left-linear) rule. Therefore, the 0-nonoverlaps of R are exactly those of R2. We show that the satisfiability of any constraint contradicts selni­ termination of R. Since the 0-nonoverlaps are between rules of R2, each constraint is of the form (z, C[z, ... , z]) for a nonempty context C not containing z. Further, C consists of function symbols appearing in lhs's of R2. Lett be any solution of a constraint. Then, p: cr(z) = t ~ R C[t, . .. , t]. All the reductions in p cannot be from R1 since lhs's of rules from R2 do not share any function symbols with rhs's of rules from R1. Hence, there must be at least one R2 reduction in p. But then we can construct a sequence containing infinitely many R2 steps from t, contradicting the selni-termination of R. 0

Theorem 21 The following conditions are sufficient for the persistence and semi-termination of a nonoverlap­ ping system R. R1 is linear (i.e., left-linear & right­ linear}, and ( 1} No function symbol that appears in the lhs of any rule in R2 appears in the rhs of any rule, or (2} All R2 rules are height decreasing, i.e. ht(l) > ht(r) for alll ~ r E R2, or (9} All R2 rules are nonlinear-height decreasing, i.e, llln > lrln for every rule l ~ r E R2.

5 Confluence of a Single Rule

We give an example to show that a single nonoverlap­ ping rule need not be confluent nor persistent. Con­ sider the nonoverlapping rule, f ( x, f ( z, y, g( z)), x) ~ g(f(a,f(a,a,g(a)),a)) and let T be the term f(a,f(a,a,g(a)),a). Clearly, T ~ g(T). Now consider the term U = f(b,f(T,f(a,a,g(a)),g(T)),b). Clearly, U 4 g(T) and U~ f(b,f(g(T),f(a,a,g(a)),g(T)),b) ~ f(b,g(T),b). Now it is easily seen that f(b,g(T),b) and g(T) do not have a common reduct, since the rule can never be applied to g(T) at the root level. For the same reason the rule cannot be applied at the root level to f(b,g(T),b) also since the inner term g(T) can never be reduced to a term of the form /( ... ). The smallest, previously known to us, non-confluent nonover­ lapping rewrite systems have three rules [Huet, 1980; Klop, 1980]. However, we have the following result:

Theorem 22 Every single persistent rule is confluent.

6 Conclusions

In this paper we have studied two fundamental concepts, uniqueness of normal forms and confluence, for nonlinear systems in the absence of termination. This is a difficult topic with only a few results so far. Through a novel ap­ proach, we have shown that every persistent system has unique normal forms. This result is tight and a substan­ tial generalization of previous work. In the process we derived a necessary and sufficient condition for persis­ tence and gave several new classes of persistent systems. We also proved the confluence of the union of a nonlin­ ear system with a left-linear system under fairly general conditions. Again persistence plays a key role in this proof. There are several promising directions for future work. First, we note that the finiteness requirement can be weakened somewhat although it cannot be dropped completely. The proof of this is likely to be difficult but fruitful since it might lead to new techniques for deal­ ing with unions (or decompositions) rather than disjoint sums. Second, our work here suggests some natural gen­ eralizations to deal with non-persistent systems. Any progress along these two lines will obviously be of con­ siderable importance to rewriting and its applications.