Termination proofs for logic programs with tabling

arXiv:cs/0003045v1[cs.LO]9Mar2000TerminationProofsforLogicProgramswithTabling⋆SofieVerbaeten⋆⋆1,DannyDeSchreye⋆⋆⋆1,andKonstantinosSagonas21DepartmentofComputerScienceK.U.Leuven,Celestijnenlaan200AB-3001Heverlee,Belgium{sofie,dannyd}@cs.kuleuven.ac.be2ComputingScienceDepartmentUppsalaUniversityBox311,S-75105Uppsala,[e-mail]receivingincreasingattentionintheLogicPro-grammingcommunity.ItavoidsmanyoftheshortcomingsofSLDexecutionandprovidesamoreflexibleandoftenextremelyefficientexecutionmechanismforlogicprograms.Inparticular,tabledexecutionoflogicprogramsterminatesmoreoftenthanexecutionbasedonSLD-resolution.Inthisarticle,weintroducetwonotionsofuniversaltermina-tionoflogicprogrammingwithTabling:quasi-terminationand(thestrongernotionof)LG-termination.Wepresentsufficientconditionsforthesetwonotionsoftermination,namelyquasi-acceptabilityandLG-acceptability,andweshowthattheseconditionsarealsonecessaryincasethetablingiswell-chosen.Startingfromtheseconditions,wegivemodularterminationproofs,i.e.,proofscapableofcombiningterminationproofsofsepa-rateprogramstoobtainterminationproofsofcombinedprograms.Finally,inthepresenceofmodeinformation,westatesufficientconditionswhichformthebasisforautomaticallyprovingterminationinaconstraint-basedway.1IntroductionTabledlogicprogramming[9,6,25,29]isreceivingincreasingattentionintheLogicProgrammingcommunity.ItavoidsmanyoftheshortcomingsofSLD(NF)executionandprovidesamoreflex-ibleandoftenextremelyefficientexecutionmechanismforlogicprograms.Furthermore,tabledexecutionoflogicprogramsterminatesmoreoftenthanexecutionbasedonSLD-resolution.Inparticular,allprogramsthatterminateunderSLDalsoterminateundertabledexecution.So,ifaprogramcanbeproventoterminateunderSLD-resolution(byoneoftheexistingautomatedtechniquessurveyedin[10]),thentheprogramwilltriviallyalsoterminateunderSLG-resolution,theresolutionprincipleoftabling;see[9].But,sincethereareSLG-terminatingprogramswhicharenotSLD-terminating,moreeffectiveprooftechniquesneedtoandcanbefound.Theideaunderlyingtablingisquitesimple.Essentially,underatabledexecutionmechanism,answersforselectedtabledatomsaswellastheseatomsarestoredinatable.Whenanidentical⋆Thisarticleisacollectionandintegrationofanumberofresultsthatappeared—sometimesinweakerforms—intheconferencepapers[27]and[28].⋆⋆ResearchAssistantoftheFundforScientificResearch—Flanders(Belgium)(F.W.O.).⋆⋆⋆SeniorResearchAssociateofF.W.O.Flanders.(uptorenamingofvariables)suchatomisrecursivelycalled,theselectedatomisnotresolvedagainstprogramclauses;instead,allcorrespondinganswerscomputedsofararelookedupinthetableandthecorrespondinganswersubstitutionsareappliedtotheatom.Thisprocessisrepeatedforallsubsequentcomputedanswersubstitutionsthatcorrespondtotheatom.WestudyuniversalterminationofdefinitetabledlogicprogramsexecutedunderSLG-resolutionusingafixedleft-to-rightselectionrule(wedropthe“S”inSLDandSLGwheneverwerefertotheleft-to-rightselectionrule).Weintroduceafirstbasicnotionofterminationundertabledexecution,calledquasi-termination.Quasi-terminationcapturesthepropertythat,underanLD-computation,agivenatomicqueryleadstoonlyfinitelymanydifferentnon-variantcallstotabledpredicatesandthereisnoinfinitederivationconsistingofquerieswithonlyselectednon-tabledatoms.Inabroadercontext,thenotionofquasi-terminationandtechniquesforprovingitareofindependentinterest;theycanbeusedtoe.g.ensureterminationofoff-linespecialisationoflogicprograms,whethertabledornot;see[8].However,thenotionofquasi-terminationonlypartiallycorrespondstoourintuitivenotionofa“terminatingcomputation”.Thisisbecauseanatomcanhaveinfinitelymanycomputedanswers(whichdoesnothavetoleadtoinfinitelymanynewcalls).Therefore,wealsointroducethestrongernotionofLG-termination.AprogramPLG-terminatesw.r.t.agivenatomicqueryiffPquasi-terminatesw.r.t.thequeryandthesetofallcomputedanswersforcallsintheLD-computationofthequeryisfinite.Wepresentsufficientconditionsforthesetwonotionsofterminationundertabledexecution:namely,quasi-acceptabilityforquasi-terminationandLG-acceptabilityforLG-termination.Weshowthattheseconditionsarealsonecessaryincasethesetoftabledpredicatesiswell-chosen;seeSection5.OurterminationconditionsareadaptedfromtheacceptabilitynotionforLD-terminationdefinedin[11],andnotfromthemore“standard”definitionofacceptabilitybyAptandPedreschiin[4].Thereasonforthischoiceisthatthequasi-terminationaswellastheLG-terminationpropertyofatabledprogramandqueryisnotclosedundersubstitution.Theacceptabilitynotionin[4]isexpressedintermsofgroundinstancesofclausesanditsassociatednotionofLD-terminationisexpressedintermsofthesetofallqueriesthatareboundedunderthegivenlevelmapping.Suchsetsareclosedundersubstitution.Becausequasi-terminationandLG-terminationlackinvarianceundersubstitution,weuseastrongernotionofacceptability,capableoftreatinganysetofqueries.Besidesacharacterisationofthetwonotionsofuniversalterminationundertabledexecution,wealsogivemodularterminationconditions,i.e.,conditionsontwoprogramsPandR,wherePextendsR,ensuringterminationoftheunionP∪R.Suchmodularproofswerealread