33 Pages
English

An Overview of Linear Logic Programming

Gain access to the library to view online
Learn more

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


Subjects

Informations

Published by
Reads 14
Language English
1AnOverviewofLinearLogicProgrammingDaleMillerINRIA/FE´uctoulresp&olytLeacbhonriaqtuoei,reRdueIndfeorSmaacltiaqyue(LIX)91128PALAISEAUCedexFRANCEAbstractLogicprogrammingcanbegivenafoundationinsequentcalculusbyviewingcomputationastheprocessofbuildingacut-freesequentproofbottom-up.Thefirstaccountsoflogicprogrammingasproofsearchweregiveninclassicalandintuitionisticlogic.Giventhatlinearlogicallowsrichersequentsandricherdynamicsintherewritingofsequentsduringproofsearch,itwasinevitablethatlinearlogicwouldbeusedtodesignnewandmoreexpressivelogicprogramminglanguages.Weoverviewhowlinearlogichasbeenusedtodesignsuchnewlanguagesanddescribebrieflysomeapplicationsandimplementationissuesfor.meht1.1IntroductionItisnowcommonplacetorecognizetheimportantroleoflogicinthefoundationsofcomputerscience.Whenamajornewadvanceismadeinourunderstandingoflogic,wecanthusexpecttoseethatadvancerippleintomanyareasofcomputerscience.SuchripplinghasbeenobservedduringtheyearssincetheintroductionoflinearlogicbyGirardin1987[Gir87].Sincelinearlogicembracescomputationalthemesdirectlyinitsdesign,itoftenallowsdirectanddeclarativeapproachestocompu-tationalandresourcesensitivespecifications.Linearlogicalsoprovidesnewinsightsintothemanycomputationalsystemsbasedonclassicalandintuitionisticlogicssinceitrefinesandextendstheselogics.Therearetwobroadapproachesbywhichlogic,viathetheoryofproofs,isusedtodescribecomputation[Mil93].Oneapproachistheproofreductionparadigm,whichcanbeseenasafoundationforfunc-1
2DaleMillertionalprogramming.Here,programsareviewedasnaturaldeductionorsequentcalculusproofsandcomputationismodeledusingproofnor-malization.Sequentsareusedtotypeafunctionalprogram:aprogramfragmentisassociatedwiththesingle-conclusionsequentΔ−→GifthecodehasthetypedeclaredinGwhenallitsfreevariableshavetypesdeclaredfortheminthesetoftypejudgmentsΔ.Abramsky[Abr93]hasextendedthisinterpretationofcomputationtomultiple-conclusionsequentsoflinearlogic,Δ−→Γ,whereΔandΓarebothmultisetsoftypingjudgments.Inthatsetting,cut-eliminationcanbeseenasspeci-fyingconcurrentcomputations.Seealso[BS94,Laf89,Laf90]forrelatedusesofconcurrencyinproofnormalizationinlinearlogic.Themoreexpressivetypesmadepossiblebylinearlogichavealsobeenusedtoprovidestaticanalysisofrun-timegarbage,aliases,referencecounters,andsingle-threadedness[GH90,MOTW99,O’H91,Wad90].Anotherapproachtousingprooftheorytospecifycomputationistheproofsearchparadigm,whichcanbeseenasafoundationforlogicprogramming.Inthispaper(whichisanupdateto[Mil95]),wefirstprovideanoverviewoftheproofsearchparadigmandthenoutlinetheimpactthatlinearlogichasmadetothedesignandexpressivityofnewlogicprogramminglanguages.1.2Goal-directedproofsearchWhenlogicprogrammingisconsideredabstractly,sequentsdirectlyen-codethestateofacomputationandthechangesthatoccurtosequentsduringbottom-upsearchforcut-freeproofsencodethedynamicsofcom-putation.Inparticular,followingtheframeworkdescribedin[MNPS91],alogicprogramminglanguageconsistsoftwokindsofformulas:programclausesdescribethemeaningofnon-logicalconstantsandgoalsarethepossibleconsequencesconsideredfromcollectionsofprogramclauses.Asingle-conclusionsequentΔ−→GrepresentsthestateofanidealizedlogicprogramminginterpreterinwhichthecurrentlogicprogramisΔ(asetormultisetofformulas)andthegoalisG.Thesetwoclassesofformulasaredualsofeachotherinthesensethatanegativesubformulaofagoalisaprogramclauseandanegativesubformulaofaprogramclauseisagoalformula.
AnOverviewofLinearLogicProgramming31.2.1UniformproofsTheconstantsthatappearinlogicalformulasareoftwokinds:logicalconstants(connectivesandquantifiers)andnon-logicalconstants(pred-icatesandfunctionsymbols).The“searchsemantics”oftheformerisfixedandindependentofcontext:forexample,thesearchfortheproofofadisjunctionoruniversalquantifiershouldbethesamenomatterwhatprogramiscontainedinthesequentforwhichaproofisrequired.Ontheotherhand,theinstructionsforprovingaformulawithanon-logicalconstanthead(thatis,anatomicformula)areprovidedbythelogicprograminthesequent.Thisseparationofconstantsintologicalandnon-logicalyieldstwodifferentphasesinproofsearchforasequent.Onephaseisthatofgoalreduction,inwhichthesearchforaproofofanon-atomicformulausestheintroductionruleforitstop-levellogicalconstant.Theotherphaseisbackchaining,inwhichthemeaningofanatomicformulaisextractedfromthelogicprogrampartofthesequent.Thetechnicalnotionofuniformproofsisusedtocapturethenotionofgoal-directedsearch.Whensequentsaresingle-conclusion,auniformproofisacut-freeproofinwhicheverysequentwithanon-atomicright-handsideistheconclusionofaright-introductionrule[MNPS91].Aninterpreterattemptingtofindauniformproofofasequentwoulddirectlyreflectthelogicalstructureoftheright-handside(thegoal)intotheproofbeingconstructed.Asweshallsee,left-introductionrulesareusedonlywhenthegoalformulaisatomicandaspartofthebackchainingphase.Aspecificnotionofgoalformulaandprogramclausealongwithaproofsystemiscalledanabstractlogicprogramminglanguageifasequenthasaproofifandonlyifithasauniformproof.Asweshallillustratebelow,first-orderandhigher-ordervariantsofHornclausespairedwithclassicalprovability[NM90]andhereditaryHarropformulaspairedwithintuitionisticprovability[MNPS91]aretwoexamplesofabstractlogicprogramminglanguages.Whilebackchainingisnotpartofthedefinitionofuniformproofs,thestructureofbackchainingisconsistentacrossseveralabstractlogicpro-gramminglanguages.Inparticular,whenprovinganatomicgoal,appli-cationsofleft-introductionrulescanbeusedinacoordinateddecompo-sitionofaprogramclausethatyieldsnotonlyamatchingatomicformulaoccurrencetotheatomicgoalbutalsopossiblynewgoalsformulasforwhichadditionalproofsmustbeattempted[NM90,MNPS91,HM91].