Proving and Disproving Termination of Higher-Order Functions

Higher-OrderFunctions⋆

J¨urgenGiesl,Ren´eThiemann,PeterSchneider-Kamp

LuFGInformatikII,RWTHAachen,Ahornstr.55,52074Aachen,Germany{giesl|thiemann|psk}@informatik.rwth-aachen.deAbstract.Thedependencypairtechniqueisapowerfulmodularmethodforautomatedterminationproofsoftermrewritesystems(TRSs).Wepresenttwoimportantextensionsofthistechnique:First,weshowhowtoproveterminationofhigher-orderfunctionsusingdependencypairs.Tothisend,thedependencypairtechniqueisextendedtohandle(un-typed)applicativeTRSs.Second,weintroduceamethodtoprovenon-terminationwithdependencypairs,whileuptonowdependencypairswereonlyusedtoverifytermination.Ourresultsleadtoaframeworkforcombiningterminationandnon-terminationtechniquesforfirst-andhigher-orderfunctionsinaveryflexibleway.Weimplementedandeval-uatedourresultsintheautomatedterminationproverAProVE.

1Introduction

Oneofthemostpowerfultechniquestoproveterminationorinnermosttermi-nationofTRSsautomaticallyisthedependencypairapproach[4,12,13].In[16],werecentlyshowedthatdependencypairscanbeusedasageneralframeworktocombinearbitrarytechniquesforterminationanalysisinamodularway.Thegeneralideaofthisframeworkistosolveterminationproblemsbyrepeatedlydecomposingthemintosub-problems.Wecallthisnewconceptthe“dependencypairframework”(“DPframework”)todistinguishitfromtheold“dependencypairapproach”.Inparticular,thisframeworkalsofacilitatesthedevelopmentofnewmethodsforterminationanalysis.AfterrecapitulatingthebasicsoftheDPframeworkinSect.2,wepresenttwonewsignificantimprovements:inSect.3weextendtheframeworkinordertohandlehigher-orderfunctionsandinSect.4weshowhowtousetheDPframeworktoprovenon-termination.Sect.5sum-marizesourresultsanddescribestheirempiricalevaluationwiththesystemAProVE.Allproofscanbefoundin[17].

2TheDependencyPairFramework

Wereferto[5]forthebasicsofrewritingandto[4,13,16]formotivationsanddetailsondependencypairs.WeonlyregardfinitesignaturesandTRSs.T(F,V)isthesetoftermsoverthesignatureFandtheinfinitesetofvariablesV={x,y,z,...,α,β,...}.RisaTRSoverFifl,r∈T(F,V)forallrulesl→r∈R.

Wewillpresentamethodforterminationanalysisofuntypedhigher-orderfunctionswhichdonotuseλ-abstraction.Duetotheabsenceofλ,suchfunctionscanberepresentedincurriedformasapplicativefirst-orderTRSs(cf.e.g.,[22]).AsignatureFisapplicativeifitonlycontainsnullaryfunctionsymbolsandabinarysymbol′forfunctionapplication.Moreover,anyTRSRoverFiscalledapplicative.Soinsteadofatermmap(α,x)wewrite′(′(map,α),x).Toeasereadability,weuse′asaninfix-symbolandwelet′associatetotheleft.Thenthistermcanbewrittenasmap′α′x.Thisisverysimilartotheusualnotationofhigher-orderfunctionswhereapplicationisjustdenotedbyjuxtaposition(i.e.,hereonewouldwritemapαxinsteadofmap′α′x).

Example1.Thefunctionmapisusedtoapplyafunctiontoallelementsinalist.Insteadofthehigher-orderrulesmap(α,nil)→nilandmap(α,cons(x,xs))→cons(α(x),map(α,xs)),weencodeitbythefollowingfirst-orderTRS.

map′α′nil→nil

map′α′(cons′x′xs)→cons′(α′x)′(map′α′xs)

(1)(2)

ATRSisterminatingifallreductionsarefinite,i.e.,ifallapplicationsoffunctionsencodedintheTRSterminate.Sointuitively,theTRS{(1),(2)}isterminatingiffmapterminateswheneveritsargumentsareterminatingterms.

ForaTRSRoverF,thedefinedsymbolsareD={root(l)|l→r∈R}andtheconstructorsareC=F\\D.Foreveryf∈Fletf♯beafreshtuplesymbolwiththesamearityasf,whereweoftenwriteFforf♯.ThesetoftuplesymbolsisdenotedbyF♯.Ift=g(t1,...,tm)withg∈D,welett♯denoteg♯(t1,...,tm).Definition2(DependencyPair).ThesetofdependencypairsforaTRSRisDP(R)={l♯→t♯|l→r∈R,tisasubtermofr,root(t)∈D}.Example3.IntheTRSofEx.1,theonlydefinedsymbolis′andmap,cons,andnilareconstructors.LetAPdenotethetuplesymbolfor′.ThenwehavethefollowingdependencypairswheresisthetermAP(map′α,cons′x′xs).

s→AP(cons′(α′x),map′α′xs)s→AP(cons,αx)s→AP(α,x)

′

(3)(4)(5)

s→AP(map′α,xs)s→AP(map,α)

(6)(7)

Fortermination,wetrytoprovethattherearenoinfinitechainsofdepen-dencypairs.Intuitively,adependencypaircorrespondstoafunctioncallandachainrepresentsapossiblesequenceofcallsthatcanoccurduringareduction.Wealwaysassumethatdifferentoccurrencesofdependencypairsarevariabledisjointandconsidersubstitutionswhosedomainsmaybeinfinite.Inthefol-lowingdefinition,Pisusuallyasetofdependencypairs.

Definition4(Chain).LetP,RbeTRSs.A(possiblyinfinite)sequenceofpairss1→t1,s2→t2,...fromPisa(P,R)-chainiffthereisasubstitutionσwith

i∗

tiσ→∗Rsi+1σforalli.Itisaninnermost(P,R)-chainifftiσ→Rsi+1σandsiσ

i

isinnormalformw.r.t.Rforalli.Here,“→R”denotesinnermostreductions.Example5.“(6),(6)”isachain:aninstanceof(6)’sright-handsideAP(map′α1,xs1)canreducetoaninstanceofitsleft-handsideAP(map′α2,cons′x2′xs2).

2

Theorem6(TerminationCriterion[4]).ATRSRis(innermost)termi-natingiffthereisnoinfinite(innermost)(DP(R),R)-chain.

