Introduction to linear logic and ludics, Part II

Introductiontolinearlogicandludics,PartIIPierre-LouisCurien(CNRS&Universit´eParisVII)∗July2,2004AbstractThispaperisthesecondpartofanintroductiontolinearlogicandludics,bothduetoGirard.Itisdevotedtoproofnets,inthelimited,yetcentral,frameworkofmultiplicativelinearlogic(section1)andtoludics,whichhasbeenrecentlydeveloppedinanaimoffurtherunveilingthefundamentalinteractivenatureofcomputationandlogic(sections2,3,4,and5).Wehopetoofferafewcomputerscienceinsightsintothisnewtheory.Keywords:Cut-elimination(03F05),Linearlogic(03F52),Logicincomputerscience(03B70),In-teractivemodesofcomputation(68Q10),Semantics(68Q55),Programminglanguages(68N15).PrerequisitesThispartdependsmostlyonthefirsttwosectionsofpartI,andshouldthereforebeaccessibletoanyonewhohasbeenexposedtotheveryfirststepsoflinearlogic.Wehaveusedthefollowingsources:[29,23,38]forproofnets,andand[35,36]forludics.1ProofnetsProofnetsaregraphsthatgiveamoreeconomicalpresentationofproofs,abstractingfromsomeirrelevantorderofapplicationoftherulesoflinearlogicgiveninsequentcalculusstyle(sections2and3ofpartI).Welimitourselvesheretomultiplicativelinearlogic(MLL),andweshallevenbeginwithcut-freeMLL.ProofnetsforMLLaregraphswhichare“almosttrees”,andwestressthisbyourchoiceofpresentation.Weinvitethereadertodrawproofnetsbyhimselfwhilereadingthesection.Whatplaysheretheroleofaproofofasequent`A1,...,AnistheforestoftheformulasA1,...,Anrepresentedastrees,togetherwithapartitionoftheleavesoftheforestinpairs(correspondingtotheapplicationofanaxiom`C,C⊥).Well,notquite.Aproofmaynotdecomposeeachformulacompletely,sinceanaxiom`C,C⊥canbeappliedtoanyformula.HencewehavetospecifypartialtreesfortheformulasA1,...,An.Onewaytodothisistospecifythesetofleavesofeachpartialtreeasasetof(pairwisedisjoint)occurrences.Formally,anoccurrenceisawordover{1,2},andthesubformulaA/uatoccurrenceuisdefinedbythefollowingformalsystem:A/=A(A1⊗A2)/1u=(A1OA2)/1u=A1/u(A1⊗A2)/2u=(A1OA2)/2u=A2/u.∗LaboratoirePreuves,ProgrammesetSyst`emes,Case7014,2placeJussieu,75251ParisCedex05,France,[e-mail].1ApartialformulatreeAUconsistsofaformulaAtogetherwithasetUofpairwisedisjointoccurrencessuchthat(∀u∈UA/uisdefined).RecallthatapartitionofasetEisasetXofnon-emptysubsetsofEwhicharepairwisedisjointandwhoseunionisE.IfX={Y1,...,Yn}weoftensimplywriteX=Y1,...,Yn.Definition1.1Aproofstructureisgivenby{AU11,...,AUnn}[X],where{AU11,...,AUnn}isamultisetofpartialformulatreesandwhereXisapartitionof{A1/u|u∈U1}∪...∪{An/u|u∈Un}(disjointunion)whoseclassesarepairsofdualformulas.Weshallsaythateachclassofthepartitionisanaxiomoftheproofstructure,andthatA1,...,Anaretheconclusionsoftheproofstructure.Moregenerally,weshallmanipulategraphsdescribedasaforestplusapartitionofitsleaves,with-outanyparticularrequirementonthepartition.ThisnotionisfaithfultoGirard’sideaofparaproof,discussedinthenextsection.Definition1.2Aparaproofstructureisgivenby{AU11,...,AUnn}[X],whereXisapartitionof{A1/u|u∈U1}∪...∪{An/u|u∈Un}(disjointunion).Weshallsaythateachclassofthepartitionisageneralizedaxiom,ordaimon(anticipatingonaterminologyintroducedinthefollowingsection),andthatA1,...,Anaretheconclusionsoftheparaproofstructure.Theactualgraphassociatedtothisdescriptionisobtainedby:•drawingthetreesoftheformulasA1,...,AnstoppingatU1,...,Un,respectively(i.e.,thereisanodecorrespondingtoeachsubformulaAi/u,whereuuiforsomeui∈Ui);and•associatinganewnodewitheachclassofthepartitionandnewedgesfromthenewnodetoeachoftheleavesoftheclass(inthecaseofproofstructures,onecandispensewiththenewnode,anddrawanedgebetweenthematchingdualformulas–suchedgesareusuallydrawnhorizontally).Wenextdescribehowtoassociateaproofstructurewithaproof.ThefollowingdefinitionfollowstherulesofMLL.Definition1.3Thesequentializableproofstructuresfor(cut-free)MLLaretheproofstructuresob-tainedbythefollowingrules:{C{},(C⊥){}}[{{C,C⊥}}]{AU11,...,AUnn,BV,CW}[X]{AU11,...,AUnn,(BOC)U}[X]{AU11,...,AUnn,BV}[X]{A0U011,...,A0U0n0n0,CW}[Y]{AU11,...,AUnn,A0U011,...,A0U0n0n0,(B⊗C)U}[X∪Y]whereU={1v|v∈V}∪{2w|w∈W}.Sequentializableproofstructuresarecalledproofnets.2ItshouldbeclearthatthereisabijectivecorrespondencebetweenMLLproofsandtheproofsofsequentialization.Letuscheckonedirection.Weshowthatifaproofstructurewithconclu-sionsA1,...,Anissequentializable,thenaproofthatitissoyieldsanMLLproofofthesequent`A1,...,An.Thisiseasilyseenbyinduction:theproofassociatedwith{C{},(C⊥){}}[{{C,C⊥}}]istheaxiom`C,C⊥,whilethelaststepsoftheproofsassociatedwith{AU11,...,AUnn,(BOC)U}[X]and{AU11,...,AUnn,A0U011,...,A0U0nn,(B⊗C)U}[X]are,respectively:`A1,...,An,B,C`A1,...,An,BOC`A1,...,An,B`A01,...A0n0,C`A1,...,An,A01,...,A0n0,B⊗CThequestionweshalladdressintherestofthesectionisthefollowing:givenaproofstructure,whenisitthecasethatitissequentializable?Itturnsoutthattherightlevelofgeneralityforthisquestionistoliftittoparaproofnets,whicharedefinednext.Definition1.4Thesequentializableparaproofstructuresfor(cut-free)MLLaretheparaproofstruc-turesobtainedbythefollowingrules:{A{}1,...,A{}n}[{{A1,...,An}}]{AU11,...,AUnn,BV,CW}[X]{AU11,...,AUnn,(BOC)U}[X]{AU11,...,AUnn,BV}[X]{A0U011,...,A0U