An Overview of Linear Logic Programming

Description

Niveau: Supérieur, Doctorat, Bac+8
1 An Overview of Linear Logic Programming Dale Miller INRIA/Futurs & Laboratoire d'Informatique (LIX) Ecole polytechnique, Rue de Saclay 91128 PALAISEAU Cedex FRANCE Abstract Logic programming can be given a foundation in sequent calculus by viewing computation as the process of building a cut-free sequent proof bottom-up. The first accounts of logic programming as proof search were given in classical and intuitionistic logic. Given that linear logic allows richer sequents and richer dynamics in the rewriting of sequents during proof search, it was inevitable that linear logic would be used to design new and more expressive logic programming languages. We overview how linear logic has been used to design such new languages and describe briefly some applications and implementation issues for them. 1.1 Introduction It is now commonplace to recognize the important role of logic in the foundations of computer science. When a major new advance is made in our understanding of logic, we can thus expect to see that advance ripple into many areas of computer science. Such rippling has been observed during the years since the introduction of linear logic by Girard in 1987 [Gir87]. Since linear logic embraces computational themes directly in its design, it often allows direct and declarative approaches to compu- tational and resource sensitive specifications. Linear logic also provides new insights into the many computational systems based on classical and intuitionistic logics since it refines and extends these logics.

• rule forms


• linear logic


• conclusion sequent


• atomic right- hand


• programming languages


• has extended


• left-introduction rules


• logic programming


• sub- sequent proof


• horn clause

Sujets

• École polytechnique
• Linear logic
• Programming language
• Logic programming
• Horn clause

Informations

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

Extrait

1 AnOverviewofLinearLogicProgramming DaleMiller INRIA/F E ´ u c t o u l r e s p & olyt L e a c b h o n r i a q t u o e i , re R d u ’ e In d f e or S m a a cl ti a q y ue(LIX) 91128PALAISEAUCedexFRANCE Abstract Logicprogrammingcanbegivenafoundationinsequentcalculusby viewingcomputationastheprocessofbuildingacut-freesequentproof bottom-up.Thefirstaccountsoflogicprogrammingasproofsearch weregiveninclassicalandintuitionisticlogic.Giventhatlinearlogic allowsrichersequentsandricherdynamicsintherewritingofsequents duringproofsearch,itwasinevitablethatlinearlogicwouldbeused todesignnewandmoreexpressivelogicprogramminglanguages.We overviewhowlinearlogichasbeenusedtodesignsuchnewlanguages anddescribebrieflysomeapplicationsandimplementationissuesfor .meht 1.1Introduction Itisnowcommonplacetorecognizetheimportantroleoflogicinthe foundationsofcomputerscience.Whenamajornewadvanceismadein ourunderstandingoflogic,wecanthusexpecttoseethatadvanceripple intomanyareasofcomputerscience.Suchripplinghasbeenobserved duringtheyearssincetheintroductionoflinearlogicbyGirardin1987 [Gir87].Sincelinearlogicembracescomputationalthemesdirectlyin itsdesign,itoftenallowsdirectanddeclarativeapproachestocompu- tationalandresourcesensitivespecifications.Linearlogicalsoprovides newinsightsintothemanycomputationalsystemsbasedonclassical andintuitionisticlogicssinceitrefinesandextendstheselogics. Therearetwobroadapproachesbywhichlogic,viathetheoryof proofs,isusedtodescribecomputation[Mil93].Oneapproachisthe proofreductionparadigm,whichcanbeseenasafoundationforfunc- 1

