ABSTRACTIONS IN LOGIC PROGRAMS

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 ?

Sujets

• Free variables and bound variables
• Computer programming

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 27
• Langue: English

Extrait

ABSTRACTIONSINLOGICPROGRAMS DaleMiller DepartmentofComputerandInformationScience UniversityofPennsylvania Philadelphia,PA19104–6389USA February1993 1.Introduction Mostlogicprogramminglanguageshavethefirst-order,classicaltheory ofHornclausesastheirlogicalfoundation.Purelyproof-theoreticalconsid- erationsshowthatHornclausesarenotrichenoughtonaturallyprovidethe abstractionmechanismsthatarecommoninmostmodern,generalpurpose programminglanguages.Forexample,Hornclausesdonotincorporatethe importantsoftwareabstractionmechanismsofmodules,datatypeabstrac- tions,andhigher-orderprogramming. Asaresultofthislack,implementersoflogicprogramminglanguages basedonHornclausesgenerallyaddseveralnonlogicalprimitivesontopof Hornclausestoprovidethesemissingabstractionmechanisms.Although themissingfeaturesareoftencapturedinthisfashion,formalsemanticsof theresultinglanguagesareoftenlackingorareverycomplex.Anotherap- proachtoprovidingthesemissingfeaturesistoenrichtheunderlyinglogical foundationoflogicprogramming.Thislatterapproachtoprovidinglogic programswiththesemissingabstractionmechanismsistakeninthispaper. Theenrichmentswewillconsiderhavesimpleanddirectoperationaland prooftheoreticalsemantics. InSection2,wepresentafirst-ordersortedlogicanddefinesequen- tialproofsystems.Theseproofsystemsareusedtodefineprovabilityin classicalandintuitionisticlogics.InSection3,wepresentfirst-orderHorn clausesanddescribecertainaspectsoftheirprooftheory.InSection4,Horn clausesareextendedbypermittingimplicationsintothebodiesofprogram clauses.Theintuitionisticinterpretationofclausesofthisextensioncanpro- videafoundationfordevelopingmodularprogrammingfacilitiesforlogic programs.InSections5and6,universalquantifiers,aswellasimplications, areaddedtothebodiesofprogramclauses.Theadditionofthisnewformof quantificationpermitsconstantstobegivenlocalscopeintheevaluationof logicprograms.Suchscopingofconstantscanbeexploitedtoprovideforms ToappearinthevolumeLogicandComputerScienceeditedbyP.Odifreddi andpublishedbyAcademicPress. 1

