搜索
Higher-OrderRewriting:Framework,ConfluenceandTerminationJean-PierreJouannaud?LIX/CNRSUMR7161&´EcolePolytechnique,F-91400Palaiseaufirstsentenceofasurveyonfirst-orderrewritingborrowedagainandagaincharacterizesbestthefundamentalreasonwhyrewriting,asatech-nologyforprocessingequations,issoimportantinourdiscipline[10].Here,weconsiderhigher-orderrewriting,thatis,rewritinghigher-orderfunctionalexpressionsathigher-types.Higher-orderrewritingisause-fulgeneralizationoffirst-orderrewriting:byrewritinghigher-orderfunc-tionalexpressions,onecanprocessabstractsyntaxasdoneforexampleinprogramverificationwiththeproverIsabelle[27];byrewritingexpres-sionsathigher-types,onecanimplementcomplexrecursionschemasinproofassistantslikeCoq[12].Inourview,theroleofhigher-orderrewritingistodesignatype-theoreticframeworksinwhichcomputationanddeductionareintegratedbymeansofhigher-orderrewriterules,whilepreservingdecidabilityoftypingandcoherenceoftheunderlyinglogic.Thelatteritselfreducestotypepreservation,confluenceandstrongnormalization.Itisimportanttounderstandwhytherehavebeenverydifferentpro-posalsforhigher-orderrewriting,startingwithKlop’sCombinatoryre-ductionsystemsin1980,Nipkow’shigher-orderrewritingin1991andJouannaudandOkada’sexecutablehigher-orderalgebraicspecificationsin1991aswell:thesethreeapproachestacklethesameproblem,indif-ferentcontexts,withdifferentgoalsrequiringdifferentassumptions.JanWillemKlopwasmostlyinterestedingeneralizingthetheoryoflambdacalculus,andmorepreciselytheconfluenceandfinitedevelop-mentstheorems.Klopdoesnotassumeanytypestructure.Asaconse-quence,themostprimitiveoperationofrewriting,searchingforaredex,isalreadyaproblem.Becausehewantedtoencodepurelambdacalculus?ProjectLogiCal,PˆoleCommundeRechercheenInformatiqueduPlateaudeSaclay,CNRS,´EcolePolytechnique,INRIA,Universit´eParis-Sud.andothercalculiascombinatoryreductionsystems,hecouldnotsticktoapuresyntacticsearchbasedonfirst-orderpatternmatching.Hethere-forechosetosearchviafinitedevelopments,theonlywaytobaseafinitesearchonbeta-reductionintheabsenceoftypingassumptions.Andbe-causeofhisinterestinsimulatingpurelambdacalculi,hehadnorealneedfortermination,henceconcentratedonconfluenceresults.Therefore,histheoryinitsvariousincarnationsisstronglyinfluencedbythetheoryofresidualsinitiallydevelopedforthepurelambdacalculus.Nipkowwasmainlyinterestedininvestigatingthemeta-theoryofIsabelleandinprovingpropertiesoffunctionalprogramsbyrewriting,goalswhichareactuallyratherclosetothepreviousone.Functionalpro-gramsaretypedlambdaterms,henceheneededatypedstructure.Hechosesearchingviahigher-orderpatternmatching,becauseplainpat-ternmatchingistoopoorforexpressinginterestingtransformationsoverprogramswithfinitelymanyrules.Thischoiceofhigher-orderpatternmatchinginsteadoffinitedevelopmentsisofcourseverynaturalinatypedframework.Heassumesterminationforwhichproofmethodswerestilllackingatthattime.His(local)confluenceresultsrelyonthecompu-tationofhigher-ordercriticalpairs-becausehigher-orderpatternmatch-ingisusedforsearchingredexes-viahigher-orderunification.NipkowrestrictedlefthandsidesofrewriterulestobepatternsinthesenseofMiller[25].Themainreasonforthisrestrictionisthathigher-orderpat-ternmatchingandunificationaretractableinthiscasewhich,bychance,fitswellwithmostintendedapplications.JouannaudandOkadawereaimingatdeveloppingatheoryoftypedrewriterulesthatwouldgeneralizethenotionofrecursorinthecalculusofinductiveconstructions,itselfgeneralizingG¨odel’ssystemT.Thisex-plainstheiruseofplainpatternmatchingforsearchingaredex:thereisnoreasonforamoresophisticatedsearchwithrecursors.Inthiscontext,theneedforstronglyterminatingcalculihastwoorigins:ensuringconsistencyoftheunderlyinglogic,thatis,theabsenceofaproofforfalsityontheonehand,anddecidabilityofthetypesysteminthepresenceofdepen-denttypesontheotherhand.Confluenceisneededaswell,ofcourse,asistypepreservation.Thelatteriseasytoensurewhiletheformerisbasedonthecomputationoffirst-ordercriticalpairs-becausefirst-orderpat-ternmatchingisusedforsearchingredexes.Thisexplainstheemphasisonterminationcriteriainthisworkanditssubsequentdevelopments.OurgoalinthispaperistopresentaunifiedframeworkborrowedfromJouannaud,RubioandvanRaamsdonk[22]forthemostpart,inwhichredexescanbesearchedforbyusingeitherplainorhigher-order2rewriting,confluencecanbeprovedbycomputingplainorhigher-ordercriticalpairs,andterminationcanbeprovedbyusingthehigher-orderrecursivepathorderingofJouannaudandRubio[19].Wefirstpresentexamplesshowingtheneedforbothsearchmecha-nismsbasedonplainandhigher-orderpatternmatchingontheonehand,andforarichtypestructureontheotherhand.Theseexamplesshowtheneedforrulesofhighertype,thereforecontradictingacommonbeliefthatapplicationmakesrulesofhighertypeunnecessary.TheyalsorecallthatKlop’sideaofvariableswitharitiesisveryhandy.Then,wepresentourframeworkinmoredetail,beforeweaddressconfluenceissues,andfinallyterminationcriteria.Missingnotationsandterminologyusedinrewritingortypet