31 Pages
English

ABSTRACTIONS IN LOGIC PROGRAMS

Gain access to the library to view online
Learn more

Description

Niveau: Supérieur, Doctorat, Bac+8
ABSTRACTIONS IN LOGIC PROGRAMS Dale Miller Department of Computer and Information Science University of Pennsylvania Philadelphia, PA 19104–6389 USA February 1993 1. Introduction Most logic programming languages have the first-order, classical theory of Horn clauses as their logical foundation. Purely proof-theoretical consid- erations show that Horn clauses are not rich enough to naturally provide the abstraction mechanisms that are common in most modern, general purpose programming languages. For example, Horn clauses do not incorporate the important software abstraction mechanisms of modules, data type abstrac- tions, and higher-order programming. As a result of this lack, implementers of logic programming languages based on Horn clauses generally add several nonlogical primitives on top of Horn clauses to provide these missing abstraction mechanisms. Although the missing features are often captured in this fashion, formal semantics of the resulting languages are often lacking or are very complex. Another ap- proach to providing these missing features is to enrich the underlying logical foundation of logic programming. This latter approach to providing logic programs with these missing abstraction mechanisms is taken in this paper. The enrichments we will consider have simple and direct operational and proof theoretical semantics. In Section 2, we present a first-order sorted logic and define sequen- tial proof systems. These proof systems are used to define provability in classical and intuitionistic logics. In Section 3, we present first-order Horn clauses and describe certain aspects of their proof theory.

  • maximum order

  • any proof

  • let ?

  • bound variable

  • variables ranging

  • programming

  • order

  • when ? inhabits

  • implies ?


Subjects

Informations