2DaleMiller tionalprogramming.Here,programsareviewedasnaturaldeduction orsequentcalculusproofsandcomputationismodeledusingproofnor- malization.Sequentsareusedtotypeafunctionalprogram:aprogram fragmentisassociatedwiththesingle-conclusionsequentΔ−→Gifthe codehasthetypedeclaredinGwhenallitsfreevariableshavetypes declaredfortheminthesetoftypejudgmentsΔ.Abramsky[Abr93] hasextendedthisinterpretationofcomputationtomultiple-conclusion sequentsoflinearlogic,Δ−→Γ,whereΔandΓarebothmultisetsof typingjudgments.Inthatsetting,cut-eliminationcanbeseenasspeci- fyingconcurrentcomputations.Seealso[BS94,Laf89,Laf90]forrelated usesofconcurrencyinproofnormalizationinlinearlogic.Themore expressivetypesmadepossiblebylinearlogichavealsobeenusedto providestaticanalysisofrun-timegarbage,aliases,referencecounters, andsingle-threadedness[GH90,MOTW99,O’H91,Wad90]. Anotherapproachtousingprooftheorytospecifycomputationis theproofsearchparadigm,whichcanbeseenasafoundationforlogic programming.Inthispaper(whichisanupdateto[Mil95]),wefirst provideanoverviewoftheproofsearchparadigmandthenoutlinethe impactthatlinearlogichasmadetothedesignandexpressivityofnew logicprogramminglanguages. 1.2Goal-directedproofsearch Whenlogicprogrammingisconsideredabstractly,sequentsdirectlyen- codethestateofacomputationandthechangesthatoccurtosequents duringbottom-upsearchforcut-freeproofsencodethedynamicsofcom- putation.Inparticular,followingtheframeworkdescribedin[MNPS91], alogicprogramminglanguageconsistsoftwokindsofformulas:program clausesdescribethemeaningofnon-logicalconstantsandgoalsarethe possibleconsequencesconsideredfromcollectionsofprogramclauses.A single-conclusionsequentΔ−→Grepresentsthestateofanidealized logicprogramminginterpreterinwhichthecurrentlogicprogramisΔ (asetormultisetofformulas)andthegoalisG.Thesetwoclassesof formulasaredualsofeachotherinthesensethatanegativesubformula ofagoalisaprogramclauseandanegativesubformulaofaprogram clauseisagoalformula.

AnOverviewofLinearLogicProgramming3 1.2.1Uniformproofs Theconstantsthatappearinlogicalformulasareoftwokinds:logical constants(connectivesandquantifiers)andnon-logicalconstants(pred- icatesandfunctionsymbols).The“searchsemantics”oftheformeris fixedandindependentofcontext:forexample,thesearchfortheproof ofadisjunctionoruniversalquantifiershouldbethesamenomatter whatprogramiscontainedinthesequentforwhichaproofisrequired. Ontheotherhand,theinstructionsforprovingaformulawithanon- logicalconstanthead(thatis,anatomicformula)areprovidedbythe logicprograminthesequent. Thisseparationofconstantsintologicalandnon-logicalyieldstwo differentphasesinproofsearchforasequent.Onephaseisthatofgoal reduction,inwhichthesearchforaproofofanon-atomicformulauses theintroductionruleforitstop-levellogicalconstant.Theotherphase isbackchaining,inwhichthemeaningofanatomicformulaisextracted fromthelogicprogrampartofthesequent. Thetechnicalnotionofuniformproofsisusedtocapturethenotion ofgoal-directedsearch.Whensequentsaresingle-conclusion,auniform proofisacut-freeproofinwhicheverysequentwithanon-atomicright- handsideistheconclusionofaright-introductionrule[MNPS91].An interpreterattemptingtofindauniformproofofasequentwoulddirectly reflectthelogicalstructureoftheright-handside(thegoal)intothe proofbeingconstructed.Asweshallsee,left-introductionrulesareused onlywhenthegoalformulaisatomicandaspartofthebackchaining phase. Aspecificnotionofgoalformulaandprogramclausealongwitha proofsystemiscalledanabstractlogicprogramminglanguageifasequent hasaproofifandonlyifithasauniformproof.Asweshallillustrate below,first-orderandhigher-ordervariantsofHornclausespairedwith classicalprovability[NM90]andhereditaryHarropformulaspairedwith intuitionisticprovability[MNPS91]aretwoexamplesofabstractlogic programminglanguages. Whilebackchainingisnotpartofthedefinitionofuniformproofs,the structureofbackchainingisconsistentacrossseveralabstractlogicpro- gramminglanguages.Inparticular,whenprovinganatomicgoal,appli- cationsofleft-introductionrulescanbeusedinacoordinateddecompo- sitionofaprogramclausethatyieldsnotonlyamatchingatomicformula occurrencetotheatomicgoalbutalsopossiblynewgoalsformulasfor whichadditionalproofsmustbeattempted[NM90,MNPS91,HM91].