Logic programming, functional programming, and ind

LogicProgramming,FunctionalProgramming,andInductiveDe¯nitionsLawrenceC.Paulson1andAndrewW.Smith21ComputerLaboratory,UniversityofCambridge,CambridgeCB23QG,England2HarlequinLimited,Barrington,CambridgeCB25RG,England2LawrenceC.PaulsonandAndrewW.SmithTableofContents1Introduction:::::::::::::::::::::::::::::::32Declarativeprogrammers:realistsversuspurists::::::::32.1Functionalprogramming::::::::::::::::::::::42.2Logicprogramming:::::::::::::::::::::::::43Logicprograms:¯rst-ordertheoriesorinductivede¯nitions?53.1Logicprogramsas¯rst-ordertheories:::::::::::::::63.2Logicprogramsasinductivede¯nitions::::::::::::::73.3LeastmodelsandtheClosedWorldAssumption:::::::::83.4Speci¯cationandveri¯cationoflogicprograms::::::::::94Extendedlogicprogramminglanguages::::::::::::::114.1Largerfragmentsof¯rst-orderlogic::::::::::::::::114.2Otherworkconcerninginductivede¯nitions::::::::::::124.3ThelanguageLoglisp:::::::::::::::::::::::134.4Alogiclanguagewithfunctions:::::::::::::::::::135APrototypeofthelanguage:::::::::::::::::::::165.1RewriteRules::::::::::::::::::::::::::::165.2TypeDeclarations::::::::::::::::::::::::::185.3Theequalityfunction`eq'::::::::::::::::::::::195.4Otherfeatures::::::::::::::::::::::::::::196Operationoftheprototype::::::::::::::::::::::206.1Uni¯cation::::::::::::::::::::::::::::::206.2Example:AnEightQueensProgram::::::::::::::::226.3Example:APropositionalcalculustheoremprover::::::::237Conclusions::::::::::::::::::::::::::::::::25LogicProgrammingandInductiveDe¯nitions31IntroductionTheuni¯cationoflogicandfunctionalprogramming,liketheHolyGrail,issoughtbycountlesspeople[6,14].Inreportingourattempt,we¯rstdiscussthemotivation.Wearguethatlogicprogrammingisstillimmature,comparedwithfunctionalprogramming,becausefewlogicprogramsarebothusefulandpure.Functionscanhelptopurifylogicprogramming,fortheycaneliminatecertainusesofthecutandcanexpresscertainnegationspositively.Moregenerally,wesuggestthatthetraditionalparadigm|logicprogram-mingas¯rst-orderlogic|isseriouslyoutofstepwithpractice.Weo®eranalternativeparadigm.Weviewthelogicprogramasaninductivede¯nitionofsetsandrelations.ThisviewexplainscertainusesofNegationasFailure,andexplainswhymostattemptstoextendPrologtolargerfragmentsof¯rst-orderlogichavenotbeensuccessful.Itsuggestsalogiclanguagewithfunctions,in-corporatingequationaluni¯cation.Wehaveimplementedaprototypeofthislanguage.Itisveryslow,butcom-plete,andappeartobefasterthansomeearlierimplementationsofnarrowing.Ourexperimentsillustratetheprogrammingstyleandshedlightonthefurtherdevelopmentofsuchlanguages.2Declarativeprogrammers:realistsversuspuristsLogicProgrammingandFunctionalProgrammingareoftenlumpedtogetherundertheheading`DeclarativeProgramming'.Ideally,adeclarativeprogramsimplyspeci¯estheproblem|whatwewant|andthecomputerworksouthowtodoit.Ofcoursethisisanoversimpli¯cation.Forthedeclarativelanguagesthatexistnow,theproblemdescriptionreallyisaprogram:notforanyphysicalmachine,butforanabstractmachine.Afunctionalprogramde¯nesasystemofrewritingrulesthatcanevaluateadesiredfunction.Alogicprogramde¯nesasearchspaceofproblemreductionsthatcansolveallinstancesofthedesiredgoal.Thedeclarativeprogramexpressesthealgorithmmoreabstractlythan,say,aPascalprogram,butthemeansofexpressionarerestrictivewhenregardedasaspeci¯cationlanguage:evenmoresoifwecareaboute±ciency.Usersofdeclarativelanguagescanbedescribedasrealistsorpurists:{Realistssetouttowriteusefulprograms.Whiletheyvaluethedeclarativereading,theyarepreparedtocompromiseitifnecessary.{Puristssetouttodemonstratetheirdeclarativeparadigm,andperhapsitsapplicationtoprogramcorrectnessandsynthesis.Theirprogramsarecom-pletelypure,regardlessoftheconsequencesfore±ciency.4LawrenceC.PaulsonandAndrewW.SmithRealistsandpuristsareequallyworthy;theysimplyhavedi®erentpriorities.Notethatanimpureprogramcanbemorereadablethanapureone,whileapureprogramcanbemoree±cientthananimpureone.Letuscomparefunctionalprogrammingandlogicprogrammingthroughtheseconcepts.ForthepuristviewwecancomparethepresentationsbyDavidTurnerandRobertKowalskiataspecialmeetingoftheRoyalSocietyinLondon.2.1FunctionalprogrammingApuristfunctionalprogrammermightuseMiranda,LazyML,orHaskell:lazyfunctionallanguageswithnoside-e®ectswhatever.DavidTurner'spresentationtotheRoyalSocietyincludesquicksort,atopologicalsort,andaprogramto¯ndaKnight'stourofthechessboard[42].Healsogivessomesimpleproofsandprogramderivations.BirdandWadler[7]giveafulleraccountofthepuristapproach;theyderivefunctionalprogramsfromformalspeci¯cations.PuristsavoidLispbecauseofitsimperativefeatures.DavidTurnersays[42,page53]:Itneedstobesaidvery¯rmlythatLisp,atleastasrepresentedbythedialectsincommonuse,isnotafunctionallanguageatall.Lisphasbeenimpurefromtheverystart.Assignmentsandgoto'sfeaturepromi-nentlyintheLisp1.5Programmer'sManual[32].Butthatsamebookdevotesachaptertoaprogramforthepropositionalcalculus(Wang'sAlgorithm).Thisisasubstantial,purelyfunctionalprogram|probablythe¯rstever|anditiswritteninLisp.ArealistfunctionalprogrammermightuseLisporML.Theselanguagessup-portafunctionalstylebut