数理解析研究所講究録
第 833 巻 1993 年 53-64

53

Church-Rosser Property and
Unique Normal Form Property of
Non-Duplicating Term Rewriting Systems-DRAFT*外山芳人

大山口通夫

Yoshihito Toyama

Michio Oyamaguchi
Mie University\ddagger

NTT\dagger

1

Introduction

The original idea of the conditional linearization of non-left-linear term rewriting systems wasintroduced by De Vrijer [4], Klop and De Vrijer [7] for giving a simpler proof of Chew’s theorem$[2, 10]$ . They developed an interesting method for proving the unique normal form property forsome non-Church-Rosser, non-left-linear term rewriting system . The method is based on thefact that the unique normal form property of the original non-left-linear term rewriting systemfollows the Church-Rosser property of an associated left-linear conditional term rewritingby linearizing the non-left-linear rules. In Klop andsystemwhich is obtained form
Bergstra [1] it is proven that non-overlapping left-linear conditional term rewriting systems are
Church-Rosser. Hence, combining these two results, Klop and De Vrijer [4, 7, 6] showed thathas the unique normal form property if
is non-overlapping.
the term rewriting system
However, as their conditional linearization technique is based on the Church-Rosser property, its application is restricted in nonfor the traditional conditional term rewriting system
containing only trivial(though this limitation may be slightly relaxed withoverlapping
critical pairs).
In this paper, we introduce a new conditonal linearization based on a left-right separated. The point of our linearization is that by replacing a
conditional term rewriting systemwith a left-right separated conditional system
we cantraditional conditional system
$R$

$R$

$R^{L}$$R$$R^{L}$$R$$R^{L}$$R^{L}$$R^{L}$$R_{L}$$R^{L}$$R_{L}$*LA Symposium (Kyotyo, February 1, 1993)\dag er
NTT CS Laboratories, Hikaridai, Seika-cho, Soraku-gun Kyoto 619-02, Japan (email: $toyama_{-1}\cap c$ ntt-20. ntt jp)\ddagger Faculty of Engineering, Mie University, Kamihama-cho, Tsu-shi 514, Japan (email: mo@info.mie-u ac jp)

54easily relax the non-overlapping limitation of conditional systems originated from Klop andBergstra [1].
By developing a new concept of weighted reduction systems we present a sufficient condition
for the Church-Rosser property of a left-right separated conditional term rewriting system
which may have overlapping rewrite rules. Applying this result to our conditional linearization,
we show a sufficient condition for the unique normal form property of a non-duplicating nonleft-linear overlapping term rewriting system .
Moreover, our result can be naturally applied to proving the Church-Rosser property ofsome non-duplicating non-left-linear overlapping term rewriting systems such as right-groundterm rewriting systems. Oyamaguch and Ota [8] proved that non-E-overlapping right-groundterm rewriting systems are Church-Rosser by using the joinability of E-graphs, and Oyamaguch
extended this result into some overlapping systems [9]. The results by conditonal linearizationin this paper strengthen some part of Oyamaguchi’s results by E-graphs $[8, 9]$ , and vice verse.
Hence, we believe that both approach should be working together for developing the potential
of non-left-linear term rewriting system theory.
$R_{L}$$R$

2

Reduction Systems

Assuming that the reader is familiar with the basic concepts and notations concerning reduction
systems in [3, 5, 6], we briefiy explain notations and definitions.
A reduction system (or an abstract reduction system) is a structure $A=\langle D,$ } consisting), called a reduction relation.
of some set
and some binary $relationarrow onD$ (i.e.,
A reduction (starting with ) in is a finite or infinite sequenceThe$ofarrow,$.
identity of elementsof is denoted byis the reflexive closure
thesymmetric closure $ofarrow,$is the transitive reflexive closure $ofarrow,$is the equivalence
relation generated $byarrow$ ( $i.e.$ , the transitive reflexive symmetric closure $ofarrow$ ).
, then we say that is a normal
If $x\in D$ is minimal with respect $toarrow$ , i.e.,
form; let $NF$ be the set of normal forms. If
and $y\in NF$ then we say has a normal
form and is a normal form of .
$arrow$$D$$arrow\subseteq D\cross D$$x_{0}$$x,$$A$$x_{0}arrow x_{1}arrow x_{2}arrow\cdots$

$D$

$y$

$arrow\underline{=}$$rightarrow is$$x\equiv y$$andrightarrow^{*}$$arrow^{*}$$\neg\exists y\in D[xarrow y]$$x$$xarrow^{*}y$$y$$\forall x,$

$x$

$y$

Definition 2.1 $A=\langle D,$$x$$arrow$} is Church-Rosser (or confluent) iff$y,$ $z\in D[xarrow^{*}y\wedge xarrow^{*}z\Rightarrow\exists w\in A, yarrow^{*}w\wedge zarrow^{*}w]$.

Definition 2.2 $A=\{D, arrow\}$ has unique normal forms iff$\forall x,$$y\in NF[xrightarrow*y\Rightarrow x\equiv y]$.

The following fact observed by Klop and De Vrijer [7] plays an essential role in our linearization too.

Proposition 2.3 [Klop and De Vrijer] Let
systems with the sets of normal forms
andforms if each of the following conditions holds:

and $A_{1}=\langle D,$
respectively. Then

$A_{\{}=\langle D, arrow\rangle 0$$NF_{0}$$NF_{1}$$arrow$$1$$A_{0}$} be two reduction
has unique normal

55
(i)

extends$arrow 1$(ii)$A_{1}$$arrow_{)}0$

is Church-Rosser,(iii) $NF_{1}$ contains$N\grave{F}_{0}$.

Weight Decreasing Joinability

