Least and greatest fixed points in linear logic Ex

LeastandgreatestxedpointsinlinearlogicExtendedVersionJune12,2007DavidBaeldeandDaleMillerINRIA&LIX/´EcolePolytechnique,Palaiseau,Francedavid.baeldeatens-lyon.orgdale.milleratinria.frAbstract.Therst-ordertheoryofMALL(multiplicative,additivelinearlogic)overonlyequalitiesisaninterestingbutweaklogicsinceitcannotcaptureun-bounded(innite)behavior.Insteadofaccountingforunboundedbehaviorviatheadditionoftheexponentials(!and?),weaddleastandgreatestxedpointoperators.Theresultinglogic,whichwecallMALL=,satisestwofundamentalprooftheoreticproperties.Inparticular,MALL=satisescut-elimination,whichimpliesconsistency,andhasacompletefocusedproofsystem.Thissecondresultaboutfocusedproofsprovidesastrongnormalformforcut-freeproofstructuresthatcanbeused,forexample,tohelpautomateproofsearch.WethenconsiderapplyingthesetworesultsaboutMALL=toderiveafocusedproofsystemforanintuitionisticlogicextendedwithinductionandco-induction.Thetraditionalapproachtoencodingintuitionisticlogicintolinearlogicreliesheavilyonus-ingtheexponentials,whichunfortunatelyweakenthefocusingdiscipline.Wegetabetterfocusedproofsystembyobservingthatcertainxedpointssatisfythestructuralrulesofweakeningandcontraction(withoutusingexponentials).TheresultingfocusedproofsystemforintuitionisticlogiciscloselyrelatedtotheoneimplementedinBedwyr,arecentmodelcheckerbasedonlogicprogramming.Wediscusshowourprooftheorymightbeusedtobuildacomputationalsystemthatcanpartiallyautomateinductionandco-induction.1IntroductionInordertojustifythedesignandimplementationarchitectureofacomputationallogicsystem,foundationalresultsconcerningthenormalformsofproofsareoftenused.Onestartswiththecut-eliminationtheoremsinceitusuallyguaranteesotherpropertiesofthelogic(e.g.,consistency)andthatthereisnoneedtoautomatethecreationoflemmasduringproofsearch.Inmanysituations,thecut-eliminationtheoremimpliesthatallformulasconsideredduringthesearchforaproofaresubformulasoftheoriginal,pro-posedtheorem.Thisdoesnothold,inparticular,whenhigher-order(relation)variablesareused,whichisthecaseinthispaperwheretherulesforinductionandco-inductionusesuchhigher-ordervariables.Asecondnormalformtheorem,usuallyrelatedtofo-cusedproofs[And92]isalsoimportanttoestablish.Such“focusing”theoremsprovidenormalformsthatorganizeinvertibleandnon-invertibleinferencerulesintocollections:suchstripingoftheinferencerulesinacut-freederivationcanbeusedtounderstandwhichchoicesinbuildingproofsmightneedtobereconsidered(viabacktracking)andwhichdonot.Asweshallsee,focusingyieldsusefulstructureincut-freeproofs,evenwhenthesubformulapropertydoesnothold.Variouscomputationalsystemshaveemployeddierentfocusingtheorems:muchofProlog'sdesignandimplementationscanbejustiedbythecompletenessofSLD-resolution[AvE82];uniformproofs(goal-directedproofs)inintuitionisticandintuition-isticlinearlogicshavebeenusedtojustifyProlog[MNPS91]andLolli[HM94];theclassicallinearlogicprogramminglanguagesLO[AP91]andForum[Mil96]haveuseddirectlyAndreoli'sgeneralfocusingresult[And92]forlinearlogic.Inthispaper,weestablishthesetwofoundationalproof-theoreticpropertiesforthefollowinglogic.Werstextendthemultiplicativeandadditivefragmentoflinearlogic(MALL)withequalityandquantication(via8and9)oversimplytyped-terms.Becauseoftheboundeduseofformulasduringproofconstruction,provabilityinthislogic,callitMALL=,canbereducedtodecidingunicationproblems(underamixedprex)whichisdecidablefortherst-orderfragmentofMALL=.Anelegantandwellknownwaytomakethislogicmoreexpressiveistoaddtheexponentials!and?andtherulesofinferencethatallowforcertainoccurrencesofformulasmarkedwiththesesystemstobecontractedandweakened[Gir87].Suchmodal-likeoperatorsarenot,however,withouttheirproblems.Inparticular,theexponentialsarenotcanonicalsincetherearedierentwaystoformulatetherulesforthepromotionandstructuralrulesforexponentialsandsomeofthesechoicesleadtodierentversionsoflogic(forexample,elementaryandlightlinearlogics[Gir98]andsoftlinearlogic[Laf04]).Evenifwextheinferencerulesfortheexponentials,asinstandardlinearlogic,therulesdonotdescribeuniqueexponentials.Ifonegivesaredtensorandabluetensorthesameinferencerules,thenonecanprovethatthesetwotensorsare,infact,equivalent.Alloflinearlogicconnectivesexcepttheexponentialsyieldsimilartheorems.Itiscertainlypossibletoconsidera(partiallyordered)collectionofexponentialsontopofMALL(see,forexample,[DJS93]).AnalternativetostrengthenMALLwithexponentialsistoextenditwithxedpoints.Earlyapproachestoaddingxedpoints[Gir92,SH93]involvedinferencerulesthatcouldonlyunfoldxedpointdescriptions:asaconsequence,suchlogicscouldnotdiscriminatebetweenaleastandgreatestxedpoint.Strongersystemsthatallowinduction[MM00]aswellasco-induction[Tiu04,MT03]includeinferencerulesusingahigher-ordervariablethatrangesoverprexedorpostxedpoints(invariants).Ofcourse,approachesthatuse(co)inductionarenotwithoutproblemsaswell:variousrestrictionsonxedpointexpressionsandoninvariantsmayneedtobeconsidered.Inanycase,weshallexplorethisalternativetoexponentials:inparticular,weextendthelogicMALL=toMALL=byaddingthetwoxedpoints