JAIST Repository: Unique normal form property of compatible term rewriting systems: a new proof of Chew's theorem

JAIST Repository

https://dspace.jaist.ac.jp/

Title

Unique normal form property of compatible term

rewriting systems: a new proof of Chew's theorem

Author(s)

Mano, Ken; Ogawa, Mizuhito

Citation

Theoretical Computer Science, 258(1-2): 169-208

Issue Date

2001-05-06

Type

Journal Article

Text version

author

URL

http://hdl.handle.net/10119/5033

Rights

NOTICE: This is the author’s version of a work

accepted for publication by Elsevier. Changes

resulting from the publishing process, including

peer review, editing, corrections, structural

formatting and other quality control mechanisms,

may not be reflected in this document. Changes

may have been made to this work since it was

submitted for publication. A definitive version

was subsequently published in Ken Mano, Mizuhito

Ogawa, Theoretical Computer Science, 258(1-2),

2001, 169-208,

http://dx.doi.org/10.1016/S0304-3975(99)00340-0

rewriting systems

{ A new proof of Chew's theorem {

Ken Mano a

, Mizuhito Ogawa b

a

NTTCommunication ScienceLaboratories, 2 Hikari-daiSeika-cho Soraku-gun Kyoto619-0237 Japan

b

NTTCommunication ScienceLaboratories, 3-1Morinosato-Wakamiya Atsugi-shiKanagawa243-0198 Japan

Abstract

We present a new and complete pro of of Chew's theorem, which states that a compatible termrewriting system hasa unique normalform prop erty,i.e., a$

3 b impliesab foranynormal formsa;b.

1 Introduction

A term rewriting system (TRS) is a set of directed equations. As a compu-tation/inference mechanism of an equational specication/logic, the natural question iswhether itscomputation/inference terminates, and the next ques-tion is whether itsresult is unique.

The unique normal form property (UN), i.e., a $ 3

b implies a  b for any normal formsa;b, guarantees that the result is unique. If a TRS is terminat-ing, UN can b e tested by using the critical pair lemma [13]. However,UN is undecidablewithout termination[14,10].

Afrequentlyused conceptinprovingUNistheChurch-Rosserproperty(CR), which says that any two convertible terms t, s are joinable, i.e., t !

3 ;

3 s. CRobviouslyimpliesUN.WhenaTRSdo esnotterminate,mostoftheknown sucient conditions forCR require that aTRS b e:

{ non-overlapping (i.e., ithas nocriticalpairs) oritsextensions, and { left-linear.

the non-overlappingrestriction [30,13,31,28,29,25].

Theorem 1.1 [30] A left-linear non-overlapping TRS is CR.

However, the non-overlap assumption alone is not sucient for concluding CR. In [13], the following two counter examplesare presented:

R 1 = 8 > > > > > < > > > > > : d(x;x) ! 0 d(x;f(x)) ! 1 2 ! f(2) 9 > > > > > = > > > > > ; ; R 2 = 8 > > > > > < > > > > > : d(x;x) ! 0 f(x) ! d(x;f(x)) 1 ! f(1) 9 > > > > > = > > > > > ; : In R 1

(from Huet), d(2;2) p ossessestwo distinctnormal forms0and 1. Thus R

1

is not UN, hence R 1

is not CR. In R 2

(from Klop and Barendregt), 1 p ossesses two distinct reduction paths 1 !

3 R 2 0 and 1 ! 3 R 2 f(0). Since the onlypossiblereduction sequence from f(0) is the innitesequence

f(0)! R 2 d(0;f(0))! R 2 d(0;d(0;f(0)))! R 2 d(0;d(0;d(0;f(0))))! R 2 111

0andf(0)cannotb ejoined,henceR 2

isnotCR.Notethatsince0isanormal formand f(0) has nonormal formstheydo not violate UN of R

2 .

Chew'sstatementthatastronglynon-overlappingTRS isUN[5]distinguishes b etweenthem.ATRSiscalledstronglynon-overlappingiftwolinearizationsof itsruleshavenocriticalpairs.Forexample,R

2

isstronglynon-overlapping,so isUN, to o;however,R

1

isnot stronglynon-overlappingbecauseof anoverlap b etween linearizationsof the rst and the second rules.

Asanextension,ChewalsostatedthatUNholds foracompatibleTRS, where a TRS is compatible if, for each pair of rules, some linearizationof apair of rules is almost non-overlapping. However, there is a general feeling of doubt ab out the original pro of in [5]. In fact, there is a \gap" in the pro of of a key lemma(see App endixfor details).

Therehaveb eenseveralattemptsatprovidinganewproofofChew'stheorem, and partial answershaveb een obtained [37,22,32].

De Vrijer rened Chew's methodology in terms of conditional linearization [37]. The conditionallinearizationR

L

of aTRS R isa semi-equational condi-tional TRS (CTRS) such that R

L

and R are the same in convertibility and in the set of normal forms. Accordingly, UN of R is reduced to CR of R

L . Based on this observation, UN of combinatory logic with paral lel-conditional isprovedusing amodel-theoretic argument.

of non-duplicatingTRSs [32].

OgawastatedthatUNholdsforalargerclassthancompatiblesystems,called weaklycompatiblesystems[22];however,hispro ofisinsucientandthe state-mentis still an op en problem (see Note7.9).

This paper presents a new complete proof of UN of compatible TRSs by showing CR of compatible LRCTRSs. We design a peak elimination system (PES) P

R

for a reduction system R, which is a reduction system on proofs t 1 $ 3 t n

in R. If a pro of is reduced to a normal form of P R , it must b e valley-shap ed t 1 ! 3 ; 3 t n , henceR isCR.

Thenweintroduceabinaryrelationonreductionstepscalledanindependence. Intuitively,anindep endence oftworeduction stepsis asucientcondition so that one reduction step do es not go into a subpro of (conditional part) of the other. We also show that the existence of an independence implies the termination of PES P

R

of an (lab eled) abstract reduction system (ARS) R undercertainrestrictions,whereasmostconventionalpro ofsofCRhavedirect weight constructionstoshow the diamond prop erty[27,2].

Our construction of the independence is ?? 1

for non-overlapping LRCTRSs and ??

3

for compatible LRCTRSs. Let  ; b e reduction steps in a pro of A. Intuitively,  ??

1

 means that  and  are separated by p ositions, that is, their positions are parallel toeach other and nointermediatereduction steps covereitherofthem.Anindep endence??

3 isdenedas?? 1 [?? 2 ,and?? 2  means that  and  are separated by a sp ecial term called barrier, that is, there is abarrier b etween and  inaproof.

This pap er is organized as follows. Section 2 provides basic denitions and states the main result. Section 3 intro duces notions of LRCTRS and a con-ditional linearization. Section 4 demonstrates the p eak elimination method of an (lab eled) ARS, and we provide the criteria to show termination of a PES in terms of an independence. Section 5 presentsour basic metho dology of constructing anindep endencefor anLRCTRS.

In Section 6, we construct an indep endence ?? 1

and prove CR of a non-overlapping LRCTRS as an introductory application. In Section 7, we prove CR of a compatible LRCTRS by extending the independence ??

1

with ?? 2 and by supplementing the argument of the overlapping case. As a result we derive UN of a compatibleTRS.

Section8describ esrelatedwork,andSection9concludesthispap er.App endix describ es Chew'soriginal proof and itsgap.

In this section, we intro duce basic notions and then state our main result. The denitions and terminology of abstract reduction systems, terms, and term rewriting systems are taken from [16].

An abstract reduction system (ARS) hD ;!i is a tuple of a domain D and a binary relation ! called a reduction relation on D. The domain D is often omitted. Each element of the reduction relation is called a reduction step, denoted by d ! d

0

. The symmetric closure, the re exive transitive closure, andthere exivetransitivesymmetricclosureof!are writtenas$,!

3 ,and $ 3 , respectively. If there is no d 0 such that d !d 0

, then d is a normal form of !. The set of all normal forms of ! is denoted by NF

! . If d ! 3 d 0 and d 0 2NF !

,thenwesayd has anormal form d 0

,andd 0

iscalledanormalform of d.

An ARS ! has the unique normal form property (UN) if d $ 3 d 0 implies d d 0

for each pair of normal forms d and d 0

, where  is the identity on D . Wesay !has the Church-Rosser property(CR) if d

1 and d 2 havea common reductd 3 (i.e.,d 1 ! 3 d 3 3 d 2 ) for anyd 1 $ 3 d 2 .

An ARS!is stronglynormalizing (or terminating,SN) if thereis noinnite reductionsequenced

1 !d

2

!111,andweaklynormalizing(WN)ifanyd2D has a normalform.

The sequence A : d 1 $ d 2 $ 111 $ d n

is called a proof (of length n01). A proof of length 0 is called an empty proof. We often write A as d

1 $ 3 d n . Each step in aproof is assumed tohavea direction, that is, ! or , evenif it is not sp ecied. A pro of d

i $ d i+1 $ 111 $ d j is a subsequence of a pro of d 1 $ d 2 $ 111 $ d n

if 1  i  j  n. A pro of of the form d 1 d 2 ! d 3 is called apeak.

Let F b e a set of function symbols, and let V b e a countably innite set of variables. Each function symbol f is supp osed to have its arity ar(f). A function symbol c such that ar(c)=0 is called a constant symbol. The set of allterms built fromF and V is denedas follows:

(i) Constant symbols inF and variablesinV are terms. (ii) Ift

1 ;:::;t

n

areterms,and f isa functionsymbolinF suchthatar (f)= n, then f(t

1 ;:::;t

n

) is aterm.

V(t) denotesthe setof variableso ccurringin a termt.

Let 2 b e afresh sp ecial constantsymb ol.A contextC[ ]is a term built from F [2 and V. When C[ ] is a context with n 2s and t

1 ;111;t

n

1 n C[ ] with t

i

for all i=1;:::;n. Fora term t, C t

[ ] is the context obtained by replacing all variablesin t with 2.

N denotes the set of all natural numb ers and N 3

denotes the set of all nite sequences of N.  denotes the null sequence.Forp;p

0 2N 3 ,p;p 0 denotestheir concatenation, and jpj isthe length of p. N

3

enco des positionsin a term.The setof allp ositionsPos(t)inatermt,the subtermt=poccurring atpint,and the head symb olhead(t)2F [V are denedsimultaneouslyas follows:

(i) If t isa constant ora variable, then

Pos(t) = fg; head(t) =t; t= =t: (ii) Ift f(t 1 ;:::;t n ),then

Pos(t) = fg[fiqj1in and q2Pos(t i )g; head(t) =f; t= t; t=ip t i =p:

For terms t, s and p osition p2 Pos(t), t[p s] is the term obtained from t byreplacing the subterm atp with s.

A substitution is a set of the form fx 1 := t 1 ;:::;x n := t n g with distinct variablesx i andtermst i ,andtfx 1 :=t 1 ;:::;x n :=t n

gdenotesatermobtained byreplacing all occurrences of x

i int witht i for alli=1;:::;n. For p ositions p 1 and p 2 , p 1  p 2 if p 1 is a prexof p 2 . We write p 1 < p 2 if p 1  p 2 and p 1 6=p 2 . When neither p 1  p 2 nor p 2 p 1 , p 1 and p 2 are called parallel, denoted by p 1 kp 2 . p 1 ^p 2

denotes the longest common prexof p 1 and p

2 .

A term rewriting system (TRS) is a set R of rewrite rules. A rewrite rule is a pair of terms denoted by l ! r satisfying two conditions: (1) l is not a variable and (2) V(l )  V(r ). We call l and r the left-hand side (LHS) and the right-handside (RHS) of l !r , respectively.

A TRS R denes the reduction relation ! R

onthe set of terms as

! R

= fC[l  ]! R

C[r ] j C[ ]is acontext,  is a substitution,and l !r2Rg:

i i l i ! r i o ccurs at p osition p i in t (i = 1;2). If p 1 k p 2 , then l 1  1 and l 2  2 are called parallel. If l 1 =q  x 2 V and p 2  p 1

;q for some q, then we say that l 1  1 nestsl 2  2 and l 2  2

o ccursinasubstitution partx 1 of l 1  1 .Otherwise,l 1  1 and l 2  2 are overlapping.

When we think of a pair of rewrite rules S 1 : l 1 ! r 1 and S 2 :l 2 ! r 2 , their variablesare appropriately renamedsothat S

1

and S 2

donotshare variables.

For rewrite rules S 1 : l 1 ! r 1 ;S 2 : l 2 ! r 2

, suppose there is a non-variable subterml 2 =psuch thatl 1 and l 2

=pare uniable with the most general unier  .Then,hl 2 [p r 1 ] ;r 2

 iiscalledacritical pairof S 1 and S 2 (obtained byan overlapof S 1 onS 2 atpositionp)unless S 1 and S 2

are thesame rules mo dulo renaming of variablesand p= . A critical pair ht

1 ;t 2 i is trivial if t 1  t 2 . A criticalpair of two rules ina TRS R is called a criticalpair of R.

A TRS R is non-overlapping if it has nocritical pairs. If each critical pair of a TRS R is an overlay, that is, an overlap at the head position , then R is called overlay.

A term t is linear if every variable o ccurs in t at most once. A rewrite rule (a TRS R, respectively) is left-linear if its LHS (the LHS of each rule in R, resp ectively)is linear.

Denition 2.1 Asubstitutioniscalledavariable substitutionifx 2V for any x 2 V. A variable substitution  is called a renaming of variables if  is injective, thatis, x 6x

0

 for anydistinct x;x 0 2V. Denition 2.2 Aterm  t is alinearization of aterm t if 

t is linear and there isavariablesubstitution suchthat



t t.Fora rewriterulel !r , 

l!ris called alinearization of l!r if thereis a variablesubstitution suchthat

{  l isa linearization of l satisfying  l l , and { rr .

Example 2.3 For a rewrite rule f(x;x;y ) ! g(y;x;x), all of the following are its linearizations: f(x

1 ;x 2 ;y) ! g (y;x 1 ;x 1 ), f(x 1 ;x 2 ;y) ! g(y;x 1 ;x 2 ), f(x 1 ;x 2 ;y)!g(y ;x 2 ;x 1 ),and f(x 1 ;x 2 ;y)!g (y;x 2 ;x 2 ). Denition 2.4 [5,36,37] A TRS R is compatible 1

if for any two rules S 1 : l 1 ! r 1 and S 2 : l 2 ! r 2

in R there exist linearizations  S i :  l i ! r i of S i (i=1;2)suchthat  S 1 and  S 2

are almost non-overlapping,thatis,anycritical pair of  S 1 and  S 2 isa trivial overlay. 1

De Vrijer's terminology [36] is used here. The corresp onding notion in Chew's originalpap er is \stronglynon-overlapping andcompatible".

CL=fSxyz!xz(yz);Kxy !x;Ix!xg

can b e regarded as a TRS by letting the symbols S, K, and I be constants and by introducing a new binary function symbol expressing the function application (e.g.,Ap in[16]). ATRS CL-pc,whichisthe unionof CLand the parallel-conditionalrules

fCTxy!x; CFxy!y; Czxx!xg

is compatible since the linearization CTxy ! x of the rst rule and a lin-earization Czx 1 x 2 ! x 1

of the third rule are almost non-overlapping, and CFxy !y and Czx 1 x 2 !x 2

are also almost non-overlapping.

The aim of this pap er isto presentacomplete pro ofof Chew's theorem [5].

Main Theorem A compatible TRS is UN.

3 Left-right separated CTRS and conditional linearization

Thissectionintroducesconditionallinearizationusingaslightlyextended ver-sion of left-right separated conditional term rewriting systems [32]. The idea of conditional linearizationoriginated with de Vrijer[36,37].

3.1 Left-right separated CTRS

Denition 3.1 Aleft-rightseparatedconditionaltermrewritingsystem (LRC-TRS) is aset of conditionalrewrite rules with extravariables

l !r(x 1 =y 1 ;111;x n =y n with V(l) = fx 1 ;:::;x n g and V(r)  fy 1 ;:::;y n

g satisfying the following conditions

2 .

(i) l is a linear non-variableterm, (ii) fx 1 ;:::;x n g\fy 1 ;:::;y n g=;, and (iii) x i 6x j if i6=j. 3 2

In the denition of LRCTRS in [32] there is an additional condition (iv) that restrictsLRCTRSstob e \non-duplicating"(see Note in[32]).

3 y

i y

j

1 1 n n condition part of l ! r (x 1 =y 1 ;111;x n =y n

. The unconditional part of R isthe setof allunconditional parts of itsrewrite rules.

Forconvenience,

(i) a condition part is oftenabbreviated toQ;Q 0

;:::,and

(ii) variablesinthe left-handside ofa ruleare indexedbyN inaleft-to-right manner, e.g., f(x 1 ;g (x 2 ;x 3 )),g(h(x 0 1 ;x 0 2 );x 0 3 ),etc. Denition 3.2 Let ^

R be an LRCTRS. The reduction relation r ! ^ R i in ^ R at level i isinductively denedas follows.

r ! ^ R0 = ;; r ! ^ R i+1 = 8 > < > : C[ ^ l ] r ! ^ R i+1 C[^r  ]        C[] isa context, ^ l!r^(x 1 =y 1 ;111;x n =y n 2 ^ R,and x j  r $ 3 ^ R i y j  for i=1;:::;n. 9 > = > ; : Then, r ! ^ R =[ i r ! ^ Ri . The pro of x j  r $ 3 R i y j

 is called the jth subproof of C[ ^ l  ] r ! ^ R i+1 C[^r ] forj =

1;:::;n. For the left-oriented reduction step C[^r ] r ^ R i+1 C[ ^ l ], y j  r $ 3 R i x j  iscalled the (n0j+1)-th subproof for j =1;:::;n.

Subpro ofsofreductionstepsatlevel1arecausedbytakingthere exiveclosure of the empty relation. Thus,

r !

^ R 1

corresponds to a reduction relation of a p ossibly non-left-linear TRS. In the sequel, most denitions are only dened forright-directedreductionsteps,buttheyareeasilyextendedtoleft-directed reduction steps.

Thereductionrelation r !

^ R

isoftentreatedasmorethan arelation;weassume that a reduction step  :C[

^ l  ] r ! ^ R C[^r] due to ^ S : ^ l ! ^r (Q, is implicitly asso ciated with the following information: the rule

^

S, the p osition pos( ) of theredex

^ l inC[

^

l ],andthesubproofs.Areductionstepin ^ Risoftendenoted ast r ! ^ S t 0

if it is due tothe rewrite rule ^ S 2

^ R.

Wesimultaneouslydene the setAddr(A)N 3

of addressesof the reduction steps ina pro of A : t 1 r $ 3 ^ R t n

, and the function r ed A

() mapping an address  2Addr(A) tothe reduction step at inA:

Addr (A) = f1;:::;n01g[fijj1i<n and  2Addr (A ij )g; r ed A (i) = t i r $ ^ R t i+1 for i=1;:::;n01, red A (ij) = r ed A ij ( );

ij A

Thus we say a reduction step  is in A when  = red A

( ) for some  2 Addr (A). The reduction step red

A

(i) is calledthe ithtop reduction step of A for i= 1;:::;n01. A reduction step r ed

A

() with jj=3 is called a subtop reductionstepofA.Topreduction stepsandsubtopreductionsteps arecalled visible. For a pro of A in

^

R , we dene size(A) as the number of elements in Addr (A).

Herewe introduce some notational conventions.

{ Wecall t i

isthe ith term in A:t 1 r $ 3 ^ R t n , and writet i 2A fori =1;:::;n. { The setofallreduction steps inAisdenoted byA itselfwhennoconfusion will arise, so we write, e.g.,  2 A. The set of all top (subtop, visible, re-sp ectively)reductionstepsofAisdenotedbytop(A)(subtop(A),visibl e(A), resp ectively).

{ The setof allreduction steps in  , that is, and all reduction steps in its subpro ofs,is denotedby sub().The setof allreductionsteps inallproper subpro ofs of  isdenoted by sub

0

(),i.e., sub 0

( )=sub( )nfg.

{ When we refer to the position of a reduction step, we adopt `automatic typ e-cast' and omit pos() when no confusion will arise. For instance, we write  <p instead of pos( )< p for a reduction step  and a position p. Moreover, we write A < p (A  p, A 6< p, A 6 p, resp ectively) if < p ( p, 6<p, 6p, resp ectively)for anyreduction step 2top(A).

3.2 Conditional linearization

In this section, we introduce (left-right separated) conditional linearization of a TRS. We show that UN of a TRS is reduced to CR of its conditional linearization.

Denition 3.3 For a rewrite rule S : l ! r , its conditional linearization ^

S : ^

l! ^r(Qisaleft-rightseparatedconditionalrewriterule constructedas follows.

(i) ^

l is a linearization of l such that V( ^ l )\V(l ) = ; and ^ l   l for some variablesubstitution , (ii) r^r , and

(iii) x=xis added tothe condition part Qfor all x2V( ^ l).

Notethatconditional linearizationsofS are unique mo dulorenamingof vari-ables in

^

l . The set of conditional linearizations of all rules in R is called the conditionallinearization of R .

Example 3.4 The LRCTRSR b elow is the conditional linearizationof R . R= 8 > > > > > < > > > > > : d(x;x)!0

f(y)!d(y ;f(y))

1!f(1) 9 > > > > > = > > > > > ; : ^ R = 8 > > > > > < > > > > > : d(x 1 ;x 2 )!0 ( x 1 =x;x 2 =x f(y 1 )!d(y;f(y))( y 1 =y 1!f(1) 9 > > > > > = > > > > > ; :

ThefollowingtheoremisaslightextensionofTheorem18in[32].Infact,b oth theorems (and their pro ofs)are easy reformulationsof Theorem 3.8 in [37].

Theorem 3.5 Let ^

R betheconditionallinearizationofa TRSR . If ^

R isUN, then R is UN.

Proof. We denote the sets of normal forms of R and ^ R by NF R and NF ^ R , resp ectively.AswithTheorem3.8in[37],theproofisdoneusingthefollowing claim.

Claim R is UN if all of these conditions hold:

(i) r $ 3 ^ R  $ 3 R . (ii) ^ R is UN. (iii) NF ^ R NF R .

Proof of Claim. Supp osethere are distinctnormal formst and t 0 suchthat t$ 3 R t 0 . Then t r $ 3 ^ R t 0

from (i). From (iii), t;t 0 2NF ^ R .Thus, tt 0 from(ii). This leads to acontradiction. 2

Nowwe showthat ^

R and R satisfy the ab ove prop erties. Since the reduction relation r ! ^ R 1 of ^

Ratlevel1coincideswith! R

,(i)apparentlyholds.(ii) holds from the assumption of the theorem. We assume for (iii) that a term exists in NF

R

but not in NF ^ R

, and derive a contradiction. Let t b e such a term that is minimal wrt the numb er of function symbols in it. Then t 

^ l  for some substitution  and a rule

^ S :

^

l ! r^ ( Q 2 ^

R that is the conditional linearizationof S :l!r 2R. Thus,thereexistp ositions p

1 and p 2 suchthat l =p 1 l =p 2 xand t=p 1 6t=p 2

for somenon-linear variablexinl;otherwise t would b e a redexof R. t=p 1 ;t=p 2 2NF R and t=p 1 r $ 3 ^ R t=p 2 . Since ^ R is NF, either t=p 1 ort=p 2 is not inNF ^ R

. This contradictsthe minimality of t. 2

Wesay an LRCTRS is non-overlapping (overlay, resp ectively) if its uncondi-tional part isnon-overlapping(overlay, respectively).

Denition 3.6 An LRCTRS ^

R is compatible if for everytwo rules ^ S 1 : ^ l 1 ! ^ r 1 ( x 11 =y 11 ;:::;x 1n 1 =y 1n 1 and ^ S 2 : ^ l 2 ! ^r 2 (x 21 =y 21 ;:::;x 2n 2 =y 2n 2

inR there existterms r 1 ;r 2 suchthat (i) r i fx ij :=y ij jj =1;:::;n i gr^ i (i =1,2), and (ii) the rewrite rules

^ l 1 !r 1 and ^ l 2 ! r 2

are almost non-overlapping.

WithDenition 2.4 and the above denition,it iseasy toprovethe following lemma.

Lemma 3.7 ATRSR iscompatibleiits conditionallinearization ^

Ris com-patible.

Inthe ab ovedenition,rand r 0

are not generallyunique.Forconvenience,we assumethatthechoicefunctionmapsapairhS

1 ;S 2 iofrulesinacompatible LRCTRStoapairhr 1 ;r 2

ithatsatisesthe conditionsofthe ab ovedenition. Wecall (hS

1 ;S

2

i)the standard pairof compatibilityof hS 1

;S 2

i.

In Section 7, we prove CR of compatible LRCTRSs. Since CR implies UN, MainTheorem will b ederived from Theorem 3.5.

3.3 Operations on proofsof an LRCTRS

In this section, we introduce operations on pro ofs that we freely use inlater sections.

Denition 3.8 For proofs A 1

;:::;A n

, a context C[ ] with n 2's, and a p osition p, we dene op erations, namely, concatenation A

1 ;A 2 , embedding C[[A 1 ;:::;A n ]], and restriction A 1

=p as the following. The operator ; is as-sumed to have higher priority than =. We asso ciate a mapping called parent with eachof them.

Forpro ofsA 1 :t 1 r $ 3 ^ R t n and A 2 :t n r $ 3 ^ R t n+m ,the concatenationA 1 ;A 2 ofA 1 andA 2 istheprooft 1 r $ 3 ^ R t n r $ 3 ^ R t n+m .Theparentofr ed A 1 ;A 2 (i )isr ed A 1 (i) if i<n, otherwise red A2 (fi+10ng).

For pro ofs A i : t i r $ 3 ^ R t 0 i (i = 1;:::;n), the embedding C[[A 1 ;:::;A n ]] of the pro ofs A 1 ;:::;A n

into C[ ] is the concatenation CA 1 ;111;CA n , where CA i =C[t 0 1 ;:::;t 0 i01 ;t i ;t i+1 ;:::;t n ] r $ 3 ^ R C[t 0 1 ;:::;t 0 i01 ;t 0 i ;t i+1 ;:::;t n ];

and the kth top reduction step of CA i

and that of A i

are the same ex-cept for the context. Wecall CA

i

the A i

-segmentof the embedding. Supp ose that red C[[A 1 ;:::;An]] (m i

) is the rst top reduction step of the A i -segment. If r ed C[[A 1 ;:::;A n ]] (fm i +k g)isalsointheA i

-segment,thenitsparentisred A

i (k) (i=1;:::;n).

Let A 1 :t 1 r $ ^ R t n

be a pro of and let p be a p osition such that A 1 6<p. Note that p 2Pos(t i ) for i = 1;:::;n since A 1 6<p. The restriction A 1 =p of A 1 to pist 1 =p r $ 3 ^ R t n =p. Here, r ed A1

(i)is theparentof t i =p r $ ^ R t i+1

=pandtheyare thesameexceptforthe contextifpos(r ed

A 1 (i))p.Otherwise,t i =pt i+1 =p, i.e., the `step' isempty.If red

A 1

(i)is the parentof red A 1 =p (j),then red A 1 (i) isthe parentof r ed A1=p (j)(i=1;:::;n01).

If a proof A o ccurs more than once in concatenations or embeddings, we as-sume that each o ccurrence is an isomorphic copy of A and we distinguish b etweenthem. Thus,theparentmapping is injective.Forsimplicity,we iden-tify a reduction step with its parentin the sequel.

Now,we introduce an op eration called attening that attens the top reduc-tion steps, which will b e extensively used in Section 6 and Section 7. This op eration decreases the maximallevel of apro of by1.

Denition 3.9 For a rule ^ S : ^ l ! ^r ( x 1 = y 1 ;:::;x n = y n and a right-oriented reduction step  : C[C

^ l [x 1  ;:::;x n  ]] r ! ^ S C[C ^ r [y j 1  ;:::;y j m  ]] with subpro ofs AS i :x i  r $ 3 ^ R y i

 (i=1;:::;n), the attening of , denoted by  [

, is anembedding of subproofsinto the substitutionparts of the LHS followed bythe reduction step b elow:

C[[C ^ l [[AS 1 ;:::;AS n ]]]];C[C ^ l [y 1  ;:::;y n ]]! ^ R C[C ^ r [y j1  ;:::;y jm ]]; where ^

S is applied in the last step whose subpro ofs are trivial. In a similar way, we dene the attening of a left-oriented reduction step, that is, a re-duction step with trivial subpro ofs followed by an embedding of subpro ofs. The attening of a proof A, denoted by A

[

, is obtained by replacing all top reduction steps of A with their attenings.

Each right-oriented (left-oriented, respectively) reduction step  2 top(A) is identiedwith thelast (rst, resp ectively)reductionstep of 

[ inA

[

.Forany reduction step in any subpro of of  2 top(A), the identication is dened according to the reduction step of the emb edding. Accordingly, the position of  2subtop(A) isdened asthe p osition of  in A

[ .

We dene [ A

to map each term t i 2 A : t 1 r $ 3 ^ R t n to an occurrence of the same term t i in A [

. The rst and last terms t 1 ;t n are mapped by [ A to the rst andlast terms inA

[

,and thejthtermt j

ismapp edtothe term b etween the attenings of the j 01th and jth reduction steps forj =2;:::;n01.

Example 3.10 Let ^

Rbethesame astheoneinExample3.4.Forareduction step  : d(d(1;f(1));1)

r !

^ R

0 with subpro ofs d(1;f(1)) ^ R f(1) and 1 ! ^ R f(1), its attening is  [ :d(d(1;f(1));1) ^ R d(f(1);1)! ^ R d(f(1);f(1)) ! ^ R 0, as shown in Fig. 1. The dash-arrows indicate identication of reduction

f(1) 1 0 d(f(1);f(1)) d(d(1;f(1));1) d(f(1);1) 0 d(d(1;f(1));1) Fig.1.Flattening steps.

The nextlemmafollowsfromthe denitionof atteningandthe factthatthe left-handside of eachrewrite rule isnot avariable.

Lemma 3.11 Suppose2top(A) and 2sub()\subtop(A).Then, <.

4 Abstract p eak elimination

In this section we introduce a variant of ARS called LARS, which is an ab-stractionofconditionalrewriting.Wedemonstrateap eakeliminationmetho d and presenta sucientcondition forCR of a LARS.

4.1 Labeled ARS and Peak elimination system

Denition 4.1 A (set-)Labeled ARS (LARS) is a triple R r

= hD ;H ;!i of a domain D , a setH of tags, and a relation !: D22

H

2D called a labeled reduction relation. Each element of a lab eled reduction relation is called a labeledreduction step,denoted byd

H !d 0 (d;d 0 2D,H H), and H iscalled the labelof d H !d 0

.Wesupp osethat eachlabelcontainsaspecial tagroot(H) called the rootof H.

Notethat alab el is non-empty since ithas atleast its ro ot.

Example 4.2 An LRCTRS ^ R induces an LARS ^ R r

as the following: for every reduction step  : t

r ! ^ R t 0 , ^ R r has  0 : t H ! t 0

, where H =sub() and r oot(H)=. That is, a reduction step in

^ R correspondsto a tag of ^ R r .

Once we forget the lab el, an LARS is a conventional ARS, so the notions relatedtopro ofsof LARSsaredenedinthesamewayasARSs.Forexample, if d i H i ! d i+1 or d i H i d i+1

for i = 1;:::;n01, then the sequence A : d 1 H1 $ d 2 H 2 $111 Hn01 $ d n iscalled a proof inR r . A subsequence d i01 H i01 d i H i !d i+1 is called apeak.

d . ..         d 0 d n d 1 d H H 0 H 1 H n01 

Fig. 2.Peakrewrite rule

For any proof A : d 1 H 1 $ d 2 H 2 $ 111 Hn01 $ d n

, we assume for convenience that H

i

and H j

are disjointfor any i 6=j, and dene the labelof A asthe disjoint union H

1

[111[H n01

, denoted by l abel (A).

Denition 4.3 Apeak elimination rule of anLARS R r

is atriple hA;J;A 0

i that satises the following prop erties.

(i) A is apeak,sayd H d 00 H 0 !d 0 . (ii) A 0 is apro of d 1 H1 $111 H n01 $ d n suchthat d 1 d and d n d 0 . (iii) J is a mapping, called ancestor mapping from l abel (A

0

) to l abel (A). If J(h

0

)=h, then h isthe ancestor of h 0

, and h 0

is adescendantof h.

A peak elimination rule is denoted as A J 7! A

0

(J is often omitted), and A and A

0

are called the left-hand side (LHS) and the right-hand side (RHS) of the rule, respectively. We also call A

0

a replacement sequence of A. Fig. 2 illustrates ap eakelimination ruleand eachdash-arrowgoesfromanancestor toits descendants. LetB :d 1 H 1 $111 H n01 $ d n

beapro ofwithapeakA:d i01 H i01 d i H i !d i+1 andlet P :A J 7!A 0

b eap eakeliminationrule.Supp osethatB 0

isobtainedfromB by replacing the peakA with A

0 . ThenB J 0 7!B 0

is called apeak elimination step, wheretheancestormappingJ

0

coincideswithJonthelabelofthereplacement sequenceandJ

0

isthe identitymappingonH 1 [111[H i02 [H i+1 [111[H n01 .

Denition 4.4 Supp ose that P R

r is a set of p eak elimination rules of R r

, and foranyp eakA thereisP 2P

R

r such thatA isthe LHSofP. ThenP R

r is called a peak elimination system (PES) of R

r

. A peak elimination step of P

R

r is a p eak elimination step of arule in P R r. Denition 4.5 If A i 7! A i+1

is a p eak elimination step in a PES P R

r for i = 1;2;:::, then the sequence A

1 7! A

2

7! 111 is called a peak elimination sequence. The ancestor mapping of a nite peak elimination sequence A

j J

j 7!

111 J 7! A k (k j)isJ j 111J k 01 .Ifh 0 2l abel (A k )andJ j 111J k01 (h 0 )=h, then h is the ancestor of h

0

, and h 0

is a descendantof h.

As a sp ecial case, a tag h is the ancestor and the descendant of h itselfwith resp ect toan emptyp eak eliminationsequence.

APESP R

r canb e regardedasanARSwith thesetofallpro ofsinR r

asthe domain.SinceaPEScanreplaceanypeakbydenition,apro ofAisanormal form of aP

R

r i A is `valley-shaped', that is,of the formd 1 H 1 !111 Hi01 ! d i H i 111 Hn01 d n

.Thus, the nextlemma follows.

Lemma 4.6 If a PESof an LARS R r

is WN, then R r

isCR.

4.2 Termination of PES by independence

Wepresenta sucientcondition for SNof a PES(hence CRof anLARS) in terms of acertain binary relation ontags, calledindependence.

InSection6andSection7,weintro ducePESsofnon-overlappingand compat-ible LRCTRSs, whose rules are classiedinto three categories: parallel, nest, and critical. The former two cases are injective, i.e., the ancestormapping is injective, and simple, i.e., one step divergence closes with at most one step valley.Thediculties areinthelastcase;some reductionstepsmaybe multi-pliedbyacriticalpeakelimination.Theindependenceisasucientcondition sothat one reduction step does not gointoasubpro of (i.e., conditional part) of the other. Thus, it guarantees that the multiplication of reduction steps do es not createunexpectedp eaks.

In this section, we present this idea in an axiomatic way and show how to construct the well-founded weight on pro ofs that decreases at each step of the PES if the indep endence exists.Therefore, SN of aPES (hence CRof an LARS)isreduced tothe constructionof the independence, whichis the main topic inSection 6and Section 7. We denotefu2Sju62S

0

g bySnS 0

.

Denition 4.7 Supp ose a binary relation ?? is dened on l abel (A) for any pro ofA inanLARSR

r

.Then??iscalledanindependenceforaPESP R

r of R

r

if the following prop erties hold for any proof A : d 1 H 1 $111 H n01 $ d n in R r

and tags h;g 2l abel (A).

(i) (dominance)r oot(H i

)6??h if h2H i

. (ii) (adherence)If h??root(H

j

) and g2H j

,then h??g . (iii) (non-incest)Supp osethatA 7!A

0 andthath 0 ;h 00 2l abel (A 0 )aredistinct descendantsof h. Then h 0 ??h 00 .

(iv) (preservation) Supp ose that A 7!A and that h and g in l abel (A) are descendantsof h and g , resp ectively.Then h??g impliesh

0 ??g 0 . Denition 4.8 Let P : A J 7! A 0

b e a p eak elimination rule with A = d H d 00 H 0 ! d 0

. We say P is injective if J is injective. We say P is root-erasing if neitherr oot(H)nor r oot(H

0

)havedescendantsinthe l abel (A 0

).A peak elim-ination step due to an injective (root-erasing, respectively) p eak elimination rule is calledinjective(ro ot-erasing, respectively).

In the rest ofthis section,A 1 J 1 7!A 2 J 2

7!111is ap eak eliminationsequence ina PESP

R

r with an indep endence??.

Denition 4.9 Theoriginofatagh2l abel (A j

)(j =1;2;:::)istheancestor inl abel (A

1

) of h, denoted by orig (h).

Weuse[and]torepresentmultisetsand]forthemultisetunion.Forexample, [a;a;b]][a;b;c] =[a;a;a;b;b;c].

Denition 4.10 We dene the weight for the proofs A i

for i = 1;2;::: and their tags.

(i) The weight w(h)of a tag h is denedas (a) w(h)=l abel (A 1 ) for h2l abel (A 1 ). (b) Let h 2 l abel (A k +1 ) (k = 1;2;:::). Assume that A k J k 7! A k+1 elimi-nates ap eak d H d 00 H 0 !d 0 . If A k J k 7!A k +1 is ro ot-erasing, then w (h)= 8 > > > > > < > > > > > : w (J k

(h))nfor ig(r oot(H))g if J k

(h)2H,

w (J k

(h))nfor ig(r oot(H 0 ))g if J k (h)2H 0 , w (J k (h)) otherwise. Otherwise,w (h)=w (J k (h)). (ii) Then w(A

k )= U h2label(A k ) [w(h)] fork =1;2;::: Let  mul

b e the multiset extension [9] of the prop er subset relation  on nite sets, and let 

mul

b e the re exive closure of  mul . Note that  mul is well-founded. Lemma 4.11 If A k J k 7! A k +1 is injective, then w (A k )  mul w(A k +1 ) for k = 1;2;:::

Proof. Since w(A k

)w (A k +1

), the result follows. 2

Lemma 4.12 Let h k

2 H. Suppose that a root-erasing peak elimination rule is applied to a peak d H d 00 H 0 ! d 0 in A k J k 7!A k +1 . If h k 2H (H 0 , respectively)

A l : . . . . . . g r oot(H) r oot(H 00 )  h k  g k  h l H H 00 A 1 : A k :

Fig.3.Pro of ofLemma 4.12

has a descendant h l in a label H 00 of a reduction step in A l for some l > k, then or ig(r oot(H)) 6= orig (root(H

00 )) (or ig(r oot(H 0 )) 6= orig (root(H 00 )), respectively).

Proof. We assume that or ig(root(H)) = or ig(r oot(H 00 )) = g 1 and derive a contradiction. Letg k 2l abel (A k

) be the ancestorof r oot(H 00

).

Since the p eak eliminationrule of A k

7!A k+1

isro ot-erasing, r oot(H) has no descendant after A k +1 , so g k 6= r oot(H). Thus, g k

and r oot(H) are distinct descendants of g

1

, and g k

?? root(H) due to the property of non-incest and preservation.Sinceh k 2H,g k ??h k

b ecauseofadherence.Hence,r oot(H 00

)?? h

l

according to preservation. However, root(H 00

) 6?? h l

due to the prop erty of dominance. This leads to a contradiction. The case h

k 2 H 0 is similarly proved. 2 Lemma 4.13 If A k J k 7! A k +1 is root-erasing, then w (A k )  mul w (A k+1 ) for k =1;2;::: Proof. Let d H d 00 H 0 ! d 0

b e the eliminated p eak in A k J k 7! A k +1 . Note that H[H 0 isnon-empty.

IfthereplacementsequenceinA k +1

isanemptyproof,thenthe resultis obvi-ous. Lethb eanytag of thereplacementsequence.Supp ose J

k

(h)2H.Then w (h) = w(J

k

(h))nforig (root(H))g, and from Lemma 4.12 orig (root(H)) 2 w (J k (h)). Thus,w (J k (h))w (h).When J k (h)2H 0

,this issimilarly proved. Therefore,w(A k ) mul w(A k +1 ). 2

Foraninjectiveand non-ro ot-erasingp eakelimination,wepreparesimpleness asdened b elow.

Denition 4.14 A pro of of the formd !  d 0  d 00

is called simple, where !



is there exive closureof !. Apeakelimination rule issimple if itsRHS is simple. A peak elimination step resulting from a simple p eak elimination rule is also called simple.

Denition 4.15 A lab eled reduction step  is left-oriented (right-oriented, resp ectively) if  is d H d 0 (d H ! d 0

, respectively) for some d, d 0

, and H. For a pro of A, the height(A)  0 and mass(A)  0 is simultaneously dened as the following.

(i) If A isan empty proof, then height(A)=mass(A)=0. (ii) IfA =A

0

; forsome pro ofA and reduction step , then { height(A) = height(A

0

) +1 and mass(A) = mass(A 0

) if  is left-oriented,and

{ height(A) =height(A 0

) and mass(A)=mass(A 0

)+height(A 0

) if  is right-oriented.

In other words, the mass is the number of tiles as showninFig. 4.

Lemma 4.16 If A k

7!A k +1

issimple, then mass(A)>mass(A 0

).

Theorem 4.17 Suppose every peak elimination rule in a PES P R

r is either root-erasingor simpleandinjective.IfP

R

r has anindependence??,thenP R

r is SN.

Proof. Let<b ethelexicographicextensionof mul and<.Thenhw (A k );mass(A k )i= hw (A k +1 );mass(A k +1

)i for k = 1;2;::: from Lemma 4.11, Lemma 4.13, and Lemma4.16. Therefore,the result follows. 2

5 Basic construction of independence for LRCTRSs

Before constructing the independences of non-overlapping and compatible LRCTRSs, we prepare the metho dology for their simplication. That is, we rstdenethebinaryrelation??onvisiblereductionsteps,andnextextend?? usingthe subpro of closure??

s

check whether?? satisesthe conditionsinDenition4.7, wheremost ofthe conditions are reducedto those in terms of ??.ForLRCTRSs,Denition 4.7 isreformulated inthe mannerinExample 4.2.

4

Denition 5.1 Anindep endence??isabinarysymmetricrelationon reduc-tion steps satisfying the followingconditions.

(i) (dominance) 6?? if  2sub().

(ii) (adherence)If  ?? and 2sub(),then  ?? . (iii) (non-incest) Supp ose that A 7! A

0

and that ; 2 A 0

are distinct de-scendants of .Then  ??.

(iv) (preservation)Supp ose thatA7!A 0 andthat  0 and 0 inA 0 are descen-dantsof  and  in A, resp ectively. Then ?? implies ??.

Theconstructionsoftheindependence inSection6andSection7are context-sensitive, i.e.,  ?? (or  ??

s

) cannotb e decidedwithout mentioningthe pro of A, which contains and . If ?? is invariantunder concatenation, restriction, and emb edding, wesay it is structural. If ?? is also invariant under the subpro of, we sayit islocal.

Section 5.1 shows that dominance is inherited from ?? to ?? s

(Lemma 5.3), and this section gives a sucient condition for ??

s

as local in terms of ?? (Lemma 5.6). The adherence of ??

s

immediately follows from the construc-tion of the subpro of closure. Section 5.2 gives a sucient condition for the preservation of ??

s

in terms of ?? (Lemma 5.10). Proving preservation of in-dep endences is the main technicaldicultyin Section 6and Section 7.

Throughoutthis section,we assume??is asymmetricbinary relationdened inthe reduction steps ina pro of A for any pro ofA in anLRCTRS.

5.1 Subproof closure

Denition 5.2 The subproof closure ?? s

of ?? is inductively dened as the following.

(base) If ??, then ?? s

. (adhere) Supposethat ??

s . (a) If 0 2sub(),then  ?? s  0 . (b) If  0 2sub( ), then 0 ?? s .

(subproof) Supp ose that ; 2sub( )for some 2A. (a) If and  are indistinct subpro ofs of , then ??

s

 in A. (b) If  ; 2B for asubpro of B of ,then ??

s

 in A if ?? s

 in B.

4

Notethat ?? isalso symmetricandthe subproofclosureoperationcommutes with the union, i.e., ??

s [?? 0s =(??[?? 0 ) s .

The next lemmaguarantees that dominance in Denition 5.1 is preservedby the subproofclosure.

Lemma 5.3 If ?? satises dominance, then the subproof closure ?? s

of ?? also satises dominance.

Proof. We assume that the result do es not hold. Supp ose A is a minimal pro of wrt size(A) in which  ??

s

 for some  2 sub(). Also supp ose that  = red A () and  = r ed A ( 0 ) are minimal wrt j j+j 0 j. According to the assumption of the lemma,  ??

s

 is inductively generated using (adhere) or (subpro of). Letus considerthe last step of itsgeneration.

Neither(subpro of)-(a)from 2sub()nor(subpro of)-(b)fromthe minimal-ityof size(A) performs the last step. Suppose that (adhere)-(a)p erforms the last step. The case of (adhere)-(b) is treated symmetrically. Then  ??

s  is derivedfrom?? s  0

such that 2sub( 0

)for some 0

. From 2sub(), ei-ther 0 =,  0 2sub(),or2sub( 0

).However,inanycase acontradiction isderived fromthe minimality of jj+j

0

j using the symmetry of ?? s

. 2

Weidentifyaparentofareductionstep(wrtconcatenation,embedding,and restriction)with .Ifabinaryrelationislo cal,thentherelationiswell-dened under suchanidentication.

Denition 5.4 If??satises

(i) ?? in A i  ?? in A 0

;A;A 00

for any reduction steps ; 2A, and pro ofs A;A

0 ;A

00 ,and

(ii)  ?? in A i  ?? inA=p for anyreduction steps ; 2 A=p, pro of A, and p osition psatises A6<p,

then ?? iscalled structural. If??subsequentlysatises

(iii) ?? inA i ?? inB for any reduction steps  ; in anysubpro of B of any reduction step in anyproof A,

then ?? iscalled local.

The followingtechnical lemmais prepared for provingLemma 5.6.

Lemma 5.5 Let?? s

bethe subproof closureof ??. Assume that

(i) 6?? s

 if 2sub() for any reduction steps ;, and

(ii)  ??  in A implies  ??  in B for any reduction steps  ; in any subproof B of any reduction step in any proof A.

Then  ??  in A implies  ??  in B for any subproof B of a reduction step in a proof A.

Proof. We assume that the result do es not hold. Supp ose A is a minimal pro ofwrt size(A)suchthat ??

s  inA and6?? s  inB.From (ii),?? s  inAisnotderivedby(base).Thus,??

s

inAisinductivelygeneratedusing (adhere)or(subpro of)ofthesubpro ofclosure.Alsosupp osethat=r ed

A () and  =r ed A ( 0 ) are minimal wrt j j+j 0 j.

Supp ose that (subpro of)-(a) performs the last step. Then,  and  are in distinct subproofs of some reduction step in A. Since B is a subpro of of a reduction step inA, 2B. Thus, ??

s

 inB is derivedby (subpro of)-(a), which leads to a contradiction. The last step is not (subpro of)-(b) from the minimality of size(A). Thus, wesupp ose that (adhere)-(a) p erforms the last step. The case of (adhere)-(b) is treated symmetrically. Then  ??

s  0 in A and  2 sub( 0 ) for some  0 . If  0

62 B, B must b e in some subpro of of  0

since  2B. Thus  2B implies  2sub( 0 ), whichviolates ?? s  0 by (i), and  0 2B.Asa result,?? s  0

inB fromthe minimalityof jj+j 0

j.Then, ??

s

 in B, whichleads to acontradiction. 2

The next lemma presentsa sucientcondition for that a subpro of closure is lo cal.

Lemma 5.6 Let?? s

bethe subproof closureof ??. Assume that

(i) ?? satises dominance, (ii) ?? is structural, and

(iii)  ?? in A implies  ?? in B for any reduction step in any subproof B of any reduction step in any proof A.

Then ?? s

islocal.

Proof. From(i),?? s

satises dominanceby Lemma5.3.LetB b easubproof of a reduction step in A. From (ii), it is easy to see that ??

s

is structural. Through(subpro of)-(b),??

s inBimplies?? s inA.From(iii),?? s  inA implies?? s  inB byLemma 5.5. 2

5.2 Simplifying case analysis of preservation

Here we show how to simplify the exhaustive case analysis in the pro of of preservation. When proving the preservation of  ??

s

 such that  and  are not inthe same subproof of a top reduction step, we restrict ourselvesto ?? for ; 2v isible(A).

S A

visibl e(A)2visibl e(A), then ?? is calleda visible relation.

Denition 5.8 For a reduction step  in A,  A

() =  if  2 v isibl e(A); otherwise, 

A

() is the subtopreduction step suchthat  2sub( A

()).

Lemma 5.9 Let ?? s

be the subproof closure of a visible relation??. For any ;; 2visibl e(A), assume that

(i) ?? and  0

2sub() imply ?? 0

, and

(ii) ?? for  and  in distinct subproofsof a top reduction step in A.

Then for any ; 2A not in the same subproof of a top reduction step in A, ?? s  i  A ( ) ?? A ().

Proof. If-partis trivial. We assumethat the only-ifpart do esnot hold. Sup-p ose A is a minimal pro of wrt size(A) in which ??

s  and  A ()6?? A () for some ; not in the same subpro of of a top reduction step in A. Also supp ose that =red

A () and  =red A ( 0 ) are minimal wrt jj+j 0 j. Since ?? is a visible relation and 

A () 6??  A (),  ?? s  cannot b e derived by (base).Then ?? s

 isinductivelygenerated using (adhere) or(subpro of) of the subproofclosure. Consider the last step of itsgeneration.

Neither(subpro of)-(a)from(ii)nor(subpro of)-(b)performsthelaststepsince  and are not inthe same subpro of. Supp osethat the last step is (adhere)-(a). The case of (adhere)-(b) is treated symmetrically. Then  ??

s  0 and  2 sub( 0 ) for some  0

. From the minimality of jj+j 0 j,  A () ??  A ( 0 ). Since2sub( 0 ),either A ()= A ( 0 )or A ()2subtop( 0 ).Ineithercase,  A ( )?? A

() holdsfrom (i), which leadsto a contradiction. 2

Lemma 5.10 Let ?? s

be the subproof closure of a visible relation ??. Let A7!A

0

be a peak elimination rule with proofsA;A 0 in an LRCTRS. Assume that (i) ?? and  0 2sub() imply ?? 0 for ;; 0 2visibl e(A),

(ii)  ??  for visible reduction steps  and  in distinct subproofs of a top reduction step in A,

(iii) for any 2Anvisibl e(A), if has a descendant 0 in A 0 then  A ( ) has a descendant 00 in A 0 with 0 2sub( 00 ), and

(iv) forany ; 2visibl e(A) notinthe samesubproof ofa topreduction step in A, if  and  have descendants 

0 and  0 , respectively, then  ??  implies  0 ?? s  0 . Then,A7!A 0 preserves 1 ?? s  2 forany 1 ; 2

2A notin thesamesubproof of a top reduction step in A.

1 2 reduction step and 

1 ??

s 

2

. Also suppose that  i has a descendant  0 i for i =1;2. By Lemma 5.9,  A ( 1 ) ??  A ( 2

) from (i) and (ii). If  i

is a visible reduction step then let 

00 i =  0 i ; otherwise, let  00 i be a descendant of  A ( i ) suchthat 0 i 2sub( 00 i

)(from (iii))fori=1;2.Then, 00 1 ?? s  00 2

from(iv), and we obtain 0 1 ?? s  0 2

by (adhere) of the subpro of closure. 2

6 The Church-Rosser property of non-overlapping LRCTRS

Inthis section,wedenea PESofa non-overlapping LRCTRS andconstruct its indep endence ??

1

. Therefore, by the result of Section 4, we complete SN of the PES and hence CR of a non-overlapping LRCTRS. For CR of non-overlappingsemi-equationalCTRSswithoutextravariables,see[1]. Through-out this section,

^

R denotes anon-overlapping LRCTRS.

6.1 Peak eliminationof non-overlapping LRCTRS

Lemma 6.1 Let AS i

be the ith subproof of a reduction step with a rule ^ S : ^ l ! ^r ( x 1 = y 1 ;111;x n = y n

for i = 1;:::;n. Suppose that rfx i := y i ji = 1;:::;ng  ^r and rC  r [x j 1 ;:::x jm ]. Then C ^ r [[AS j 1 ;:::;AS jm ]] is a proof of the form r r $ 3 ^ S ^ r . Proof. Let ^rC ^ r [y k 1 ;:::y k m ]. Notethat C  r [ ]C ^ r [ ].Then, y j i x j i fx i := y i ji=1;:::;ng y k i

for i=1;:::;m, and the result follows. 2

Denition 6.2 We dene a PES P ^ R

of ^

R as the following. Let ^ S i : ^ l i ! ^ r i ( x i1 = y i1 ;111;x ini = y ini

b e any rewrite rule in ^ R (i = 1;2), and let A : t 1 r ^ S 1 t 2 r ! ^ S 2 t 3

b e any p eak, where t 1  C[^r 1 ], t 2  C[ ^ l 1 ]  C 0 [ ^ l 2  ], andt 3 C 0 [^r 2  ]. Wedenotet 1 r ^ S 1 t 2 and t 2 r ! ^ S 2 t 3 as 1 and 2 ,respectively. Then, P ^ R

has the p eak elimination rule A J 7!A

0

asfollows. Peak elimination rules are classied into three categories; P

k , P < , and P ] , according to the relativep ositions of the redexes of

1 and 2 . (P k

) [parallel] If the redexes of 1

and 2

are parallel, then A 0 = t 1 r ! ^ S 2 t 0 2 r ^ S1 t 3

isobtainedbyexchangingtheorderof 1

and 2

.Foranyreduction step 2A 0 , J( )= 8 > < > : red A (1) if =r ed A (2), red A (2) if =r ed A (1).

< 2 1 1 b elowthesubstitution partx

2k

 . Alsosupp ose thatC 0 []=p 2 and ^ l 2 =q  x 2k . Then, A 0 = t 1 r ! ^ S 2 t 3

, which is the same as 2

except for the kth

subpro of mo died into t 1 =p;q r ^ S1 x 2k  r $ 3 ^ R y 2k

. For any reduction step 2A 0 , J()= 8 > > > > > < > > > > > : red A (1) if =r ed A 0 (1k1), red A (2kj) if  =red A 0 (1kfj +1g)for some j 2, red A

(2) otherwise, assume =red A

0(1).

The case when 1

'sredexnests 2

's isdealt with symmetrically. (P

]

) [critical] Supp ose that the redexes of 1

and 2

are overlapping. This kindofp eakiscalledcritical.Since

^ Risnon-overlapping,C[]C 0 [],andS 1 andS 2

arethesamemo dulorenamingofvariables.Sincedierentsubproofs yielddierentreducts inLRCTRSs,t

1 and t

3

can still b e dierent. Let AS 1j : y 1j  r $ 3 ^ R x 1j  be the jth subpro of of 1 (j = 1;:::;n 1 ), and let AS 2j 0 : x 2j 0 r $ 3 ^ R y 2j 0  b e the j 0 th subproof of 2 (j 0 = 1;:::;n 2 ). Let ^r i  C ^ r i [y i1 ;:::;y ik ] (i= 1;2). C[[C ^ r 1 [[AS 1j 1 ;:::;AS 1j k ]]]] is of the form t 1 r $ 3 ^ R C[C ^ r 1 [x 1j 1  ;:::;x j k  ]], and C[[C ^ r 2 [[AS 2j 1 ;:::;AS 2j k ]]]] is of the form C[C ^ r 2 [x 2j 1  ;:::;x 2j k  ]] r $ 3 ^ R t 3 byLemma6.1.Moreover,C[C ^ r 1 [x 1j 1  ;:::;x j k ]] C[C ^ r2 [x 2j1  ;:::;x 2j k  ]]. Thus,we dene A 0 as C[[C ^ r 1 [[AS 1j 1 ;:::;AS 1j k ]]]];C[[C ^ r 2 [[AS 2j 1 ;:::;AS 2j k ]]]]:

Forareduction step 2A 0 , if =r ed AS ij (),then J( )=red A (ij). Note 6.3 (i) 1 and 2

havenodescendantswhen P ] isappliedtoacritical p eak 1 ; 2 .

(ii)  may have multiple descendants only when P ] is applied to a critical p eak 1 ; 2 and 2sub 0 ( 1 )[sub 0 ( 2 ).

Weoften refer to the rules inP k

(P <

, P ]

, resp ectively) as simply P k (P < , P ] , resp ectively). Observe that P

k

and P <

are simple and injective while P ]

is ro ot-erasing.

Example 6.4 We illustrate the p eak elimination steps shown above in ex -amples. Let

^

R b e the same as the one in Example 3.4 and let the ith rule from the top b e

^ S i

(i =1;2;3). Supp ose that there are proofs AS 1 :1 r $ 3 ^ R s, AS 2 :t r $ 3 ^ R s, andAS 3 :u r $ 3 ^ R

t forsometermss, t,and u.Inthe following,a line under asubterm(aline overasubterm, resp ectively)indicates the redex of the left-oriented(right-oriented, resp ectively)reduction step in the peak.

d(f(1);d(s;f(s))) d(1;f(t)) d(f(1);f(t)) t s s * * d(1;d(s;f(s))) Fig. 5.RuleP k * t s 0 1 s t d(1;t) d(f(1);t) f(1) 1 s s * * * Fig. 6.RuleP < d(t;f(t)) * * f(t) t d(u;f(u)) s u t * * * * d(s;f(t)) d(s;f(s)) d(t;f(u)) Fig.7.Rule P ] (P k

) Let us consider a p eak d(f(1);f(t)) r ^ S 3 d(1 ;f(t)) r ! ^ S 2 d(1;d(s;f(s))), wherethe right-oriented reduction step has a subpro of AS

2 . Then, itis re-placed with d(f(1);f(t)) r ! ^ S 2 d(f(1);d(s;f(s))) r ^ S 3 d(1;d(s;f(s))) using P k asshownin Fig. 5. (P < ) Consider a p eak d(f(1);t) r ^ S 3 d(1 ;t) r ! ^ S 1

0, where the right-oriented reduction step has the subpro ofs AS

1

and AS 2

. Using P <

, the peak is re-placedwith d(f(1);t) r ! ^ S1 0as shownin Fig.6. (P ]

) Withthedierentsubpro ofsAS 2 andAS 3 , ^ S 2

hasacriticalp eakd(u;f(u)) r ^ S 2 f(t) r ! ^ S 2

d(s;f(s)).Thepeakisreplacedwiththeconcatenationofd(u;f(u)) r $ ^ R d(t;f(u)) r $ ^ R d(t;f(t))and d(t;f(t)) r $ ^ R d(s;f(t)) r $ ^ R d(s;f(s)) usingP ] asshownin Fig.7.

The followinglemma directly follows from the denition of peak elimination rules.

Lemma 6.5 The PES P ^ R

of a non-overlapping LRCTRS ^

R dened above works monotonically downwards wrt the position, that is, if a peak

1 ;

2 is

^ R 1 2 top(A). 6.2 Independence ?? 1 of non-overlapping LRCTRS

Hereweintroduce arelation?? 1

, whichisprovedtobeanindependencefor a PES P ^ R of a non-overlapping LRCTRS ^ R. Intuitively, ?? 1  means that  and  are separated by positions, that is, their p ositions are parallel to each other and no intermediate reduction steps cover either of them. This is rst denedforthetopreductionsteps,thenextendedtothevisiblereductionsteps using attening, and nally extended to all reduction steps by the subpro of closure. Denition 6.6 Let A : t 1 r $ 3 ^ R t n be a pro of in ^ R, and let  i

b e the ith top reduction step. Supp osej 6=k.An openinterval A(

j ; k ) isthe subsequence t j+1 r $ 3 ^ R t k ofA ifj < k ,and otherwiset k +1 r $ 3 ^ R t j .A closedintervalA[ j ; k ] ist j r $ 3 ^ R t k +1 if j < k,and otherwise t k r $ 3 ^ R t j+1 .

Inanop eninterval,insteadofthereductionstep i

,weadmitthetermt i

.They are dened as the following: A(

j ; k )=A( j ;t k )=A(t j+1 ; k )=A(t j+1 ;t k ) if j < k , and otherwise A( j ; k )=A( j ;t k +1 )=A(t j ; k )=A(t j ;t k +1 ).

Denition 6.7 For any pro of A in ^

R and ; 2 top(A),  ?? T 1

 in A if A[;]6^,that is,noreduction steps inA[;] o ccuraboveorequal to ^.

 6?? T 1

 in A for any  2 top(A) since A[ ;] =  and pos( ) = ^ . If the pro of A is clear from the context, \in A" is often omitted. There are some direct consequences of the ab ove denition: (1) ??

T 1 is symmetric, and (2) ?? T 1  implies k.In addition, 6^ if k or k.

Lemma 6.8 Let ;; 2top(A). Suppose that  2A( ; ) and A[;]. Then  ?? T 1 i  ?? T 1 . Proof. If ?? 1

, 6^ .Since  A[;], . Thus,^ =^ , and  ??

1 .

If  ?? 1

, then  k . Since   A[;],   , then  ^ = ^ . Since ^ < A[;], then ?? 1 . 2 Weextend ?? T 1

to visible reduction steps using attening. Note that [ A

() 2 top(A

[

) i 2visibl e(A).

Denition 6.9 For; 2visibl e(A), ?? M 1  inA if[ A ()?? T 1 [ A ()inA [ .

Lemma 6.10 ?? 1

and ?? 1

are structural.

Note 6.11 Bydenition,itiseasytoseethatthePESand?? M 1

satisfythe as-sumptions(i),(ii),(iii)inLemma5.10.Inthesequel,wewillapplyLemma5.10 withoutmentioningthese assumptions.

Denition 6.12 Wedene ?? 1

as the subpro of closure of ?? M 1

.

Example 6.13 For proofs A i : s i r $ 3 ^ R s 0 i

, let us consider an emb edding A : C[[A

1

;:::;A n

]].Let  b e a reductionstep inan A i

-segment ofthe emb edding and  be one in an A

j

-segment such that i 6= j. If b oth  and  are top reduction steps in A, then  ??

1

 since A 6  ^. Otherwise,  ?? 1

 is derivedby (adhere) of the subpro of closure. Therefore, ??

1

 in A.

We show that a non-overlapping LRCTRS is CR by proving that ?? 1

is an indep endence.

Theorem 6.14 The relation ?? 1

is an independence for the PES P ^ R of a non-overlapping LRCTRS ^ R.

To prove the ab ove theorem, we show in the following that ?? 1

satises the four prop ertiesin Denition5.1. The hardest part is(iv) preservation,which will be provedin Section6.3.

Lemma 6.15 ?? 1

satises dominance.

Proof. Let; 2visibl e(A).If 2sub()then[ A ()[ A ()formLemma3.11. Thus,6?? M 1

. Therefore,thedominance of ?? 1

followsfromLemma5.3. 2

Lemma 6.16 ?? 1

is local.

Proof. By Lemma5.6 and Lemma6.10. 2

Lemma 6.17 ?? 1

satises adherence.

Proof. Obvious since ?? 1

satises (adhere) ofthe subpro of closure. 2

Lemma 6.18 ?? 1

satises non-incest.

Proof. By using Note 6.3, it is sucient to consider the descendants of  when P

]

is applied to some critical p eak 1 ; 2 and  2 sub 0 ( 1 )[sub 0 ( 2 ). However, twodistinct descendantsof , 

1 ;

2

reside indierent segmentsof theemb eddinginthereplacementsequenceforthep eak.Therefore,

1 ?? 1  2 . (See Example 6.13.) 2

(a)-(1) (b)-(2) (b)-(3) 2 (b)-(1) (a)-(3) (a)-(2)  1 ; 2  1  2  1  1  1 ; 2  2  1  2  2 1 * * 1 2

Fig. 8.Caseanalysis inLemma6.16

6.3 Preservation of independence ?? 1 Lemma 6.19 ?? 1 satises preservation. Proof. Let 1 and 2

b e reductionsteps ina proofA.Supposethat A7!A 0 , and that  0 i in A 0 is adescendant of i (i=1;2). Let A= A 1 ; 1 ; 2 ;A 2 , where 1 ; 2

isthe eliminated peak.Let B 1

;B 2

b e the replacementsequence.Wep erform acaseanalysis dep endingonwhere

1 and 

2

o ccur in A. The followingcases mustbeconsidered:

(a)-(1)  1 ; 2 2A 1 . (a)-(2)  i 2A i (i=1;2). (a)-(3)  1 ; 2 2sub( 1 ). (b)-(1)  1 2A 1 and  2 2sub( 1 ). (b)-(2)  1 2A 1 and  2 2sub( 2 ). (b)-(3)  i 2sub( i ) (i=1;2).

Fig. 8 shows an analysis of the ab ovecases. The other cases are obtained by exchanging

1 and

2

and/orreversingA.Claim6.20,Claim6.21,Claim6.22, and Claim 6.23 provepreservation.

Claim 6.20 Preservationof ?? 1

holds in cases (a)-(1) to (3).

Proof. In case(a)-(1),preservationfollowssince ?? 1

is lo calby Lemma6.16. In case (a)-(2), preservation holds since P

^ R

works monotonically downwards b ecause of Lemma 6.5. In case (a)-(3),if 

1

and  2

are in the same subpro of and  0 1 and  0 2

are in the same copy of that subproof, preservation again followssince??

1

islo calbyLemma6.16.Otherwise, 0 1 and 0 2 are indierent segments of the embedding, so

0 1 ?? 1  0 2 . 2 Claim 6.21 Preservationof ?? 1

holds in cases (b)-(1) to (3) when P k

is ap-plied.

k i 30i (i= 1;2). In case (b)-(1), preservation is obvious since B

1 k B

2

. In case (b)-(2), preservationisobvioussince the descendantof

1

simply disappearsfrom A 0 ( 0 1 ; 0 2 ).In case (b)-(3),  0 1 ?? 1  0 2 inA 0 sinceB 1 ?? T 1 B 2 in A 0 . 2 Claim 6.22 Preservation of ?? 1

holds in cases (b)-(1) to (3) when P <

is applied.

Proof. Without loss of generality, we can assume that  1 ; 2 2 v isibl e(A) and  1 ?? M 1  2 byLemma 5.10. Supp ose 2 nests 1 . Then B 1 is empty and B 2 is 2 with 1 prexed to the kth subpro of for some k. Let AS

i

be the ith subpro of of 2

for i = 1;:::;n. Then,the k thsubpro of of B

2 is

1 =p;AS

k

for ap ositionp.Thedescendant 0 1 of

1

is asubtop reduction step inA 0 and pos( 1 )=pos( 0 1 ). The case  2 = 1

from Lemma 3.11 and Lemma6.8 is sucient for case (b)-(1). Then,  1 ?? M 1  2 implies  0 1 ?? M 1  0 2 since  k [ B 2 ( 0 2

) for any reduction step  inan AS i -segmentin B [ 2 (i=1;:::;k01). In case (b)-(2),if  0 2 isin AS i

-segmentsuch thati6=k, thenthe preservation is obvioussince 0 1 k 0 2 . If  0 2 is inthe AS k

-segment, the preservation follows frompos( 1 )=pos( 0 1 ).

Let us consider (b)-(3). We borrow notations from Denition 6.2, so 2 = C 2 [ ^ l 2 ] r ! ^ S 2 C 2 [^r 2  ]. If  2 = 2 , then  1 6?? 1  2 . Supp ose  2 2 AS j . If j 6=k, then  0 1 ?? 1  0 2 in A 0 . Ifj =k, then  1 ?? M 1  2 inA, ,  1 ?? T 1  2 inA [ (by denition), ,  1 ?? T 1  2 in [ 1 ;C 2 [[C ^ l2 [[AS 1 ;:::;AS n 1 ]]]], ,  1 ?? T 1  2 in [ 1 =p;AS k (since?? T 1 is structural); ,  0 1 ?? M 1  0 2 in 1 =p;AS k , )  0 1 ?? 1  0 2 inA 0 (by denition).

In the step from the third line to the fourth line, we used the fact that [ 1 =p;AS k = [ 1 ;C 2 [[C ^ l2 [[AS 1 ;:::;AS n 1 ]]]]=p.

Next supp osethat 1 nests 2 .The case  2 = 1

fromLemma6.8 is sucient forcases (b)-(1)and (2),so preservationis obvious.Incase (b)-(3),the result isprovedinthe same way aswhen

2

nests 1

1 ] plied. Proof. When P ] is applied, B i

consists of multiple copies of subpro ofs of i (i=1;2).Web orrownotationsin(P ] )ofDenition6.2,soB 1 =C[[C ^ r 1 [[AS 1j 1 ;:::;AS 1j k ]]]] andB 2 =C[[C ^ r2 [[AS 2j1 ;:::;AS 2j k

]]]].Withoutlossofgenerality,wecanassume that  1 ; 2 2v isible(A),and  1 ?? M 1  2 by Lemma5.10. Thecaseof 2 = 1

fromLemma3.11andLemma6.8issucientforcases (b)-(1) and (2). Thus, preservation follows since P

^ R

works monotonically down-wardsaccording to Lemma6.5.

Incase(b)-(3),supposethat  0 1 isinanAS 1j n -segmentand 0 2 isinanAS 2j m -segment. Ifn 6=m, then  0 1 ?? 1  0 2 . Otherwise,  1 ?? M 1  2 in A, ,  1 ?? T 1  2 in A [ (bydenition), ,  1 ?? T 1  2 in C[[C ^ l 1 [[AS 11 ;:::;AS 1n1 ]]]];C[[C ^ l 2 [[AS 21 ;:::;AS 2n2 ]]]], ,  1 ?? T 1  2 in AS 1jn ;AS 2jn (since ?? T 1 is structural), ,  0 1 ?? T 1  0 2 in B 1 ;B 2 (since ?? T 1 is structural), ,  0 1 ?? T 1  0 2 in A 0 ,

WeusedthefactthatAS 1jn ;AS 2jn isarestrictionofC[[C ^ l 1 [[AS 11 ;:::;AS 1n1 ]]]]; C[[C ^ l2 [[AS 21 ;:::;AS 2n2

]]]]inthe stepfromthethirdline tothe fourthline, and the fact that it is also a restriction of B

1 ;B

2

in the step from the fourth line tothe fthline. 2

Proof of Theorem 6.14 By Lemma 6.15, Lemma 6.17, Lemma 6.18, and Lemma6.19. 2

Theorem 6.24 A non-overlapping LRCTRSis CR.

Proof. By Lemma4.6, Theorem 4.17, and Theorem 6.14. 2

7 The Church-Rosser property of compatible LRCTRS

We now extend the results in the previous section to compatible LRCTRSs bysupplementingthe argumentof theoverlappingcase. Asaconsequence, we derive CRof a compatibleLRCTRS, and hence UN of a compatibleTRS. In this section,

^

* g(t;a;a) g(s 1 ;a;a) g (s 1 ;s 2 ;a) g(s 1 ;s 2 ;s 2 ) f(g(t;a;a);a) g (t;a;a) u a s 2 u * * * s 1 * * * Fig.9.Rule P ]

7.1 Peak eliminationof compatible LRCTRS

Denition 7.1 The denition of a PES P ^ R

of a compatible LRCTRS ^ R is obtainedbyreplacingthedescriptionofP

]

inDenition6.2withthefollowing.

(P ]

) [critical]Supp oseredexesof 1

and 2

areoverlapping.Thiskindofpeak iscalledcritical.Since

^ Riscompatible,C[]C 0 [].LetAS 1j :y 1j  r $ 3 ^ R x 1j  b e the jth subpro of of 1 (j = 1;:::;n 1 ), and let AS 2j 0 : x 2j 0 r $ 3 ^ R y 2j 0 b e the j 0 th subpro of of 2 (j 0 = 1;:::;n 2 ). Let hr 1 ;r 2 i b e the standard pair of compatibility of hS 1 ;S 2 i. Let r 1  C ^ r 1 [x 1j 1 ;:::;x 1j k ] and let r 2  C ^ r2 [x 2j 0 1 ;:::;x 2j 0 k 0 ].Notethat r 1   r 2

 asa result of compatibility.Then

A 0 =C[[C ^ r 1 [[AS 1j 1 ;:::;AS 1j k ]]]];C[[C ^ r 2 [[AS 2j 0 1 ;:::;AS 2j 0 k 0 ]]]]:

Forthe reduction step  2A 0 , if =r ed ASij ( ), then J()=r ed A (ij).

Observe that the P ]

is root-erasing. Lemma 6.5 also holds for a compatible case.

Lemma 7.2 The PES P ^ R

of a compatible LRCTRS ^

R dened above works monotonical ly downwards wrt the position.

Example 7.3 Let ^

R bethe followingcompatibleLRCTRS:

^ R = 8 > < > : ^ S 1 : f(x 1 ;a)!y 1 (x 1 =y 1 ; ^ S 2 : f(g(x 0 1 ;a;a);x 0 2 )!g(y 0 1 ;y 0 2 ;y 0 2 ) (x 0 1 =y 0 1 ;x 0 2 =y 0 2 9 > = > ; :

The standard pair of compatibility of h ^ S 1 ; ^ S 2 i is hx 1 ;g(x 0 1 ;x 0 2 ;x 0 2

)i. Supp ose that u r $ 3 ^ R g(t;a;a), a r $ 3 ^ R s 2 , and t r $ 3 ^ R s 1

. Then, there is a critical peak u r ^ S1 f(g (t;a;a);a) r ! ^ S2 g(s 1 ;s 2 ;s 2 ). Using P ]

, the p eak is replaced with

u r $ 3 ^ R g(t;a;a) r $ 3 ^ R g(s 1 ;a;a) r $ 3 ^ R g(s 1 ;s 2 ;a) r $ 3 ^ R g (s 1 ;s 2 ;s 2 ) as shown in Fig. 9.

1

not work for compatible systems. In the above example, let us consider the reduction steps  1 in u r $ 3 ^ R g(t;a;a) corresponding to x 1 = y 1 , and  2 in a r $ 3 ^ R s 2 corresp onding to x 0 2 = y 0 2 . Then  1 ?? 1  2

in the p eak. However, if 

1

touches the head position (i.e., pos( 1 ) = ), then  0 1 6?? 1  0 2 for any descendants 0 i of  i (i=1;2).

In the nextsection, we introduce a modied version of an indep endence ?? 3

. Before introducing??

3

, we will explain itskey idea inExample 7.12 by using Example 7.3 again.

Denition 7.4 A term t is ahead normal form of ^

R if s is not a redexof ^ R for alls such that t

r ! 3 ^ R s. 5 Lemma 7.5 Let ^

l be the left-hand side of any rule in a compatible LRCTRS ^

R. For any non-variable proper subterm t of ^

l and any substitution  , t is a headnormal form of

^ R.

Proof. This is obtained by a straightforward induction on the length of the reduction sequence t r ! 3 ^ R s since ^ R is an overlay. 2

In fact, sucha prop ertyholds for anyoverlay semi-equational CTRS.

Denition 7.6 Foruniabletermst 1

andt 2

,thesetofminimalvariable posi-tionsMV

t1;t2

isthesetofallminimalelementswrtinfpjt 1 =p2V or t 2 =p2 Vg. Notethat MV t 1 ;t 2 =MV t 2 ;t 1 . Lemma 7.7 Let ^ S i : ^ l i ! ^r i (Q i

be the rewrite rules in a compatible LRC-TRS ^ R for i=1;2. Suppose ^ l 1 and ^ l 2

are uniable andhr 1 ;r 2 i isthestandard pairofcompatibilityofh ^ S 1 ; ^ S 2 i.Assumethatq~2MV  r1;r2 andr 1 =~q  ^ l 1 =~p2V. Let be any unier of

^ l 1 and ^ l 2 .

(i) Supposethatr 2 =~q;qx2V.If x2V( ^ l 2 =~p),then ^ l 2 =~p;qx.Otherwise, x is a ground normal form of

^ R. (ii) Suppose that r

2

=~q ;q62V. Then (r 2

=q ;~ q) is a head normal form of ^ R.

Proof. Let be the most general unierof ^ l 1 and ^ l 2 constructed as fx:= ^ l 2 =pjp2MV ^ l1; ^ l2 and x ^ l 1 =pg [ fx:= ^ l 1 =pjp2MV ^ l 1 ; ^ l 2 ;x ^ l 2 =p; and ^ l 1 =p62Vg: 5

The notion of a headnormal formis the sameasthat of a root-stable form of a TRSin[21].

 = for some substitution . Then (r 2

=q )~  (r 1

=~q ) from the compati-bility of ^ R, and ( ^ l 1 =~p)  ^ l 2 =~p from ^ l 1 =~p 2 V. Since ^ l 1 =~p  r 1 =~q , (r 2 =~q )  ( ^ l 1 =~p) ^ l 2 =~p.

(i) Supp ose that r 2 =~q ;q  x 2 V and x 2V( ^ l 2 =~p).Since ^ l 1 =~p2 V, x  x fromthe constructionof . Thus

^ l 2 =p;~ qx follow from(r 2 =~q ) ^ l 2 =~p. Next assume that x 62 V(

^ l 2 =~p). Since (r 2 =~q )  ^ l 2 =~p, x 62 V( ^ l 2 =~p) impliesthatx:= ^ l 2 =p;~ qisin.Fromx2V(r 2 =~q ),xisaprop ersubterm of ^ l 1

according to the denition of . Since ^ l 1 and ^ l 2 share no variables and x  ^ l 2

=~p;q, x cannot contain variables. Therefore, x  x and x isa groundnormal formof

^

R by Lemma 7.5. (ii) Supp ose thatr

2

=~q ;q 62V.Since ^ l

1

=~p2V, p~6= fromthe denition ofan LRCTRS. Thus (r 2 =~q ;q)  ^ l 2

=~p;q is a proper non-variable subterm of ^

l 2

. Therefore,(r 2

=~q;q) is ahead normal formof ^

R byLemma 7.5. 2

Denition 7.8 Web orrownotationsfromDenition7.1andLemma7.7.Let ~ q 2MV  r 1 ; r 2

. Supp ose that r 1 =~q  ^ l 1 =~p2V. If x 2m 2V(r 2 =~q )\V( ^ l 2 =~p),then theAS 2m -segmentinA 0

iscalledapreservedsegment.Ifx 2m 2V(r 2 =~q)nV( ^ l 2 =p),~ thenthe AS 2m -segmentin A 0

is calleda skewed segment. When r 2 =~q ^ l 2 =~p2 V, preservedsegments and skewedsegments are denedsymmetrically.

Note 7.9 It is easy to see that any segment in a replacement sequence is a preserved segment with a non-overlapping LRCTRS. The proof of UN of a weaklycompatible TRS in[22] is insucient since the metho dology neglects skewedsegments.

The following example explains the key idea of the modied indep endence ?? 3 =?? 1 [?? 2 , where ?? 2

isa new relation denedinthe nextsection.

Example 7.10 Letus considerExample 7.3 again. Suppose that the reduc-tion steps  1 ,  2 , and  3

are in subpro ofs u r $ 3 ^ R g(t;a;a), a r $ 3 ^ R s 2 , and t r $ 3 ^ R s 1

of the p eak, respectively.Let  0 1 ,  0 2 ,and  0 3 b e descendants(byP # ) of 1 , 2 ,and 3

,respectively.Theintuitionbehindthemodiedindep endence isas follows.

{ The reduction steps  0 1

and  0 2

are in preserved segments. Since relative p ositions of preserved segments are preserved by using (i) of Lemma 7.7, we can prove preservation of the indep endence of 

1

and  2

by using an argument similar to that of the non-overlapping case. This case is handled with??

1 .

{ The reduction step  0 3

is ina skewedsegmentin the replacementsequence. Thenthe p osition of 

0 3

may overlap with the positionof  0 1

. However,the intermediate term g(t;a;a) plays the role of barrier b etween 

0 1 and  0 3 so that they do not interfere with each other. Note that g(t;a;a) is a head normalformand aisagroundnormalformby(ii) ofLemma7.7. Thiscase

pos()     6<p 6<p 0 . .. . . .

head normal forms p p 0 pos( ) Fig. 10.Relation ?? T 2 when p 0 and A(;t)6<p 0 hold

will b e handled with ?? 2

.

In the followingsections, we will formally discuss the ab ove idea.

7.2 Independence ?? 3

of compatible LRCTRS

Inthissectionweintro duceabinaryrelation?? 3

,whichistheunionof?? 1 and ?? 2 .Then ?? 3

isprovedto bean independence for aPES P ^ R of a compatible LRCTRS ^ R .Intuitively,?? 2

meansthatandareseparatedbyaspecial term called abarrier.

Denition 7.11 For any proof A in ^ R and ; 2 top(A),  66 T 2  in A if a term t2A(;) and a p osition p2Pos(t)exist such that

(i) p^, (ii) A(;)6<p, and (iii) there exists p

0  p satisfying   p 0 and A(;t) 6< p 0 such that t=q is a head normal formfor eachq 2Pos(t=p) with q6kp

0 .

Then t is called a barrier between  and . We also say t=p is the b ody and t=p

0

isthero ckofthebarriertinordertomake thepositionspand p 0 explicit. Fig. 10illustrates  66 T 2 . Wewrite ?? T 2  if either  66 T 2  or  66 T 2  . Example 7.12 Let ^

R be the same as the one in Example 7.3. Consider the followingpro of in

^ R :

f(g(f(a;a);a;a);a)  1 ! ^ S 0 g(f(a;a);a;a) 2 ! ^ S g(a;a;a)  3 ^ S

g(a;f(a;a);a) 4

^ S