3This section introduces the new concept of weight decreasing joinability. In the later sections
this concept is used for analyzing the Church-Rosser property of conditional term rewriting
systems with extra variables occurring in conditional parts of rewriting rules.
be the set of positive integers. $A=\{D,$ ) is a weighted reduction system if
Letthat is, positive integers (weights ) are assigned to each reduction to represent
costs.
such thatandis a sequence
A proof of$y\equiv x.$ . The weight. We usually abbreviate a proof
ofof the proof is:by. The form of a proof may be indicated by writing, for example,
for proofs.
, etc. We use the symbols$N^{+}$$arrow$$arrow=\bigcup_{w\in N+}arrow_{w}$$w$$xrightarrow^{*}y$$x\equiv x_{0}$$\mathcal{P}:x_{0}rightarrow_{w_{1}}x_{1}rightarrow_{w_{2}}x_{2}\cdotsrightarrow_{\iota v_{n}}x_{n}$$w(\mathcal{P})$$\mathcal{P}$$\mathcal{P}$$\sum_{i=1}^{n}w_{i}$$xrightarrow^{*}y$$\mathcal{P}:xarrow^{*}\cdotarrow^{*}y,$$\mathcal{P}:xrightarrow^{*}y$$xarrow\cdotarrow^{*}\cdotarrow y$$\mathcal{P},$$\mathcal{Q},$$\mathcal{P}’$$\cdots$

Definition 3.1 A weighted reduction system $A=\langle D,$ } is weight decreasing joinable iff$y\in D$ [for any proof
such that
there exists some proof :$arrow$$\mathcal{P}:xrightarrow^{*}y$$\forall x,$$]$$xarrow^{*}\cdotarrow^{*}y$$\mathcal{P}’$$w(\mathcal{P})\geq w(\mathcal{P}’)$.

isis weight decreasing joinable thenIt is clear that if a weighted reduction system
Church-Rosser. We will now show a sufficient condition for the weight decreasing joinability.
$A$

$A$

Lemma 3.2 Let be a weighted reduction system. Then is weight decreasing joinable if thefollowing condition holds::
such that (i)there exists a proof
for any $y\in D$ [for any proof].
and :, or (ii)$A$$A$$\mathcal{P}:xarrow\cdotarrow y$$x,$$w(\mathcal{P})>w(\mathcal{P}’)$$w(\mathcal{P})\geq w(\mathcal{P}’)$$\mathcal{P}’$$xrightarrow^{*}y$$xarrow\equiv\cdotarrow\equiv y$$\mathcal{P}’$Proof. The lemma can be easily proven by induction on the weight of a proof of$xrightarrow^{*}y$.

$\square$

The following lemma is used to show the Church-Rosser property of non-duplicating systems.
Lemma 3.3 Let $A_{0}=\{D, arrow\}0$ and$\Sigma_{i=1}^{n}w(\mathcal{P}_{i})$. Assume that for any

exists proofs

proofs$\mathcal{P}_{i}’$$\mathcal{P}’$:$aarrow^{*}carrow^{*}b11$

with

$a,$

$A_{1}=\langle D, arrow\rangle 1$$b\in D$

$Q;y_{1}^{rightarrow^{*}}z$$\mathcal{P}_{i}$and any proof$w(\mathcal{P}’)\leq w(\mathcal{P})$: $x_{i}arrow^{*}z0(i=1, \cdots n)$ and

Let

and

with

: $x_{i}rightarrow^{*}y1(i=1, \cdots n)$ and let $w=$$\mathcal{P}:arightarrow^{*}b1$$aarrow^{*}carrow^{*}b00$$w(\mathcal{Q})\leq w$

such that$w(\mathcal{P})\leq w$

there

for some $c\in D.$ Then, there exist
for some .
$z$

56
Proof. By induction on
proofs$w$. Base step $w=0$ is trivial. Induction step: From I.H., we haveandsuch that.
for some$\tilde{\mathcal{P}}_{i}:x_{i}arrow^{*}z’0(i=1, \cdots n-1)$

By connecting the proofs 2 andand$w(\hat{\mathcal{P}})=w(\tilde{\mathcal{Q}})+w(\mathcal{P}_{n})$$\check{\mathcal{P}}:z’arrow^{*}zarrow^{*}x_{n}11$

with, it follows that

Note that
as if$\mathcal{Q}’’:yrightarrow^{*}x_{n}arrow^{*}z11$$)$. Takeand$\Sigma_{i=1}^{n-1}w(\mathcal{P}_{i})\geq w(\tilde{\mathcal{Q}})$

Since$\hat{\mathcal{P}}:z’rightarrow^{*}yrightarrow^{*}x_{n}11$$w\geq w(\hat{\mathcal{P}})$$z’arrow^{*}zarrow^{*}x_{n}00$$\Sigma_{i=1}^{n-1}w(\mathcal{P}_{i})\geq w(\tilde{\mathcal{Q}})$. By the assumption, we have proofs

for some . Thus we obtain proofs$z$$\mathcal{P}_{i}’$:.

