JAIST Repository
https://dspace.jaist.ac.jp/
Title
項書換え系の簡略戦略に関する研究Author(s)
長谷, 崇Citation
Issue Date
1999‑03Type
Thesis or DissertationText version
authorURL
http://hdl.handle.net/10119/872Rights
Description
Supervisor:外山 芳人, 情報科学研究科, 博士by
Takashi NAGAYA
submitted to
Japan Advanced Institute of Science and Technology
in partial fulllment of the requirements
for the degree of
Doctor of Philosophy
Supervisor: Professor Dr. Yoshihito Toyama
Scho ol of Information Science
Japan Advanced Institute of Science and Technology
March 1999
Copyright c
1999byTakashi Nagaya
Term rewriting systems have b een widely studied as a mo del for computation. In a
termrewriting system,theymayexistaninnitereductionsequencestartingwithaterm
havingnormalforms. Inordertoget anormalformforagiventerm,werequireanormal-
izing strategy guaranteeing to nd a normal form of terms whenever their normal forms
exist. Huet andLevy(1979) showedthat acall-by-need strategy isnormalizingfor every
orthogonal (i.e., left-linearand non-overlapping)term rewriting systems. Unfortunately,
in general a call-by-need strategy is undecidable. They formalized strong sequentiality
guaranteeing adecidable normalizingcall-by-needstrategy for orthogonalterm rewriting
system. The workof Huet andLevy has been extendedto several kinds of systems.
In this thesis we rst extend the class of left-linear term rewriting systems having a
decidable call-by-need strategy. We present the class of NVNF-sequential systems. This
classproperlyincludestheclassofNV-sequentialsystemswhichwasintro ducedbyOyam-
aguchi(1993). We provethat everyorthogonal NVNF-sequential system has adecidable
normalizingcall-by-needstrategy. Thenwegivegrowingapproximationsoftermrewriting
systemswithouttheassumptionoftheright-linearitywhereasJacuemard(1993)assumed
theright-linearity. Weshowthatourapproximationsextend theclassoforthogonalterm
rewriting systems having a decidable normalizingcall-by-need strategy.
Secondly, we investigate the normalizability of a call-by-need strategy for left-linear
overlapping term rewriting systems. We rst intro duced the notion of stable balanced
joinability. Itisshownthatacall-by-needstrategyisnormalizingforeverystablebalanced
joinable strongly sequential system. This is a generalization of Toyama's result (1992).
Wenextintro ducethe notionofNV-stablebalanced joinabilityand provethateveryNV-
stable balanced joinable NV-sequential system has a decidable normalizing call-by-need
strategy.
Finally, we apply the results on call-by-need strategy to the E-strategy adopted by
the OBJ algebraic specication languages. The E-strategy chooses a redex according to
local strategies which are given to each function symb ol. We consider how to give local
strategiestomaketheE-strategynormalizing. Forthispurpose,weintro ducedthe notion
index-transitivity and carefulness. We show that for every index-transitive orthogonal
term rewriting system, if careful local strategies are given to each function symbol then
the E-strategy is normalizing.
I am very grateful to my sup ervisor Professor Yoshihito Toyama of Japan Advanced
Instituteof Scienceand Technology forhisguidance. I am alsograteful toAssociatePro-
fessorMasahikoSakaiofNagoyaUniversityforhissuggestionsand kindencouragements.
Part of the work onthis thesis has been done under hissupervision.
IwouldliketothankProfessorHiroakiraOnoandAssociateProfessorHajimeIshihara
ofJapanAdvancedInstituteofScienceandTechnologyfortheirsuggestions. Iwouldalso
liketo thank Professor Michio Oyamaguchiof MieUniversityfor his useful comments.
I would like to thank Professor Kokichi Futatugi and Associate Kazuhiro Ogata of
Japan Advanced Institute of Scienceand Technologyand Michihiro Matsumoto of PFU
Limited fortheir helpful discussions.
I also wish to thank Eiichi Horita of NTT Software Laboratories and Ken Mano of
NTT Communication Science Lab oratories for their guidance in training at NTT Com-
munication Science Lab oratories.
Abstract i
Acknowledgments ii
1 Intro duction 1
2 Preliminaries 4
2.1 Abstract Reduction Systems : : : : : : : : : : : : : : : : : : : : : : : : : : 4
2.2 Term Rewriting Systems : : : : : : : : : : : : : : : : : : : : : : : : : : : : 5
2.3 Sequential TRSs : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 8
2.3.1 Sequentiality : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 8
2.3.2 StrongSequentiality : : : : : : : : : : : : : : : : : : : : : : : : : : 11
2.3.3 NV-sequentiality : : : : : : : : : : : : : : : : : : : : : : : : : : : : 12
2.4 Tree Automata : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 14
3 NVNF-Sequentiality of Left-Linear TRSs 15
3.1 NVNF-Sequentiality : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 15
3.2 Decidability of Indices with respect to NVNF-Sequentiality : : : : : : : : : 17
4 Index Reduction of Overlapping TRSs 22
4.1 A Normalizing Strategyfor Stable Balanced JoinableTRSs : : : : : : : : : 22
4.1.1 Stable BalancedJoinability : : : : : : : : : : : : : : : : : : : : : : 22
4.1.2 Normalizability of Index Reduction : : : : : : : : : : : : : : : : : : 23
4.1.3 Decidability of Stable TransitiveIndices : : : : : : : : : : : : : : : 25
4.2 A Normalizing Strategyfor NV-Stable Balanced Joinable TRSs : : : : : : 27
4.2.1 NV-Stable Balanced Joinability and aNormalizing Strategy : : : : 27
4.2.2 Decidability of Stable TransitiveNV-Indices : : : : : : : : : : : : : 29
4.3 Remarks : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 32
5 Growing Term Rewriting Systems 33
5.1 Left-LinearGrowingTRSs : : : : : : : : : : : : : : : : : : : : : : : : : : : 33
5.1.1 Recognizability : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 34
5.1.2 Reachability and Joinability : : : : : : : : : : : : : : : : : : : : : : 39
5.1.3 Decidable Approximations : : : : : : : : : : : : : : : : : : : : : : : 40
5.2 Termination of Almost OrthogonalGrowing TRSs : : : : : : : : : : : : : : 42
6.1 The Evaluation Strategy : : : : : : : : : : : : : : : : : : : : : : : : : : : : 45
6.2 Normalizability : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 49
6.3 A SucientCondition for Carefulness : : : : : : : : : : : : : : : : : : : : : 52
6.4 A Necessary and Sucient Condition forIndex-Transitivity : : : : : : : : : 54
7 Conclusion 57
References 59
Publications 62
Introduction
A term rewriting system consists of a set of directed equations, called rewrite rules. If
a term t contains an instance of the left-hand side of a rewrite rules l ! r, so-called
redex then t can berewritten totheterm obtained fromt by replacingthis instancewith
the corresponding instance of the right-hand side r. A term which cannot be further
rewritten is the result of the computation, and called a normal form. Term rewriting
systemsplayanimportantroleinvariouseldsof computersciencesuchasabstractdata
typ especications,implementationsof functionalprogramming languages, programming
verication and automated deduction. The fundamental prop erties of term rewriting
systems are strongly normalizing property (or termination) and Church-Rosser property
(or conuence). Aterm rewriting systemissaid tobestrongly normalizingifthere exists
no innite reduction sequence. In a strongly normalizing term rewriting system, every
computationeventually ends ina normalform. Wecall aterm rewriting system Church-
Rosser if any two terms that are reduced from some term can reach same term by the
reduction. IfatermrewritingsystemsisChurch-Rossertheneverytermcanhaveatmost
onenormalform. InatermrewritingsystembeingChurch-Rosser,theremayexistinnite
reduction sequences starting with a term having the normal form. In order to compute
the normal form of a given term, we require some strategies telling us which redex to
contract. Areduction strategyis said tobenormalizing if wecan alwaysnd the normal
form ofa term having anormal formby it. It is well-known that the leftmost-outermost
reductionisanormalizingstrategyinthe-calculusandthe combinatorylogic. However,
it has been shown that the leftmost-outermost strategy is not normalizing for arbitrary
term rewriting systems.
O'Donnell[25]wasthersttoconsiderreductionstrategiesfororthogonaltermrewrit-
ing systems. Heshowedthat the parallel-outermostreduction strategyis normalizingfor
orthogonaltermrewritingsystems. HuetandLevyinvestigatedone-stepreductionstrate-
gies fororthogonaltermrewritingsystems in[13]. HuetandLevyprovedthateveryterm
not in normal forms contains a needed redex and rep eated rewriting of needed redexes
leads tothe normal form if it exists. A needed redex is a redex which must be contract
in order to reach a normal form. However, it is undecidable whether a redex in a term
is needed. Huet and Levy formulated the notion of strong sequentiality for orthogonal
term rewriting systems. Theyshowedthat for everystrongly sequential orthogonal term
rewritingsystemR,indexreductionisanormalizingstrategy,thatis,byrewritingaredex
called an index at eachstep, everyreduction startingwith a term havinga normal form
eventually terminates at the normal form. Here, the index is dened as a needed redex
of the rewriterules of term rewriting systems. Oyamaguchi[28] intro duced the notionof
NV-sequentiality whichis a proper extension of strong sequentiality. NV-sequentialityis
not only based on the analysis of the left-hand sides of the rewrite rules of term rewrit-
ing systems but also on the non-variable parts of the right-hand sides. Extensions of
NV-sequentiality were proposed by Nagaya et al. [21], Comon [3] and Jacquemard [14].
The notion of strong sequentiality wasextended to left-linear term rewriting systems by
Toyama [30]. He showed that index reduction is a normalizing strategy for every root
balanced joinable strongly sequential system. Kennaway [16] proved that every almost
orthogonaltermrewritingsystemhasadecidableone-stepnormalizingstrategy. However,
the strategyof Kennawayiscomplicated. Antony andMiddeldorp [1]proposeda simpler
and intuitiveone-step reduction strategy for every term rewriting systems. Theyproved
that their strategy is normalizingfor weakly orthogonal term rewriting systems.
The rest of this chapter gives anoverviewof this thesis.
Chapter 2 gives the basic denitions of term rewriting systems. Werst present ab-
stract reduction systems which are set equipped with a binary relation. Term rewriting
systems are special abstract reduction systems. The notions of sequentiality and indices
are explainedinSection2.3. In Section2.4, weintro ducetree automata whichare gener-
alization of sequentialautomata.
In Chapter 3, we intro duce an extension of NV-sequentiality, which is called NVNF-
sequentiality [21]. We rst show that the class of NVNF-sequential systems properly
includestheclassofNV-sequentialsystems. Wenextshowthedecidabilityofindiceswith
respect to NVNF-sequentiality for left-linear term rewriting systems. Every orthogonal
NVNF-sequentialsystem hasadecidable normalizingcall-by-needstrategy. It wasshown
by Comom[3]that NVNF-sequentiality ofleft-lineartermrewriting systemsisdecidable.
In Chapter 4,weshowthat index reduction isnormalizing for the class of stable bal-
anced joinable strongly sequential systems [22]. A stable balanced joinable system is a
left-linear term rewriting system in which every critical pair is joinable with balanced
stable reduction. In stable reduction, transitive index being stable under substitutions
is contracted. This class includesall ro ot balanced joinable strongly sequential systems.
Instable balancedjoinable stronglysequential systems,index reductionhas the balanced
weaklyChurch-Rosserproperty. Thuswecan showthe normalizabilityof indexreduction
byusingToyama'stheorem[30]concerningreductionstrategies. Wenextshowthatevery
NV-stable balanced joinable NV-sequential system has a normalizing strategy by intro-
ducingthenotionsoftransitivityandstabilityforindiceswithrespecttoNV-sequentiality.
In Chapter 4, we do not consider more general sequential systems (NVNF-, shallow [3]
or growing [14] sequentialsystems). The reason is that index reduction is not balanced
weakly Church-Rosser even ifthe system is orthogonal.
InChapter 5,weextendJacquemard'sresultin[14] toleft-lineargrowingtermrewrit-
ing systems [23]. Jacquemard showedthat the setofnormalizableground termsis recog-
nized by a tree automaton if the term rewriting system is linear and growing. We rst
show that the set of reachable terms tosome recognizable set by the reduction is recog-
nized by a tree automaton if a term rewriting system is left-linearand growing. We can
removethe right-linearcondition by constructinga deterministicautomaton. This result
gives us better approximations of term rewriting systems which are left-linear growing
systems obtained by renaming variables in the right-side hands of rewrite rules. These
approximationsyieldthe classof left-linearterm rewriting systems forwhichthere exists
ability of reachability for left-linear growing systems. It is also shown that reachability
and joinability for some subclass of right-linear systems are decidable. We next prove
that terminationforalmostorthogonal growingterm rewritingsystems isdecidable. Our
proof use Gramlich's theorem that a weakly innermost normalizing rewriting system R
is terminating if every critical pair of R is trivial and overlay. We show that the set of
allgroundtermbeingreachableanormalformbyinnermost reductionisrecognized by a
tree automaton for left-linear growing systems. By basic property of tree automata, the
decidability result isobtained.
In Chapter 6, we study the evaluation strategy (E-strategy) [9, 11, 20, 24]. The E-
strategyisareductionstrategyadoptedbytheOBJalgebraicspecicationlanguagessuch
that OBJ2 [9], OBJ3 [11] and CafeOBJ [24]. The outermost strategy has a better termi-
nationbehaviorthanthe innermoststrategy although the outermost strategycan not be
implemented as eciently as the innermost strategy. The E-strategy is a compromise
betweenthe outermostand the innermoststrategies. Eachfunction symb olisgivenalist
of natural numbers which is called local strategy. By local strategies, it is determined
which redex is contracted. The result of the reduction by the E-strategy is not always
a normal form. We rst consider a restriction for local strategies to avoid this problem.
Next we present the class of term rewriting systems for which the E-strategy is normal-
izing. Because our normalizability proof relies on Huet and Levy's theorem, this class is
undecidable. In Sections6.3 and 6.4, wegivea sucient condition for normalizability of
the E-strategy and we explain howto give local strategies to function symbols for term
rewriting systems satisfying this condition.
Preliminaries
Inthischapter,wepresentthebasicconceptoftermrewritingwhichisusedinthisthesis.
Following Klop [17], we rst intro duce abstract reduction systems. Moredetails onterm
rewriting can be found in [2,7, 17]. In Section 2.3, we explain the landmark theorem of
Huet and Levy [13] and give the notions of index and sequentiality. In Section 2.4, tree
automata are introduced. Several decidability resultsin this thesisare obtained byusing
tree automata techniques.
2.1 Abstract Reduction Systems
Inthissection,wedeneabstractreductionsystemswhicharesetequippedwithabinary
relation. Most properties of term rewriting systems are described on this abstract level.
Wecan avoid repeatingsimilar denitions and prop erties by dening them.
Denition 2.1.1 An abstract reduction system (ARS) is a structure A = hD;!i con-
sisting of a set D and a binary relation ! on D, called a reduction relation. We write
a!b if(a;b) 2!
Denition 2.1.2 Let A=hD;!ib e an ARS.
1. The identity of elements of Dis denoted by .
2. The transitive-reexiveclosureof !isdenoted by! 3
. The transitiveclosureof!
isdenoted by ! +
and !
denotes the reexiveclosure of !.
3. The set of natural numbers is denoted by N. Let k 2 N. Then ! k
denotes the
k-stepsreduction.
4. The symmetricclosureof!is denotedby$. Thetransitive-reexiveclosureof$
isdenoted by =.
5. Wewrite a b ifb !a.
6. An element a 2D is a normal form if there exists nob 2 D such that a !b. The
setof normal formsis denoted byNF
A
. An element a has a normal formif a! 3
b
for some normalform b.
Denition 2.1.3 Let A=hD;!ib e an ARS.
sequences x
0
!x
1
!x
2
!111.
2. A (or ! ) is Church-Rosser orconuent if 8a
1
;a
2
;a
3
2 D, a
1
! 3
a
2 and a
1
! 3
a
3
imply a
2
! 3
b and a
3
! 3
b forsome b 2D.
3. A(or !)has thenormal form propertyif 8a2D,8b2NF
A
,a =b impliesa! 3
b.
Denition 2.1.4 Let A=hD;!ib e an ARS.
1. A relation !
s
on D is a reduction strategy for A (or !) if !
s
!
+
and every
normal formwith respect to!
s
is also a normalform with resp ect to!. If !
s is
asubrelation of !then itis calleda one-step reductionstrategy. Otherwise,!
s is
called amany-step reduction strategy.
2. A reduction strategy !
s
for A is normalizing if for each a having a normal form
with respect to!, there are no innitesequences aa
0
!
s a
1
!
s a
2
!
s 111.
2.2 Term Rewriting Systems
Denition 2.2.1 A signature F isanite setof functionsymbolsdenoted byf;g;h;....
Every f 2 F is associated with a natural numb er denoting its arity. Function symbols
of arity 0 are called constant. F
n
denotes the set of all n-ary function symb ols. Hence
F = S
n0 F
n .
Denition 2.2.2 Let F be a signature and let V b e an enumerable set of variables
denoted by x;y;z;... where F \V =. The set T(F;V) of all terms built from F and
V is the smallest setsuch that
V T(F;V);
if f 2F
n and t
1
;...;t
n
2T(F;V) then f(t
1
;...;t
n
)2T(F;V).
The set T(F;V) is sometimes denoted by T. Terms not containing variables are called
ground terms. The setof all groundterms built fromF is denoted byT(F). A termt is
linear if every variablein t occurs only once.
Denition 2.2.3 Let 2 be an extra constant. A context C[;...;] is a term in T(F [
f2g;V). If C[;...;] is a context with n occurrences of 2 and t
1
;...;t
n
2 T(F;V) then
C[t
1
;...;t
n
]istheresultofreplacingfromlefttorighttheo ccurrencesof2byt
1
;...;t
n . A
contextcontainingpreciselyone occurrenceof2isdenotedbyC[]. Ifthasanoccurrence
of some(function orvariable)symb ol ethen wewrite e2t. Thevariableoccurrence z of
C[z]is fresh if z 62C[].
Denition 2.2.4 Let t2T(F;V).
1. The height(t) of t is denedby
(t)= (
1+maxf(t
1
);...;(t
n
)g if tf(t
1
;...;t
n
) and n>0;
1 otherwise:
+
N 3
+
, i.e., a nite sequence of positive integers. The empty position is denoted by
" and the concatenation of positions p and q is denoted by p:q. The set Pos(t) of
p ositions int is dened asfollows:
Pos(t)= (
f"g if t 2V;
f"g[fi:pj 1in; p2Pos(t
i
)g if tf(t
1
;...;t
n ):
Positionsare partially ordered by the prex ordering , i.e., p q if there exists r
such that p:r =q. In this case we dene q=pas r. Ifp 6 q and q 6p then we say
that p and q are disjoint, and write p?q. The depth jpj of apositionp is dened
by
jpj= (
0 if p=";
1+jqj if p=i:q:
3. If p2Pos(t) then the subterm tj
p
of t ata p osition pis denedby
tj
p
(
t if p=";
t
i j
q
if tf(t
1
;...;t
n
) and p=i:q:
If s is a subtermof t then we write s t. A subterm s of t is proper if s 6 t. We
write st to indicate that s is apropersubterm of t.
4. If p2Pos(t) then the symb ol t(p) atp of t is denedas follows:
t(p)= (
tj
p if tj
p 2V;
f if tj
p f(t
1
;...;t
n ):
The set of variable positions in t is denoted by Pos
V
(t), i.e., Pos
V
(t) = f p 2
Pos(t)j t(p)2V g. Wedene Pos
F
(t) asPos(t)nPos
V
(t). Hence Pos
F
(t)=fp2
Pos(t)j t(p)2F g.
5. Ifp2Pos(t)and s2T(F;V) thenthe termt[s]
p
obtained fromt by replacing the
subtermtj
p
with s isdened asfollows:
t[s]
p
(
s if p=";
f(t
1
;...;t
i [s]
q
;...;t
n
) if t f(t
1
;...;t
n
)and p=i:q:
If p
1
;...;p
n
2Pos(t) are pairwisedisjoint then we write t[s
1
;...;s
n ]
p1;...;pn
instead
of t[s
1 ]
p
1 111[s
n ]
p
n .
Example 2.2.5 Let F = ff;g;a;bg. Consider the linear term t f(g(x);f(g(a);y)).
We have (t) = 4, Pos(t) = f"; 1; 2;1:1; 2:1; 2:2; 2:1:1g and Pos
V
(t) = f1:1; 2:2g.
Then tj
2:1
g(a), t(1)=g and t[g(b)]
2
f(g(x);g(b)).
Denition 2.2.6 A substitution is a mapping from V to T(F;V). Every substitu-
tion is extended to a homomorphism from T(F;V) to T(F;V), i.e., (f(t
1
;...;t
n ))
f((t
1
);...;(t
n
)) for each n-ary function symbol f and terms t
1
;...;t
n
. A variable re-
naming is a bijective substitution. A term s is an instance of a term t if there exists a
substitution such that s (t). We writet instead of (t).
F and a nite set R of rewrite rules. A rewrite rule is a pair hl ;ri of terms in T(F;V)
such that:
(1) l 62V,
(2) anyvariablein r also occurs in l.
We write l ! r for hl ;ri. An instance of the left-hand side of a rewrite rule is a redex.
The rewrite rules of a term rewriting system (F;R) dene a reduction relation !
R on
T(F;V) asfollows: t!
R
s ithere exista rewriterulel !r2R, apositionp2Pos(t)
and a substitution such that tj
p
l and s t[r ]
p
. We call r the contractum of l .
Wemay write t p
!
R s or t
1
!
R
s to specify the redex position p or the redex occurrence
1 l of t inthis reduction. When noconfusion can arise, we omit the subscript R.
Example 2.2.8 Let F =fadd; mul t; s; 0gand
R= 8
>
>
>
<
>
>
>
:
add(x;0)!x
add(x;s(y))!s(add(x;y))
mul t(x;0)!0
mul t(x;s(y))!add(mult(x;y);x):
Wehavethefollowingreductionsequence(ateachsteptheunderlinedredexiscontracted):
mult(add(s(0);0);s(s(0))) !
R
add(mul t(add(s(0);0) ;s(0));add(s(0);0))
!
R
add(mul t(s(0);s(0)) ;add(s(0);0))
!
R
add(add(mul t(s(0);0) ;s(0));add(s(0);0))
!
R
add(add(0;s(0)) ;add(s(0);0))
!
R
add(s(add(0;0));add(s(0);0))
!
R
add(s(0));add(s(0);0) )
!
R
add(s(0);s(0))
!
R
s(add(s(0);0))
!
R
s(s(0)):
All notions dened in the previous section for abstract reduction systems carry over
to term rewriting systems byassociating the ARS hT(F;V);!
R
i with the TRS (F;R).
Wesometimes write R instead of (F;R) if the signature isclear from the context.
Denition 2.2.9 Let R be aTRS.
1. R is ground (linear) if for everyl !r2R, l and r are ground (linear).
2. R is left-linear (right-linear)if forevery l!r 2R, l (r) islinear.
Example 2.2.10 Consider the TRS R of Example 2.2.8. R is left-linear. But R is not
right-linear(linear) b ecause the right-handside of the fourth rewriterule isnon-linear.
Denition 2.2.11 Let l !r and l ! r be tworewrite rules of a TRS R. Weassume
that they are renamed to have no common variables. Supp ose that p is a position in
Pos
F
(l)suchthatlj
p and l
0
areuniable with amost generalunier. Thenwesaythat
l ! r and l 0
!r 0
are overlapping and the pair hl[r 0
]
p
;r 0
i is called a critical pair of R.
Ifl !rand l 0
!r 0
are samerule, then wedonot considerthecase p=". A criticalpair
hl [r 0
]
p
;r 0
i with p=" is anoverlay. A critical pair ht;si is trivial if t s.
Example 2.2.12 Let
R= 8
>
<
>
:
f(g(x);y)!f(x;x)
f(x;a)!g(x)
g(b) !b:
Then R has three critical pairs hf(x;x);g(g(x))i, hg(g(x));f(x;x)i and hf(b;y);f(b;b)i.
The critical pairs hf(x;x);g(g(x))i and hg(g(x));f(x;x) are overlays.
Denition 2.2.13 Let R be a TRS.
1. R is non-overlapping if R has no criticalpair.
2. R is orthogonal if R is left-linearand non-overlapping.
3. Risalmostorthogonal ifRisleft-linearandallcriticalpairsofRaretrivialoverlays.
Theorem 2.2.14 ([29]) Everyorthogonal TRS is Church-Rosser. 2
2.3 Sequential TRSs
2.3.1 Sequentiality
Huetand Levy [13] investigated normalizingone-step reductionstrategies fororthogonal
TRSs. They provedthat everyorthogonal TRS has a normalizing call-by-need strategy.
Werst explain this theorem.
Let A : t
0
! t
1
! 111 ! t
n
be a reduction sequence. We denote the rst i steps of
A by A[i] and denote the rest of A by A[i;n]. We may write A : t
0
! 3
t
n
instead of
A:t
0
!t
1
!111!t
n .
Denition 2.3.1 Let A:t !s be a reduction step contracting the redex at p2 Pos(t)
by the rewrite rule l !r 2R. Let q 2Pos(t). The set qnA of descendants of q in s by
A is denedas follows:
qnA= 8
>
<
>
:
fqg if q<p or q?p;
fp:p
3 :p
2 j r j
p3 l j
p1
g if q=p:p
1 :p
2
with p
1
2Pos
V (l)
otherwise:
If QPos(t)then QnA denotes the set S
q2Q
qnA. Thenotion of descendant extends to
reduction sequences as follows. Let A : t
0
! t
1
! 111 ! t
n
. The set qnA is dened by
qnA =fqgif n =0and qnA=(qnA[1])nA[1;n] if n >0.
R= (
f(g(x);y)!f(x;f(x;a))
h(x)!g(x)
and A : t f(h(a);a) ! f(g(a);a) ! f(a;f(a;a)) t 0
. Then position 1:1 has two
descendants1 and 2:1 in t 0
. All positions int except 1:1 haveno descendants int 0
.
Denition 2.3.3 Let R be aTRS.
1. A redex position p in a term t is needed if in every reduction sequence from t to a
normalformaredex atsome descendantof piscontracted. Inthis case wealso say
that the redex atposition pis needed.
2. The needed reduction !
N
is dened on T as follows: t !
N
s i t p
! s and p is
neededin t.
Note that if aterm t do esnot havea normalform then allredexes in t are needed.
Example 2.3.4 Consider the TRS R of Example 2.3.2 and the term t f(h(a);h(a)).
The redex h(a) in t at position 1 is needed. However, the redex h(a) in t at position 2
is not needed because we have f(h(a);h(a)) ! f(g(a);h(a)) ! f(a;f(a;a)), which is a
needed reductionsequence.
Theorem 2.3.5 ([13]) Let R be an orthogonal TRS. The needed reduction !
N is a
normalizing reduction strategy forR. 2
The theorem proved in [13] is actually stronger: if a term t has a normal form then
thereexistsnoinnitereductionsequencestartingwitht inwhichinnitelymanyneeded
redexes are contracted. Middeldorp [19] generalized this theorem to computations to
root-stable term.
Denition 2.3.6 Let R be aTRS.
1. A term t is root-stableif there existsno redex s such that t! 3
s.
2. A redex position p (or a redex tj
p
) in a term t is root-needed if in every reduction
sequencefromttoaroot-stabletermaredex atsome descendantofpiscontracted.
Theorem 2.3.7 ([19]) Let R b e anorthogonal TRS.
(1) Everynon-root-stable term has a root-needed redex.
(2) If a term t is reducible to some root-stable term then every innite reduction se-
quence startingwith t inwhich innitelymany root-needed redexes are contracted
contains aroot-stable term. 2
Theabovetheoremsgiveusanormalizingreductionstrategy. However,neededredexes
are dened as redexes which contracted in all reduction to the normal form. Hence, in
ordertodecidewhichare neededredexes,wehavesearchallreductiontothenormalform
i.e., we require lo ok-ahead. Huet and Levy intro duced the class of sequential TRSs in
whichcall-by-need computations are possible withoutlook-ahead.
T(F [fg;V) are called -terms. The set T(F [fg;V) is abbreviated to T
. An
-normal form is an -term without redexes, containing at least one occurrence of .
Only terms containing neither redexes nor 's are called normal forms. The set of all
normalformsisdenoted byNF
R . t
denotesthe -termobtained fromt by replacing all
variables int with . The setR ed is denedby Red=f l
j l!r 2R g.
Denition 2.3.9
1. The prex ordering onT
is dened asfollows:
t for allt 2T
,
f(s
1
;...;s
n
)f(t
1
;...;t
n ) if s
i t
i
for any 1in,
x x for allx2V.
Wewrite t<s if t sand t6s.
2. Two -terms t and s are compatible, written by t " s, if there exists an -term r
suchthatt r andsr;otherwise, tand s areincompatiblewhichisindicated by
t#s. Theleast upperboundoftwo-termstand s isdenoted by ttsif t"s. Let
S T
. Wewrite t"S if there existssome s2S such that t"s; otherwise, t#S.
Example 2.3.10 LetRbetheTRSofExample2.3.2. ThenR ed=ff(g();); h()g.
We have f(;f(;)) f(g();f(;a)) and f(;f(g(a);)) " f(h();f(;x)). We
obtain f(;f(g(a);))tf(h();f(;x))f(h();f(g(a);x)).
Denition 2.3.11 Let P be a predicate on T
. An -position p of an -term t is an
index with resp ect to P if for every -term s with t s, P(s) = true implies sj
p 6 .
The setof indices of t with respect to P isdenoted by I
P (t).
Let t2T and p2Pos(t). Thenwecan see that p2I
P (t[]
p
)i P(t[]
p
)=fal se.
Denition 2.3.12 LetRbeaTRS.Wedenethepredicatenf onT
asfollows: nf(t)=
true i t! 3
R
s forsome normalforms.
NotethatifRisaleft-linearTRS thennf isamonotonicpredicate,i.e., nf(t)=true
implies nf(s)=tr ue wheneverts. The followinglemma can beeasilyproven.
Lemma 2.3.13 Let R be an orthogonal TRS. Let t 2 T. A redex position p of t is
needed ip2I
nf (t[]
p
). 2
Denition 2.3.14 A left-linear TRS is sequential if every -normal form has an index
w.r.t. nf
Example 2.3.15 Let R be Berry's TRS, i.e.,
R = 8
>
<
>
:
f(a;b;x)!c
f(b;x;a) !c
f(x;a;b) !c:
Consider the -normal form t f(;;). Position 1 is not an index of t w.r.t. nf
because wehavethe -termsf(;a;b) witht s and nf(s)=true. Similaly,neither
position 2 nor 3 isanindex of t w.r.t. nf. ThusR is not sequential.
Unfortunately,in generalneither indices w.r.t.nf nor sequentiality is decidable.
Huet and Levy [13] formalized strong sequentiality which is a sucient condition for
sequentiality. Strongsequentialityisaprop ertybasedonthe left-handsidesoftherewrite
rulesof TRSsalone. Theyintroducedthe arbitraryreductioninordertoforgetthe right-
hand sides of the rewrite rules.
Denition 2.3.16 Let R be a TRS.
1. Thearbitraryreduction !
? onT
isdenedasfollows: t!
?
s ist[s 0
]
p
forsome
redex position p int ands 0
2T
.
2. The predicate nf
? on T
is dened as follows: nf
?
(t) = true i t ! 3
?
s for some
normalform s.
Denition 2.3.17 A left-linear TRS is strongly sequential if every -normal form has
anindex w.r.t. nf
? .
Indices of a termt w.r.t. nf
?
are indicesof t w.r.t. nf because !
R
!
?
. Thus every
strongly sequential TRS is sequential.
Huet and Levy [13] gave aprocedure tocompute the indiceswith respect to nf
? .
Denition 2.3.18 The -reduction !
is denedon T
asfollows: t!
s i st[]
p
for some p 2 Pos(t) such that tj
p
" R ed and tj
p
6 . The set of normal forms with
respect to -reductionis denoted byNF
.
Example 2.3.19 Let
R= (
f(x;f(y;a))!x
f(a;b)!a
andt f(f(;b);f(a;)). ThenRed=ff(;f(;a)); f(a;b)gand wehavethe follow-
ing ve -reductionsequences fromt to the normal formof t w.r.t. -reduction:
t !
;
t !
f(;f(a;))!
;
t !
f(;f(a;))!
f(;)!
;
t !
f(f(;b);)!
;
t !
f(f(;b);)!
f(;)!
:
The following lemmaholds for -reduction.
Lemma 2.3.20 ([18]) -reductionis Church-Rosserand strongly normalizing. 2
Denition 2.3.21 Lettbean-term. Thenormalformoftwithresp ectto-reduction
is denoted by!(t).
Note that !(t) is well-dened according to the previous lemma. We write e 2!(t) if
the normal formof t with respect to-reduction has anoccurrence ofsome symb ol e.
Theorem 2.3.22 ([13]) Let t be an -term and let p be an-position int. Then p is
anindex of t w.r.t. nf
?
iz 2!(t[z]
p
) wherez is fresh. 2
obtain I
nf
?
(f(;))=f2g because !(f(z;))and !(f(;z))f(;z).
The decidability of strongsequentiality for orthogonalTRSs wasrst shown by Huet
and Levy [13] and then simplied pro ofs were presented by Klop and Middeldorp [18].
Jouannaud and Sad [15] proved the decidability of strong sequentiality assuming left-
linearity instead of orthogonality. Alsothis result wasprovenbyComon [3].
Theorem 2.3.24 Strongsequentiality of left-linear TRSs isdecidable. 2
WecanobtainthefollowingdecidablereductionstrategyforstronglysequentialTRSs.
Denition 2.3.25 The index reduction !
I
is dened on T as follows: t !
I s i t
p
! s
for some pwith p2I
nf
? (t[]
p ).
Huet and Levy [13] showed that index reduction is a normalizing strategy for every
orthogonal strongly sequential TRSs. Toyama [30] generalized this result to the class of
rootbalanced joinablestrongly sequential TRSs. The root reduction t!
r
s isdened by
t p
!s and p=".
Denition 2.3.26 A TRS Ris root balanced joinableif for anycritical pairhp; qiof R,
there exista term t and k 0 suchthat p! k
r
t and q! k
r t.
Theorem 2.3.27 ([30]) LetR be a left-linearTRS. IfR is root balanced joinable and
strongly sequential then R has the normal form property and index reduction is a nor-
malizing strategy for R. 2
Huet and Levy gave a syntactic characterization, which is called left-normal [25], for
orthogonal strongly sequential TRSs in [13]. Toyama [30] removed the non-overlapping
condition.
Denition 2.3.28 ATRSRisleft-normal ifineveryrewriterulel!r 2Rthefunction
symb olsinl precedethe variablein l .
Example 2.3.29 The TRS ofExample 2.3.2isleft-normal. The TRS ofExample 2.3.19
isnot left-normal since the variablesxand y precedethe constant ain the left-handside
f(x;f(y;a)).
Theorem 2.3.30 ([30]) Let R be a left-linear left-normal TRS. Then R is strongly
sequential. Furthermore,if p isthe leftmost-outermost redex p osition of a term t then p
is anindex of t[]
p
w.r.t. nf
?
. 2
2.3.3 NV-sequentiality
Oyamaguchi [28] intro duced a more general sucient condition for sequentiality, which
is calledNV-sequentiality. NV-sequentiality is not only based onthe analysis of the left-
handsidesoftherewriterulesofTRSsbutalsoonthenon-variablepartsoftheright-hand
sides.
Denition 2.3.31 Let R be a TRS.
SequentialTRSs
NV-sequentialTRSs
Strongly sequentialTRSs
Figure 2.1.
1. The reduction relation !
nv on T
is dened as follows: t !
nv
s i there exist a
rewriterulel !r2R,apositionp2Pos(t)andasubstitution suchthattj
p l
and st[s 0
]
p
for somes 0
r
.
2. The predicateterm onT
is denedasfollows: ter m(t)=true i t! 3
nv
s forsome
s2T.
Example 2.3.32 Let
R= 8
>
<
>
:
f(g(a);x)!x
f(a;x)!g(f(x;x))
g(x)!g(x)
and t f(f(a;a);). We have term(t) = true because t !
nv
f(g(f(a;a));) !
nv
f(g(a);)!
nv
a. Notethat nf(t)=fal se.
Denition 2.3.33 A left-linear TRS is NV-sequential if every -normal form has an
index w.r.t. term.
Oyamaguchi[28] showedthat everyNV-sequential TRS issequential and the class of
NV-sequential TRSs prop erly includesthe class of strongly sequentialTRSs.
Theorem 2.3.34 ([28]) Let R be a left-linear TRS. Let t 2 T
and p 2 Pos(t) with
tj
p
. It is decidablewhether p isan index of t w.r.t. ter m inpolynomialtime. 2
Oyamaguchi[28] also showedthat NV-sequentiality of orthogonal TRSs is decidable.
This result was generalizedto left-linearTRSs by Comon[3].
Theorem 2.3.35 NV-sequentialityis a decidable prop erty of left-linearTRSs. 2
Tree automata are generalization of sequential automata. Tree automata are useful for
the decision problems in term rewriting [3, 5, 6, 8, 14]. Following Comon et al. [4], we
adopt the denition of tree automata whichis based on rewrite rules. More information
ontree automata can be found in[4, 10].
Denition 2.4.1 A treeautomaton isatupleA=(F;Q;Q f
;1) whereF isasignature,
Q isa nite setof states, Q f
Q is aset of nal states and 1is a setof ground rewrite
rulesofthe formf(q
1
;...;q
n
)!qorq!q 0
wheref 2F,q
1
;...;q
n
;q;q 0
2Q. Thelatter
rules are called -rules.
We use !
A
for the reduction relation!
1
on T(F[Q).
Denition 2.4.2
1. A term t2T(F) isaccepted by A if t! 3
A
q for some q2 Q
f .
2. The tree language L(A) recognized byA is the set of allterms accepted by A.
3. A set L T(F) is recognizable if there exists a tree automaton A such that L =
L(A).
Denition 2.4.3
1. A tree automaton A is deterministic if there are neither -rules nor dierent rules
with the same left-hand side.
2. A tree automaton A is complete if there is atleast one rule f(q
1
;...;q
n
)! q in 1
for allf 2F and q
1
;...;q
n 2Q.
The followingprop erties of tree automata are well-known [4, 10].
Lemma 2.4.4 LetL be a recognizableset. Then there existsa complete and determin-
istic tree automaton recognizing L. 2
Lemma 2.4.5 Theclassofrecognizabletreelanguagesisclosedunderunion,intersection
and complementation. 2
Lemma 2.4.6 The emptiness problem for tree automata is decidable. 2
NVNF-Sequentiality of Left-Linear
TRSs
In this Chapter, we intro duce an extension of NV-sequentiality [28]. This sequentiality
iscalled NVNF-sequentiality. LikeNV-sequentiality,NVNF-sequentialityisbased onthe
analysis of left-hand sides and the non-variable parts of the right-hand side of rewrite
rules. However, the reachability to a normal form is considered in NVNF-sequentiality.
We rst show that the class of NVNF-sequential TRSs properly includes the class of
NV-sequential TRSs. Next we prove the decidability of indices with respect to NVNF-
sequentiality. This implies that every orthogonal NVNF-sequential TRS has a decidable
normalizing call-by-need strategy.
3.1 NVNF-Sequentiality
In this section we explain the notion of NVNF-sequentiality. NVNF-sequentiality is
dened by using the reduction !
nv
like NV-sequentiality. But indices w.r.t. NVNF-
sequentialityaredeterminedbythe reachabilitytonormalforms. Thefollowingpredicate
was given in[28].
Denition 3.1.1 Let R be a TRS. The predicate nvnf on T
is dened as follows:
nvnf(t)=true i t! 3
nv
s forsome normal forms.
Note that for every-termt, nvnf(t)=true impliesterm(t)=true.
Example 3.1.2 Let F
1
=ff;a;b;cg and
R
1
= 8
>
>
>
<
>
>
>
:
f(a;b;x)!a
f(b;x;a) !b
f(x;a;b) !c
c!c:
Consider the -term t f(;;). Position 1 is an index of t w.r.t. nvnf. But the
position 1 isnot anindex of t w.r.t. term because wehave term(f(;a;b))=true.
Denition 3.1.3 A left-linear TRS is NVNF-sequential if every -normal form has an
index with respect to nvnf.
Theorem 3.1.4 NVNF-sequentiality of left-linear TRSs isdecidable. 2
In the remainder of this section we discuss the relationship between sequentiality,
NVNF-sequentiality and NV-sequentiality.
Lemma 3.1.5
(i) EveryNV-sequential TRS isNVNF-sequential.
(ii) Every NVNF-sequential TRS is sequential.
Proof.
(i) SupposethatRisNV-sequential. Lettbean-normalform. Thenthasanindex
pw.r.t.term. Wewillshowthatpisanindexw.r.t.nvnf. Letsbean-termsuch
that t s and nvnf(s) =ture. Since term(s)= ture and p is an index of t w.r.t.
ter m, we obtainsj
p
6. Thusp is anindex of t w.r.t. nvnf.
(ii) Similarto(i). 2
We nowprove thatNVNF-sequentiality isa properextension of NV-sequentiality.
Lemma 3.1.6 The TRS (F
1
;R
1
) of Example 3.1.2 is NVNF-sequential but not NV-
sequential.
Proof. Because the-normalformf(;;)has noindicesw.r.t.term,R
1
isnotNV-
sequential. In order to show that R
1
is NVNF-sequential, we rst prove the claim: for
every-term t, if p2I
nvnf (t[]
p
) and q 2I
nv nf (tj
p
) thenp:q 2 I
nvnf (t).
Proof of the claim. Because !
nv
=!
R
1
, nvnf(t) = true i nf(t) = true for every
-termt. Thusitsucestoshowthatif p2 I
nf (t[]
p
)andq 2I
nf (tj
p
)then p:q 2I
nf (t).
This follows from Theorem 6.4.10 in Chapter 6 b ecause every variable in the left-hand
side of the rewrite rule occurs at depthone.
We now prove that every -normal formt has an index w.r.t. nvnf. The proof is by
induction on the size of t. The case t is trivial. Let t f(t
1
;t
2
;t
3
). We have the
following four cases.
Case 1. t
1
is an-normal form. Then by induction hyp othesis,t
1
has anindex w.r.t.
nvnf. Since 1 2 I
nvnf
(f(;t
2
;t
3
)), it follows from the claim that t has an index w.r.t.
nvnf.
Case 2. t
1
a. If t
2
contains 's then t
2
has an index w.r.t. nvnf by induction
hyp othesis. Since we have 22 I
nvnf
(f(a;;t
3
)), it follows from the claim that t has an
index w.r.t.nvnf. Otherwise,t
3
isan-normal form. From induction hyp othesis, t
3 has
an index w.r.t. nvnf. We can obtain 3 2 I
nvnf (f(a;t
2
;)) because t
2
is a normal form
and t
2
6b. Thereforefromthe claim, t has anindex w.r.t. nvnf.
Case 3. t
1
b. SimilartoCase 2.
Case 4. Otherwise, t
2 or t
3
is an -normal form. Thus from induction hyp othesis,
t
2 or t
3
has an index w.r.t. nvnf. Because we can obtain 2 2 I
nv nv (f(t
1
;;t
3
)) and
32I
nvnv (f(t
1
;t
2
;)), itfollowsfrom the claimthat t has anindex w.r.t. nvnf. 2
NVNF-sequentialTRSs
NV-sequentialTRSs
R
1
Figure 3.1.
Remark. The claim inthe pro ofof Lemma3.1.6 do es not hold for arbitrary left-linear
TRSs. Let R = ff(g(x);a) ! ag. Consider the -normal form f(g();). We have
12I
nvnf
(f(;)) and 12 I
nvnf
(g()). However,1:162I
nvnf
(f(g();)).
FromLemmas 3.1.5 and 3.1.6, we obtainthe following theorem.
Theorem 3.1.7 The class of NVNF-sequentialTRSs properly includesthe class of NV-
sequential TRSs. 2
3.2 Decidability of Indices with respect to NVNF-
Sequentiality
Inthis sectionweshowthatfor agiven-termt, itisdecidable whether an-p ositionis
an index of t w.r.t. nvnf. Throughout this section we assume that we are dealing with
left-linear TRSs.
Werst giveacharacterizationof indicesw.r.t. nvnf. Forthis purpose, weintroduce
the
V
-reduction [28].
Denition 3.2.1 The
V
-reduction is dened onT
asfollows: t !
V
s i there exist
l !r 2R and p2Pos(t)such that tj
p
"l
, tj
p
6and st[r
]
p .
Example 3.2.2 Let
R= (
f(x;f(a;y))!g(y)
f(g(x);b)!f(x;a):
We have the
V
-reduction t f(;f(g(a);)) !
V
f(;g()). We have also the
V -
reduction sequence t!
V
f(;f(;a))!
V g().
V
V
nv
Lemma 3.2.3
(i) If t! 3
nv
s and t 0
t then t 0
! 3
V s
0
for some s 0
s.
(ii) Ift! 3
V
s then t 0
! 3
nv
s for some t 0
t.
Proof.
(i) Wewill prove the claim that if t!
nv
s and t 0
t then t 0
!
V s
0
for some s 0
s.
Lett!
nv
s. Thenthereexistl !r 2R,p2Pos(t)andasubstitution suchthat
tj
p
l and s t[s
1 ]
p
for some s
1 r
. We rst consider the case p 62 Pos(t 0
).
Clearly t 0
s. Thus the claim holds. Next we consider the case p 2 Pos(t 0
).
If t 0
j
p
then t 0
s and therefore the claim holds. Otherwise, we can obtain
t 0
!
V t
0
[r
]
p
becauset 0
j
p
"l
. Wehavet 0
[r
]
p t[s
1 ]
p
s. Hencethe claimholds.
Using the claim,wecan prove(i) by induction on the length of t! 3
nv s.
(ii) This is proven by induction on the length of t ! 3
V
s. The case of zero length
is trivial. Assume that t !
V s
1
! 3
V
s where tj
p
"l
; tj
p
6 and s
1 t[r
]
p
for l ! r 2R and p2Pos(t). From induction hyp othesis, there exists an -term
s
2
such that s
2
! 3
nv
s and s
2 s
1
. Let t 0
s
2 [tj
p tl
]
p
. Because s
2 j
p r
, we
have t 0
!
nv s
2
and thus t 0
! 3
nv
s. Since s
2 t[r
]
p
and tj
p tl
tj
p
, we obtain
t 0
s
2 [tj
p tl
]
p t[tj
p ]
p
t. 2
We use t
x
todenote the term obtained from t2T
by replacing all 's with x.
Lemma 3.2.4 Let t be an -term and let p be an -position in t. Let z be a variable
such that z 62 t. Then p is not an index of t w.r.t. nvnf i t[z]
p
! 3
V
s for some s
containingneither redexes nor z's.
Proof.
()) Supp osethat pis not an index of t w.r.t. nvnf. Thenthere exists an-term t 0
such that t 0
t, t 0
j
p
and nvnf(t 0
) =true. Because t does not containz's, we
canassume w.l.o.g.that t 0
! 3
nv
s for somenormalfromswith z 62s. Fromthe left-
linearity of R, we obtain t 0
[z]
p
! 3
nv
s. According toLemma 3.2.3 (i), t 0
[z]
p
! 3
V s
0
for some s 0
s. Becase s containsneither redexes nor z's, neitherdoes s 0
.
(() Weassumethat t[z]
p
! 3
V
s forscontainingneitherredexes norz's. Then from
by Lemma 3.2.3 (ii), t 0
! 3
nv
s for some t 0
t[z]
p
. Let t 00
t 0
x []
p and s
0
s
x . We
can easily show t 00
! 3
nv s
0
. Because s does not cotain redexes, s 0
is a normal form
and hence nvnf(t 00
) = true. Clearly t 00
t and t 00
j
p
. Therefore p is not an
index of t w.r.t.nvnf. 2
Wenextshow that ifthere existsan-terms containingneither redexesnor z's such
that t[z]
p
! 3
V
s then we havean upper bound of the least hight ofsuch -terms.
Denition 3.2.5 LetR beaTRS. The setRH
R
is denedbyRH
R
=fr
jl !r2Rg.
RH 3
R
isthe smallestsetsuchthatRH
R
RH
3
R
and ift 2RH 3
R
, p2Pos(t) andr 2RH
R
then t[r ]
p 2RH
3
R .
It is clear that if r2 RH
R
and r ! 3
V
t then t2RH
R .
Lemma 3.2.6 Ift ! +
V
sthenthereexistp
1
;...;p
n
2Pos(t)whicharepairwisedisjoint
and satisfy the followingconditions.
1. st[sj
p
1
;...;sj
pn ]
p
1
;...;pn ,
2. for each1in, there existsr
i 2RH
R
suchthat tj
p
i
! +
V r
i
! 3
V sj
p
i .
Proof. Weassume the following
V
-reduction sequence:
tt
0 q
0
!
V t
1 q
1
!
V 111
q
n
!
V t
n+1 s
where n 0. Let q
i
1
;...;q
i
k
be the minimal positions in fq
0
;q
1
;...;q
n
g w.r.t. . Then
q
i
1
;...;q
i
k
2Pos(t)and theyare pairwisedisjoint. Bythe minimalityofq
i
1
;...;q
i
k , they
satisfy the conditions in the lemma. 2
Denition 3.2.7 Let R be a TRS. The maximum hight of the left-hand sides and the
right-handsides ofrewrite rules inR isdenoted by
R .
Lemma 3.2.8 Let r 2 RH
R
. Let r ! 3
V
s and (s) >
R
2n for some n 0. Then
there existp
0
;p
1
;...;p
n
2Pos(s)such that:
1. p
0
<p
1
<111<p
n ,
2. for each0in, there existsr
i 2RH
R
suchthat r ! +
V s[r
i ]
p
i and r
i
! 3
V sj
p
i .
Proof. We prove the lemma by induction on n. Base step. The case n = 0 is trivial
becausewecantake"asp
0
. Inductionstep. Weuseinductiononthelengthmofr ! 3
V s.
Assume that
r t
0 q
0
!
V t
1 q
1
!
V 11111
qm01
!
V t
m s:
Let S be the set of minimal positions in fq
0
;q
1
;...;q
m01
g w.r.t. . Because (s)>
R ,
S isnot empty and for any q 2S,q 2Pos(r )and q 2Pos(s).
Case 1. S = f"g. Then we have t
j
2 RH
R
for some j 1. Applying induction
hyp othesis on m to t
j
! 3
V
s, weobtain p
0
;p
1
;111;p
n
2 Pos(s) such that: 1. p
0
< p
1
<
111 < p
n
, 2. for each 0 i n, there exists r
i
2 RH
R
such that t
j
! +
V s[r
i ]
p
i and
r
i
! 3
V sj
p
i
. Clearly r ! +
V s[r
i ]
p
i
for each0in. Thusthe lemmaholds.
Case 2. S 6= f"g. Let S = fq 0
1
;...;q 0
m
0g with m 0
> 0. Then from the minimality
of q 0
1
;...;q 0
m 0
, s r[sj
q 0
1
;...;sj
q 0
m 0 ]
q 0
1
;...;q 0
m 0
and for each 1 i m 0
there exist r 0
i 2
RH
R
such that rj
q 0
i
! +
V r
0
i
! 3
V sj
q 0
i
. Because (s) >
R
2n, we have j such that
(sj
q 0
j ) >
R
2(n01). Applying induction hyp othesis on n to r 0
j
! 3
V sj
q 0
j
, we obtain
p
0
;111;p
n01
2 Pos(sj
q 0
j
) such that: 1. p
0
< 111 < p
n01
, 2. for each 0 i n01, there
existsr
i 2RH
R
suchthatr 0
j
! 3
V sj
q 0
j [r
i ]
p
i and r
i
! 3
V sj
q 0
j :p
i
. Letp 0
0
=" andp 0
i
=q 0
j :p
i01
for each 1 i n. Then p 0
0
< p 0
1
< 111 < p 0
n
2 Pos(s) and we have r ! 3
V s[r ]
p
0 and
r ! 3
V sj
p
0
. Because r ! 3
V s[r
0
j ]
q 0
j
, we obtain r ! 3
V s[sj
q 0
j [r
i01 ]
p
i01 ]
q 0
j
s[r
i01 ]
p 0
i and
r
i01
! 3
V sj
p 0
i
foreach 1in. Thereforethe lemma holds. 2
Denition 3.2.9 Let R bea TRS. Let t b e an-term. The prex -termpref
R
(t) of t
is denedbypref
R
(t)t[;...;]
p1;...;pn
wherefp
1
;...;p
n
g=fp2Pos(t) jjpj=
R g.
R p
pref
R
(s) then t[s]
p
doesnot containredexes.
Proof. From the left-linearityof R. 2
Denition 3.2.11 Let R be a TRS. The constant
R
isdened asfollows:
R
=
R
2(jfpref
R
(t) j t2RH 3
R
gj2jRj+1)
where jAj denotesthe numb erof elementsin aset A.
Lemma 3.2.12 Let t be an -termand letp b e an -position in t. Letz bea variable
with z 62 t. Then p 62I
nvnf
(t) i there exists an-term s containing neither redexes nor
z's suchthat t[z]
p
! 3
V
s and (s)(t)+
R .
Proof.
()) Assume that p 62 I
nvnf
(t). Using Lemma 3.2.4, we can obtain the minimal -
term s containing neither redexes nor z's such that t[z]
p
! 3
V
s. Supp ose (s) >
(t)+
R
. Since s does not contain z's, t[z]
p
! +
V
s. From Lemma 3.2.6, there
exist p
1
;...;p
n
2 Pos(s) such that: 1. s t[z]
p [sj
p1
;...;sj
pn ]
p1;...;pn
, 2. for each
1 i n, there exists r
i
2 RH
R
such that t[z]
p jp
i
! +
V r
i
! 3
V sjp
i
. By the
assumption that(s)>(t)+k
R ,(sj
p
j )>
R
forsome j. From Lemma3.2.8 and
thedenitionof
R
,wecanobtainr 2RH
R andq
1
;q
2
2Pos(sj
pj
)withq
1
<q
2 such
thatpref
R (sj
p
j :q
1
)pref
R (sj
p
j :q
2
)andfori=1;2,r
j
! 3
V sj
p
j [r]
q
i
andr ! 3
V sj
p
j :q
i .
Lets 0
s[sj
p
j :q
2 ]
p
j :q
1
,seeFigure3.2. Thenz 62s 0
and itfollowsfromLemma3.2.10
that s 0
do es not contain redexes. Because r
j
! 3
V sj
p
j [r]
q1
and r ! 3
V sj
p
j :q2
, we
havet[z]
p
! 3
V s[r
j ]
p
j
! 3
V s[sj
p
j [r ]
q
1 ]
p
j
s[r]
p
j :q
1
! 3
V s[sj
p
j :q
2 ]
p
j :q
1 s
0
. However,
this contradictsthe minimality ofs.
(() From Lemma 3.2.4. 2
By Lemma3.2.12,inordertodetermine whether an-position pinan-termt isan
index w.r.t. nvnf, we need to check the reachability from t[z]
p
to a nite numb er of -
terms by
V
-reduction. It wasshown by Oyamaguchi [28] that -reduction is simulated
by the usual reduction of some TRS.
Denition 3.2.13 Let R be a TRS. The TRS R
is denedas follows:
R
=fl !r
j l !r2Rg[f!t j tl
; l !r 2Rg:
Fromthe assumption that R is left-linear,R
is left-linear and right-ground(i.e., all
the right-hand side of itsrewrite rules is ground).
Lemma 3.2.14 ([28]) LetR b e a left-linearTRS.
(i) If t! 3
V
s then t! 3
R
s.
(ii) Ift ! 3
R
s and t 0
t then t 0
! 3
V s
0
for some s 0
s. 2
We can replace! 3
V
with ! 3
R
in Lemma 3.2.12.
r
r
s s
Figure3.2.
Lemma 3.2.15 Let t be an -termand letp b e an -position in t. Letz bea variable
with z 62 t. Then p 62I
nvnf
(t) i there exists an-term s containing neither redexes nor
z's suchthat t[z]
p
! 3
R
s and (s)(t)+
R .
Proof. From Lemmas 3.2.12and 3.2.14. 2
It has b een shown that the reachability problem isdecidable forleft-linear and right-
ground TRSs [5,26]. Thus we obtainthe following theorem.
Theorem 3.2.16 Let R be a left-linear TRS. Let t 2 T
and p 2 Pos(t) with tj
p
.
It is decidable whether p isan index of t w.r.t nvnf. 2
Index Reduction of Overlapping
TRSs
In this chapter, we investigate normalizing strategies for left-linear overlapping TRSs.
HuetandLevy[13]showedthateveryorthogonalstronglysequentialTRShasadecidable
normalizing strategy which is called index reduction. Toyama [30] extended this result
to ro ot balanced joinable strongly sequential TRSs. In Section 4.1, we prove that index
reduction is normalizing for stable balanced joinable strongly sequential TRSs. This
class properly includes the class of root balanced joinable strongly sequential TRSs. In
Section4.2,wediscussreductionstrategiesforNV-sequentialTRSswhichwereintro duced
byOyamaguchi[28]. Weintro ducethenotionofNV-stablebalancedjoinabilityandprove
that every NV-stable balanced joinable NV-sequential TRS has a decidable normalizing
strategy.
In this chapterweare dealing with left-linearTRSs only.
4.1 A Normalizing Strategy for Stable Balanced
Joinable TRSs
4.1.1 Stable Balanced Joinability
In this subsection, we dene stable balanced joinable TRSs. For that purpose, we need
the notions of transitivity, which was intro duced by Toyama et al. [31], and stability for
indices w.r.t nf
?
. In the following we will refer to an index w.r.t. nf
?
as an index for
short. We write C[
I
] if the displayed occurrence of in C[] is an index. Thus by
Theorem 2.3.22, C[
I
] i z 2 !(C[z]) where z is fresh. Let C[
I
] and let 1 be a redex.
Then 1is also called anindex of C[1] and we write C[1
I ].
Denition 4.1.1 The displayed index in C[
I
] is transitive if C 0
[C[
I
]] for any C 0
[
I ].
The transitiveindex is denoted by C[
T ].
Example 4.1.2 LetRed=ff(g())g. The-occurrenceing() isanindex. However,
this index in g() is not transitivebecause the -occurrence in f(g()) is not an index.
We recallproperties of indicesand transitive indices [13, 15, 18, 31].
Lemma 4.1.3
(i) If C[
I
] and C[z]C [z] where z isfresh, then C[
I ].
(ii) IfC[C 0
[
I
]]then C 0
[
I
]. 2
Lemma 4.1.4 IfC[
T
]and C[z]C 0
[z] wherez is fresh,then C 0
[
T ].
Proof. Let C 00
[
I
]. Since C[
T
], we have C 00
[C[
I
]]. Clearly C 00
[C[z]] C 00
[C 0
[z]]. By
Lemma 4.1.3 (i), it isobtained that C 00
[C 0
[
I
]]. ThusC 0
[
T
]. 2
Denition 4.1.5
The displayed transitive index in C[
T
] is stable, which is denoted by C[
S ], if
C[
T
] forany substitution .
The stable reduction !
S
is denedas C[l]!
S
C[r]where C[
S
]and l !r2R.
Lemma 4.1.6 Ift !
S
s and C[
I
] then C[t]!
I
C[s]for any .
Proof. Let t C 0
[l 0
] !
S C
0
[r 0
] s. From C 0
[
S
], it follows that C 0
[
T
] for any
. By the denition of transitivity, we have C[C 0
[
I
]]. Thus C[t ] C[C 0
[l 0
]] !
I
C[C 0
[r 0
]]C[s ]. 2
Denition 4.1.7 A critical pair hp; qi is stable balanced joinable if p ! k
S
t and q ! k
S t
for some t and k 0. A TRS R is stable balanced joinable if every critical pair isstable
balanced joinable.
Notethat everyrootbalanced joinableTRS isstable balanced joinablebecause !
r
!
S .
4.1.2 Normalizability of Index Reduction
In this subsection, weshowthat index reduction is normalizingforeverystable balanced
joinable strongly sequential TRS. Our proof uses the theorem of Toyama [30] concerning
reduction strategies. Werst explainthis theorem.
Denition 4.1.8 Let A=hD;!i bean ARS.Wewrite a !!b if thereexistsa connec-
tion a ! m1
1 n1
1 ! m2
1 n2
111 ! mp
1 np
b with P
m
i
>
P
n
i
. We write a !b if
b !!a.
Denition 4.1.9 Let A=hD;!i be anARS. A reduction relation !on D isbalanced
weaklyChurch-Rosser if8a
1
;a
2
;a
3
2D,a
1
!a
2 anda
1
!a
3
implya
2
! k
band a
3
! k
b
for some b2D and k 0.
Theorem 4.1.10 ([30]) Let A = hD;!i be an ARS. Let !
s
be a reduction strategy
for ! suchthat:
(i) !
s
is balanced weaklyChurch-Rosser,
(ii) Ifa!b then a=
s
b or a !!
s
1$1 !
s b.
Then ! has the normal formproperty and !
s
is a normalizingstrategy. 2
Let 1 and 1 be two redex occurrences of t 2 T. Let 1 C[s
1
;...;s
n ] and
C[;...;]2R ed. Wesay that 1and 1 0
(or 1 0
and 1) are overlapping if 1 0
1and
1 0
6s
i
for any 1in.
Lemma 4.1.11 LetRbestablebalancedjoinable. Lett 1
!
I t
0
andt 1
0
!t 00
,where1 0
1
and 1 and 1 0
are overlapping. Then t 0
! k
I
s and t 00
! k
I
s forsome s and k0.
Proof. Let t C[1] C[C 0
[1 0
]]. Then t 0
C[q ] and t 00
C[p] for some critical
pair hp;qi and . Since R is stable balanced joinable, we have p ! k
S s
0
and q ! k
S s
0
for some s 0
. Thus, from Lemma 4.1.6 and C[
I
], we obtain t 0
C[q] ! k
I C[s
0
] and
t 00
C[p]! k
I C[s
0
]. 2
Lemma 4.1.12 ([30]) LetC[1
I
;1 0
]. Then C[1
I
;t] for anyt. 2
Lemma 4.1.13 Let R be stable balanced joinable. Ift !
I t
0
and t !
I t
00
then t 0
! k
I s
and t 00
! k
I
s for some s and k 0.
Proof. Let t 1
!
I t
0
and t 1
0
!
I t
00
. If 1 and 1 0
are disjoint then from Lemma 4.1.12 the
lemma follows. If1 and 1 0
are not disjoint,then by Theorem 2.3.22, 1and 1 0
mustb e
overlapping. Thusthe lemmaholds by Lemma4.1.11. 2
The parallel reduction t jj
0!s isdened ast C[1
1
;...;1
n ]
1
1
!111 1
n
!s (n 0). We
write t jj
0! 0
s if t 1
1 1111
n
jj
0! s and n>0.
Lemma 4.1.14 Let R be strongly sequential and stable balanced joinable and t jj
0!s.
Then t=
I
s or t !!
I 1
jj
0! 1 !
I s.
Proof. Lett 1
1 1111
n
jj
0! s. Weprovethe lemmabyinduction onn. The casen =0istrivial.
Let t 111111n
jj
0! s (n >0). Thereare twocases.
(1) Some1
i
,say 1
1
,isanindex. Lett 1
1
!
I t
0
121111n
jj
0! s. Applyinginduction hyp othesis
tot 0
1
2 1111n
jj
0! s, weobtain the lemma.
(2) No 1
i
is an index. Since R is strongly sequential, t has an index. Let 1 be an
index of t andt 1
!
I t
00
. Furthermore,consider the following twocases.
(2-1) 1 and 1
i
are non-overlapping for any i. Using the left-linearity of R and
Lemma 4.1.12, we can easilyshowthat t 00
jj
0!s 0
and s !
I s
0
for some s 0
. Thuswe
havet !!
I 1
jj
0! 1 !
I s.
(2-2) 1 and some 1
i
, say 1
1
, are overlapping. Let t 1
1
! t 0
1
2 1111
n
jj
0! s. By The-
orem 2.3.22, we have 1
1
1. From Lemma 4.1.11, it follows that t 00
! k
I s
0
and
t 0
! k
I s
0
forsomes 0
andk0. Thuswehavet !!
I t
0
. Applyinginductionhyp othsis
tot 0
1
2 1111
n
jj
0! s, weobtain the lemma. 2
Theorem 4.1.15 Let R be strongly sequential and stable balanced joinable. Then R
has the normal form property, and index reduction !
I
is anormalizing strategy for R.