TheideaoftheDPframework[16]istotreatasetofdependencypairsPtogetherwiththeTRSRandtoproveabsenceofinfinite(P,R)-chainsinsteadofexamining→R.Formally,adependencypairproblem(“DPproblem”)1consistsoftwoTRSsPandR(whereinitially,P=DP(R))andaflage∈{t,i}standingfor“tnnermosttermination”.Insteadof“(P,R)-chains”wealsospeakof“(P,R,t)-chains”andinsteadof“innermost(P,R)-chains”wespeakof“(P,R,i)-chains”.Ourgoalistoshowthatthereisnoinfinite(P,R,e)-chain.Inthiscase,wecalltheproblemfinite.

ADPproblem(P,R,e)thatisnotfiniteiscalledinfinite.Butinaddition,(P,R,t)isalreadyinfinitewheneverRisnotterminatingand(P,R,i)isal-readyinfinitewheneverRisnotinnermostterminating.Thus,therecanbeDPproblemswhicharebothfiniteandinfinite.Forexample,theDPproblem(P,R,t)withP={F(f(x))→F(x)}andR={f(f(x))→f(x),a→a}isfinitesincethereisnoinfinite(P,R,t)-chain,butalsoinfinitesinceRisnottermi-nating.SuchDPproblemsdonotcauseanydifficulties,cf.[16].Ifonedetectsaninfiniteproblemduringaterminationproofattempt,onecanaborttheproof,sinceterminationhasbeendisproved(ifallproofstepswere“complete”,i.e.,iftheypreservedtheterminationbehavior).

ADPproblem(P,R,e)isapplicativeiffRisaTRSoveranapplicativesignatureF,andforalls→t∈P,wehavet∈/V,{root(s),root(t)}⊆F♯,andallfunctionsymbolsbelowtherootofsortarefromF.WealsosaythatsuchaproblemisanapplicativeDPproblemoverF.Thus,inanapplicativeDPproblem(P,R,e),thepairss→tofPmusthaveashapewhichissimilartotheoriginaldependencypairs(i.e.,therootsofsandtaretuplesymbolswhichdonotoccurbelowtheroot).ThisrequirementisneededinSect.3.3inordertotransformapplicativetermsbacktoordinaryfunctionalform.

TerminationtechniquesshouldnowoperateonDPproblemsinsteadofTRSs.Werefertosuchtechniquesasdependencypairprocessors(“DPprocessors”).Formally,aDPprocessorisafunctionProcwhichtakesaDPproblemasinputandreturnsanewsetofDPproblemswhichthenhavetobesolvedinstead.Alternatively,itcanalsoreturn“no”.ADPprocessorProcissoundifforallDPproblemsd,disfinitewheneverProc(d)isnot“no”andallDPproblemsinProc(d)arefinite.ProciscompleteifforallDPproblemsd,disinfinitewheneverProc(d)is“no”orwhenProc(d)containsaninfiniteDPproblem.

SoundnessofaDPprocessorProcisrequiredtoprovetermination(inpartic-ular,toconcludethatdisfiniteifProc(d)=∅).Completenessisneededtoprovenon-termination(inparticular,toconcludethatdisinfiniteifProc(d)=no).

SoterminationproofsintheDPframeworkstartwiththeinitialDPproblem(DP(R),R,e),whereedependsonwhetheronewantstoproveterminationorinnermosttermination.ThenthisproblemistransformedrepeatedlybysoundDPprocessors.IfthefinalprocessorsreturnemptysetsofDPproblems,then

terminationisproved.Ifoneoftheprocessorsreturns“no”andallprocessorsusedbeforewerecomplete,thenonehasdisprovedterminationoftheTRSR.Example7.Ifd0istheinitialDPproblem(DP(R),R,e)andtherearesoundprocessorsProc0,Proc1,Proc2withProc0(d0)={d1,d2},Proc1(d1)=∅,andProc2(d2)=∅,thenonecanconcludetermination.ButifProc1(d1)=no,andbothProc0andProc1arecomplete,thenonecanconcludenon-termination.

3DPProcessorsforHigher-OrderFunctions

Sincewerepresenthigher-orderfunctionsbyfirst-orderapplicativeTRSs,allexistingtechniquesandDPprocessorsforfirst-orderTRSscanalsobeusedforhigher-orderfunctions.However,mostterminationtechniquesrelyontheouter-mostfunctionsymbolwhencomparingterms.Thisisalsotruefordependencypairsandstandardreductionorders.Therefore,theyusuallyfailforapplicativeTRSssincehere,alltermsexceptvariablesandconstantshavethesamerootsymbol′.Forexample,adirectterminationproofofEx.1isimpossiblewithstandardreductionordersanddifficult2withdependencypairs.

Therefore,inSect.3.1andSect.3.2weimprovethemostimportantproces-sorsoftheDPframeworkinordertobesuccessfulonapplicativeTRSs.More-over,weintroduceanewprocessorinSect.3.3whichremovesthesymbol′andtransformsapplicativeTRSsandDPproblemsintoordinary(functional)formagain.Sect.5showsthatthesecontributionsindeedyieldapowerfulterminationtechniqueforhigher-orderfunctions.Sect.3.4isacomparisonwithrelatedwork.3.1

ADPProcessorBasedontheDependencyGraph

Thedependencygraphdetermineswhichpairscanfolloweachotherinchains.Definition8(DependencyGraph).Let(P,R,e)beaDPproblem.Thenodesofthe(P,R,e)-dependencygrapharethepairsofPandthereisanarcfroms→ttou→viffs→t,u→visan(P,R,e)-chain.

Example9.ForEx.1,weobtainthefollowing(P,R,e)-dependencygraphforbothe=tande=i.Thereasonisthattheright-handsidesof(3),(4),and(7)havecons′(α′x),cons,ormapastheirfirstarguments.Noinstanceofthesetermsreducestoaninstanceofmap′α(whichisthefirstargumentofs).

s→AP(α,x)(5)s→AP(map,α)(7)s→AP(map′α,xs)(6)s→AP(cons,α′x)(4)s→AP(cons′(α′x),map′α′xs)(3)AsetP′=∅ofdependencypairsisacycleiffforalls→tandu→vinP′,thereisapathfroms→ttou→vtraversingonlypairsofP′.AcycleP′isa