By combining subproofs of“$w\geq w(\mathcal{Q}$

we have a proof$w\geq w(\hat{\mathcal{P}})\geq w(\check{\mathcal{P}})$$x_{i}arrow^{*}z0(i=1, \cdots, n)$and$\mathcal{P}_{n}$$z’$$\tilde{\mathcal{Q}}:yrightarrow^{*}z’1$$\mathcal{Q}’$

$Q$

and

$\hat{\mathcal{P}}:z’rightarrow^{*}yrightarrow^{*}x_{n}11$$\check{\mathcal{P}}:z_{11}^{\prime_{arrow^{*}Zarrow^{*}X_{n}}}$, we can make$w+w\geq w(\hat{\mathcal{P}})+w(\check{\mathcal{P}})=w(\mathcal{Q}’)+w(\mathcal{Q}’’)$$w\geq w(\mathcal{Q}’)$; otherwise, takeas Q.

$\mathcal{Q}’’$. Thus$\mathcal{Q}’:y_{11}^{rightarrow^{*}z’arrow^{*}Z}$or$w\geq w(\mathcal{Q}’)$$\square$Term Rewriting Systems

4

In the following sections, we briefly explain the basic notions and definitions concerning term
rewriting systems [3, 5, 6].
, and letLet
be an enumerable set of function symbols denoted by $f,g,$
be an
. By
, we
where
enumerable set of variable symbols denoted byis sometimes denoted
denote the set of terms constructed from and V. The term set
by .
toA substitution is a mapping from a term set
such that for a term ,is completely determined by its values on the variable symbols occurring in . Following.
common usage, we write this as
instead of. ThenConsider an extra constant called a hole and the set) is called a context on . We use the notation $C[, , ]$ for the context containing, thenholes $(n\geq 0)$ , and if
denotes the result of placing,in the holes of $C[, , ]$ from left to right. In particular, $C[]$ denotes a context
containing precisely one hole. is called a subterm of $t\equiv C[s]$ . If is a subterm occurrence of. If a term has an occurrence of some (function or variable) symbol , we
, then we write, $z_{n}\not\in C[, \cdots, ]$write $e\in t$ . The variable occurrencesofare fresh if
and.
A rewriting rule is a pair ( } of terms such thatand any variable in also occurs
in . We write $larrow r$ for. A redex is a term , where $larrow r$ . In this caseis called acontractum of . The set of rewriting rules defines a reduction $relationarrow onT$ as follows:$tarrow s$ iff
for some rule $larrow r$ , and some $C[],$ .
$h,$$\mathcal{F}$$x,$ $y,$ $z,$$\cdots$$\mathcal{V}$$\mathcal{F}\cap \mathcal{V}=\phi$$\cdots$$\mathcal{F}$$T(\mathcal{F}, \mathcal{V})$$T(\mathcal{F}, \mathcal{V})$$T$$\theta$$t$$T(\mathcal{F}, \mathcal{V})$$T(\mathcal{F}, \mathcal{V})$$t$$\theta(t)$$t\theta$$\theta(t)$$\square$$\{\square \},$$\mathcal{F}$$\mathcal{V}$$n$$t_{1},$$t_{1},$$\ldots$$\ldots,$$t_{n}\in T(\mathcal{F}, \mathcal{V})$$C[t_{1}, \ldots, t_{n}]$$t_{n}$$s$$s\subseteq t$$t$$C\in T(\mathcal{F}\cup$$T(\mathcal{F}\cup\{\square \}, \mathcal{V})$

$s$

$t$

$e$

$z_{1},$$\cdots,$$z_{n}$$C[z_{1}, \cdots, z_{n}]$$z_{1},$$\cdots$$z_{i}\not\equiv z_{j}(i\neq j)$$l,$ $r$$l$$l\not\in \mathcal{V}$$r$$r\theta$$l\theta$$\langle l, r\rangle$$l\theta$$t\equiv C[l\theta],$$s\equiv C[r\theta]$$\theta$

When we want to specify the redex occurrence$\triangle\equiv l\theta$

of

$t$

in this reduction, we write

Definition 4.1 A term rewriting system is a reduction system
the reduction
is defined by a set of rewriting rules. If$R$$relationarrow onT(\mathcal{F}, \mathcal{V})$$R=\langle T(\mathcal{F}, \mathcal{V}),$ $arrow$$R$$tarrow\triangle s$.

} such thathas $larrow r$ as a

57
rewriting rule, we write $larrow r\in R$ .

We say that is left-linear if for any $larrow r\in R,$ is linear (i.e., every variable in occurs
only once). If has critical pair then we say that is overlapping: otherwise non-overlapping$[5, 6]$ .
A rewriting rule $larrow r$ is duplicating if contains more occurrences of some variable thenis non-duplicating if every $larrow r\in R$ is; otherwise, $larrow r$ is non-duplicating. We say that
non-duplicating.
$R$

$l$

$l$

$R$

$R$

$r$

$R$

$l$

5

Left-Right Separated Conditional Systems

in which 1 and of
In this section we introduce a new conditional term rewriting system
any rewrite rule $larrow r$ do not share the same variable; every variable in is connected tosome variable in thorough an equational condition. A decidable sufficient condition for the
Church-Rosser property of is presented.
$V(t)$ denotes the set of variables occurring in a term .
$R$

$r$

$r$

$l$

$R$

$t$

Definition 5.1 A left-right separated conditional term rewriting system is a conditional term
rewriting system with extra variables in which every conditional rewrite rule has the form:$larrow r\Leftarrow x_{1}=y_{1},$ $\cdots,$ $x_{n}=y_{n}$$V(l)=\{x_{1}, \cdots , x_{n}\}$ andsuch that (i) 1 is left-linear,with(ii) $\{x_{1}, \cdots, x_{n}\}\cap\{y_{1}, \cdots, y_{n}\}=\phi$ , (iii)
if $i\neq j$ , (iv) does not contain more
$x_{n}=y_{n}$ .
occurrences of some variables than the conditional part $x_{1}=y_{1},$$V(r)\subseteq\{y_{1}, \cdots, y_{n}\}$$l,$ $r\in T(\mathcal{F}, \mathcal{V}),$$x_{i}\not\equiv x_{j}$$r$$\cdots,$

Definition 5.2 Let be a left-right separated conditional term rewriting system. We inductively define term rewriting systems
for $i\geq 1$ as follows:$R$$R_{i}$$R_{1}=\{l\thetaarrow r\theta|larrow r\Leftarrow x_{1}=y_{1},$ $\cdots,$ $x_{n}=y_{n}\in R$and$x_{j}\theta\equiv y_{j}\theta(j=1, \cdots, n)$},$R_{i+1}=\{l\thetaarrow r\theta|larrow r\Leftarrow x_{1}=y_{1},$ $\cdots,$ $x_{n}=y_{n}\in R$

andproofs of
reduction by
for some .
In$R_{t+1)}$$x_{j}\theta\underline{*}y_{j}\theta$$l\thetaarrow r\theta$$R$,. Note that$(j=1, \cdots, n)$$R_{i}\subseteq R_{i+1}$$x_{j} \theta\frac{*}{R_{t}}y_{j}\theta(j=1, \cdots, n)$}.

are called subproofs associating with one stepfor all$i\geq 1$. We have $sarrow tR$ if and only if$sarrow_{l}tR$$i$

The weight $w(sarrow t)R$ of one step reduction $sarrow tR$ is inductively defined as follows:(i) $w(sarrow t)R=1$ if$sarrow tR_{1}$(ii) $w(sarrow t)R=1+w(\mathcal{P}_{1})+\cdots+w(\mathcal{P}_{n})$ if$s_{R}arrow_{?+1}t$

subproofs associating with one step reduction$(i\geq 1)$$sarrow tR_{i+1}$, where$\mathcal{P}_{1},$$\cdots,$$P_{m}(m\geq 0)$

are

