Least and greatest xed points in linear logic Extended Version

David Baelde

Description

Niveau: Supérieur, Doctorat, Bac+8
Least and greatest xed points in linear logic Extended Version June 12, 2007 David Baelde and Dale Miller INRIA & LIX/Ecole Polytechnique, Palaiseau, France david.baelde at ens-lyon.org dale.miller at inria.fr Abstract. The first-order theory of MALL (multiplicative, additive linear logic) over only equalities is an interesting but weak logic since it cannot capture un- bounded (infinite) behavior. Instead of accounting for unbounded behavior via the addition of the exponentials (! and ?), we add least and greatest fixed point operators. The resulting logic, which we call µMALL=, satisfies two fundamental proof theoretic properties. In particular, µMALL= satisfies cut-elimination, which implies consistency, and has a complete focused proof system. This second result about focused proofs provides a strong normal form for cut-free proof structures that can be used, for example, to help automate proof search. We then consider applying these two results about µMALL= to derive a focused proof system for an intuitionistic logic extended with induction and co-induction. The traditional approach to encoding intuitionistic logic into linear logic relies heavily on us- ing the exponentials, which unfortunately weaken the focusing discipline. We get a better focused proof system by observing that certain fixed points satisfy the structural rules of weakening and contraction (without using exponentials).

• inference rules


• linear logic


• since negation normal


• cused proofs


• normal forms


• logic into linear


• xed point

Sujets

• Philippus Baldaeus
• École polytechnique
• Rule of inference
• Linear logic
• Database normalization

Informations

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

Extrait

Leastandgreatestfixedpointsinlinearlogic ExtendedVersion June12,2007 DavidBaeldeandDaleMiller INRIA&LIX / E ´ colePolytechnique,Palaiseau,France david.baeldeatens-lyon.orgdale.milleratinria.fr Abstract. Thefirst-ordertheoryofMALL(multiplicative,additivelinearlogic) overonlyequalitiesisaninterestingbutweaklogicsinceitcannotcaptureun- bounded(infinite)behavior.Insteadofaccountingforunboundedbehaviorvia theadditionoftheexponentials(!and?),weaddleastandgreatestfixedpoint operators.Theresultinglogic,whichwecall µ MALL = ,satisfiestwofundamental prooftheoreticproperties.Inparticular, µ MALL = satisfiescut-elimination,which impliesconsistency,andhasacompletefocusedproofsystem.Thissecondresult aboutfocusedproofsprovidesastrongnormalformforcut-freeproofstructures thatcanbeused,forexample,tohelpautomateproofsearch.Wethenconsider applyingthesetworesultsabout µ MALL = toderiveafocusedproofsystemfor anintuitionisticlogicextendedwithinductionandco-induction.Thetraditional approachtoencodingintuitionisticlogicintolinearlogicreliesheavilyonus- ingtheexponentials,whichunfortunatelyweakenthefocusingdiscipline.Weget abetterfocusedproofsystembyobservingthatcertainfixedpointssatisfythe structuralrulesofweakeningandcontraction(withoutusingexponentials).The resultingfocusedproofsystemforintuitionisticlogiciscloselyrelatedtotheone implementedinBedwyr,arecentmodelcheckerbasedonlogicprogramming. Wediscusshowourprooftheorymightbeusedtobuildacomputationalsystem thatcanpartiallyautomateinductionandco-induction. 1Introduction Inordertojustifythedesignandimplementationarchitectureofacomputationallogic system,foundationalresultsconcerningthenormalformsofproofsareoftenused.One startswiththe cut-eliminationtheorem sinceitusuallyguaranteesotherpropertiesofthe logic( e.g. ,consistency)andthatthereisnoneedtoautomatethecreationof lemmas duringproofsearch.Inmanysituations,thecut-eliminationtheoremimpliesthatall formulasconsideredduringthesearchforaproofaresubformulasoftheoriginal,pro- posedtheorem.Thisdoesnothold,inparticular,whenhigher-order(relation)variables areused,whichisthecaseinthispaperwheretherulesforinductionandco-induction usesuchhigher-ordervariables.Asecondnormalformtheorem,usuallyrelatedtofo- cusedproofs[And92]isalsoimportanttoestablish.Such“focusing”theoremsprovide normalformsthatorganizeinvertibleandnon-invertibleinferencerulesintocollections: suchstripingoftheinferencerulesinacut-freederivationcanbeusedtounderstand whichchoicesinbuildingproofsmightneedtobereconsidered(viabacktracking)and