stronglyconnectedcomponent(SCC)ifP′isnotapropersubsetofanothercycle.AsabsenceofinfinitechainscanbeprovedseparatelyforeachSCC,terminationproofscanbemodularizedbydecomposingaDPproblemintosub-problems.Theorem10(DependencyGraphProcessor[16]).ForaDPproblem(P,R,e),letProcreturn{(P1,R,e),...,(Pn,R,e)},whereP1,...,PnaretheSCCsofthe(P,R,e)-dependencygraph.ThenProcissoundandcomplete.ForEx.1,westartwiththeinitialDPproblem(P,R,e),whereP={(3),...,(7)}.TheonlySCCofthedependencygraphis{(5),(6)}.Sotheaboveprocessortransforms(P,R,e)into({(5),(6)},R,e),i.e.,(3),(4),and(7)aredeleted.

Unfortunately,thedependencygraphisnotcomputable.Therefore,forau-tomationoneconstructsanestimatedgraphcontainingatleastallarcsoftherealgraph.Theexistingestimationsthatareusedforautomation[4,18]assumethatallsubtermswithdefinedrootcouldpossiblybeevaluated.Therefore,theyuseafunctioncap,wherecap(t)resultsfromreplacingallsubtermsoftwithdefinedrootsymbolbydifferentfreshvariables.Toestimatewhethers→tandu→vformachain,onecheckswhethercap(t)unifieswithu(afterrenamingtheirvariables).Moreover,ifoneregardsterminationinsteadofinnermostter-mination,onefirsthastolinearizecap(t),i.e.,multipleoccurrencesofthesamevariableincap(t)arerenamedapart.Furtherrefinementsofthisestimationcanbefoundin[18];however,theyrelyonthesamefunctioncap.

TheseestimationsarenotsuitableforapplicativeTRSs.Theproblemisthatthere,allsubtermsexceptvariablesandconstantshavethedefinedrootsymbol′andarethusreplacedbyvariableswhenestimatingthearcsofthedependencygraph.SoforEx.1,theestimationsassumethat(3)couldbefollowedbyanydependencypairinchains.Thereasonisthattheright-handsideof(3)isAP(cons′(α′x),map′α′xs)andcapreplacesbothargumentsofAPbyfreshvariables,sincetheirrootsymbol′isdefined.TheresultingtermAP(y,z)uni-fieswiththeleft-handsideofeverydependencypair.Therefore,theestimateddependencygraphcontainsadditionalarcsfrom(3)toeverydependencypair.

Theproblemisthattheseestimationsdonotcheckwhethersubtermswithdefinedrootcanreallybereducedfurtherwhenbeinginstantiated.Forexample,thefirstargumentcons′(α′x)of(3)’sright-handsidecanneverbecomearedexforanyinstantiation.Thereasonisthatallleft-handsidesoftheTRShavetheformmap′t1′t2.Thus,oneshouldnotreplacecons′(α′x)byafreshvariable.

Therefore,wenowrefinecap’sdefinition.Ifasubtermcanclearlyneverbe-comearedex,thenitisnotreplacedbyavariableanymore.Here,icapisusedfori

ermination.Definition11(icap,tcap).LetRbeaTRSoverF,letf∈F∪F♯.(i)icap(x)=xforallx∈V

(ii)icap(f(t1,...,tn))=f(icap(t1),...,icap(tn))ifff(icap(t1),...,icap(tn))

doesnotunifywithanyleft-handsideofarulefromR(iii)icap(f(t1,...,tn))isafreshvariable,otherwise

Wedefinetcaplikeicapbutin(i),tcap(x)isadifferentfreshvariablefor

5

everyoccurrenceofx.Moreoverin(ii),weusetcap(ti)insteadoficap(ti).Nowonecandetectthat(3)shouldnotbeconnectedtoanypairinthede-pendencygraph,sinceicap(AP(cons′(α′x),map′α′xs))=AP(cons′y,z)doesnotunifywithleft-handsidesofdependencypairs.Similarremarksholdfortcap.Thisleadstothefollowingimprovedestimation.3

Definition12(ImprovedEstimatedDependencyGraph).Intheesti-mated(P,R,t)-dependencygraphthereisanarcfroms→ttou→vifftcap(t)anduareunifiable.Intheestimated(P,R,i)-dependencygraphthereisanarcfroms→ttou→vifficap(t)anduareunifiablebyanmguµ(afterrenamingtheirvariables)suchthatsµanduµareinnormalformw.r.t.R.NowtheestimatedgraphisidenticaltotherealdependencygraphinEx.9.Theorem13(SoundnessoftheImprovedEstimation).Thedependencygraphisasubgraphoftheestimateddependencygraph.

Ofcourse,thenewestimationofdependencygraphsfromDef.12isalsousefulfornon-applicativeTRSsandDPproblems.Thebenefitsofourimprovements(alsoforordinaryTRSs)isdemonstratedbyourexperimentsinSect.5.3.2

DPProcessorsBasedonOrdersandonUsableRules

Classicaltechniquesforautomatedterminationproofstrytofindareductionorder≻suchthatl≻rholdsforallrulesl→r.Inpractice,mostordersaresimplificationorders[10].However,terminationofmanyimportantTRSscannotbeprovedwithsuchordersdirectly.Therefore,thefollowingprocessorallowsustousesuchordersintheDPframeworkinstead.Itgeneratesconstraintswhichshouldbesatisfiedbyareductionpair[23](󰀁,≻)where󰀁isreflexive,transitive,monotonic,andstableand≻isastablewell-foundedordercompatiblewith󰀁(i.e.,󰀁◦≻⊆≻and≻◦󰀁⊆≻).Nowonecanuseexistingtechniquestosearchforsuitablerelations󰀁and≻,andinthisway,classicalsimplificationorderscanproveterminationofTRSswheretheywouldhavefailedotherwise.

Foraproblem(P,R,e),theconstraintsrequirethatatleastoneruleinPisstrictlydecreasing(w.r.t.≻)andallremainingrulesinPandRareweaklyde-creasing(w.r.t.󰀁).Requiringl󰀁rforl→r∈Rensuresthatinchainss1→t1,s2→t2,...withtiσ→∗Rsi+1σ,wehavetiσ󰀁si+1σ.Hence,ifareductionpairsatisfiestheseconstraints,thenthestrictlydecreasingpairsofPcannotoccurinfinitelyofteninchains.Thus,thefollowingprocessordeletesthesepairsfromP.ForanyTRSPandanyrelation≻,letP≻={s→t∈P|s≻t}.

Theorem14(ReductionPairProcessor[16]).Let(󰀁,≻)beareductionpair.ThenthefollowingDPprocessorProcissoundandcomplete.ForaDPproblem(P,R,e),Procreturns