2.AFirst-OrderLogic ofdataabstractions.ThisenrichmentofHornclauses,containingimplica- tionsanduniversalquantifiersinthebodyofprogramclauses,isknownas hereditaryHarropformulas. Ahigher-orderlogicispresentedinSection7andhigher-ordergener- alizationstoHornclausesandhereditaryHarropformulasarepresentedin Section8.Severalexamplesofhigher-orderlogicprogramsareprovidedin Section9.WeconcludeinSection10. Thispaperisessentiallyanoverviewandsummaryoftheworkthe authorandhiscolleagueshavebeenengagedinoverthepastfouryears.All themainresultsandtheoremsreportedinthispaperhaveappearedinthe papers[20,21,22,25,26,27,28]. 2.AFirst-OrderLogic LetSbeafixed,finitesetofprimitivetypes(alsocalledsorts).We assumethatthesymboloisalwaysamemberofS.FollowingChurch[4], oisthetypeforpropositions.Thesetoftypesisthesmallestsetofexpres- sionsthatcontainstheprimitivetypesandisclosedundertheconstruction offunctiontypes,denotedbythebinary,infixsymbol→.TheGreeklet- tersτandσareusedassyntacticvariablesrangingovertypes.Thetype constructor→associatestotheright:readτ 1 →τ 2 →τ 3 asτ 1 →(τ 2 →τ 3 ). Letτbethetypeτ 1 →∙∙∙→τ n →τ 0 whereτ 0 ∈Sandn≥0.(By convention,ifn=0thenτissimplythetypeτ 0 .)Thetypesτ 1 ,...,τ n are theargumenttypesofτwhilethetypeτ 0 isthetargettypeofτ.Theorder ofatypeτisdefinedasfollows:Ifτ∈Sthenτhasorder0;otherwise,the orderofτisonegreaterthanthemaximumorderoftheargumenttypesofτ. Thus,τhasorder1exactlywhenτisoftheformτ 1 →∙∙∙→τ n →τ 0 where n≥1and{τ 0 ,τ 1 ,...,τ n }⊆S.Wesay,however,thatτisafirst-ordertype iftheorderofτiseither0or1andthatnoargumenttypeofτiso.The targettypeofafirst-ordertypemaybeo. Foreachtypeτ,weassumethattherearedenumerablymanyconstants andvariablesofthattype.Constantsandvariablesdonotoverlapandif twoconstants(orvariables)havedifferenttypes,theyaredifferentconstants (orvariables).Asignature(overS)isafinitesetΣofconstants.Weoften enumeratesignaturesbylistingtheirmembersaspairs,writtena:τ,wherea isaconstantoftypeτ.Althoughattachingatypeinthiswayisredundant,it makesreadingsignatureseasier.Asignatureisfirst-orderifallitsconstants areoffirst-ordertype. Wecannowdefinethefirst-orderlogicF.ThelogicalconstantsofFare thesymbols∧(conjunction),∨(disjunction),⊃(implication),>(truth),⊥ (absurdity),andforeveryτ∈S−{o},∀ τ (universalquantificationovertype 2

2.AFirst-OrderLogic τ),and∃ τ (existentialquantificationovertypeτ).Thus,Fhasonlyafinite numberoflogicalconstants.Negationwillnotbeofmuchinterestinthis paper,butwhenneeded,thenegationofaformulaBiswrittenasB⊃⊥. Letτbeatypeoftheformτ 1 →∙∙∙→τ n →τ 0 whereτ 0 isaprimitive typeandn≥0.Ifτ 0 iso,aconstantoftypeτisapredicateconstant ofarityn.Ifτ 0 isnoto,thenaconstantoftypeτiseitheranindividual constantifn=0orafunctionconstantofaritynifn≥1.Similarly,wecan definepredicatevariableofarityn,individualvariable,andfunctionvariable ofarityn. Boldfacelettersareusedforsyntacticvariablesasfollows:a,b,crange overindividualconstants;x,y,zrangeoverindividualvariables;f,g,hrange overfunctionconstants;andp,qrangeoverpredicateconstants.Itisnot untilSection6thatweareinterestedinfunctionandpredicatevariables. Letτbeaprimitivetypedifferentfromo.Afirst-ordertermoftypeτ iseitheraconstantorvariableoftypeτ,oroftheform(ft 1 ...t n )where fisafunctionconstantoftypeτ 1 →∙∙∙→τ n →τand,fori=1,...,n,t i isatermoftypeτ i .Inthelattercase,fistheheadandt 1 ,...,t n arethe argumentsofthisterm. Afirst-orderformulaiseitheratomicornon-atomics.Anatomicformula isoftheform(pt 1 ...t n ),wheren≥0,pisapredicateconstantofthefirst- ordertypeτ 1 →∙∙∙→τ n →o,andt 1 ,...,t n arefirst-ordertermsofthe typesτ 1 ,...,τ n ,respectively.Thepredicateconstantpistheheadofthis atomicformula.Non-atomicformulasareoftheform>,⊥,B 1 ∧B 2 ,B 1 ∨B 2 , B 1 ⊃B 2 ,∀ τ xB,or∃ τ xB,whereB,B 1 ,andB 2 areformulasandτisa primitivetypedifferentfromo.Theusualnotionsoffreeandboundvariables andofopenandclosedtermsandformulasareassumed. Theboldfaceletterst,srangeoverterms;theromanlettersB,Crange overformulas;Arangesoveratomicformulas;andtheGreeklettersΓ,Δ rangeoversetsofformulas. Letsbeafirst-ordertermoftypeτandletxbeavariableoftype τ.Theoperationofsubstitutingsforfreeoccurrencesofxiswrittenas [x7→s].Boundvariablesareassumedtobechangedinasystematicfashion inordertoavoidvariablecapture.Simultaneoussubstitutioniswrittenas theoperator[x 1 7→s 1 ,...,x n 7→s n ]. LetΣbeafirst-ordersignature.AΣ-termisaclosedtermallofwhose constantsaremembersofΣ.Likewise,aΣ-formulaisaclosedformulaallof whosenonlogicalconstantsaremembersofΣ. ProvabilityforFisgivenintermsofsequentcalculusproofs[9].A sequentofFisatripleΣ;Γ−→Δ,whereΣisafirst-ordersignatureover SandΓandΔarefinite(possiblyempty)setsofΣ-formulas.ThesetΓ isthissequent’santecedentandΔisitssuccedent.TheexpressionsΓ,B 3