Higher-order logic programming

CS-1994-38Higher-OrderLogicProgrammingGopalanNadathurDaleMillerDepartmentofComputerScienceDukeUniversityDurham,NorthCarolina27708{0129December1994Higher-OrderLogicProgrammingyGopalanNadathurzComputerScienceDepartment,DukeUniversityDurham,[e-mail]:[phone],Fax:[phone]DaleMillerComputerScienceDepartment,UniversityofPennsylvaniaPhiladelphia,[e-mail]:[phone],Fax:[phone]yThispaperistoappearintheHandbookofLogicinArticialIntelligenceandLogicProgramming,D.Gabbay,C.HoggerandA.Robinson(eds.),OxfordUniversityPress.zThisaddressisfunctionalonlyuntilJanuary1,1995.Afterthisdate,pleaseusethefollowingaddress:DepartmentofComputerScience,UniversityofChicago,RyersonLaboratory,1100E.58thStreet,Chicago,IL60637,Email:[e-mail]1Introduction32MotivatingaHigher-OrderExtensiontoHornClauses53AHigher-OrderLogic123.1TheLanguage::::::::::::::::::::::::::::::::::::::::123.2EqualitybetweenTerms::::::::::::::::::::::::::::::::::143.3TheNotionofDerivation:::::::::::::::::::::::::::::::::173.4ANotionofModels::::::::::::::::::::::::::::::::::::193.5PredicateVariablesandtheSubformulaProperty::::::::::::::::::::214Higher-OrderHornClauses235TheMeaningofComputations275.1RestrictiontoPositiveTerms:::::::::::::::::::::::::::::::285.2ProvabilityandOperationalSemantics::::::::::::::::::::::::::326TowardsaPracticalRealization356.1TheHigher-OrderUnicationProblem::::::::::::::::::::::::::356.2P-Derivations::::::::::::::::::::::::::::::::::::::::386.3DesigninganActualInterpreter::::::::::::::::::::::::::::::427ExamplesofHigher-OrderProgramming457.1AConcreteSyntaxforPrograms:::::::::::::::::::::::::::::457.2SomeSimpleHigher-OrderPrograms:::::::::::::::::::::::::::487.3ImplementingTacticsandTacticals::::::::::::::::::::::::::::517.4ComparisonwithHigher-OrderFunctionalProgramming::::::::::::::::548Using-TermsasDataStructures568.1ImplementinganInterpreterforHornClauses:::::::::::::::::::::578.2DealingwithFunctionalProgramsasData:::::::::::::::::::::::608.3AShortcomingofHornClausesforMeta-Programming::::::::::::::::669HereditaryHarropFormulas689.1PermittingUniversalQuantiersandImplicationsinGoals::::::::::::::689.2RecursionoverStructuresthatIncorporateBinding:::::::::::::::::::7010Conclusion7811Acknowledgements7921IntroductionModernprogramminglanguagessuchasLisp,SchemeandMLpermitprocedurestobeencapsulatedwithindatainsuchawaythattheycansubsequentlyberetrievedandusedtoguidecomputations.Thelanguagesthatprovidethiskindofanabilityareusuallybasedonthefunctionalprogrammingparadigm,andtheproceduresthatcanbeencapsulatedinthemcorrespondtofunctions.Theobjectsthatareencapsulatedare,therefore,ofhigher-ordertypeandsoalsoarethefunctionsthatmanipulatethem.Forthisreason,theselanguagesaresaidtoallowforhigher-orderprogramming.Thisformofprogrammingispopularamongtheusersoftheselanguagesanditstheoryiswelldeveloped.Thesuccessofthisstyleofencapsulationinfunctionalprogrammingmakesisnaturaltoaskifsimilarideascanbesupportedwithinthelogicprogrammingsetting.Notingthatproceduresareimplementedbypredicatesinlogicprogramming,higher-orderprogramminginthissettingwouldcorrespondtomechanismsforencapsulatingpredicateexpressionswithintermsandforlaterretrievingandinvokingsuchstoredpredicates.Atleastsomedevicessupportingsuchanabilityhavebeenseentobeusefulinpractice.AttemptshavethereforebeenmadetointegratesuchfeaturesintoProlog(see,forexample,[War82]),andmanyexistingimplementationsofPrologprovideforsomeaspectsofhigher-orderprogramming.Theseattempts,however,areunsatisfactoryintworespects.First,theyhavereliedontheuseofadhocmechanismsthatareatvariancewiththedeclarativefoundationsoflogicprogramming.Second,theyhavelargelyimportedthenotionofhigher-orderprogrammingasitisunderstoodwithinfunctionalprogrammingandhavenotexaminedanotionthatisintrinsictologicprogramming.Inthischapter,wedeveloptheideaofhigher-orderlogicprogrammingbyutilizingahigher-orderlogicasthebasisforcomputing.Thereare,ofcourse,manychoicesforthehigher-orderlogicthatmightbeusedinsuchastudy.Ifthedesireisonlytoemulatethehigher-orderfeaturesfoundinfunctionalprogramminglanguages,itispossibletoadopta\minimalistapproach,i.e.,toconsiderextendingthelogicofrst-orderHornclauses|thelogicalbasisofProlog|inassmallawayaspossibletorealizetheadditionalfunctionality.Theapproachthatweadopthere,however,istoenunciateanotionofhigher-orderlogicprogrammingbydescribingananalogueofHornclauseswithinarichhigher-orderlogic,namely,Church’sSimpleTheoryofTypes[Chu40].Followingthiscoursehasanumberofpleasantoutcomes.First,theextensiontoHornclauselogicthatresultsfromitsupports,inanaturalfashion,theusualhigher-orderprogrammingcapabilitiesthatarepresentinfunctionalprogramminglanguages.Second,theparticularlogicthatisusedprovidestheelegantmechanismof-termsasameansforconstructingdescriptionsofpredicatesandthisturnsouttohavebenetsataprogramminglevel.Third,theuseofahigher-orderlogicblursthedistinctionbetweenpredicatesandfunctions|predicatescorrespond,afterall,totheirch