Japan Advanced Institute of Science and Technology

Japan Advanced Institute of Science and Technology

JAIST Repository

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

Title

Author(s)

Citation

Issue Date

Type

Text version

URL

Rights

Description

of Left-Linear Term Rewriting Systems

Toshimasa Matsumoto

Scho ol of Information Science,

Japan Advanced Institute of Science and Technology

February 15, 2000

Keywords: Term Rewriting System, Left-Linear,Conuence, CriticalPair,

Conuence Condition.

Thisthesisstudiesconuenceconditionsofleft-linearTermRewritingSystems(TRSs).

Conuence conditionsare based onthe notion of criticalpairs, whichare generated from

overlap between rewrite rules. Two kinds of critical pairs have been proposed, that is,

the ordinarycriticalpairsand theextended ones. The ordinarycriticalpairsgivesimpler

conuence conditions than the extended ones. On the other hand, the extended critical

pairs give conuence conditionswith weakerrestrictions. The purposeof this studyis to

give a new conuence condition, which is simple like that based on the ordinary critical

pairs and has weakrestriction likethat based onthe extended ones.

1 Background

A TRS is a set of oriented equations called rewrite rules. In TRS the left-hand side can

be replaced by the right-handside, but not vice versa. This emphasizes the computation

property of equations. For example, we can write 1+2 = 3, or conversely 3 = 1+2

in equational logic. However, when we see it as computations, the equation should be

regardedas1+2!3,whichsays1+2becomes3. Itisjustarewriterulewhichreplaces

1+2 with 3. Generally, in order to obtain a reduction from a term, we have toidentify

a part of it that matches the left-hand side of some rewrite rule. Then we can replace

the matched part of the term with the right-hand side of the rule. Thus, we can get

a natural computational mo del with oriented equations. TRSs are applicable in various

elds, for example, program transformation, automatic theorem proving and functional

programming languages.

Copyright c

2000byToshimasaMatsumoto

swer in non-deterministic computations, and decides whether an equation holds or not.

Hence, it plays an imp ortant role infunctional programming languages, automatic theo-

rem proving, and so on. Unfortunately, conuence is an undecidable property of TRSs.

Thus,several decidable criteria of conuence haveb een proposed based on criticalpairs.

For terminating TRSs, conuence is equivalent to conuence of critical pairs. However,

for non-terminatingTRSs, conuence ofcritical pairs does not guarantee conuence.

In1980,forleft-linearnon-terminatingTRSs,Huetproposedafundamentalconuence

condition, where each ordinary critical pair is closed by a parallel reduction. In 1988,

Toyama extended Huet's conuence condition by analyzing overlap situation. In 1997,

Oostrom extended them further with development, which includesparallel reduction. In

1998, Oyamaguchi and Ohta proposed a conuence condition, with some restriction of

rewrite p ositions,based on ordinarycritical pairs.

In 1981, Toyama proposed a condition based onparallel critical pairs. In 1998, Okui

proposed a condition based on simultaneous critical pairs. Their closed conditions of

extended critical pairs are weaker than those based on ordinary critical pairs. This fact

leads ustoa newcondition based onordinarycritical pairs,whichhas a weakrestriction

similar tothat based onextended critical pairs.

2 Results

In this study, we propose a conuence condition, called most indep endence condition,

based on ordinary critical pairs for left-linear non-terminating TRSs. Since our conu-

ence condition has a closed condition similar to parallel criticalpairs, it has the weakest

restriction amongwell-known conuence conditionsbased onordinarycriticalpairs. The

restriction of rewrite positions in our condition is essential and plays a very important

role in the proof of the conuence prop erty.

Considering several examples, it follows that we can apply our condition to some

TRSstowhichwecannotapply conditionsbasedonextendedcriticalpairs. Therefore,as

the case may be, conditions based onordinarycritical pairs are eective. We display the

followingTRSR

1

(byOkui1998). R

1

doesnotsatisfytheconditionbasedonsimultaneous

critical pairs,but doesthe condition based onparallelcritical pairs orour condition.

R

1

= 8

>

>

>

>

>

>

>

>

>

>

>

>

>

<

>

>

>

>

>

>

>

>

>

>

>

>

>

:

f(g(g(x))) ! a

f(g(h(x))) ! b

f(h(g(x))) ! b

f(h(h(x))) ! c

g(x) ! h(x)

a ! b

b ! c

c ! c

R

1

has a simultaneous critical pair ha;f(h(h(x)))i, which is not closed by a develop-

ment. Therefore, R

1

doesnot satisfy the condition based on simultaneouscritical pairs.

1

ical pairs. Since the arity of everyfunction symb olin R

1

is 1, R

1

satises the restriction

of our condition. Thus,fromour conuence condition, we can showthat R

1

is conuent.