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

Masaki NAKAMURA

Scho ol of Information Science,

Japan Advanced Institute of Science and Technology

February 15, 1999

Keywords: Term Rewriting System, Termination, Transformation, Elimination,

DependencyPair .

This thesis isab out terminationof Term Rewriting Systems (TRSs). The purp ose of

this studyis to improve the elimination methods,which are transformation methods for

simplifyingthetaskofprovingterminationofTRSs. Wehaveknownthatthe elimination

methods are soundwith resp ect to termination,i.e., if the transformed TRS terminates,

so does the original one. The elimination methods can be quite useful in the eld of

automatic termination proofs, since they can easily b e implemented and used to pre-

process the TRSs to be proved terminating. In this thesis, we extend the elimination

methodsbyremovingrules thatare not necessaryfor soundnessfrom transformedTRSs.

Using theimprovedeliminationmetho ds,wecan transformTRSs thatcannot beapplied

by original metho ds intoterminating ones.

1 background

TermRewriting systemsprovideasimpleformalismusefulforthe studyofcomputational

procedures. For equational reasoning, TRSs are applicable in various elds, for exam-

ple, algebraic specication, functional programming languages and automated theorem

proving. A TRS isa setof oriented equations that we call rules describing some relation

between terms. In order to obtaina reduction froma term,we have toidentify apart of

itthat matches the left-handside ofsome rewriterule. Then wecan replacethematched

part of the term with the right-hand side of the rule matched.

A TRS is said to be terminating if no term admits an innite reduction sequence.

Terminationisanimportantprop ertyof TRSs. ForaterminatingTRS, anormalformof

agiventermcanbefoundbyasimpledepth-rstsearch. Unfortunately,terminationisan

undecidableprop ertyofTRSs;nevertheless,thereare sometechniquesthataresuccessful

in particular cases. Those techniques can be divided into two main groups: syntactical

Copyright c

1999byMasakiNAKAMURA

terms isused toprovetermination. Thewell-knownsyntacticalmethod isrecursivepath

order (rpo) by Dershowiz(1982). Given a nite TRS, it is decidable if termination of

the TRS can b e proved with rpo. However, these TRSs are restricted to simplication

orderingsinwhichanytermisgreaterthanitsstrictsubterms. Inthe secondclass,terms

are interpreted insome algebrain order to provetermination. Forany terminated TRS,

some algebraguarantees itstermination.

There are many TRSs whose termination is dicult to prove with current methods

like rp o. One of the approaches to proving termination of such TRSs is a method for

transforming TRSs such that the transformed systems are easier to deal with than the

originalones. Theeliminationmetho dsare thetransformationmethodsinwhichfunction

symb olsconsidered 'useless' are eliminated tosimplify the rewriterules.

Supp osewe wanttoproveterminationofthe followingsystem R

1

of whichwecannot

provetermination with rpo.

R

1

=ff(f(x))!f(g(f(x)))g

Intuitively termination of this system is not dicult: at every step, the numb er of

nested operation symb olsf decreases. By dummy elimination proposed by Ferreiraand

Zantema(1995),wecan eliminate a function symbol g and transform the TRS R

1 into

E(R

1 )=

(

f(f(x)) ! f(3)

f(f(x)) ! f(x)

where 3 is a esh constant. Termination of the TRS E(R

1

) is proved with rpo. In the

denitionof dummyelimination,termswhosero ot symbolisthe onetobeeliminatedare

replaced bya freshconstant 3and itssubterms are treatedasseparate entitiesthat add

the right-hand side of rules. The TRS R

1

terminates since dummy elimination is sound

transformationwithrespecttotermination. Usingapre-processoftheTRSstobeproved

terminating,wecan getthe procedureforautomatic terminationpro ofs,whichcan apply

to TRSs of which termination can not be proveddirectly.

Another approach is the notion of dependency pairs by Arts and Giesl(1997), which

gives an eective method for analyzing an innite reduction sequence. Given a TRS,

dened symb ols of the TRS are dened assymbols inthe rootpositions of the left-hand

side of its rules. Since every left-hand side has of course a dened symbol as its root

symb ol,norulematchesatermwithoutdenedsymb ols. Thesubtermsofthe right-hand

sides of which the root symb ol is a dened symb ol are of importance for the analysis

of innite reduction sequence. The notion of dependency pairs fo cuses on the subterms

of the right-hand sides that have a dened symb ol as the ro ot symb ol. By regarding a

sequence of these dependencypairs, the occurrences of denedsymb olscan betraced.

2 our results

In this thesis, we extend the sphere of the application of dummy elimination.

in transformed rules and remove rules that do not aect soundness. The following is

an example of the TRS that can not be transformed into terminated one by dummy

elimination.

R

2

= (

f(a) ! f(b)

b ! g(a)

We can eliminate the function symb olg and transform the TRS R

1 into

E(R

2 )=

8

>

<

>

:

f(a) ! f(b)

b ! 3

b ! a:

Clearly, the TRS E(R

2

) does not terminate because of the rule b ! a added to the

transformedTRS. Therule b!aiswhattopreservethe subtermaunderthe eliminated

function symb ol g. In the dummy elimination, we have to preserve the subterms under

the eliminatedfunctionsymb olsastheright-handsidesof transformedrules. Wepropose

that it is not necessary to add the subterms in which the dened symb ols donot o ccur.

By our extended dummy elimination, we transform the TRS R

2

intothe following TRS

E 0

(R) without the rule b!a.

E 0

(R

2 )=

(

f(a) ! f(b)

b ! 3

ItiseasytoproveterminationofTRSE 0

(R)withrpo. Hence,wecangettheprocedure

that can apply to more TRSs, including R

2

, than the current procedures induced from

originaldummy eliminationfor automatic termination proofs.

In theproof ofsoundness ofthe extendeddummy elimination,aweakreductionorder

plays an important role. We introduce the argument ltering method to make a weak

reduction order and generally show the inclusion relation between a given TRS and a

transformed TRS in order toensure soundness.

Furthermore,weintro ducetheothereliminationmethods,thedistributionelimination

byZantema(1994),andthegeneraldummyeliminationbyFerreira(1995). Wecanimprove

theirmethodsinasimilarwayandprovetheirsoundness withargumentlteringmethod.