Published by
Reads 27
Language English
ABSTRACTIONSINLOGICPROGRAMSDaleMillerDepartmentofComputerandInformationScienceUniversityofPennsylvaniaPhiladelphia,PA19104–6389USAFebruary19931.IntroductionMostlogicprogramminglanguageshavethefirst-order,classicaltheoryofHornclausesastheirlogicalfoundation.Purelyproof-theoreticalconsid-erationsshowthatHornclausesarenotrichenoughtonaturallyprovidetheabstractionmechanismsthatarecommoninmostmodern,generalpurposeprogramminglanguages.Forexample,Hornclausesdonotincorporatetheimportantsoftwareabstractionmechanismsofmodules,datatypeabstrac-tions,andhigher-orderprogramming.Asaresultofthislack,implementersoflogicprogramminglanguagesbasedonHornclausesgenerallyaddseveralnonlogicalprimitivesontopofHornclausestoprovidethesemissingabstractionmechanisms.Althoughthemissingfeaturesareoftencapturedinthisfashion,formalsemanticsoftheresultinglanguagesareoftenlackingorareverycomplex.Anotherap-proachtoprovidingthesemissingfeaturesistoenrichtheunderlyinglogicalfoundationoflogicprogramming.Thislatterapproachtoprovidinglogicprogramswiththesemissingabstractionmechanismsistakeninthispaper.Theenrichmentswewillconsiderhavesimpleanddirectoperationalandprooftheoreticalsemantics.InSection2,wepresentafirst-ordersortedlogicanddefinesequen-tialproofsystems.Theseproofsystemsareusedtodefineprovabilityinclassicalandintuitionisticlogics.InSection3,wepresentfirst-orderHornclausesanddescribecertainaspectsoftheirprooftheory.InSection4,Hornclausesareextendedbypermittingimplicationsintothebodiesofprogramclauses.Theintuitionisticinterpretationofclausesofthisextensioncanpro-videafoundationfordevelopingmodularprogrammingfacilitiesforlogicprograms.InSections5and6,universalquantifiers,aswellasimplications,areaddedtothebodiesofprogramclauses.Theadditionofthisnewformofquantificationpermitsconstantstobegivenlocalscopeintheevaluationoflogicprograms.SuchscopingofconstantscanbeexploitedtoprovideformsToappearinthevolumeLogicandComputerScienceeditedbyP.OdifreddiandpublishedbyAcademicPress.1
2.AFirst-OrderLogicofdataabstractions.ThisenrichmentofHornclauses,containingimplica-tionsanduniversalquantifiersinthebodyofprogramclauses,isknownashereditaryHarropformulas.Ahigher-orderlogicispresentedinSection7andhigher-ordergener-alizationstoHornclausesandhereditaryHarropformulasarepresentedinSection8.Severalexamplesofhigher-orderlogicprogramsareprovidedinSection9.WeconcludeinSection10.Thispaperisessentiallyanoverviewandsummaryoftheworktheauthorandhiscolleagueshavebeenengagedinoverthepastfouryears.Allthemainresultsandtheoremsreportedinthispaperhaveappearedinthepapers[20,21,22,25,26,27,28].2.AFirst-OrderLogicLetSbeafixed,finitesetofprimitivetypes(alsocalledsorts).WeassumethatthesymboloisalwaysamemberofS.FollowingChurch[4],oisthetypeforpropositions.Thesetoftypesisthesmallestsetofexpres-sionsthatcontainstheprimitivetypesandisclosedundertheconstructionoffunctiontypes,denotedbythebinary,infixsymbol.TheGreeklet-tersτandσareusedassyntacticvariablesrangingovertypes.Thetypeconstructorassociatestotheright:readτ1τ2τ3asτ1(τ2τ3).Letτbethetypeτ1→∙∙∙→τnτ0whereτ0Sandn0.(Byconvention,ifn=0thenτissimplythetypeτ0.)Thetypesτ1,...,τnaretheargumenttypesofτwhilethetypeτ0isthetargettypeofτ.Theorderofatypeτisdefinedasfollows:IfτSthenτhasorder0;otherwise,theorderofτisonegreaterthanthemaximumorderoftheargumenttypesofτ.Thus,τhasorder1exactlywhenτisoftheformτ1→∙∙∙→τnτ0wheren1and{τ01,...,τn}⊆S.Wesay,however,thatτisafirst-ordertypeiftheorderofτiseither0or1andthatnoargumenttypeofτiso.Thetargettypeofafirst-ordertypemaybeo.Foreachtypeτ,weassumethattherearedenumerablymanyconstantsandvariablesofthattype.Constantsandvariablesdonotoverlapandiftwoconstants(orvariables)havedifferenttypes,theyaredifferentconstants(orvariables).Asignature(overS)isafinitesetΣofconstants.Weoftenenumeratesignaturesbylistingtheirmembersaspairs,writtena:τ,whereaisaconstantoftypeτ.Althoughattachingatypeinthiswayisredundant,itmakesreadingsignatureseasier.Asignatureisfirst-orderifallitsconstantsareoffirst-ordertype.Wecannowdefinethefirst-orderlogicF.ThelogicalconstantsofFarethesymbols(conjunction),(disjunction),(implication),>(truth),(absurdity),andforeveryτS−{o},τ(universalquantificationovertype2
2.AFirst-OrderLogicτ),andτ(existentialquantificationovertypeτ).Thus,Fhasonlyafinitenumberoflogicalconstants.Negationwillnotbeofmuchinterestinthispaper,butwhenneeded,thenegationofaformulaBiswrittenasB⊃⊥.Letτbeatypeoftheformτ1→∙∙∙→τnτ0whereτ0isaprimitivetypeandn0.Ifτ0iso,aconstantoftypeτisapredicateconstantofarityn.Ifτ0isnoto,thenaconstantoftypeτiseitheranindividualconstantifn=0orafunctionconstantofaritynifn1.Similarly,wecandefinepredicatevariableofarityn,individualvariable,andfunctionvariableofarityn.Boldfacelettersareusedforsyntacticvariablesasfollows:a,b,crangeoverindividualconstants;x,y,zrangeoverindividualvariables;f,g,hrangeoverfunctionconstants;andp,qrangeoverpredicateconstants.ItisnotuntilSection6thatweareinterestedinfunctionandpredicatevariables.Letτbeaprimitivetypedifferentfromo.Afirst-ordertermoftypeτiseitheraconstantorvariableoftypeτ,oroftheform(ft1...tn)wherefisafunctionconstantoftypeτ1→∙∙∙→τnτand,fori=1,...,n,tiisatermoftypeτi.Inthelattercase,fistheheadandt1,...,tnaretheargumentsofthisterm.Afirst-orderformulaiseitheratomicornon-atomics.Anatomicformulaisoftheform(pt1...tn),wheren0,pisapredicateconstantofthefirst-ordertypeτ1→∙∙∙→τno,andt1,...,tnarefirst-ordertermsofthetypesτ1,...,τn,respectively.Thepredicateconstantpistheheadofthisatomicformula.Non-atomicformulasareoftheform>,,B1B2,B1B2,B1B2,τxB,orτxB,whereB,B1,andB2areformulasandτisaprimitivetypedifferentfromo.Theusualnotionsoffreeandboundvariablesandofopenandclosedtermsandformulasareassumed.Theboldfaceletterst,srangeoverterms;theromanlettersB,Crangeoverformulas;Arangesoveratomicformulas;andtheGreeklettersΓ,Δrangeoversetsofformulas.Letsbeafirst-ordertermoftypeτandletxbeavariableoftypeτ.Theoperationofsubstitutingsforfreeoccurrencesofxiswrittenas[x7→s].Boundvariablesareassumedtobechangedinasystematicfashioninordertoavoidvariablecapture.Simultaneoussubstitutioniswrittenastheoperator[x17→s1,...,xn7→sn].LetΣbeafirst-ordersignature.AΣ-termisaclosedtermallofwhoseconstantsaremembersofΣ.Likewise,aΣ-formulaisaclosedformulaallofwhosenonlogicalconstantsaremembersofΣ.ProvabilityforFisgivenintermsofsequentcalculusproofs[9].AsequentofFisatripleΣ;Γ−→Δ,whereΣisafirst-ordersignatureoverSandΓandΔarefinite(possiblyempty)setsofΣ-formulas.ThesetΓisthissequent’santecedentandΔisitssuccedent.TheexpressionsΓ,B3