数理解析研究所講究録
第 833 巻 1993 年 65-68

65

J. Yamada: WN TRSs

RIMS K\^okyuroku

On the Confluence of Weakly Normalizing TRSs *(Note)
山田順之介

Junnosuke Yamada
NTT Communication Science Laboratones
Hikari-dai, Seika-cho, Soraku-gun, Kyoto 619-02 Japane-mail: junQnttlab. ntt. jp

abstract
This note investigates the confluence(CONF) and unique normal form property w.r. .
$t$reduction$(UN^{arrow})$of weakly normalizing(WN) TRSs. The main devices are the transforma-tion of WN TRSs into a kind of membership conditional TRSs called normalized MCTRSs,
and the observation of critical pairs in them. By these two, it becomes possible to determine$UN^{arrow}$of WN TRSs, and it seems promising to extend them for detections of CONF.

1. Introduction.

TRSs are ubique scheme as formal models of functional programming languages, automated theorem
proving, and program synthesis/transformation/verification. The research on TRSs focuses to show their two
important properties, namely, confluence(CONF) and normalizability. As for the latter property, there exist
two subproperties, i.e., strongly and weakly normalizing(SN and WN). SN means every reduction sequence

is not infinite and WN does every term has at least one finite sequence from it. Oftenly, it is difficult toshow TRSs to be SN and it happens that TRSs are only WN. Thus, we aim to propose a method to detect

CONF for WN TRSs.
The following TRS defines factorial$R:\{ff_{x}$$f$on the set of natural numbers $\mathcal{N}=\{0, sO, s^{2}0, \cdots\}$ .

$pth_{emultiplicationdenoted_{asso}}^{aconstant,sthe}bo_{y^{is}}*th_{infixnotati\circ nwithright}^{epredecessor,and^{successor}’}$ciativity.

This

$R$

is WN but non-SN, as is illustrated by the next two reduction sequences:$fs^{2}xarrow s^{2}x*fps^{2}xarrow s^{2}x*ps^{2}x*fp^{2}s^{2}xarrow ps^{2}x*p^{2}s^{2}x*fp^{3}s^{2}xarrow\cdots$$fs^{2}xarrow s^{2}x*fps^{2}xarrow ins^{2}x*fsxarrow s^{2}x*sx*fpsxarrow ins^{2}x*sx*fx$$wherearrow in^{S})$$(\infty)$,(finite)are innermost reductions.

The author came to an idea to approximate WN TRSs by a kind of MCTRSs[6]. But soon [1] appeared

and executed research in this direction to a full extent based the one for typed$\lambda$-calculi[3]. Though [6]objected Knuth-Bendix like completion of first order TRSs, and this note is in its direction.

Anothermotivation of this note is to make non-overlapping in [4] more precise. Because it is mentioned only as
similar to unconditional case...”*This note is based on the presentation at RIMS, Kyoto University on 1st February 1993.

$($66J. Yamada: WN TRSsRIMS K\^okyuroku

2. Preliminaries.

First of all, some necessary notions are defined. For general notions and facts, please refer to someliterature, e.g., [2].

Definition. A TRS$R$isconfluent(CONF), iff$\forall t,$$s$[$(t\underline{*}s$uniquely normalizing(UN), iff$\forall t,$

A$t,$$s\in NF)\Rightarrow t\equiv s$$s[(t\underline{*}s\wedge t, s\in NF)\Rightarrow t\equiv s])$uniquely normalizing $w.r.t$ . $reduction(UN^{arrow})$ , iff

where$\underline{*}$],$\forall t,$$s_{1},$and,$s_{2}[(tarrow^{*}s_{j}\wedge s_{1}, s_{2}\in NF)\Rightarrow t\equiv s]$.

is the transitive, reflexive and symmetric closure $ofarrow$ . Now, the relationship between these threeproperties is noticed:

CONF$\subset$UN$\subset UN^{arrow}$.

For the simplicity, the next additional as sumption will be added:

Assumption.

$WN\wedge\forall t,$$s\in T[(tarrow^{*}s\wedge s\in NF)\Rightarrow tarrow in*s]$.

$(*)$

The membership conditional TRS (MCTRS) is a kind of TRS, whose rules are attached with themembership conditions on their variables. In a MCTRS, rules are applied only when membership conditions