58
$x_{n}’=y_{n}’$ be two rules
Let $larrow r\Leftarrow$ $x_{1}=y_{1},$$x_{m}=y_{m}$ and $l’arrow r’x_{1}’=y_{1}’,$in a left-right separated conditonal term rewriting system . Assume that we have renamed
the variables appropriately, so that two rules share no variables. Assume that $s\not\in V$ is a
subterm occurrence in , i.e., $t\equiv C[s]$ , such that and are unifiable, i.e.,, with$y_{i}\theta\equiv y_{i}(i=1, \cdots, m)$ anda minimal unifier . Note that$(j=1, \cdots, n)$ as $\{x_{1}, \cdots, x_{m}\}\cap\{y_{1}, \cdots, y_{m}\}=\phi$ and. Thus,, two reductions starting with , i.e.,
, can
from
and
$x_{n}’=y_{n}’$ if
be obtained by using $larrow r\Leftarrow x_{1}=y_{1},$$x_{m}=y_{m}$ and $l’arrow r’\Leftarrow x_{1}’=y_{1}’,$
we have subproofs ofand. Then we say that$larrow r\Leftarrow x_{1}=y_{1},$are overlapping, and$x_{m}=y_{m}$ and $l’arrow r’x_{1}’=y_{1}’,$$\cdots,$$\cdots,$

$R$

$l$

$l’$

$s$

$r’\theta\equiv r’,$

$r\cdot\theta\equiv r,$$\theta$$s\theta\equiv l’\theta$$y_{j}’\theta\equiv y_{j}’$$\{x_{1}’, \cdots, x_{n}’\}\cap\{y_{1}’, \cdots, y_{n}’\}=\phi$$l\theta\equiv C[s]\theta\equiv C\theta[l’\theta]$$l\theta$$l\thetaarrow r$$l\thetaarrow C\theta[r’]$$\cdots,$$x_{1}\thetarightarrow^{*}y_{1},$$\cdots,$$\cdots,$$x_{m}\thetarightarrow^{*}y_{m}$$x_{1}’\thetarightarrow^{*}y_{1}’,$$\cdots,$$E\vdash\langle C\theta[r’],$$r$$\cdots,$$\cdots,$$x_{n}’\thetarightarrow^{*}y_{n}’$$x_{n}’=y_{n}’$}is a conditional critical pair associated with the multiset of equations $E=[x_{1}\theta=y_{1},$,$larrow
r\Leftarrowx_{1}=y_{1},$] in . We may choose$x_{m}=y_{m}$ and$l’arrow r’x_{1}’=y_{1}’,$to be the same rule, but in this case we shall not consider the case. If
has no critical pair, then we say that is non-overlapping.
$EuE’$ denotes the union of multisets
and $E’$ . We write
if no elements in occur
more than $E’$ .
$\cdots$$x_{m}\theta=y_{m},$$x_{1}’\theta=y_{1}’,$$\cdots,$$s\equiv l$$\cdots,$$R$$x_{n}’\theta=y_{n}’$$\cdots,$$x_{n}’=y_{n}’$

$R$

$R$

$E$

$E$

$E\subseteq E’$

Definition 5.3 Let be a multiset of equations $t’=s’$ and a fresh constantandon terms is inductively defined as follows:$E$$t\sim sE$

(i)
(ii)

$\bullet$.

Then relations$t\sim_{E}\triangleright s$$t\sim t,\phi$$t\sim s[t=s]$(iii) If(iv) If(v) If$t\sim sE$$t\sim rE$$t\sim sE$

then
and

$s\sim tE$$r\sim s,E$

then $t\sim sEuE$then $C[t]\sim C[s]_{y}E$(vi) If $larrow r\Leftarrow x_{1}=y_{1},$$\cdots$, $x_{n}=y_{n}\in R$ and$x_{i}\theta\sim_{t}y_{i}\theta E(i=1, \cdots, n)$, then $C[l\theta]r*EC[r\theta]$

where $E=E_{1}u\cdots uE_{n}$ ,(vii) If $t\cap*rE$ then $t\sim s$ .
$Eu[\cdot]$Lemma 5.4 Let $E=[\rho_{1}=q_{1}, \cdots, p_{m}=q_{m}, \bullet, \cdots, \bullet]$ be a multiset in which$(n\geq 0)$ , and let:.
$\mathcal{P}_{i}$(1) If(2) If$t\sim sE$$t\sim_{E}\triangleright s$$\bullet$occurs$p_{i}\thetarightarrow^{*}q_{i}\theta(i=1, \cdots, m)$then there exists a proof$\mathcal{Q}:t\thetarightarrow^{*}s\theta$

then there exists a proof$\mathcal{Q}’$

:

with

$t\thetaarrow s\theta$$w( \mathcal{Q})\leq\sum_{i=1}^{m}w(\mathcal{P}_{i})+n$

with

.

$w(\mathcal{Q}’)\leq\Sigma_{\dot{\iota}=1}^{m}w(\mathcal{P}_{i})+n+1$

.

$n$

times

59
Proof. By induction on the construction ofand (2) simultaneously.
Base Step: Trivial as (i)$t\sim s\phi\equiv t$or (ii)$t\sim sE$$t\sim s[t=s]$

andin Definition 5.3, we prove (1)$t\sim_{E}\triangleright s$of Definition 5.3.

by (vi) of Definition 5.3, then fromby (iii) (iv) (v) andInduction Step: If we have$an^{E}d(2)$clearly follow. Assume that $t’*s$ by (v) of Definition 5.3.
the induction hypothesis (1)$s\equiv C[r\theta’]$ ,Then we have a rule $larrow r$$x_{1}=y_{1},$$x_{k}=y_{k}$ such thatfor some and $E=E_{1}u\cdots uE_{k}$ . From the induction hypothesis and$t\sim s$$t\sim_{E}\triangleright s$$E$$\Leftarrow$$t\equiv C[l\theta’],$$\cdots,$$\theta’$$x_{i}\theta’\sim_{:}y_{i}\theta’E(i=1, \cdots, k)$$E=E_{1}u\cdots uE_{k}$$\Sigma_{i=1}^{m}w(\mathcal{P}_{i})+n$, it can be easily shown that

. Therefore we have a proof$\mathcal{Q}_{i}$;$x_{i}\theta’\thetarightarrow^{*}x_{i}\theta’\theta(i=1, \cdots, k)$with$\mathcal{Q}’:t\thetaarrow s\theta$and$\sum_{i=1}^{k}w(\mathcal{Q}_{i})\leq$$w(\mathcal{Q}’)\leq\Sigma_{i=I}^{m}w(\mathcal{P}_{i})+n+1$.