•{(P\\P≻,R,e)},ifP≻∪P󰀁=PandR󰀁=R•{(P,R,e)},otherwise

DPproblems(P,R,i)forinnermostterminationcanbesimplifiedbyre-placingthesecondcomponentRbythoserulesfromRthatareusableforP(i.e.,bytheusablerulesofP).ThenbyThm.14,aweakdecreasel󰀁risnotrequiredforallrulesbutonlyfortheusablerules.Asdefinedin[4],theusablerulesofatermtcontainallf-rulesforallfunctionsymbolsfoc-curringint.Moreover,iff’srulesareusableandthereisarulef(...)→rinRwhoseright-handsidercontainsasymbolg,thengisusable,too.TheusablerulesofaTRSParedefinedastheusablerulesofitsright-handsides.

Forinstance,afterapplyingthedependencygraphprocessortoEx.1,wehavetheremainingdependencypairs(5)and(6)withtheright-handsidesAP(α,x)andAP(map′α,xs).WhileAP(α,x)hasnousablerules,AP(map′α,xs)con-tainsthedefinedfunctionsymbol′andtherefore,all′-rulesareusable.

ThisindicatesthatthedefinitionofusableruleshastobeimprovedtohandleapplicativeTRSssuccessfully.Otherwise,whenever′occursintheright-handsideofadependencypair,thenallrules(exceptrulesoftheformf→...)wouldbeusable.Theproblemisthatthecurrentdefinitionof“usablerules”assumesthatall′-rulescanbeappliedtoanysubtermwiththerootsymbol′.

Thus,werefinethedefinitionofusablerules.Nowasubtermstartingwith′onlyinfluencesthecomputationoftheusablerulesifsomesuitableinstantiationofthissubtermwouldstartnewreductions.Todetectthis,weagainusethefunctionicapfromDef.11.Forexample,map′αcanneverbereducedifαisinstantiatedbyanormalform,sincemap′αdoesnotunifywiththeleft-handsideofanyrule.Therefore,theright-handsideAP(map′α,xs)of(6)shouldnothaveanyusablerules.4

Definition15(Improved󰀁UsableRules).ForaDPproblem(P,R,i),wede-finetheusablerulesU(P)=s→t∈PU(t).HereU(t)⊆Risthesmallestsetwith:•Ift=f(t1,...,tn),f∈F∪F♯,andf(icap(t1),...,icap(tn))unifieswith

aleft-handsidelofarulel→r∈R,thenl→r∈U(t).•Ifl→r∈U(t),thenU(r)⊆U(t).

•Ift′isasubtermoft,thenU(t′)⊆U(t).

Theorem16(UsableRuleProcessor).ForaDPproblem(P,R,e),letProcreturn{(P,U(P),i)}ife=iand{(P,R,e)}otherwise.ThenProcissound.5Example17.InEx.1,nowthedependencypairsintheremainingDPproblem({(5),(6)},R,i)havenousablerules.Thus,Thm.16transformsthisDPprob-leminto({(5),(6)},∅,i).ThenwiththeprocessorofThm.14wetrytofindareductionpairsuchthat(5)and(6)aredecreasing.Anysimplificationorder≻(eventheembeddingorder)makesbothpairsstrictlydecreasing:s≻AP(α,x)ands≻AP(map′α,xs)fors=AP(map′α,cons′x′xs).Thus,bothdepen-dencypairsareremovedandtheresultingDPproblem(∅,R,i)istransformed

intotheemptysetbythedependencygraphprocessorofThm.10.Soinnermostterminationofthemap-TRSfromEx.1cannoweasilybeprovedautomatically.NotethatthisTRSisnon-overlappingandthus,itbelongstoawell-knownclasswhereinnermostterminationimpliestermination.

Similartotheimprovedestimationofdependencygraphsintheprevioussection,thenewimproveddefinitionofusablerulesfromDef.15isalsobeneficialforordinarynon-applicativeTRSs,cf.Sect.5.

In[32],weshowedthatundercertainconditions,theusablerulesof[4]canalsobeusedtoprovefullinsteadofjustinnermosttermination(forarbitraryTRSs).Then,evenfortermination,itisenoughtorequirel󰀁rjustfortheusablerulesinThm.14.ThisresultalsoholdsforthenewimprovedusablerulesofDef.15,providedthatoneusestcapinsteadoficapintheirdefinition.3.3

ADPProcessortoTransformApplicativetoFunctionalForm

SomeapplicativeDPproblemscanbetransformed(back)toordinaryfunctionalform.Inparticular,thisholdsforproblemsresultingfromfirst-orderfunctions(encodedbycurrying).Thistransformationisadvantageous:e.g.,theprocessorinThm.14issignificantlymorepowerfulforDPproblemsinfunctionalform,sincestandardreductionordersfocusontherootsymbolwhencomparingterms.Example18.Weextendthemap-TRSbythefollowingrulesforminusanddiv.Notethatadirectterminationproofwithsimplificationordersisimpossible.

minus′x′0→x

(8)

div′0′(s′y)→0

(10)

minus′(s′x)′(s′y)→minus′x′y(9)div′(s′x)′(s′y)→s′(div′(minus′x′y)′(s′y))(11)

Whilemapisreallyahigher-orderfunction,minusanddivcorrespondtofirst-orderfunctions.Itagainsufficestoverifyinnermosttermination,sincethisTRSRisnon-overlapping.TheimprovedestimateddependencygraphhasthreeSCCscorrespondingtomap,minus,anddiv.Thus,bythedependencygraphandtheusableruleprocessors(Thm.10and16),theinitialDPproblem(DP(R),R,i)istransformedintothreenewproblems.Thefirstproblem({(5),(6)},∅,i)formapcanbesolvedasbefore.TheDPproblemsforminusanddivare:

({AP(minus′(s′x),s′y)→AP(minus′x,y)},∅,i)

(12)

({AP(div′(s′x),s′y)→AP(div′(minus′x′y),s′y)},{(8),(9)},i)(13)

Since(12)and(13)donotcontainmapanymore,onewouldliketochangethembacktoconventionalfunctionalform.ThentheycouldbereplacedbythefollowingDPproblems.Here,every(new)functionsymbolislabelledbyitsarity.

({MINUS2(s1(x),s1(y))→MINUS2(x,y)},∅,i)

({DIV2(s1(x),s1(y))→DIV2(minus2(x,y),s1(y))},

{minus2(x,00)→x,minus2(s1(x),s1(y))→minus2(x,y)},i)

