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

Kenji Nakano

Scho ol of Information Science,

Japan Advanced Institute of Science and Technology

February 14, 1997

Keywords: AC-TRS,atting, stacking,Reconstruction Ordering,SDL-Ordering.

Termrewriting system (TRS) isregarded ascomputational model thatreducesterms

by applying directed equations, called rewrite rules. TRS is widely used as a model of

functionalprogramming languages and asbasisof automated theoremproving,specica-

tion and verication.

The termination and conuent prop erties are fundamental notions of TRS as com-

putational models. A rewriting system is said to b e terminating, if there are no innite

reducton sequences of reductions. IfTRS is terminating,any strategycan always reduce

a term into the its normal form. Moreover, we can easily check whether a terminating

TRSisconuent. Thus,theterminationpropertyisveryimportantinthetheoryofTRS.

In general, it is undecidable whether a given TRS is terminating or not. Thus sev-

eral sucient conditions have b een successfully develop ed in particular cases. Generally

speaking,thosetechniquescanbeclasiedintotwoapproaches: semanticorderingmethod

andsyntacticorderinfgone. Inthe former,termsare interpretedcompositionallyinsome

(well-founded monotone) algebra in order to prove termination. The semantionc order-

ing methoed is dicult to b e used in automated proof. The other while, the syntactic

ordering is based on the syntactical structure of terms. The precedence is an order on

function symb ols. Then, Syntactic ordering extends precedece to order on terms. This

paperadoptssyntacticapproach,sincesyntacticorderings can b e implementedeasily for

the termination of TRS. The simplicationordering plays an important roll in syntactic

ordering metho d. The simplicationorderingisdenedasapartialorderthat has mono-

tonic and subterm properties,and the simplication ordering is well-founded. Then itis

wellknownif >is simplicationordering andallreduction rules l!r inaTRS Rsatisfy

l > r, then R is terminating. Many kinds of simpliation orderings have been prop osed

by many researches. Forexample, D. Plaisted intro ducedthe Path of Subterm Ordering

(PSO), N. Dershowitz intro duced the Recursive Path Ordering (RPO), and P. Lescanne

intro duced the RecursiveDecomposition Ordering (RDO),and so on.

Copyright c

1997byKenjiNakano

equations in E are either an Asso ciativity or Commutativity axiom. In AC-TRS, the

equations can be reagrded as unorientedrewrite rules. Thus the equation make innitly

reduction sequences, because equations make non-terminating sequences no matter how

they are used asa rewrite rule. In termination pro of of AC-TRS, we must considerAC-

equivalenceclasses of terms insteadof simpleterms. Indeed, this method has b een widly

used inautomatic termination proofs of rewritesystems with AC equations.

The simplicationordering can not use directly for terminationpro of ofAC-TRS.To

overcome this diculty, the transformation by atting have been introduced. Let f be

AC-op erator, and X ;Y bemultisetsof terms. Then atting transformationisdened by

f(X;f(Y))!

Fl

f(X;Y).

The attened terms have no nesting occurrences of AC operators and the order of

subterms occuring as arguments does not matter. We use a multiset notation to denote

such subterms. Through atting transformation, AC-equivalence class is represented by

a single term. The simplication ordering that satises AC-compatibility can be ap-

plied for proving termination of AC-TRS. The ordering of RPO with atting have AC-

compatibility. Unfortunatly, this ordering is not simplication ordering. Therefore, for

being simplication ordering, a numb er of attempts have been tried to overcome this

diculty.

Bachmairintroduced AssociativePath Ordering (APO), but this require alimitation

on precedence. Kapur intro duced AC-ordering with pseudo-copying transformation and

elevating transformation. It supposed precedence is total order. This ordering does not

require limitationsonprecedence,but ituses non-deterministicprocedurethat ishard to

inplement. RubiointroducedInterpretationrulethatcontainsselectingmaximalordering

term. This metho d does not have non-deterministic procedure. These orderings use

atting transformations for satisfying simplication ordering and AC-compatibility. In

this pap er, weintro ducesanothermethod withoutatting.

In chapter 4, instead of atting, we give the stacking that is a new transformation.

Let f be AC-op erator and X;Y are multisets of terms. The stacking is f(X;f(Y)) !

St

f(f(X;Y)),wheref(111(f

| {z }

n

(T)111)representsf n

(T)

（

）

compress coherentsAC-op erators toone. The stackingkeeps the infomation ofanumber

of continuous AC-op erators in degree. We rst consider RPO with stacking. Unfortu-

nately,thisorderingisnotsimplicationordering. Itdoesnothavemonotonicity. Because

stackingassemblesAC-op eratorstothero otsymb ol,itdisturbsrelationbetweensubterms

and AC-op erators. We must treat transformation carefully for satisfying simplication

ordering and AC-compatibility.

The vanishingAC-op erators causesthat RPOwithattingisnotsimplicationorder-

ing and AC-compatibility. The stacking do es not have vanishing of AC-op erator. How-

ever,the AC-op eratorsinsubterms movestotherootsymb ol. Hence thestackingcrashes

the relation between AC-operators and subterms. We think the degree of AC-op erators

is the inclination of subterms, the stacking changes the inclination of subterms, and the

ordering that RPO with stackingdo es not havemonotonicity.

Weintro ducednewtransformationsfortheinclination. WetreattheinclinationofAC-

AC-op eratorsforsubtermsiscausedbyassemblingAC-op eratortotherootsymbol. Since

the ReconstructiondistributeAC-op erators forsubterms, itmayvanishtheinclinationof

AC-op erators. Reconstruction Ordering (RCO) isbased onReconstuctionand RPO. We

apply Reconstruction for the stackingterm, and compare them byRPO.

We prove that RCO satisfy AC-compatibility, irreducibility, subterm property, and

monotonicity. Unfortunatly, transivity have never proven, because Reconstuction has a

lot of case of degree of AC-op erators and subterms. Thus, itis to o dicult to prove the

transivity.

ThesecondapproachiscalledDepartmenttransformationandLifting transformation.

We examine the condition that disturb realtion b etween AC-op erators and subterms.

There are conditions that stacking crashs relaton and, it is clasifyedinto twocase. The

rst condition is called inclination, the second one called take-in. We can search terms

that have possibility to disturbmonotonicity fortwocondition.

If a term satises inclinatoin condition, we apply Department transformation. De-

partmenttransformationextracts subtermsfromoriginalterm. Ifthe termsatisfytake-in

condition,we apply Lifting transformation. The Lifting transformationchangesthe term

tomultisetofterms. ThesetransformationsareappliedtotermsthathasAC-op eratorsas

the rootsymb ol. SDLOisbasedonRPO, andtermsare transfomed bystacking,Depart-

ment, and Lifting transformations. However, SDLO does not saitisfy the monotonicity.

and it has a problem intrsnaformation.

Therefor, fromtheseobservatoinswecanconclude that anew ordering methodbased

onstackingtransformationhasseveralesentialdicultiesforguaranteeingAC-compatibility.