on their variables hold. The membership conditions are assumed to be decidable apart from the reduction
relations to prevent from their harmful interferences. More details can be found in [4] and [7].
The notion of normalized MCTRS was originally introduced in [4] to prove that non-left-linear(LL)
and non-overlapping(OVLP) MCTRSs are CONF. The normalized MCTRS$R=(T,$$arrow\rangle$$R_{nf}=\langle T, arrow nj\rangle$for a TRS

can be obtained by posing the membership condition to the set of normal forms(NF) on theevery variable in its rules, as is exemplified below:$R:\{\begin{array}{l}f0\triangleright 1fx\triangleright x*fpxpsx\triangleright xspx\triangleright x\end{array}$$\Rightarrow$$R_{nf}$:$\{\begin{array}{l}f0\triangleright 1fx\triangleright x*fpxpsx\triangleright xspx\triangleright x\end{array}$$x\in N^{x}F^{\in NF}x\in NF$

A fact on CONF of MCTRSs is quoted, and it will be utilized in the next section.
Fact. (Toyama[5]) For MCTRSs, $quasi- LL\wedge non- OVLP\Rightarrow CON$F.

A MCTRS is called quasi-LL iff every non-linear variable in LHS of every rule is restricted by some
non-trivial membership condition. Thus every normalized MCTRS is quasi-LL.

3. CONF and$UN^{arrow}$of Weakly Normalizing TRSs.

Preliminarily, the correspondence between TRSs and their normalized MCTRSs is stated. The former
part of the next lemma is clear from the definition $ofarrow nj$ , and immediately the latter follows.

Lemma.

$arrow\supsetarrow_{n}f$and $NF(arrow)\subset NF(arrow_{nj})$ .

From the assumption $(*)$ and this lemma:
Lemma. Let$R$

be a WN TRS satisfying $(*)$ . Then$t_{1}arrow t_{2}arrow\cdotsarrow t_{k}arrow t\sim\in NF(arrow)$$\Rightarrow t_{1}arrow nft_{2}’arrow nj$$arrow nf^{t_{l}’}arrow nft\sim\in NF(arrow nf)$.

67
J. Yamada: WN TRSs

RIMS K\^okyuroku

After these preparations, central device of this note and main result are presented.

Definition. Let$\{x_{j}/t_{j}\}$.

for $j=1,2$ be rules overlapping at $u\in O(l_{1}),$$l_{j}\triangleright r_{j}$$(P\sigma, Q\sigma\rangle :x_{1}’\in NF, \cdots x_{n}’)\in NF$

the $CP$ at$\langle P, Q\rangle$

is a normalized $CP$ (at u) wheresuch that $x_{1}’\in NF\wedge\cdots$ A $x_{n}’\in NF$ implies$\bigwedge_{i}x_{i}\sigma\in NF$

A$\bigwedge_{j}t_{j}\sigma\in NF$$\sigma$$u$$u$$\theta=$

is a most general substitution, where $\{x_{1}’, \cdots , x_{n}’\}=Var(Im(\sigma))$ .

It can be easily understood that a classical CP may have multiple$\sigma’ s$and normalized CPs. Therefore,

all the normalized CPs of $Rj$ is all the ones derived from any CP of original TRS$\bigwedge_{\mathfrak{i}}x_{i}\in NF\wedge\bigwedge_{j}t_{j}\in NF$

with the m.g. .

$R$. As the condition

cannot appear in normalized MCTRSs, CPs with such conditio $ns$ must be interpreted

as equivalent sets of normalized CPs defined here.
An example of generation of normalized CPs is demonstrated for the normalized MCTRS below:$R_{mf}$:$\{\begin{array}{l}fx\triangleright fgxfgx\triangleright gxgfx\triangleright gxg^{2}x\triangleright gx\end{array}$$x\in NFx\in NFx\in NFx\in NF$:

on the set of terms $T=(\{f^{1}, g^{1}, h^{1}\}, V)$ where the superfixes of function symbols denote their arities and$V$

does the set of variables.
The first two rules of $Rf$ overlap at root and a conventional

have normalized $CP,$$\sigma’ s$$CP\langle gx, fg^{2}x\rangle$is generated from $fgx$ . To

must be found under $x\in NF\wedge gx\in NF$ and the LHSs of rules in$R_{nj}$are obeserved

by a method similar to covering set induction. For this case, $\{x/hz\}$ with $x\in NF$ is only possible:$\langle ghz, fg^{2}hz\rangle$

Theorem. Let$R$$R_{nj}$$z\in NF$

be a WN TRS satisfying the condition $(*)$ , and $Rf$ the normalized MCTRS of$R_{nf}$Proof.

:

has no normalized CP$\Rightarrow R_{nf}$is CONF and$R$

is$UN^{arrow}$.

.

is non-OVLP from the absence of normalized CP, and obviously $Rf$ is always quasi-LL. Thenby the fact by Toyama,$R_{mj}$is CONF. Let $tarrow^{*}t_{j}\in NF(arrow)$ for $j=1,2$ . These$t_{j}’ s$exist by $WN$ oflemmas an $d(*)$ , there are reduction sequences $tarrow^{*}nft_{j}\in NF(arrow_{n}f)$ for $j=1,2$ andThus $R$ is$R$$UN^{arrow}$$t_{1}\equiv t_{2}$by$R$. By$UN^{arrow \mathfrak{n}f}$.

.

If the TRS under discussion fulfills some stronger demands on it as $(**)$ in the remark below, then wehave:
Corollary. If every normalized CP converges in $Rf$ , then$R$

is CONF.

Once this corollary is obtained, Knuth-Bendix like completion becomes possible by adding normalized
CPs to original systems as [7]:$R$

$R_{nf}$:$WN\Downarrow+etc$.

: the normalized MCTRS of$==\Rightarrow$$R$

but it is still open which of properties of original$\Rightarrow$$R$$R’$: obtained $by_{\Uparrow}dropping\in NF’ s$$R_{nf}’$: completed

are preserved for $R’$ .

Remark.
Even if $Rf$ is known to be CONF, much stronger assumption seems to be necessitated for

$R$

to be

CONF, for example:$\forall t,$$s\in T[(tarrow t_{1}arrow t_{2}arrow\cdotsarrow t_{k}arrow s\wedge s\in NF)\Rightarrow tarrow_{in}t_{1}’arrow\iota_{n}t_{2}’arrow in .

.

.

arrow int_{l}’arrow ins]$$(**)$

68
RIMS K\^okyuroku

J. Yamada: WN TRSs

where$\{t_{1},t_{2}, \cdots , t_{k}\}\subset\{t_{1}’, t_{2}’, \cdots , t\}\}$Furthermorein$R_{nj}$.

is only $WN$ and not necessarily $SN$ , because not all the innermost reduction sequences

are not guaranteed to terminate.

$R$Discussion.
Here, the result above is compared with the preceding results in [1] and [5]. In this note, the following(1) $-(4)$ hold for the relationship $betweenarrow andarrow nj^{;}$(1) $arrow is$ WN and $(**)$ for CONF $ofarrow$ ( $(*)$ for
(2)

(3)

$arrow nf$$UN^{arrow}$),is CONF,$\underline{*}\supsetarrow nj$)

and(4) $NF(arrow)\subset NF(arrow nj)$ .

On the other hand, (3’)$ofarrow$$\underline{*}\subset\underline{*}nj$

in both [1] and [5], and (4) $NF(arrow)=NF(arrow_{nj})$ in$[5]^{**}$for $CONF$.

Thus, our result is not in cluded in either of [1] and [5], but it assumes a much stronger condition $(**)$ .
It will be desirable to relax $(**)$ and to find some result which is applicable for more wider cases.

References.
[1] J.-L. Curien, G. Gehlli : Confluence of WN TRS, Springer LNCS 488 (1991), pp.215-225.
[2] J. W. Klop : Term Rewriting Systems, in S. Abramsky et al. (eds.): Handbook of Logic in Computer Science,
Vol.2, Oxford, 1992.
[3] G. Pottinger : The Church Rosser Theorem for the Typed Lambda C alculus with Surjective Pairing, Notre
Dome Journal of Formal Logic 22 (1981), pp.264-268.
[4] Y. Toyama : Membership Conditional TRS, Springer LNCS 308 (1988), pp.228-244 : also in IEICE Japan
E72 (1989), pp.1224-1229.
[5] Y. Toyama: How to P rove Equivalence of Term Rewriting Systems without Induction, Theoretical Computer
Science 90 (1991), pp.369-390[6] J. Yamada: Confluence of WN TRSs, personal memorandum, April 1991 or around.
[7] J. Yamada: Confluence of Terminating Membership Conditional TRSs, Springer LNCS 656 (1993), pp.378392.

$**$[5] has proven more stronger results on equivalence relations, and corollary 3.2 deduces CONF in a similar setup.