Tabled higher-order logic programming

Tabledhigher-orderlogicprogrammingBrigittePientkaCarnegieMellonUniversityAbstract.Elfisageneralmeta-languageforthespecicationandimplementa-tionoflogicalsystemsinthestyleofthelogicalframeworkLF.Basedonalogicprogramminginterpretation,itsupportsexecutinglogicalsystemsandreasoningwithandaboutthem,therebyreducingtheeortrequiredforeachparticularlogi-calsystem.Thetraditionallogicprogrammingparadigmisextendedbyreplacingrst-ordertermswithdependentlytyped-termsandallowingimplicationanduniversalquanticationinthebodiesofclauses.Thesehigher-orderfeaturesallowustomodelconciselyandelegantlyconditionsonvariablesandthedischargeofassumptionswhichareprevalentinmanylogicalsystems.However,manyspec-icationsarenotexecutableunderthetraditionallogicprogrammingsemanticsandperformancemaybehamperedbyredundantcomputation.Toaddresstheseproblems,Iproposeatabledhigher-orderlogicprogramminginterpretationforElf.Someredundantcomputationiseliminatedbymemoizingsub-computationandre-usingitsresultlater.Ifwedonotdistinguishdierentproofsforaproperty,thensearchbasedontabledlogicprogrammingiscompleteandterminatesforprogramswithboundedrecursion.Inthisproposal,Ipresentaproof-theoreticalcharacterizationfortabledhigher-orderlogicprogramming.ItisthebasisoftheimplementedprototypefortabledlogicprogramminginterpreterforElf.Preliminaryexperimentsindicatethatmanymorelogicalspecicationsareexecutableunderthetabledsemantics.Inaddition,tabledcomputationleadstomoreecientexecutionofprograms.Thegoalofthethesisistodemonstratethattabledlogicprogrammingallowsustoecientlyautomatereasoningwithandaboutlogicalsystemsinthelogicalframe-workLF..ToachievethisIintendtoshowsoundnessofthesearchbasedontabledlogicprogramming,developecientimplementationtechniques,anddemonstratethatthisallowsmanymorespecicationstobeexecutedandpropertiesproven.21IntroductionOneofthechallengesincomputersciencetodayistoprovidesomeformofguaranteeabouttherun-timebehaviorofprograms.Thisproblemisaddressedbyresearchon\cer-tiedcodewhereprogramsareequippedwithacerticate(proof)thatassertscertainsafetyproperties.Beforeexecutingtheprogram,thehostmachinecanthenquicklyver-ifythecode’ssafetypropertiesbycheckingthecerticateagainsttheprogram.Ithasbeenshownthatawiderangeofsafetypolicies,basedontypesystems[24]andrst-orderlogic[2,27],canbecheckedecientlyusingtheoremproverstailoredtothespecicsafetypolicy.Changingandextendingthesafetypolicyrequiresmodicationsofthetheoremprover.Moreover,everytimewewanttoexperimentwithanewsafetypolicy,weneedtowriteanewtheoremproverwhichisnotatrivialtask.ThelogicalframeworkLF[18]isageneralmeta-languageforthespecicationandimplementationoflogicalsystems.BasedonthelogicalframeworkLF,Pfenning[30]developedahigher-orderlogicprogramminglanguage,Elf.Thetraditionallogicpro-grammingparadigmisextendedbyreplacingrst-ordertermswithdependentlytyped-termsandallowingimplicationanduniversalquanticationinthebodiesofclauses.Thesehigher-orderfeaturesallowustomodelconciselyandelegantlyconditionsonvari-ablesandthedischargeofassumptionswhichareprevalentinmanylogicalsystems.Thisstandsinsharpcontrasttohigher-orderfeaturessupportedinmanytraditionallogicprogramminglanguages(seeforexample[7])wherewecanencapsulatepredicateexpressionswithintermstolaterretrieveandinvokesuchstoredpredicates.Theinferencerulesdescribingthesafetypolicyarerepresentedasahigher-orderlogicprogram.Toverifythatagivenprogramfulllsaspeciedsafetypolicy,thespecicationisexecutedbyalogicprogramminginterpreter.Theinterpreterdoesnotonlygenerateananswersubstitutionfortheexistentiallyquantiedvariables,butalsoacerticatefortheactualproof,aproofterm.Elfoersonegenericenvironmentforspecifyingsafetypoliciesandexecutingthem,therebyfactoringtheeortrequiredtobuiltaproverforaspecicsafetypolicy.Inadditiontocheckingwhetheragivenprogramfulllsaspecicsafetypolicy,itisequallyimportanttoverifypropertiesofthesafetypolicy,forexampleitssoundness.Thisisespeciallyimportantifwechangeandextendthepolicies.PfenningandSchurmann[35,44]demonstratedthatitisfeasibletoautomateinductivereasoningaboutlogicalspecicationsandcomplementedthehigher-logicprogramminginterpreterwiththemeta-theoremproverTwelf.Akeycomponentofthemeta-theoremproveristoderiveagoalbyapplyingprogramclauses,lemmas,assumptionsandinductionhypotheses.Boththelogicprogramminginterpreterandthemeta-theoremproverarebasedonthetraditionallogicprogrammingsemantics,althoughtheactualsearchstrategyemployeddiers.However,manyspecicationsarenotexecutableunderthetraditionallogicprogram-mingsemanticsandtheperformanceofimplementationsmaybehamperedbyredundantcomputation.Thesourceoftheseproblemsliesinthefactthatwehavethreedierentkindsofcomputationpaths:pathsthatleadtosuccess,pathsthatleadtoafailure,andinnitepathsthatdonotterminate.Innitepathsareclearlyundesirableastheypro-duceananswerandwastevaluablecomputingresourceswithoutmakinganyprogress.Inaddition,theperformanceoftraditionallogicprogrammingoftensuersfromredundantpathsofcomputation.Ifthesamesub-goaloccursmultipletimesinthesearchtree,thenDRAFTDecember6,