(14)(15)

TheseDPproblemsareeasytosolve:forexample,theconstraintsofthere-ductionpairprocessor(Thm.14)aresatisfiedbythepolynomialorderwhich

8

mapss1(x)tox+1,minus2(x,y)tox,andeveryothersymboltothesumofitsarguments.Thus,terminationcouldimmediatelybeprovedautomatically.NowwecharacterizethoseapplicativeTRSswhichcorrespondtofirst-orderfunctionsandcanbetranslatedintofunctionalform.IntheseTRSs,foranyfunctionsymbolfthereisanumbern(calleditsarity)suchthatfonlyoccursintermsoftheformf′t1′...′tn.Sotherearenoapplicationswithtoofewortoomanyarguments.Moreover,therearenotermsx′twherethefirstargumentof′isavariable.Def.19extendsthisideafromTRSstoDPproblems.Definition19(ArityandProperTerms).Let(P,R,e)beanapplicativeDPproblemoverF.Foreachf∈F\\{′}letarity(f)=max{n|f′t1′...′tnor(f′t1′...′tn)♯occursinP∪R}.Atermtisproperifft∈Vort=f′t1′...′tnort=(f′t1′...′tn)♯whereinthelasttwocases,arity(f)=nandalltiareproper.Moreover,(P,R,e)isproperiffalltermsinP∪Rareproper.TheDPproblems(12)and(13)forminusanddivareproper.Here,minusanddivhavearity2,shasarity1,and0hasarity0.Buttheproblem({(5),(6)},∅,i)formapisnotproperas(5)containsthesubtermAP(α,x)withα∈V.

Thefollowingtransformationtranslatespropertermsfromapplicativetofunctionalform.Tothisend,f′t1′...′tnisreplacedbyfn(...),wherenisf’sarity(asdefinedinDef.19)andfnisanewn-aryfunctionsymbol.Inthisway,(12)and(13)weretransformedinto(14)and(15)inEx.18.

Definition20(TransformationA).AmapseverypropertermfromT(F∪F♯,V)toatermfromT({fn,Fn|f∈F\\{′},arity(f)=n},V):•A(x)=xforallx∈V

•A(f′t1′...′tn)=fn(A(t1),...,A(tn))forallf∈F\\{′}•A((f′t1′...′tn)♯)=Fn(A(t1),...,A(tn))forallf∈F\\{′}

ForanyTRSRwithonlyproperterms,letA(R)={A(l)→A(r)|l→r∈R}.WenowdefineaDPprocessorwhichreplacesproperDPproblems(P,R,e)by(A(P),A(R),e).Itssoundnessisduetothefactthatevery(P,R,e)-chainre-′∗

sultsinan(A(P),A(R),e)-chain,i.e.,thattiσ→∗Rsi+1σimpliesA(ti)σ→A(R)A(si+1)σ′forsomesubstitutionσ′.Thereasonisthattiandsi+1areproperandwhileσmayintroducenon-properterms,everychaincanalsobeconstructedwithasubstitutionσ(x)areproper.Thus,whilesoundnessandcompletenessofthefollowingprocessormightseemintuitive,theformalproofincludingthisconstructionisquiteinvolvedandcanbefoundin[17].

Theorem21(DPProcessorforTransformationinFunctionalForm).ForanyDPproblem(P,R,e),letProcreturn{(A(P),A(R),e)}if(P,R,e)isproperand{(P,R,e)}otherwise.ThenProcissoundandcomplete.

WiththeprocessorofThm.21andournewimprovedestimationofdepen-dencygraphs(Def.12),itdoesnotmatteranymorefortheterminationproofwhetherfirst-orderfunctionsarerepresentedinordinaryfunctionalorinapplica-9

tiveform:inthelattercase,dependencypairswithnon-properright-handsidesarenotinSCCsoftheimprovedestimateddependencygraph.Hence,afterap-plyingthedependencygraphprocessorofThm.10,allremainingDPproblemsareproperandcanbetransformedintofunctionalformbyThm.21.

AsanalternativetotheprocessorofThm.21,onecanalsocouplethetrans-formationAwiththereductionpairprocessorfromThm.14.ThenaDPproblem(P,R,e)istransformedinto{(P\\{s→t|A(s)≻A(t)},R,e)}if(P,R,e)isproper,ifA(P)≻∪A(P)󰀁=A(P),andifA(R)󰀁=A(R)holdsforsomere-ductionpair(󰀁,≻).Anadvantageofthisalternativeprocessoristhatitcanbecombinedwithourresultsfrom[32]onapplyingusablerulesforterminationinsteadofinnermostterminationproofs,cf.Sect.3.2.3.4

ComparisonwithRelatedWork

Mostapproachesforhigher-orderfunctionsintermrewritingusehigher-orderTRSs.Whilethereexistpowerfulterminationcriteriaforhigher-orderTRSs(e.g.,[7,29]),themainautomatedterminationtechniquesforsuchTRSsaresimplificationorders(e.g.,[20])whichfailonfunctionslikedivinEx.18.

Exceptionsarethemonotonichigher-ordersemanticpathorder[8]andtheexistingvariantsofdependencypairsforhigher-orderTRSs.However,thesevari-antsrequireconsiderablerestrictions(e.g.,ontheTRSs[31]orontheordersthatmaybeused[3,24,30].)Soincontrasttoourresults,theyarelesspowerfulthantheoriginaldependencypairtechniquewhenappliedtofirst-orderfunctions.

Terminationtechniquesforhigher-orderTRSsoftenhandlearicherlanguagethanourresults.Buttheseapproachesareusuallydifficulttoautomate(therearehardlyanyimplementationsofthesetechniquesavailable).Incontrast,itisveryeasytointegrateourresultsintoexistingterminationproversforordinaryfirst-orderTRSsusingdependencypairs(andfirst-orderreductionorders).

Otherapproachesrepresenthigher-orderfunctionsbyfirst-orderTRSs[1,2,19,25,33],similartous.However,theymostlyusemonomorphictypes(thisre-strictionisalsoimposedinsomeapproachesforhigher-orderTRSs[8]).Inotherwords,therethetypesareonlybuiltfrombasictypesandtypeconstructorslike→or×,buttherearenotypevariables,i.e.,nopolymorphictypes.Thentermslike“map′minus′xs”and“map′(minus′x)′xs”cannotbothbewelltyped,butoneneedsdifferentmap-symbolsforargumentsofdifferenttypes.Incontrast,ourapproachusesuntypedtermrewriting.Hence,itcanbeappliedfortermi-nationanalysisofpolymorphicoruntypedfunctionallanguages.Moreover,[25]and[33]onlyconsiderextensionsofthelexicographicpathorder,whereaswecanalsohandlenon-simplyterminatingTRSslikeEx.18.

