数理解析研究所講究録
918 巻 1995 年 109-117

109

NVNF-sequentiality of Left-linear Term Rewriting Systems
Masahiko Sakai Yoshihito Toyama
Takashi Nagaya
School of Information Science, JAIST
Tatsunokuchi, Ishikawa, 923-12, Japan-mail: {nagaya, sakai,}$\mathrm{t}\mathrm{o}\mathrm{y}\mathrm{a}\mathrm{m}\mathrm{a}$$\mathrm{e}$$@\mathrm{i}^{\mathrm{a}\mathrm{i}}\mathrm{S}\mathrm{t}.\mathrm{a}\mathrm{c}.\mathrm{j}\mathrm{P}$Abstract-sequentiality defined by Oyamaguchi
This paper introduces an extension ofin [6]. We call the extension NVNF-sequentiality. It is showed that the class of-sequential systems, and
NVNF-sequential systems properly includes the class of
a indices with respect to NVNF-sequentiality are computed for a given term when aterm rewriting system is NVNF-sequential.
$\mathrm{N}\mathrm{V}$$\mathrm{N}\mathrm{V}$1

introduction

Term rewriting systems can be regarded as a model for computation in which terms are
reduced using a set of directed equations, called rewrite rules. Term rewriting systems
play an important role in various fields of computer science such as abstract data typespecifications, implementations of functional programming languages and automated deduction.
In a term rewriting system, there are possibilities that a term having normal forms has
infinite reduction sequences starting with it. We require some strategies telling us whichredex to contract in order to get the desired result. Therefore, it is important to havea normalizing strategy which is guaranteed to find the normal form of terms whenevertheir normal forms exist. Huet and L\’evy [2] showed that the needed reduction strategy
is normalizing for every orthogonal (i.e., left-linear and non-overlapping) term rewriting
system. The needed reduction strategy always rewrites one of needed redexes which haveto be rewritten in order to reach a normal form. Unfortunately, it is undecidable ingeneral whether a redex is needed or not. However, they show that for strong sequential
orthogonal term rewriting systems at least one of the needed redexes in a term not innormal form can be efficiently computed. The work of Huet and L\’evy was extended toseveral kinds of systems. Toyama [8] extended the notion of strong sequentiality to leftlinear term rewriting systems. Decidability of strong sequentiality was showed for leftlinear systems by Jouannaud and Sadfi [3]. Oyamaguchi [6] introduced NV-sequentiality
which is also decidable.
-sequentiality. This sequentiality is
In this paper, we introduce an extension of-sequentiality, NVNF-sequentiality is based on
called NVNF-sequentiality [5]. Like
the analysis of left-hand sides and the non-variable parts of the right-hand side of rewrite$\mathrm{N}\mathrm{V}$$\mathrm{N}\mathrm{V}$110rules. However, the reachability to the normal form is considered in NVNF-sequentiality.
We first show that the class of NVNF-sequential systems properly includes the class of-sequential systems. Next we prove that, for a given term , it is decidable whether
an occurrence in is an index with respect to NVNF-sequentiality. This problem canbe reduced to the problem to decide whether a term has a normal form for left-linear
and right-ground term rewriting systems. When a term rewriting system is left-linear
and right-ground, there exists an upper bound of the least hight of normal forms whicha term can reduce to if has a normal form. The reachability problem for left-linear
and right-ground term rewriting systems has been shown to be decidable in $[1, 7]$ . Hencean index with respect to NVNF-sequentiality can be computed.
$\mathrm{N}\mathrm{V}$

$t$

$t$

$u$

$t$

2

$t$

Definition