$\square$be a left-right separated conditional term rewriting system. Then
Theorem 5.5 Letisone of the following
weight decreasing joinable if for any conditional critical pair{conditions holds:
$R$

$R$

$E\vdash$(i)$q_{E}^{\sim}q’$(ii)

for some$q\sim_{1}>E\triangleleft_{2}\cdot q’E$(iii)

$q\sim\triangleright q’E$

(or

$q,$

$q’\rangle$

such that $E’\subseteq Eu$ [ ] or,$E’$$\bullet$for some$q^{;_{r}}*q$$E_{1}$

and$E_{2}$

such that $E_{1}uE_{2}\subseteq E$ or,) and $E’\subseteq Eu$ [ ].
$\bullet$$E$

Note. The above conditions (i) (ii) (iii) are decidable if has finite rewrite rules. Thus, thetheorem presents a decidable condition for guaranteeing the Church-Rosser property of .
$R$

$R$

Proof. The theorem follows from Lemma 3.2 if for any$\mathcal{P}:tarrow parrow s(t\not\equiv s)$

there exists some. Hence we

and
proof
such that (i) $w(P)>w(\mathcal{Q})$ , or (ii).
will show a proof satisfying (i) or (ii) for a given proof
andare associated with two rules :where two redexesLet, respectively.
$larrow r\Leftarrow x_{1}=y_{1},$, $x_{m}=y_{m}$ and : $l’arrow r’\Leftarrow x_{1}’=y_{1}’,$for some context $C[, ]$ andare disjoint. ThenandCase 1.
for some and . Thus, we can take.
with(i.e.,
occurs in of
occurs below the pattern ). Without loss ofCase 2.
$x_{m}=y_{m}$generality we may assume that : $C_{L}[x_{1}, \cdots, x_{m}]arrow C_{R}[y_{1}, \cdots, y_{n}]\Leftarrow x_{1}=y_{1},$(all the variable occurrences are displayed and $n\leq m$ ),with subproofs : $p_{i}rightarrow^{*}t_{j}(i=1, \cdots, m)$ , and “: $p\equiv C[C_{L}[p_{1},p_{2}, \cdots, p_{m}]]$and $w(\mathcal{P}’)=1+$
by. Since we have a proofwith, we can apply
to $s\equiv C[C_{L}[p_{1}’,p_{2}, \cdots,p_{m}]]$ too. Then, we have a proof $\mathcal{Q}:s\equiv C[C_{L}[p_{1}’, \cdots,p_{m}]]arrow t\equiv$
.
with
and
coincide by the application of the same rule, i.e., $r=r_{1}=r_{2}$ . (Note.
Case 3.
In a left-right separated conditional term rewriting system the application of the same rule at$\mathcal{Q}:trightarrow^{*}s$$\mathcal{Q}:tarrow\underline{=}\cdotarrow\underline{=}s$$w(\mathcal{P})\geq w(\mathcal{Q})$$\mathcal{P}:tarrow parrow s$$\mathcal{Q}$$\mathcal{P}:tarrow parrow’s\triangle\triangle$$\triangle\equiv l\theta$$\triangle’\equiv l’\theta’$$r_{1}$$\cdots$$\triangle$$r_{2}$$\triangle’$$x_{m}’,$$=y_{m}’$$\mathcal{P}:t\equiv$$p\equiv C[\triangle, \triangle^{J}]$$C[t’, \triangle’]arrow C[\triangle, \triangle]\triangle;arrow’\triangle C[\triangle, s’]\equiv s$$C[t’, s’]arrow C[\triangle, s’]\triangle\equiv s$$\triangle’$$\cdots,$$t’$$\mathcal{Q}:t\equiv C[t’, \triangle^{J}]arrow’\triangle$$s’$$w(\mathcal{Q})=w(\mathcal{P})$$\theta$$\triangle\equiv l\theta$$\triangle’$$l$$r_{1}$$\cdots,$$\mathcal{P}’:p\equiv C[C_{L}[p_{1}, \cdots, p_{m}]]arrow t\triangle\equiv$$C[C_{R}[t_{1}, \cdots, t_{n}]]$$\mathcal{P}$$\mathcal{P}_{i}$$arrow’\triangle s\equiv C[C_{L}[p_{1}’,p_{2}, \cdots, p_{m}]]$$p_{1^{arrow’}}^{\triangle}p_{1}’.Thu_{*}s\triangle w(\mathcal{P})=w(\mathcal{P}’)+w(\mathcal{P}’’)$$\mathcal{Q}’:p_{1}arrow p_{1}rightarrow t_{1}$$\Sigma_{i=1}^{m}w(\mathcal{P}_{i})$$w(\mathcal{Q}’)=w(\mathcal{P}’’)+w(\mathcal{P}_{1})$$r_{1}$$C[C_{R}[t_{1}, \cdots, t_{n}]]$$\triangle$$w(\mathcal{Q})=1+w(\mathcal{Q}’)+\Sigma_{i=2}^{m}w(\mathcal{P}_{i})=w(\mathcal{P})$$\triangle^{J}$

60
the same position does not imply the same result as the variables occurring in the left-handside of a rule does not cover that in the right-hand side. Thus this case is necessary even ifand
be $r:C_{L}[x_{1}, \cdots, x_{m}]arrow$the system is non-overlapping.) Let the rule applied to$x_{1}=y_{1},$$x_{m}=y_{m}$ (all the variable occurrences are displayed and$n\leq m)$ , and letwith subproofs:$(i=1, \cdots, m)$ andwith subproofs:$p_{i}rightarrow^{*}s_{i}(i=1, \cdots, m)$ .
.
HereThus we have a proof.
withoverlaps with the pattern
but neither Case 2 nor Case 3 (i.e.,
occurs inCase 4.
1 of). Then, there exists a conditional critical pair $[p_{1}=q_{1}, \cdots,p_{m}=q_{m}]$with subproofs :betweenand , and we can write. From the assumption about critical. Thuspairs the possible relations between and are give in the following subcases.
for some $E’$ such that $E’\subseteq Eu$ [ ]. By Lemma 5.4 and $E’\subseteq Eu$ [ ], we
Subcase 4.1.
$\triangle^{J}$$\triangle$$C_{R}[y_{1}, \cdots, y_{n}]\Leftarrow$$\cdots,$$\mathcal{P}’:p\equiv C[C_{L}[p_{1}, \cdots, p_{m}]]^{\Delta}arrow t\equiv C[C_{R}[t_{1}, \cdots, t_{n}]]$$\mathcal{P}_{i}’$$p_{i}rightarrow^{*}t_{i}$$\mathcal{P}’’:p\equiv C[C_{L}[p_{1}, \cdots,p_{m}]]^{\Delta}arrow’s\equiv C[C_{R}[s_{1}, \cdots, s_{n}]]$$\mathcal{P}_{i}’’$$w(\mathcal{P})=w(\mathcal{P}’)+w(\mathcal{P}^{J/})=1+\Sigma_{i=1}^{m}w(\mathcal{P}_{i})+1+\Sigma_{i=1}^{m}w(\mathcal{P}_{i}’)$$\mathcal{Q}:t\equiv C[C_{R}[t_{1}, \cdots, t_{n}]]rightarrow^{*}C[C_{R}[p_{1}, \cdots,p_{n}]]rightarrow^{*}C[C_{R}[s_{1}, \cdots, s_{n}]]\equiv s$$w(\mathcal{Q})=\Sigma_{i=1}^{m}w(\mathcal{P}_{i})+\Sigma_{i=1}^{m}w(\mathcal{P}_{i}’)<w(\mathcal{P})$$\triangle’$$\triangle’$$\triangle$$\triangle\equiv l\theta$$\{q, q’\}$$\vdash$$\mathcal{P}:t\equiv C[q\theta]^{\Delta}arrow p\equiv C[\triangle]arrow’s\triangle\equiv C[q’\theta]$$r_{1}$$\mathcal{P}_{i}$$r_{2}$$p_{i}\thetarightarrow^{*}q_{i}\theta(i=1, \cdots, m)$$w( \mathcal{P})=\sum_{i=1}^{m}w(\mathcal{P}_{i})+2$

$q’$

$q$

$\bullet$$\bullet$$q_{E}^{\sim}q’$

have a proof$t\equiv C[q\theta]rightarrow^{*}s\equiv C[q’\theta]$

Subcase 4.2.
$E_{1}uE_{2}\subseteq E$

with
with
for some$w( \mathcal{Q}’)=\sum_{i=1}^{m}w(\mathcal{P}_{i})+1<w(\mathcal{P})$$Q’:q\thetarightarrow^{*}q’\theta$.
and$\mathcal{Q}$:$w(\mathcal{Q})<w(\mathcal{P})$$E_{1}$$q_{E^{A_{1}>}}^{\wedge}\cdot E_{2}q’$, we have a proof

we can take
Subcase 4.3. $q’*q’$ (orwe have a proof$t\equiv C[q\theta]arrow s\equiv C[q’\theta]$ withsimilarly.
with$E_{2}$$\mathcal{Q}’:q\thetaarrow\cdotarrow q’\theta$

with

with

$w( \mathcal{Q}’)=\sum_{i1}^{m_{=}}w(\mathcal{P}_{i})+2\leq w(\mathcal{P})$. Hence$w(\mathcal{Q})\leq w(\mathcal{P})$$\bullet$$q^{J_{r_{E}}}*q$$\mathcal{Q}’:q\theta E’arrow q’\theta$such that $E_{1}uE_{2}\subseteq E.$ By Lemma 5.4 and.
) and $E’\subseteq Eu$ [ ]. By Lemma 5.4 and $E’\subseteq Eu$ [ ],. Hence we obtain :with. For the case of $q^{J,}*qE$ we can obtain $Q:sarrow t$$\mathcal{Q}:t\equiv C[q\theta]arrow\cdotarrow s\equiv C[q’\theta]$$w(\mathcal{Q})\leq w(\mathcal{P})$. Hence it is obtained that$\bullet$$w( \mathcal{Q}’)=\sum_{i=1}^{m}w(\mathcal{P}_{i})+2\leq w(\mathcal{P})$$\mathcal{Q}$$w(\mathcal{Q})\leq w(\mathcal{P})$$\square$Corollary 5.6 Let
be a left-right separated conditional term $rew$ ri ting system. Then
weight decreasing joinable if is non-overlapping.
$R$

$R$

is

$R$

be the left-right separated conditional term rewriting system with the
Example 5.7 Let
following rewriting rules:$R_{L}$$R_{L}$$\{\begin{array}{l}f(x’,x’’)arrow h(x,f(x,b))\Leftarrow x’=x,x’’=xf(g(y’),y’)arrow h(y,f(g(y),a))\Leftarrow y’=y,y’’=yaarrow b\end{array}$Here, we have a conditonal critical pair$[g(y’)=x, y”=x, y’=y, y”=y]\vdash\{h(x, f(x, b)),$ $h(y, f(g(y), a))\rangle$

Since $h(x, f(x, b)),\sim h(y^{n}, f(x, b))[y=x]$$h(y, f(g(y), a))$ ,we have$\sim$$h(y”, f(g(y’), b))$$\sim$$h(y, f(g(y), b))\sim_{J}[\cdot$$h(x, f(x, b))\sim’h(y, f(g(y), a))[g(y)=x]Ewher^{1}e^{y’’=y,y’y]}E’=^{=}[g(y’)=x,$$y”=x,$ $y”=$

61

$y,$

$y’=y$ ,$\bullet$]. Thus, from Theorem 5.5 it follows that

$R_{L}$

is weight decreasing$\gamma oinable$.

$\square$

In Theorem 5.5 we request that every conditional critical pair $E\vdash\{q, q’\}$ satisfies (i), (ii) or(iii). However, it is clear that we can ignore the conditional critical pairs which cannot appear
in the actual proofs of . Thus, we can strengthen Theorem 5.5 as follows.
$R$

be a left-right separated conditional term rewriting system. Then
Corollary 5.8 Let
isweight decreasing joinable if any conditional critical pair $E\vdash\{q, q’\}$ such that $E$ is satisfiablein satisfies (i), (ii) or (iii) in Theorem 5.5.
Note. The satisfiability of is generally undecidable.
$R$

$R$

$R$

$E$

6

Conditonal Linearization

The original idea of the conditional linearization of non-left-linear term rewriting systems wasintroduced by De Vrijer [4], Klop and De Vrijer [7] for giving a simpler proof of Chew’s theorem$[2, 10]$ . In this section, we introduce a new conditonal linearization based on left-right separated conditional term rewriting systems. The point of our linearization is that by replacing
traditional conditional systems with left-right separated conditional systems we can easily relax
the non-overlapping limitation because of the results of the previous section.
Now we explain a new linearization of non-left-linear rules. For instance, let consider anon-duplicating non-left-linear rule $f(x, x, x, y, y, z)arrow g(x, x, x, z)$ . Then, by replacing all thefrom left to right in the left handside with distinct fresh
variable occurrences $x,$ $x,$ $x,$
variable occurrences $x’,$ “, $x”’,$ $y’,$ $y”,$ respectively and connecting every fresh variable to corresponding original one with equation, we can make a left-right separated conditional rule$f(x’, x”, x”’, y’, y”, z’)arrow g(x, x, x, z)\Leftarrow x’=x,$ $x”=x,$ $x”’=x,$ $y’=y,$ $y’=y,$ $z’=z$ . Moreformally we have the following definition, the framework of which originates essentially fromDe Vrijer [4], Klop and De Vrijer [7].
$y,$ $y,$ $z$

$z’$

$x$

Definition 6.1 (i) If is a non-duplicating rewrite rule $larrow r$ , then the (left-right separated)conditional linearization of is a left-right separated conditional rewrite rule : $l’arrow$
$r$

$r$

$r_{L}$$r\Leftarrow x_{1}=y_{1},$ $\cdots,$ $x_{m}=y_{m}$such that$l’\theta\equiv l$for the substitution$\theta=[x_{1} :=y_{1}, \cdots, x_{m} :=y_{m}]$(ii) If $R$ is a non-duplicating term rewriting system, then, is defined as the set of the rewrite rules $\{r_{L}|r\in R\}$ .

$R_{L)}$.

the conditional linearization of$R$

Note. The non-duplicating limitation of in the above definition is necessary to guarantee
thatis a left-right separated conditional term rewriting system.
$R$$R_{L}$

Note. The above conditional linearization is different form the original one by Klop and De
Vrijer $[4, 7]$ in which the left-linear version of a rewrite rule is a traditional conditonal rewrite$r$62rule without extra variables in the right handside and the conditional part. Hence, in the caseis already left-linear, Klop and De Vrijer $[4, 7]$ can take itself as its conditional linearization.
On the other hand, in our definition we cannot take itself as its conditional linearization
because must be translated into a left-right separated rewrite rule.
$r$

$r$

$r$

$r$

Theorem 6.2 If a conditional linearizationof a non-duplicating term rewriting system
is Church-Rosser, thenhas unique normal forms.
$R_{L}$$R$$R$

Proof. By Propsiton 2.3, similar to Klop and De Vrijer $[4, 7]$ .
Example 6.3 Let
rules:$R$$R$$\square$be the non-duplicating term rewriting system with the following rewriting$\{\begin{array}{l}f(x,x)arrow h(x,f(x,b))f(g(y),y)arrow h(y,f(g(y),a))aarrow b\end{array}$

Note thatis non-left-linear and non-terminating.
linearization of :$R$

Then we have the following$R_{L}$

as the$R$$\{\begin{array}{l}f(x’,x’’)arrow h(x,f(x,b))\Leftarrow x’=x,x’’=xf(g(y’),y’)arrow h(y,f(g(y),a))\Leftarrow y’=y,y’’=yaarrow b\end{array}$$R_{L}$In Example 5.7 the Church-Rosser property ofhas already been shown. Thus, form Theorem 6.2 it follows thathas unique normal forms.
$R_{L}$$R$

7$\square$

Church-Rosser Property of Non-Duplicating Systems

In the previous section we have shown a general method based on the conditional linearization technique to prove the unique normal form property for non-left-linear overlapping nonduplicating term rewriting systems. In this section we show that the same conditional linearization technique can be used as a general method for proving the Church-Rosser propertyof some class of non-duplicating term rewriting systems.
-ground ($i.e,$ no variables occur in the right handside of rewrite
Theorem 7.1 Let be arules) term rewriting system. If the conditional linearizationof is wetght decreasing
joinable thenis Church-Rosser.
$R$$r\iota ght$

$R_{L}$$R$$R$

Proof. Letandhave reduction $relationsarrow andarrow L$ respectively. $Sincearrow L$ extends$arrow andR_{L}$ is weight decreasing joinable, the theorem clearly holds if we show the claim: for
any
and :
there exist proofs :
with
and
$t,$

$s$

$R$

$R_{L}$$\mathcal{P}$$trightarrow^{*}SL$$\mathcal{Q}$$tarrow^{*}rLarrow^{*}SL$$w(\mathcal{P})\geq w(\mathcal{Q})$$tarrow^{*}rarrow^{*}s$63. Base Step $w(\mathcal{P})=0$
for some term . We will prove this claim by induction on
is trivial. Induction Step $w(\mathcal{P})=w(w>0)$ : Form the weight decreasing joinability of
.
with
. Let
, we have a proof
have the form $t-s’arrow^{*}$ .
Without loss of generality we may assume that $C_{L}[x_{1}, \cdots, x_{m}]arrow C_{R}\Leftarrow x_{1}=x,$$x_{m}=x$(all the variable occurrences are displayed) is a linearization of $C_{L}[x, \cdots, x]arrow C_{R}$ and “:: $t_{i}rightarrow^{*}t’L(i=1, \cdots, m)$ for some . Then,$t\equiv C[C_{L}[t_{1}, \cdots, t_{m}]]arrow s’L\equiv C[C_{R}]$ with subproofs$w(\mathcal{P})$$r$$R_{L}$$\mathcal{P}’:tarrow^{*}L$$w\geq w(\mathcal{P}’)$$arrow^{*}sL$$\mathcal{P}’$$arrow^{*}SL$$\cdots,$$\mathcal{P}$$t’$$\mathcal{P}_{i}$from Lemma 3.3 and the induction hypothesis we have proofs $t_{i}arrow^{*}t’’(i=1, \cdots m)$ . Hence we
can take the reduction $t\equiv C[C_{L}[t_{1}, \cdots, t_{m}]]arrow^{*}C[C_{L}[t’’, \cdots, t’’]]arrow s’\equiv C[C_{R}]$ . Let$\hat{\mathcal{P}}:s’arrow^{*}Larrow^{*}SL$From
and I.H., we haveThus, the theorem follows.
$w>w(\hat{\mathcal{P}})$$\hat{\mathcal{Q}};s’arrow^{*}rarrow^{*}sLL$

with$w(\hat{\mathcal{P}})\geq w(\hat{\mathcal{Q}})$

and

$s$

$‘arrow^{*}rarrow^{*}s$

for some .
$r$$\square$

The following corollary is originally proven by Oyamaguchi [8].
be a right-ground term rewriting system having a nonCorollary 7.2 [Oyamaguchi] Let. Thenis Church-Rosser.
overlapping conditional linearization
$R$

$R$

$R_{L}$

Next we relax the right-ground limitation of$R$

in Theorem 7.1.

be a term rewriting system in which every rewrite rule $larrow r$ is rightTheorem 7.3 Let
linear and no non-linear variables in occur in . If the conditional linearizationof is
is Church-Rosser.
weight decreasing joinable then
$R$

$l$

$R$

$R_{L}$$r$$R$

Proof. The proof is similar to that of Theorem 7.1. Letandhave reduction relations$arrow andarrow L$ respectively. Since $arrow Lextendsarrow andR_{L}$ is weight decreasing joinable, the theorem

clearly holds if we show the claim: for any

$t,$

$s$

and

$\mathcal{P}:trightarrow^{*}SL$$R$$R_{L}$

there exist proofs$\mathcal{Q};tarrow^{*}rLarrow^{*}SL$with.
for some term . We will prove this claim by induction on
is trivial. Induction Step $w(P)=w(w>0)$ : Form the weight decreasing
Base Step. Let
have the formwithjoinability of , we have a proof$x_{m}=$
Without loss of generality we may assume that $C_{L}[x_{1}, \cdots, x_{m}, y_{1}]arrow C_{R}[y]\Leftarrow x_{1}=x,$$y_{1}=y$ (all the variable occurrences are displayed) is the linearization of $C_{L}[x, \cdots, x, y]arrow$with subproofs : $t_{i}rightarrow^{*}t’L(i=1, \cdots, m)$and$w(\mathcal{P})\geq w(\mathcal{Q})$and$tarrow^{*}rarrow^{*}s$$w(\mathcal{P})$$r$$w(\mathcal{P})=0$$R_{L}$$w\geq w(\mathcal{P}’)$$\mathcal{P}’:tarrow^{*}\cdotarrow^{*}sLL$$\mathcal{P}’$$tarrow\hat{s}arrow^{*}\cdotarrow^{*}sLLL$$\cdots,$$x,$$C_{R}[y]$for some$t\equiv C[C_{L}[t_{1}, \cdots, t_{m}, p_{1}]]arrow\hat{s}L\equiv C[C_{R}[p]]$

$t’$

and

$p_{1}rightarrow^{*}pL$$C[C_{R}[p]]arrow^{*}Larrow^{*}Ls$

Then, we can takewith the weight$w(\mathcal{P}’)$$\mathcal{P}_{i}$$t\equiv C[C_{L}[t_{1}, \cdots, t_{m},p_{1}]]arrow s’L\equiv C[C_{R}[p_{1}]]rightarrow^{*}L\hat{s}\equiv$. Let $\mathcal{P}’’:t\equiv C[C_{L}[t_{1}, \cdots, t_{m}, p_{1}]]arrow Ls’\equiv C[C_{R}[p_{1}]]$ .

. HenceThen, from Lemma 3.3 and the induction hypothesis we have proofs
we can take the reduction $t\equiv C[C_{L}[t_{1}, \cdots, t_{m},p_{1}]]arrow^{*}C[C_{L}[t’’, \cdots, t’’,p_{1}]]arrow s’\equiv C[C_{R}’[p_{1}]]$ . Let
.
and
with
and I.H., we haveFrom$t_{i}arrow^{*}t^{\prime/}(i=1, \cdots m)$$\hat{\mathcal{P}}:s’rightarrow^{*}\hat{s}arrow^{*}LL$$s’arrow^{*}rarrow^{*}s$$w>w(\hat{\mathcal{P}})$$arrow^{*}sL$

for some . Thus, the theorem follows.
$r$$\hat{\mathcal{Q}};s_{LL}^{\prime_{arrow^{*}\gammaarrow^{*}S}}$$\square$$w(\hat{\mathcal{P}})\geq w(\hat{\mathcal{Q}})$64
be a term rewriting system in which every rewrite rule $larrow r$ is rightCorollary 7.4 Let
linear and no non-linear variables in occur in . If the conditional linearizationof is
non-overlapping then is Church-Rosser.
$R$

$l$

$r$

$R_{L}$$R$$R$

References[1] J. A. Bergstra and J. W. Klop, Conditional rewrite rules: Confluence and termination,
J. Comput. and Syst. Sci. 32 (1986) 323-362.

[2] P. Chew, Unique normal forms in term rewriting systems with repeated variables, Proc.
13th STOC (1981) 7-18.
[3] N. Dershowitz and J. P. Jouannaud, Rewrite Systems, in: J. V. Leeuwen, ed., Handbookof Theoretical Computer Science B (North-Holland, 1990) 244-320.
[4] R. C. de Vrijer, Unique normal forms for combinatory logic with parallel conditional, acase study in conditional rewriting, Techn. Report Free University Amsterdam (1990)[5] G. Huet, Confluent reductions: Abstract properties and applications to term rewriting
systems, J. ACM27 (1980) 797-821.
[6] J. W. Klop, Term rewriting systems, to appear in: S. Abramsky, D. Gabbay and
T. Maibaum, eds., Handbook of Logic in Computer Science I (Oxford University Press,
1992).

[7] J. W. Klop and R. C. de Vrijer, Unique normal forms for lambda calculas with surjective
pairing. Information and Computation 80 (1989) 97-113.
[8] M. Oyamaguchi and Y. Ota, On the confluent property of right-ground term rewriting
systems, to appear.
[9] M. Oyamaguchi, On the Church-Rosser property of nonlinear and nonterminating term
rewriting systems, LA Symp (Summer) (1992).

[10] M. Ogawa, Chew’s theorem revisited: uniquely normalizing property of nonlinear term
rewriting systems, Lecture Notes in Comput. Sci. 650 (Springer-Verlag, 1992) 309-318.