4ADPProcessorforProvingNon-Termination

Almostalltechniquesforautomatedterminationanalysistrytoprovetermina-tionandtherearehardlyanymethodstoprovenon-termination.Butdetectingnon-terminationautomaticallywouldbeveryhelpfulwhendebuggingprograms.

WeshowthattheDPframeworkisparticularlysuitableforcombiningboth

10

terminationandnon-terminationanalysis.WeintroduceaDPprocessorwhichtriestodetectinfiniteDPproblemsinordertoanswer“no”.Then,ifallprevi-ousprocessorswerecomplete,wecanconcludenon-terminationoftheoriginalTRS.AsshownbyourexperimentsinSect.5,ournewprocessoralsosuccess-fullyhandlesnon-terminatinghigher-orderfunctionsiftheyarerepresentedbyfirst-orderTRSs.AnimportantadvantageoftheDPframeworkisthatitcancouplethesearchforaproofandadisproofoftermination:Processorswhichtrytoproveterminationarealsohelpfulforthenon-terminationproofbecausetheytransformtheinitialDPproblemintosub-problems,wheremostofthemcaneasilybeprovedfinite.Sotheydetectthosesub-problemswhichcouldcausenon-termination.Therefore,thenon-terminationprocessorsshouldonlyoperateonthesesub-problemsandthus,theyonlyhavetoregardasubsetoftheruleswhensearchingfornon-termination.Ontheotherhand,processorsthattrytodisproveterminationarealsohelpfulfortheterminationproof,evenifsomeofthepreviousprocessorswereincomplete.Thereasonisthattherearemanyin-determinismsinaterminationproofattempt,sinceusuallymanyDPprocessorscanbeappliedtoaDPproblem.Thus,ifonecanfindoutthataDPproblemisinfinite,oneknowsthatonehasreacheda“deadend”andshouldbacktrack.

Toprovenon-terminationwithintheDPframework,inSect.4.1weintroduceloopingDPproblemsandinSect.4.2weshowhowtodetectsuchDPproblemsautomatically.Finally,Sect.4.3isacomparisonwithrelatedwork.4.1

ADPProcessorBasedonLoopingDPProblems

AnobviousapproachtofindinfinitereductionsistosearchforatermswhichevaluatestoatermC[sµ]containinganinstanceofs.ATRSwithsuchreduc-tionsiscalledlooping.Clearly,anaivesearchforloopingtermsisverycostly.

Incontrastto“loopingTRSs”,whenadaptingtheconceptofloopingnesstoDPproblems,weonlyhavetoconsidertermssoccurringindependencypairsandwedonothavetoregardanycontextsC.Thereasonisthatsuchcontextsarealreadyremovedbytheconstructionofdependencypairs.Thm.23showsthatinthiswayonecanindeeddetectallloopingTRSs.

Definition22(LoopingDPProblems).ADPproblem(P,R,t)isloopingiffthereisa(P,R)-chains1→t1,s2→t2,...withtiσ→∗Rsi+1σforallisuchthats1σmatchesskσforsomek>1(i.e.,s1σµ=skσforasubstitutionµ).Theorem23.ATRSRisloopingifftheDPproblem(DP(R),R,t)islooping.Example24.ConsiderToyama’sexampleR={f(0,1,x)→f(x,x,x),g(y,z)→y,g(y,z)→z}andP=DP(R)={F(0,1,x)→F(x,x,x)}.Wehavethe(P,R)-chainF(0,1,x1)→F(x1,x1,x1),F(0,1,x2)→F(x2,x2,x2),sinceF(x1,x1,x1)σ→∗RF(0,1,x2)σforσ(x1)=σ(x2)=g(0,1).AsthetermF(0,1,x1)σmatchesF(0,1,x2)σ(theyareevenidentical),theDPproblem(P,R,t)islooping.OurgoalistodetectloopingDPproblems.Intheterminationcase,everyloopingDPproblemisinfiniteandhence,ifallprecedingDPprocessorswerecomplete,thenterminationisdisproved.However,thedefinitionof“looping”fromDef.22cannotbeusedforinnermosttermination:inEx.24,(DP(R),R,t)

11

islooping,but(DP(R),R,i)isfiniteandRisinnermostterminating.6

Nevertheless,fornon-overlappingDPproblems,(P,R,i)isinfinitewhenever(P,R,t)isinfinite.Sohereloopingnessof(P,R,t)indeedimpliesthat(P,R,i)isinfinite.Wecall(P,R,e)non-overlappingifRisnon-overlappingandnoleft-handsideofRunifieswithanon-variablesubtermofaleft-handsideofP.Lemma25(LoopingandInfiniteDPProblems).

(a)If(P,R,t)islooping,then(P,R,t)isinfinite.

(b)If(P,R,t)isinfiniteandnon-overlapping,then(P,R,i)isinfinite.NowwecandefinetheDPprocessorforprovingnon-termination.

Theorem26(Non-TerminationProcessor).ThefollowingDPprocessorProcissoundandcomplete.ForaDPproblem(P,R,e),Procreturns•“no”,if(P,R,t)isloopingand(e=tor(P,R,e)isnon-overlapping)•{(P,R,e)},otherwise4.2

DetectingLoopingDPProblems

OurcriteriatodetectloopingDPproblemsautomaticallyusenarrowing.Definition27(Narrowing).LetRbeaTRSwhichmayalsohaverulesl→rwithV(r)⊆V(l)orl∈V.Atermtnarrowstos,denotedt󰀂R,δ,ps,iffthereisasubstitutionδ,a(variable-renamed)rulel→r∈Randanon-variablepositionpoftwhereδ=mgu(t|p,l)ands=t[r]pδ.Let󰀂R,δbetherelationwhichpermitsnarrowingstepsonallpositionsp.Let󰀂(P,R),δdenote󰀂P,δ,ε∪󰀂R,δ,whereεistherootposition.Moreover,󰀂∗(P,R),δisthesmallestrelationcontaining󰀂(P,R),δ1◦...◦󰀂(P,R),δnforalln≥0andallsubstitutionswhereδ=δ1...δn.Example28.LetR={f(x,y,z)→g(x,y,z),g(s(x),y,z)→f(z,s(y),z)}andP=DP(R)={F(x,y,z)→G(x,y,z),G(s(x),y,z)→F(z,s(y),z)}.ThetermG(x,y,z)canonlybenarrowedbytheruleG(s(x′),y′,z′)→F(z′,s(y′),z′)ontherootpositionandhence,weobtainG(x,y,z)󰀂P,[x/s(x′),y′/y,z′/z],εF(z,s(y),z).Tofindloops,wenarrowtheright-handsidetofadependencypairs→tuntilonereachesaterms′suchthatsδsemi-unifieswiths′(i.e.,sδµ1µ2=s′µ1forsomesubstitutionsµ1andµ2).Here,δisthesubstitutionusedfornarrowing.ThenweindeedhavealoopasinDef.22bydefiningσ=δµ1andµ=µ2.Semi-unificationencompassesbothmatchingandunificationandalgorithmsforsemi-unificationcanforexamplebefoundin[21,27].