We mainly follow the notation of $[2, 4]$ . Let be a finite set of function symbols andlet be a countably infinite set of variables where. The set of all terms built
from $F$ and is denoted. The setis sometimes denoted by . Terms
not containing variables are called ground terms. Identity of terms is denoted by .
For any term , we define the set $O(t)$ of occurrences as follow:$\mathcal{F}$$\mathcal{V}$$\mathcal{F}\cap \mathcal{V}=\phi$$\mathcal{V}$$\mathcal{T}(F, \mathcal{V})$$\mathcal{T}$$\mathcal{T}(\mathcal{F}, \mathcal{V})$$\equiv$$t$,
if
if $t\equiv F(t_{1}, \ldots, t_{n})$ .
$t\in \mathcal{V}$$\{\epsilon\}$$O(t)=\{$$\{\epsilon\}\cup\{i.u|1\leq i\leq n, u\in O(t_{i})\}$

If $u\in O(t)$ then the subterm $t/u$ of at
$t$

$t$

$t/u\equiv\{$$t_{i}/v$$u$

is defined by,
if
if $t\equiv F(t_{1}, \ldots,t_{n})$ and $u=i.v$ .
$u=\epsilon$

If is a subterm of then we write. If $u\in O(t)$ then the term $t[uarrow s]$ obtained$t/u$
by replacingwith is defined as follow:
$t$

$s$

$s\subseteq t$

$s$

,
if
if $t\equiv F(t_{1}, \ldots,t_{n})$ and $u=i.v$ .
$u=\epsilon$$s$$t[uarrow s]\equiv\{$$p(t_{1}, \ldots,t_{i[v}arrow s], \ldots,t_{n})$Occurrences are partially ordered by the prefix ordering , i.e. $u\leq v$ if there exists
such that $u.w=v$ . In this case we define $v/u$ as . If
andthen we say$u\perpv$
that and are disjoint, and write,. If
are pairwise disjoint, we use$t[u_{i}arrow s_{i}|1\leq i\leq n]$ to denote.
A substitution is a mapping from into
. Substitutions are extended intohomomorphisms frominto
. In following we write instead of .
A term rewriting system is a pairconsisting of a setof function symbols
and a finite set of rewrite rules. A rewrite rule is a pairof terms such thatand any variable in also occurs in . We write $larrow r$ for. An instance of a left-handside of a rewrite rule is a redex. The rewrite rules of a term rewriting systemdefine a reduction relationon
as follow: $tarrow ns$ if there exist a rewrite, a occurrence $u\in O(t)$ and a substitution such that
rule
and
$w$

$\leq$$u$$v$$u_{1},$$\ldots$$v\not\leq u$$u\not\leq v$$w$$u_{n}$$t[u_{1}arrow s_{1}]\cdots[u_{n}arrow s_{n}]$$\theta$$\mathcal{V}$$\mathcal{T}(\mathcal{F}, \mathcal{V})$$t\theta$$\mathcal{T}(F, \mathcal{V})$$\mathcal{T}(\mathcal{F}, \mathcal{V})$$(F,\mathcal{R})$$\mathcal{R}$$\langle l,r\rangle$

$l$

$r$

$\theta(t)$$\mathcal{F}$$l\not\in \mathcal{V}$$\langle l,r\rangle$$(\mathcal{F},\mathcal{R})$$arrow n$$larrow r\in \mathcal{R}$$\mathcal{T}(\mathcal{F}, \mathcal{V})$$\theta$$t/u\equiv l\theta$

111.
denotes theis denoted. A normal form
denotes the reflexive closuretransitive closure
for some normal form
is a term without redexes. We say has a normal form if. When no. The set of normal forms of a term rewriting system is denoted by
confusion can arise, we omit the subscript .
, every variable in occurs
A term rewriting system is left-linear if for any
left-linear term rewriting
class
of
to
the
restrictourselves
paper
we
this
only once. In
systems.
$s\equiv t[uarrow s]$. The transitive-reflexive closure of$\mathrm{b}\mathrm{y}arrow^{*}R$$arrow n$$-_{R}^{+}$$\mathrm{o}\mathrm{f}\sim_{R}$$\mathrm{o}\mathrm{f}-R\mathrm{a}\mathrm{n}\mathrm{d}arrow\overline{\overline{\overline{R}}}$$t\sim_{R^{S}}^{*}$$t$$\mathcal{R}$$\mathrm{N}\mathrm{F}_{R}$$s$$\mathcal{R}$$larrow r\in \mathcal{R}$$\mathcal{R}$3$l$

NVNF-sequentiality

In this section we will explain NVNF-sequentiality. In order to define this concept, weneed some preliminaries.
Let be a new constant symbol representing an unknown part of a term. The set
are called -terms. An -normal. Elements ofis abbreviated to.
form is an -term without redexes, and the set of all -normal forms is denoted bydenotesare said to be normal form.
Only terms containing neither redexs nor
the -term obtained from by replacing all variables in by , and denotes the term
denotes the set of -occurrences of , i.e.
obtained from by replacing all by .
$O_{\Omega}(t)=\{u\in O(t)|t/u\equiv\Omega\}$ . The prefix ordering
is defined as follows:$\Omega$$\mathcal{T}(\mathcal{F}\cup\{\Omega\}, \mathcal{V})$$\Omega$$\Omega$$\mathcal{T}_{\Omega}$$\mathcal{T}_{\Omega}$$\Omega$$\Omega$$\mathrm{N}\mathrm{F}_{\Omega}$$\Omega’ \mathrm{s}$$t_{\Omega}$$\Omega$$t$$t$$\Omega$$\Omega$$t$$x$$t_{l}$$t$$\Omega$$O_{\Omega}(t)$$\leq \mathrm{o}\mathrm{n}\mathcal{T}_{\Omega}$(i)$\Omega\leq t$

for all$t\in T_{\Omega}$

,

(ii)

$F(s_{1,\ldots,n}s)\leq F(t_{1}, \ldots, t_{n})$(iii)$x\leq x$

for all$x\in \mathcal{V}$

if $s_{i}\leq t_{i}(1\leq i\leq n)$ ,.

, if there exists an -term
Two -terms and are compatible, writtenthat $t\leq r$ and $s\leq r$ . In this case the least upper bound of and is denoted by$t$$\Omega$$\Omega$$t\uparrow s$

$s$

$t$

Let be a predicate on . An
Definition 3.1 (respect to if for all -term $s\geq t$ and $P(s)$ imply$P$$[2]\rangle$$P$$\Omega$$\mathcal{T}_{\Omega}$$\Omega$$s$-occurrence$s/u\not\equiv\Omega$

$s,$

.

$u$

$r$

such

$t\mathrm{U}s$.

of is index with$t$

The set of indices of with respect to $P$ is denoted by $I_{P}(t)$ . Intuitively, if is anindex with respect to $P$ in , then the term at has to been evaluated in order to makethe predicate $P$ true.
$u$

$t$

$u$

$t$

Definition 3.2$([6]\rangle$(1) The reduction relation is defined as follow: $t-_{nv}s$ iff there exists.
$u\in O(t)$ such thatand $s\equiv t[uarrow s’]$ for some$\mathcal{T}_{\Omega}$,$s’\geq r_{\Omega}$$t/u\geq l_{\Omega}$(2) The predicate nvnf on
normal form.

$larrow r\in \mathcal{R}$as follow: nvnf$(t)$holds iff$tarrow_{nv}^{*}s$

for some$s$Definition 3.3 A left-linear term rewriting system is NVNF-sequential if every
normal form containing at least one occurrence of has index with respect to nvnf.
$\Omega$in$\Omega-$112

In definition offor some$\mathrm{N}\mathrm{V}$-sequentiality, a predicate term is used, where term $(t)$ holds iff. Note that may be a reducible term.

$s\in \mathcal{T}$$tarrow_{nv}^{*}s$

Example 3.4

$s$

Let
$F(A, B, x)arrow A$$F(B, x, A)arrow B$$\mathcal{R}=\{$$F(x,A, B)arrow C$$Carrow C$

Consider the -term-term such that $s\geq t,$
is not-sequential since$\Omega$$\Omega$.

. $I_{nvnf}(t)=\{1\}$ because there does not exist anandfor some normal form . Note thathas no indices with respect to the predicate term.

$t\equiv F(\Omega, \Omega, \Omega)$$s$$\mathrm{N}\mathrm{V}$$s/1\equiv\Omega$$s’$$s\sim_{nv}^{*}s’$$\mathcal{R}$$F(\Omega, \Omega, \Omega)$

Next we show thatin Example 3.4 is NVNF-sequential system. For this purpose
we need the following lemma.
$\mathcal{R}$Lemma 3.5

Let$t\in \mathcal{T}_{\Omega}$. If $u\in I_{nvnf}(t),$$t\leq s$and$s/u\equiv\Omega$then $u\in I_{nvnf^{()}}s$ .

Proof. If $u\not\in I_{nvnf}(S)$ then there exists $s’\geq s$ such that $s’/u\equiv\Omega$ and nvnf $(s’)$ istrue. Since $s’\geq t,$ $u\not\in I_{nvnf}(t)$ .
$\square$Lemma 3.6

72 of Example 3.4 is NVNF-sequential system.

Proof. We first prove the following claim: If $u\in I_{nvnf}(t)$ and $v\in I_{nvnf^{()}}s$ then$u.v\in I_{nv}nf^{(}t[uarrow s])$.

Proof of the claim. Suppose $u.v\not\in I_{nvnf^{(}}t[uarrow s])$ . Then there exists $t’\geq t[uarrow s]$
such that $t’/u.v\equiv\Omega$ and nvnf $(t’)$ is true. Hence there exists a reduction$t’ \equiv t_{0}-u_{0}nvt_{1}\frac{u_{\mathrm{t}}}{},nv$. ... .

$u_{n-1 ’arrow nv}t_{n}\in \mathrm{N}\mathrm{F}$.

We distinguish two case:(1)
for all $i(0\leq i\leq n-1)$ . Because there exists nosuch that $u_{i}<u$ ,we have. Hence nvnf $(t’/u)$ is true. Clearly $t’/u>s$ and$t’/u.v\equiv\Omega$ . This contradicts theassumption $v\in I_{nvnf}(s)$ .
(2) $u_{i}<u$ for some . Let be the smallest number satisfying $u_{j}<v$ . Note that$t’/uarrow^{*}nvt_{j}/u$ .
is a redex but. Moreoverandbecause $t’/u\geq s,$ $t’/u.v\equiv\Omega$ and $v\in I_{nvnf}(s)$ . Thus
. We canobtain the following reduction: $t’[uarrow\Omega]arrow^{*}t_{j}[nvuarrow\Omega]arrow_{nv}t_{j+1}arrow^{*}nvt_{n}$ . Hence$t’[uarrow\Omega]\geq t$ ,nvnf $(t’[uarrow\Omega])$ is true. But this is contradictory to $u\in I_{nvnf}(t)$ .
Therefore the claim follows.
Let be an -normal form containing at least one occurrence of . We prove, by
induction on size of that has an index with respect to nvnf. When, it is clearthat has an index. Induction step:$u_{i}\not\simeq u$$u_{i}$$t’/uarrow^{*}nvt_{n}/u\in \mathrm{N}\mathrm{F}$

$i$

$j$

$t_{j}/u_{j}$$t_{j}/u_{j}\not\equiv C$$t_{j}\not\equiv A$$t_{j}\not\equiv B$$t_{j}[uarrow\Omega]-_{nv}u_{j}t_{j+1}$$t$$\Omega$$\Omega$$t$$t\equiv\Omega$

$t$

$t$

(1)

. If

contains then by induction hypothesis, has an index.
By
and Lemma 3.5,
. Therefore, fromthe claim it follows that has an index. Otherwise we distinguish three cases:$t\equiv F(t_{1}, t_{2,3}t)$$\Omega$$t_{1}$$t_{1}$$1\in I_{nvnf}(F(\Omega, \Omega, \Omega))$$1\in I_{nvnf}(F(\Omega,t2, t\mathrm{s}))$

$t$

113

. If contains then by induction hypothesis, has an index.
(1-1)
By $2\in I_{nvnf}(F(A, \Omega, \Omega))$ and Lemma 3.5, $2\in I_{nvnf}(F(A, \Omega,t_{3}))$ . From thecontains . By induction hypothesis,
claim, has an index. Otherwise$3\in
I_{nvnf}(F(A,t_{2},\Omega))$ . Therefor by the claim,
has an index. We can obtainhas an index.
. Similar to (1-1).
(1-2)(1-3) Otherwise we have $I_{nvnv}(F(t1, \Omega, \Omega))=\{2,3\}$ . By induction hypothesis,or has an index. By Lemma 3.5 and the claim, has an index.
(2) $t\equiv G(t_{1}, \cdots,t_{n})(G\neq F)$ . Suppose contains . Then by induction hypothesis,
has an index. Because $i\in I_{nvnf}(c(t1, \cdots,t_{i}-1, \Omega,ti+1, \cdots , t_{n})),$ has an index
from the claim.
$t_{1}\equiv A$$\Omega$$t_{2}$$t_{2}$$t$$\Omega$$t_{3}$$t_{3}$$t$$t_{1}\equiv B$$t_{2}$$t$$t_{3}$$\Omega$$t_{i}$$t$$t_{i}$$\square$By Example 3.4 and Lemma 3.6 we have the following theorem.

Theorem 3.7 The class of NVNF-sequential term rewriting systems properly includes
the class of $NV$-sequential systems.

-sequential system is NVNF-sequential because an index with respect to
Proof.
of Example 3.4 is NVNF-sequential but
term is also an index with respect to nvnf.
proper.
isinclusion
theTherefore-sequential.
not$\mathrm{N}\mathrm{V}$$\mathcal{R}$$\square$$\mathrm{N}\mathrm{V}$4

Indices with respect to NVNF-sequentiality

is an, it is decidable whether
In this section we show that for a given
which is given in [6].
index with respect to nvnf in . We introduce the$u\in O_{\Omega}(t)$$t\in \mathcal{T}_{\Omega}$$t$$\mathrm{r}\mathrm{e}\mathrm{d}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}arrow\omega$

Definition 4.1 ([6]) The reduction$u\in O(t)$ such thatexists$relat\dot{i}on\sim_{\omega}$$t/u\uparrow l_{\Omega},$$larrow r\in \mathcal{R},$is defined as follows:.
and$tarrow_{\omega}s$

iff there$s\equiv t[uarrow r_{\Omega}]$$t/?\mathrm{A}\not\equiv\Omega$

We explain a relationship between this’ and show the condition
for ensuring that -occurrence is an index with respect to nvnf.
$\mathrm{r}\mathrm{e}\mathrm{d}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{i}_{0}\mathrm{n}arrow \mathrm{a}\omega \mathrm{n}\mathrm{d}-\tau\iota v$$\Omega$Lemma 4.2

If(2) If(1)$t-_{nv}^{*}s$$tarrow^{*}s\omega$

and $t’\leq t$ then$t’\sim_{\omega}^{*}s’$for some$s’\leq s$.

then $t’arrow^{*}snv$ for some $t’\geq t$ .

Proof.

for some $s’\leq s$ . If $tarrow_{nv}s$$u\in O(t)$ such thatand $s\equiv t[uarrow s_{1}]$ forthen there exist
and. Hencethen. If $u\in O(t’),$some$t’[uarrow r_{\Omega}]\leq s$ . Otherwise it is clear that $t’\leq s$ . Using this fact, we can prove (1)by induction on length of $tarrow^{*}snv$ .

(1) We prove that if $tarrow nvs$ and $t’\leq t$ then$larrow r\in \mathcal{R},$$s_{1}\geq r_{\Omega}$$t’/u\not\equiv\Omega$$t’-_{\omega}^{\equiv}s’$$t/u\geq l_{\Omega}$$t’/u\uparrow l_{\Omega}$$t’-_{\omega}t’[uarrow r_{\Omega}]$

114

(2)

This is proved by induction on length of. The case of zero is trivial.
Assume that
where
and
for
some
and $u\in O(t)$ . Rom induction hypothesis, for some,
. Let
. Define. Because,$t’\equiv s_{2}[uarrow t_{1}]\geq t$ . We have $t’\sim_{nv}s_{2}$ by. Therefore.
$t-_{\omega}^{*}s$$t/u\uparrow l_{\Omega},$$tarrow_{\omega}s_{1}arrow_{\omega}^{*}s$$t/u\not\equiv\Omega$$s_{1}\equiv t[uarrow r_{\Omega}]$$larrow r\in \mathcal{R}$$s_{2}arrow^{*}Snv$$s_{2}\geq s_{1}$$t’\equiv s_{2}[uarrow t_{1}]$$t_{1}\equiv t/u\mathrm{u}l_{\Omega}$$s_{2}\geq s_{1}\equiv t[uarrow r_{\Omega}]$$s_{2}/u\geq r_{\Omega}$Let
and $u\in O_{\Omega}(t)$ . Let$u\not\in I_{nvnf}(t)$such that
iff there exists

Lemma 4.3

$t\in \mathcal{T}_{\Omega}$$\bullet$$t’arrow_{nv}^{*}s$

be a fresh constant symbol.
and.

$t[uarrow\bullet]-_{\omega}^{*}s$$s\in \mathrm{N}\mathrm{F}_{\Omega}$$\square$Then$\bullet\not\subset s$

Proof.

only-if part. If $u\not\in I_{nvnf}(t)$ then there exists $t’\geq t$ such that $t’/u\equiv\Omega$ andand left-linearity,nvnf is true. Thus $t/-_{nv}*s’$ for some normal from . From
we can obtain $t’[uarrow\bullet]arrow^{*}nvs’$ and. Using Lemma 4.2 (1), we obtain $s\leq s’$ suchthat $t[uarrow\bullet]-_{nv}^{*}s$ . Because is a normal form, is an -normal form and.
$t’\geqt[uarrow\bullet]$, then there exists
andsuch that
if part. If$t’arrow^{*}Snv$ by Lemma 4.2 (2). Let. We can transform the reduction$t’-_{nv}^{*}s$ into
. Because is an normal from, ’ is a normal form and henceis true. Clearly $t”\geq t$ and $t”/u\equiv\Omega$ . Therefore $u\not\in I_{nvnf}(t)$ .
nvnf
$(d)$

$s’$

$\Omega\not\subset s’$$\bullet\not\subset s’$$s’$$\Omega$$s$$t[uarrow\bullet]\sim_{\omega}^{*}s\in \mathrm{N}\mathrm{F}_{\Omega}$$\bullet\not\subset s$$\bullet\not\subset s$$t”\equiv t_{x}’[uarrow\Omega],$ $s’\equiv s_{x}$$t^{N}-_{nv}^{*}s’$$\Omega$$s$$s$$(t\prime\prime)$$\square$, there exists an upper bound of the least hight of
Next we show that for any-normal form which can reduce
when it exists.
$Rh_{R}$ is defined with $Rh_{R}=\{r_{\Omega}|larrow r\in \mathcal{R}\}$ ,For given a term rewriting system
and $Rhn_{R}$ is the smallest set such thatand if $t\in Rhn_{R},$ $u\in O(t)$ and$r\in Rh_{R}$ then $t[uarrow r]\in Rhn_{R}$ . It is clear that if $r\in Rh_{R}$ andthen $t\in Rhn_{R}$ .
In the sequel we often omit the subscript .
$t\in \mathcal{T}_{\Omega}$$\Omega$$t$$\mathrm{b}\mathrm{y}-_{\omega}$$\prime \mathcal{R},$$Rh_{R}\subseteq Rhn_{\mathcal{R}}$’$r-_{\omega}^{\mathrm{s}}t$$\mathcal{R}$Lemma 4.4 Ifthen there exists
and the following conditions hold.
(i) $s\equiv t[u_{i}arrow s/u_{i}|1\leq i\leq n]$ ,(ii)
for some$tarrow+_{S}\omega$$t/u_{i}arrow_{\omega\omega^{S}}^{+*}r_{i}arrow/u_{i}$Proof. By$t-_{\omega}+s$$u_{1},$$\ldots,$$u_{n}\in O(t)$$r_{i}\in Rh_{\mathcal{R}},$

which are $pair.wi_{S}e$ disjoint,$1\leq i\leq n$.

, there exists a reduction$t \equiv t_{0}arrow_{\omega}u_{0}t_{1}\frac{u_{1}}{}.\omega\ldots..arrow\omega u_{n-1}t_{n}\equiv s(n>0)$Let$\{u_{i_{1}}, \ldots,u_{i_{k}}\}$$u_{i_{1}},$$\ldots$,$u_{i_{k}}\in O(t)$.

be the set of minimal redex occurrences of $\{u_{0}, u_{1}, \cdots,u_{n}-1\}$ . Thenare pairwise disjoint. By minimality ofhold.
$u_{i_{1}},$$\ldots,$ $u_{i_{k}},$$(\mathrm{i}),$$\square$$(\mathrm{i}\mathrm{i})$We use $|u|$ for the length of the word . The heightof an -term is defined by$|t|= \max\{|u||u\in O(t)\}$ . The maximum hight of the left-hand sides and right-handsides of a given is denote by. We write when confusion does not occur.
is a$uarrow\Omega|u\inO(t)$prefix term of whose hight is , i.e.,[
A $|u|=\rho$ ].
$|t|$

$u$

$\mathcal{R}$$\rho_{R}$$t$$\rho$$\rho$$\Omega$$t$$(t)_{\rho}$$(t)_{\rho}\equiv t$

Let $r\in Rh_{R},$where $|s|>\rho\cross n(n>0)$ . Then, there exists$\epsilon<u_{0}<\cdots<u_{n-1}\in O(s)$ and$i(0\leq i\leq n-1)$ , the following condition holds:
anyfor$r_{i}\in Rh_{R}$ .
and
some
for

Lemma 4.5

$rarrow^{*}\omega S[u_{i}arrow r_{i}]$$r\sim_{\omega}^{*}s$$r_{i}arrow^{*}s\omega/u_{i}$115

Proof. The proof is by induction on

$n$

. By

$rarrow_{\omega}^{*}s$, there exists a reduction.

.

$.arrow_{\omega}v_{1}v_{m-1t_{m}\equiv}s$$.,$$r\equiv t_{0}arrow_{\omega}v_{0}t_{1}arrow_{\omega}$.

Because $|s|>\rho\cross n(n>0)$ , we can obtain $j<m$ such that $t_{j}\in Rh_{R}$ andfor all $i(j\leq i\leq m-1)$ . When $n=1$ , using Lemma 4.4, we can easily show thatfor some
andthere exists $u\in O(s)$ such that$r-_{\omega}^{*}s[uarrow
r’]$
4.4,
.
Lemma
we can$n>1$.
SupposeUsing. By
and $|s/u|>\rho\cross(n-1)$ for somesuch thatobtain$r’\in Rh_{R}$ By induction hypothesis, there exists $\epsilon<u_{1}’<\cdots<u_{n-1}’\in O(s)$ and for any$i(1\leq i\leq n-1)$ , the following condition holds: $r’-_{\omega}^{*}(s/u)[u_{i}/arrow r_{i}]\equiv s[u.u_{i}’arrow r_{i}]/u$
for some $r_{i}\in Rh_{R}$ . Let $u_{0}=u,$ $u_{i}=u.u_{i}’(1\leq i\leq n-1)$ .
and. For allClearly $\epsilon<u_{0}<\cdots<u_{n-1}\in O(s)$ and $rarrow_{\omega}^{*}s[uarrow r’],$$i(1\leq i\leq n-1)$ , we haveand
. Therefore the lemma holds.
. By$v_{i}\neq\epsilon$$t_{j}arrow_{\omega}^{*}s[uarrow r’],$$u\neq\epsilon$$r’\in Rh_{\mathcal{R}},$$r’arrow^{*}\omega s/u$$r-^{\mathrm{s}}t_{j},$$t_{j}arrow_{\omega}^{*}s[uarrow r’],$$u\neq\epsilon$$r’\sim_{\omega}^{*}s/u$$r_{i}arrow_{\omega}^{*}(s/u)/u_{i}^{l}\equiv s/u.u_{i}’$$r’arrow_{\omega}^{*}s/u$$t_{j}arrow^{*}\omega s[uarrow r’]arrow_{\omega}^{*}s[uarrow s[u.u_{i}^{l}arrow r_{i}]/u]\equiv s[u_{i}arrow r_{i}]$$r_{i}-_{\omega}^{*}s/u_{i}$$rarrow^{*}trarrow^{*}\omega j,\omega s[u_{i}arrow r_{i}]$Lemma 4.6

Let$t,$ $s\in \mathrm{N}\mathrm{F}_{\Omega}$. If$\square$$(t/u)_{\rho}\equiv(s)_{\rho}$then$t[uarrow s]\in \mathrm{N}\mathrm{F}_{\Omega}$.

Proof. Nivial.

$\square$For given a term rewriting system$\tau=||\{(t)_{\rho}|t\in Rhn_{R}\}||,$

cardinality of a set
Lemma 4.7
$u\not\in I_{nvnf}(t)\dot{i}ff$$A$$\mathcal{R}$$\sigma=||R||$

.

, let
and

$\tau$, , and$\sigma$$k_{R}$

be constants defined as follow:, where $||A||$ is the$k_{R}=\rho_{R}\cross(\tau\cross\sigma+1)$

Let
and $u\in O_{\Omega}(t)$ . Let be a fresh constant symbol. Then
and.
there exists
such that $|s|\leq|t|+k_{R},$$t\in \mathcal{T}_{\Omega}$$\bullet$$t[uarrow\cdot]-_{\omega}^{*}s$$s\in \mathrm{N}\mathrm{F}_{\Omega}$$\bullet\not\subset s$

Proof. if part. By Lemma 4.3.
such that
only-if part. If $u\not\in I_{nvnf}(t)$ then by Lemma 4.3 there exists
and. Let be an -normal form with the least size satisfying this, we cancondition. Suppose $|s|>|t|+k_{R}$ . By Lemma 4.5 and the definition of$u_{2}\in O(s)(u_{1}<u_{2})$ such that,show that there exists $r\in Rh,$for $i=1,2$ , see Figure 4.1. Let $s’\equiv s[u_{1}arrow s/u_{2}]$ .
and,. Because the size of is smallerand
By Lemma 4.6,
than the size of , we obtain a contradiction.
$s\in \mathrm{N}\mathrm{F}_{\Omega}$$t[uarrow\bullet]arrow^{*}\omega s$$\bullet\not\subset s$$\Omega$$s$$k_{R}$$(s/u_{1})_{\rho}\equiv(s/u_{2})_{\rho}$$u_{1},$$t[uarrow\bullet]\sim_{\omega}^{*}s[u_{i}arrow r]$$r-_{\omega}^{*}s/u_{i}$$t[uarrow\bullet]-_{\omega}^{*}s’$$s’\in \mathrm{N}\mathrm{F}_{\Omega}$$s’$$\bullet\not\subset s’$$\square$$s$

By Lemma 4.7, in order to determine whether an -occurrence is an index w.r.t.
nvnf, we need to check the reachability to a finite number of -normal form. For a term
as follow [6]:rewriting system 72, we define$\Omega$$\Omega$$\mathcal{R}^{\Omega}$$\mathcal{R}^{\Omega}=\{larrow r_{\Omega}|larrow r\in \mathcal{R}\}\cup\{\Omegaarrow t|t\subseteq l_{\Omega}, larrow r\in \mathcal{R}\}$We can prove that in the condition of Lemmatransitive-reflexive closure of a usual reduction$4.7-_{\omega}^{*}$

Lemma 4.8 ([6])(1)

If$t-_{\omega}^{*}s$then$t-_{R^{\Omega}}^{*}s$.

can be$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}-n\Omega$.

$\mathrm{r}\mathrm{e}_{\mathrm{P}^{\mathrm{l}\mathrm{a}\mathrm{C}\mathrm{e}\mathrm{d}}\Omega}\sim^{*}R$defined by$\mathcal{R}^{\Omega}$which is the

.

116

$\Rightarrow$

Figure 4.1

(2)

If

Lemma 4.9
such thatand $t’\leq t$ then $t’-_{\omega}^{*}s’for$ some $s’\leq s$ .

$t\sim_{R^{\Omega}}^{*}s$Let$t\in \mathcal{T}_{\Omega}$$|s|\leq|t|+k_{\mathcal{R}},$and $u\in O_{\Omega}(t)$ . Then $u\not\in I_{nvnf}(t)\dot{i}ff$ there exists
and.

$t[uarrow\bullet]arrow^{*}R^{\Omega}s$$s\in \mathrm{N}\mathrm{F}_{\Omega}$$\bullet\not\subset s$

Proof. By Lemma 4.7 and Lemma 4.8$\square$

We assume that 72 is left-linear, so
is left-linear and right-ground (i.e. is groundterm for any). It is show that the reachability problem is decidable forleft-linear and right-ground systems $[1, 7]$ . Thus we obtain the following theorem.
$\mathcal{R}^{\Omega}$$r$$larrow r\in \mathcal{R}^{\Omega}$

Theorem 4.10 It is decidable, forrespect to nvnf in .

$t\in \mathcal{T}_{\Omega},$$u\in O_{\Omega}(t)$, whether$u$is an index with$t$References[1] M. Dauchet, S. Tison, T. Heuillard, and P. Lescanne, Decidability of The Confluenceof Finite Ground Term Rewriting Systems and of Other Related Term Rewriting
Systems, Information and Computation 88, pp.187-201, 1990.
[2] G. Huet and J.-J. L\’evy, Call by Need Computations in Non-Ambiguous Linear
Term Rewriting Systems, Report 359, INRIA, 1979; Computations in Orthogonal
Rewriting Systems, I and II, Computational Logic, Essays in Honor of Alan Robinson(eds. J.-L.Lassez, G.Plotkin), MIT Press, pp.396-443, 1991.

117[3] J.-P. Jouannaud and W. Sadfi, Strong Sequentiality of Left-linear Overlapping
Rewrite Systems, In Workshop on Conditional Term Rewriting Systems, Jerusalem,
July, 1994.
[4] J.W. Klop and A. Middeldorp, Sequentiality in Orthogonal Term Rewriting Systems,
Journal of Symbolic Computation 12, pp.161-195, 1991.
[5] T. Nagaya, M. Sakai and Y. Toyama, Decidability of Indices on NVNF-sequentiality
Term Rewriting Systems, IEICE Technical Report COMP94-63, Vol.94, No.354,

pp.87-94, 1994.
[6] M. Oyamaguchi, NV-Sequentiality: A Decidable Condition for Call-by-Need Computations in Term Rewriting Systems, SIAM Journal on Computation 22(1), pp.112135, 1993.
[7] M. Oyamaguchi, The Reachability Problem for Quasi-Ground Term Rewriting Systems, Journal of Information Processing 9, pp.232-236, 1986.
[8] Y. Toyama, Strong Sequentiality of Left-Linear Overlapping Term Rewriting Systems, Proceedings of the 7th IEEE Symposium on Logic in Computer Science,

pp.274-284, 1992.