whichdonot.Asweshallsee,focusingyieldsusefulstructureincut-freeproofs,even whenthesubformulapropertydoesnothold. Variouscomputationalsystemshaveemployeddi ff erentfocusingtheorems:much ofProlog’sdesignandimplementationscanbejustifiedbythecompletenessofSLD- resolution[AvE82];uniformproofs(goal-directedproofs)inintuitionisticandintuition- isticlinearlogicshavebeenusedtojustify λ Prolog[MNPS91]andLolli[HM94];the classicallinearlogicprogramminglanguagesLO[AP91]andForum[Mil96]haveused directlyAndreoli’sgeneralfocusingresult[And92]forlinearlogic. Inthispaper,weestablishthesetwofoundationalproof-theoreticpropertiesforthe followinglogic.Wefirstextendthemultiplicativeandadditivefragmentoflinearlogic (MALL)withequalityandquantification(via ∀ and ∃ )oversimplytyped λ -terms. Becauseoftheboundeduseofformulasduringproofconstruction,provabilityinthis logic,callit MALL = ,canbereducedtodecidingunificationproblems(underamixed prefix)whichisdecidableforthefirst-orderfragmentof MALL = .Anelegantandwell knownwaytomakethislogicmoreexpressiveistoaddtheexponentials!and?and therulesofinferencethatallowforcertainoccurrencesofformulasmarkedwiththese systemstobecontractedandweakened[Gir87].Suchmodal-likeoperatorsarenot, however,withouttheirproblems.Inparticular,theexponentialsarenotcanonicalsince therearedi ff erentwaystoformulatetherulesforthepromotionandstructuralrulesfor exponentialsandsomeofthesechoicesleadtodi ff erentversionsoflogic(forexample, elementaryandlightlinearlogics[Gir98]andsoftlinearlogic[Laf04]).Evenifwe fixtheinferencerulesfortheexponentials,asinstandardlinearlogic,therulesdo notdescribeuniqueexponentials.Ifonegivesaredtensorandabluetensorthesame inferencerules,thenonecanprovethatthesetwotensorsare,infact,equivalent.Allof linearlogicconnectivesexcepttheexponentialsyieldsimilartheorems.Itiscertainly possibletoconsidera(partiallyordered)collectionofexponentialsontopofMALL (see,forexample,[DJS93]). AnalternativetostrengthenMALLwithexponentialsistoextenditwithfixed points.Earlyapproachestoaddingfixedpoints[Gir92,SH93]involvedinferencerules thatcouldonlyunfoldfixedpointdescriptions:asaconsequence,suchlogicscould notdiscriminatebetweenaleastandgreatestfixedpoint.Strongersystemsthatallow induction[MM00]aswellasco-induction[Tiu04,MT03]includeinferencerulesusing ahigher-ordervariablethatrangesoverprefixedorpostfixedpoints(invariants).Of course,approachesthatuse(co)inductionarenotwithoutproblemsaswell:various restrictionsonfixedpointexpressionsandoninvariantsmayneedtobeconsidered.In anycase,weshallexplorethisalternativetoexponentials:inparticular,weextendthe logicMALL = to µ MALL = byaddingthetwofixedpoints µ and ν . Besidesconsideringfixedpo = intsasalternativestotheexponentials,thereareother reasonsforexamining µ MALL.First,leastandgreatestfixedpointsaredeMorgan dualsofoneanotherand,hence,theclassicalnatureoflinearlogicshouldo ff ersome economyandeleganceindevelopingtheirprooftheory,incontrasttointuitionistic logic.Second,sincelinearlogiccanbeseenasthelogicbehindintuitionisticlogic, itwillberathereasytodevelopafocusingproofsystemforintuitionisticlogicand fixedpointsbasedonthestructureoftheonewedevelopfor µ MALL = . 2