Theorem29(LoopDetectionbyForwardNarrowing).Let(P,R,e)bea

′

DPproblem.Ifthereisans→t∈Psuchthatt󰀂∗(P,R),δsandsδsemi-unifieswiths′,then(P,R,t)islooping.

Example30.WecontinuewithEx.28.WehadG(x,y,z)󰀂(P,R),δF(z,s(y),z)whereδ=[x/s(x′),y′/y,z′/z].Applyingδtotheleft-handsides=F(x,y,z)ofthefirstdependencypairyieldsF(s(x′),y,z).NowF(s(x′),y,z)semi-unifieswithF(z,s(y),z),sinceF(s(x′),y,z)µ1µ2=F(z,s(y),z)µ1forthesubstitutionsµ1=[z/s(x′)]andµ2=[y/s(y)].(However,thefirsttermdoesnotmatchorunifywiththesecond.)Thus,(P,R,t)isloopingandRdoesnotterminate.However,whiletheDPproblemofToyama’sexample(Ex.24)islooping,thisisnotdetectedbyThm.29.Thereasonisthattheright-handsideF(x,x,x)oftheonlydependencypaircannotbenarrowed.Therefore,wenowintroducea“back-ward”variant7oftheabovecriterionwhichnarrowswiththereversedTRSsP−1andR−1.Ofcourse,ingeneralP−1andR−1mayalsohaverulesl→rwithV(r)⊆V(l)orl∈V.However,theusualdefinitionofnarrowingcanimmediatelybeextendedtosuchTRSs,cf.Def.27.

Theorem31(LoopDetectionbyBackwardNarrowing).Let(P,R,e)

′′

beaDPproblem.Ifthereisans→t∈Psuchthats󰀂∗(P−1,R−1),δtandtsemi-unifieswithtδ,then(P,R,t)islooping.

Example32.TodetectthatToyama’sexample(Ex.24)islooping,westartwiththeleft-handsides=F(0,1,x)andnarrow0tog(0,z)usingy→g(y,z)∈R−1.Thenwenarrow1tog(y′,1)byz′→g(y′,z′).ThereforeweobtainF(0,1,x)

′

󰀂∗(P−1,R−1),[y/0,z′/1]F(g(0,z),g(y,1),x).Nowt=F(g(0,z),g(y,1),x)(semi-)unifieswiththecorrespondingright-handsidet=F(x,x,x)usingµ1=[x/g(0,1),y/0,z/1].Thus,(DP(R),R,t)isloopingandtheTRSisnotterminating.However,therearealsoTRSswherebackwardnarrowingfailsandforwardnarrowingsucceeds.8NotethatEx.24whereforwardnarrowingfailsisnotright-linearandthattheexampleinFootnote8wherebackwardnarrowingfailsisnotleft-linear.Infact,ourexperimentsshowthatmostloopingDPproblems(P,R,t)canbedetectedbyforwardnarrowingifP∪Risright-linearandbybackwardnarrowingifP∪Risleft-linear.Therefore,weusethenon-terminationprocessorofThm.26withthefollowingheuristicinoursystemAProVE[15]:•IfP∪Risright-andnotleft-linear,thenuseforwardnarrowing(Thm.29).•Otherwise,weusebackwardnarrowing(Thm.31).IfP∪Risnotleft-linear,thenmoreoverwealsopermitnarrowingstepsinvariables(i.e.,t|p∈VispermittedinDef.27).ThereasonisthatthenthereareloopingDPproblemswhichotherwisecannotbedetectedbyforwardorbackwardnarrowing.9•Moreover,toobtainafinitesearchspace,weuseanupperboundonthenumberoftimesthatarulefromP∪Rcanbeusedfornarrowing.

4.3ComparisonwithRelatedWork

WeusenarrowingtoidentifyloopingDPproblems.ThisisrelatedtotheconceptofforwardclosuresofaTRSR[10].However,ourapproachdiffersfromforwardclosuresbystartingfromtherulesofanotherTRSPandbyalsoallowingnarrow-ingswithP’srulesonrootlevel.(Thereasonisthatweprovenon-terminationwithintheDPframework.)Moreover,wealsoregardbackwardnarrowing.

Thereareonlyfewpapersonautomaticallyprovingnon-terminationofTRSs.Anearlyworkis[28]whichdetectsTRSsthatarenotsimplyterminating(buttheymaystillterminate).Recently,[36,37]presentedmethodsforprovingnon-terminationofstringrewritesystems(i.e.,TRSswhereallfunctionsymbolshavearity1).Similartoourapproach,[36]uses(forward)narrowingand[37]usesancestorgraphswhichcorrespondto(backward)narrowing.However,ourapproachdifferssubstantiallyfrom[36,37]:ourtechniqueworkswithintheDPframework,whereas[36,37]operateonthewholesetofrules.Therefore,wecanbenefitfromallpreviousDPprocessorswhichdecomposetheinitialDPprob-lemintosmallersub-problemsandidentifythosepartswhichcouldcausenon-termination.Moreover,weregardfulltermrewritinginsteadofstringrewriting.Therefore,weusesemi-unificationtodetectloops,whereasforstringrewriting,matchingissufficient.Finally,wealsopresentedaconditiontodisproveinner-mosttermination,whereas[36,37]onlytrytodisprovefulltermination.

5ExperimentsandConclusion

