Call-by-value Termination in the Untyped lambda-ca

LogicalMethodsinComputerScienceVol.4(1:3)2008,pp.1–39λ-CALCULUSNEILD.JONESaANDNINABOHRbaDIKU,UniversityofCopenhagen,Denmarke-mailaddress:[e-mail]-UniversityofCopenhagen,Denmarke-mailaddress:[e-mail]-automatedalgorithmisdevelopedabletoshowthatevaluationofagivenuntypedλ-expressionwillterminateunderCBV(call-by-value).The“size-changeprinciple”fromfirst-orderprogramsisextendedtoarbitraryuntypedλ-expressionsintwosteps.ThefirststepsufficestoshowCBVterminationofasingle,stand-aloneλ-expression.ThesecondsufficestoshowCBVterminationofanymemberofaregularsetofλ-expressions,definedbyatreegrammar.(Asimpleexampleisaminimumfunction,whenappliedtoarbitraryChurchnumerals.)Thealgorithmissoundandprovensointhispaper.TheHaltingProblem’sundecidabilityimpliesthatanysoundalgorithmisnecessarilyincomplete:someλ-expressionsmayinfactterminateunderCBVevaluation,butnotberecognisedasterminating.Theintensionalpoweroftheterminationalgorithmisreasonablyhigh.Itcertifiesaster-minatingmanyinterestingandusefulgeneralrecursivealgorithmsincludingprogramswithmutualrecursionandparameterexchanges,andColson’s“minimum”algorithm.Further,ourtype-freeapproachallowsuseoftheYcombinator,andsocanidentifyasterminatingasubstantialsubsetofPCF.Contents1.Introduction3Contributionofthispaper31.1.Relatedwork3Terminationofuntypedprograms3Terminationoftypedλ-calculi32.Thecall-by-valueλ-calculus42.1.Classicalsemantics42.2.Nonterminationissequential4The“calls”relation5Asmallimprovementtotheoperationalsemantics51998ACMSubjectClassification:F.3.2,D.3.1.Keywordsandphrases:Programanalysis,Terminationanalysis,UntypedLambdacalculus,TheSize-ChangePrinciple.LOGICALMETHODSlINCOMPUTERSCIENCEDOI:10.2168/LMCS-4(1:3)2008cN.D.JonesandN.BohrCCCreativeCommons2N.D.JONESANDN.BOHR3.Anapproachtoterminationanalysis63.1.Anenvironment-basedsemantics73.2.Statesaretreestructures73.3.Nonterminationmadevisibleinanenvironment-basedsemantics83.4.Acontrolpointisasubexpressionofaλ-expression93.5.Finitelydescribingaprogram’scomputationspace93.6.Staticcontrolflowgraphsforλ-expressions104.Aquickreviewofsize-changeanalysis115.Tracingdatasizechangesincall-by-valueλ-calculusevaluation135.1.Sizechangesinacomputation:awell-foundedrelationbetweenstates136.Size-changegraphsthatsafelydescribeaprogram146.1.Safelydescribingstatetransitions146.2.Generatingsize-changegraphsduringacomputation156.3.Constructionofsize-changegraphsbyabstractinterpretation187.Someexamples197.1.Asimpleexample197.2.fnx=x+2nbyChurchnumerals197.3.Ackermann’sfunction,second-order207.4.Arbitrarynaturalnumbersasinputs217.5.Aminimumfunction,withgeneralrecursionandY-combinator217.6.Ackermann’sfunction,second-orderwithconstantsandY-combinator217.7.Imprecisionofabstractinterpretation227.8.Acounterexampletoaconjecture238.Arbitraryλ-regularprograminputs(Extendedλ-calculus)238.1.λ-regulargrammars238.2.Extendedenvironment-basedsemantics.258.3.Relatingextendedandpureλ-calculus278.4.Thesubexpressionproperty298.5.Approximateextendedsemanticswithsize-changegraphs298.6.Simulationpropertiesofapproximateextendedsemantics309.Concludingmatters32Acknowledgements.32AppendixA.ProofofLemma2.632AppendixB.ProofofLemma3.1132AppendixC.ProofofLemma5.433AppendixD.ProofofTheorem6.834AppendixE.ProofofLemma6.1035AppendixF.ProofofLemma8.1936References38CALL-BY-VALUETERMINATIONINTHEUNTYPEDλ-CALCULUS31.IntroductionThesize-changeanalysisbyLee,JonesandBen-Amram[14]canshowterminationofpro-gramswhoseparametervalueshaveawell-foundedsizeorder.Themethodisreasonablygeneral,easilyautomated,anddoesnotrequirehumaninventionoflexicalorotherpa-rameterorders.Itappliestofirst-orderfunctionalprograms.Thispaperappliessimilarideastoterminationofhigher-orderprograms.Forsimplicityandgeneralitywefocusonthesimplestsuchlanguage,theλ-calculus.Contributionofthispaper.Article[12](preparedforaninvitedconferencelecture)showedhowtoliftthemethodsof[14]toshowterminationofclosedλ-expressions.Thecurrentpaperisajournalversionof[12].Itextends[12]todealnotonlywithasin-gleλ-expressioninisolation,butwitharegularsetofλ-expressionsgeneratedbyafinitetreegrammar.Forexample,wecanshowthataλ-expressionterminateswhenappliedtoChurchnumerals,eventhoughitmayfailtoterminateonallpossiblearguments.Thispaperincludesanumberofexamplesshowingitsanalyticalpower,includingprogramswithprimitiverecursion,mutualrecursionandparameterexchanges,andColson’s“minimum”algorithm.Further,examplesshowthatourtype-freeapproachallowsfreeuseoftheYcombinator,andsocanidentifyasterminatingasubstantialsubsetofPCF.1.1.Relatedwork.Jones[11]wasanearlypaperoncontrol-flowanalysisoftheuntypedλ-calculus.Shivers’thesisandsubsequentwork[22,23]onCFA(controlflowanalysis)developedthisapproachconsiderablyfurtherandappliedittotheSchemeprogramminglanguage.Thislineiscloselyrelatedtotheapproximatesemantics(staticcontrolgraph)ofSection3.6[11].Terminationofuntypedprograms.Papersbasedon[14]haveusedsize-changegraphstofindboundsonprogramrunningtimes(FrederiksenandJones[5]);sol