An Overview of Linear Logic Programming
33 pages
English

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

An Overview of Linear Logic Programming

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
33 pages
English
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

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

Informations

Publié par
Nombre de lectures 14
Langue English

Exrait

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].
  • Accueil Accueil
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • BD BD
  • Documents Documents