TheDPframeworkisageneralconceptforcombiningterminationtechniquesinamodularway.Wepresentedtwoimportantimprovements:First,weex-tendedtheframeworkinordertohandlehigher-orderfunctions,representedasapplicativefirst-orderTRSs.Tothisend,wedevelopedthreenewcontributions:arefinedapproximationofdependencygraphs,animproveddefinitionofusablerules,andanewprocessortotransformapplicativeDPproblemsintofunctionalform.Theadvantagesofourapproach,alsocomparedtorelatedwork,arethefollowing:itissimpleandveryeasytointegrateintoanyterminationproverbasedondependencypairs(e.g.,AProVE[15],CiME[9],TTT[19]).Moreover,itencompassestheoriginalDPframework,e.g.,itisatleastassuccessfulonordinaryfirst-orderfunctionsastheoriginaldependencypairtechnique.Finally,ourapproachtreatsuntypedhigher-orderfunctions,i.e.,itcanbeusedforter-minationanalysisofpolymorphicanduntypedfunctionallanguages.

AsasecondextensionwithintheDPframework,weintroducedanewpro-cessorfordisprovingterminationautomatically(animportantproblemwhichwashardlytackleduptonow).AmajoradvantageofourapproachisthatitcombinestechniquesforprovingandfordisprovingterminationintheDPframe-work,whichisbeneficialforbothterminationandnon-terminationanalysis.

Weimplementedallthesecontributionsinthenewestversionofourtermi-nationproverAProVE[15].Duetotheresultsofthispaper,AProVE1.2wasthemostpowerfultoolforbothterminationandnon-terminationproofsofTRSsattheAnnualInternationalCompetitionofTerminationTools2005[34].Inthefol-14

lowingtable,wecompareAProVE1.2withitspredecessorAProVE1.1d-γ,whichwasthewinningtoolforTRSsatthecompetitionin2004.WhileAProVE1.1d-γalreadycontainedourresultsonnon-terminationanalysis,thecontributionsonhandlingapplicativeTRSsfromSect.3weremissing.Fortheexperiments,weusedthesamesettingasinthecompetitionwithatimeoutof60secondsforeachexample(wherehowevermostproofstakelessthantwoseconds).

higher-order(61TRSs)non-term(90TRSs)TPDB(838TRSs)

tnt

8259572492

erminationresp.n

13.J.Giesl,T.Arts,andE.Ohlebusch.Modularterminationproofsforrewriting

usingdependencypairs.JournalofSymbolicComputation,34(1):21–58,2002.14.J.Giesl,R.Thiemann,P.Schneider-Kamp,andS.Falke.Improvingdependency

pairs.InProc.LPAR’03,LNAI2850,pages165–179,2003.

15.J.Giesl,R.Thiemann,P.Schneider-Kamp,andS.Falke.Automatedtermination

proofswithAProVE.InProc.RTA’04,LNCS3091,pages210–220,2004.

16.J.Giesl,R.Thiemann,andP.Schneider-Kamp.TheDPframework:Combining

techniquesforautom.terminationproofs.InProc.LPAR’04,LNAI3452,2005.17.J.Giesl,R.Thiemann,andP.Schneider-Kamp.Provinganddisprovingtermi-nationofhigher-orderfunctions.TechnicalReportAIB-2005-03,RWTHAachen,2005.Availablefromhttp://aib.informatik.rwth-aachen.de.

18.N.HirokawaandA.Middeldorp.AutomatingtheDPmethod.InProc.CADE’03,

LNAI2741,pages32–46,2003.FullversioninInformationandComputation.19.N.HirokawaandA.Middeldorp.TyroleanTerminationTool.InProc.RTA’05,

LNCS3467,pages175–184,2005.

20.J.-P.JouannaudandA.Rubio.Higher-orderrecursivepathorderings.InProc.

LICS’99,pages402–411,1999.

21.D.Kapur,D.Musser,P.Narendran,andJ.Stillman.Semi-unification.Theoretical

ComputerScience,81(2):169–187,1991.

22.R.Kennaway,J.W.Klop,R.Sleep,andF.-J.deVries.Comparingcurriedand

uncurriedrewriting.JournalofSymbolicComputation,21(1):15–39,1996.

23.K.Kusakari,M.Nakamura,andY.Toyama.Argumentfilteringtransformation.

InProc.PPDP’99,LNCS1702,pages48–62,1999.

24.K.Kusakari.Onprovingterminationoftermrewritingsystemswithhigher-order

variables.IPSJTransactionsonProgramming,42(SIG7(PRO11)):35–45,2001.25.M.LifantsevandL.Bachmair.AnLPO-basedterminationorderingforhigher-ordertermswithoutλ-abstraction.InProc.TPHOLs’98,LNCS1479,1998.

26.A.Mycroft.Thetheoryandpracticeoftransformingcall-by-needintocall-by-value.InProc.4thInt.Symp.onProgramming,LNCS83,pages269–281,1980.27.A.OliartandW.Snyder.Afastalgorithmforuniformsemi-unification.InProc.

CADE’98,LNCS1421,pages239–253,1998.

28.D.A.Plaisted.Asimplenon-terminationtestfortheKnuth-Bendixmethod.In

Proc.CADE’86,LNCS230,pages79–88,1986.

29.J.vandePol.Terminationofhigher-orderrewritesystems.PhD,Utrecht,1996.30.M.Sakai,Y.Watanabe,andT.Sakabe.Anextensionofdependencypairmethod

forprovingterminationofhigher-orderrewritesystems.IEICETransactionsonInformationandSystems,E84-D(8):1025–1032,2001.

31.M.SakaiandK.Kusakari.Ondependencypairmethodforprovingtermination

ofhigher-orderrewritesystems.IEICETrans.onInf.&Sys.,2005.Toappear.32.R.Thiemann,J.Giesl,andP.Schneider-Kamp.Improvedmodulartermination

proofsusingdependencypairs.InProc.IJCAR’04,LNAI3097,pages75–90,2004.33.Y.Toyama.TerminationofS-expressionrewritingsystems:Lexicographicpath

orderingforhigher-orderterms.InProc.RTA’04,LNCS3091,pages40–54,2004.34.TPDBwebpage.http://www.lri.fr/~marche/termination-competition/.

35.P.WadlerandJ.Hughes.Projectionsforstrictnessanalysis.InProc.3rdInt.

Conf.FunctionalProg.Lang.&Comp.Arch.,LNCS274,pages385–407,1987.36.J.Waldmann.Matchbox:Atoolformatch-boundedstringrewriting.InProc.15th

RTA,LNCS3091,pages85–94,2004.

37.H.Zantema.TORPA:Terminationofstringrewritingprovedautomatically.Jour-nalofAutomatedReasoning,2005.Toappear.

16