Under consideration for publication in Math Struct in Comp Science

chaeh

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

21 pages

English

Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

A propos
Informations
Extrait

Description

Niveau: Supérieur
Under consideration for publication in Math. Struct. in Comp. Science A System of Interaction and Structure V: The Exponentials and Splitting Alessio Guglielmi1† and Lutz Straßburger2‡ 1Department of Computer Science University of Bath Bath BA2 7AY United Kingdom http: // alessio. guglielmi. name/ 2INRIA Saclay–Ile-de-France and Ecole Polytechnique Laboratoire d'Informatique (LIX) Rue de Saclay 91128 Palaiseau Cedex France http: // www. lix. polytechnique. fr/ ~ lutz/ Received 22 January 2004; Revised 3 December 2010 System NEL is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials, or, equivalently, it is MELL augmented with the non-commutative self-dual connective seq. NEL is presented in deep inference, because no Gentzen formalism can express it in such a way that the cut rule is admissible. Other, recent works, show that system NEL is Turing-complete, it is able to directly express process algebra sequential composition and it faithfully models causal quantum evolution. In this paper, we show cut elimination for NEL, based on a technique that we call splitting. The splitting theorem shows how and to what extent we can recover a sequent-like structure in NEL proofs. Together with a ‘decomposition' theorem, proved in the previous paper of this series, splitting yields a cut-elimination procedure for NEL.

elimination procedure

connective

linear logic

system nel

gentzen calculi

show cut elimination

free system

like bv

paper provides

Sujets

Kingdom

École polytechnique

Connective

Linear logic

Informations

Publié par	chaeh
Nombre de lectures	12
Langue	English

Extrait

UnderconsiderationforpublicationinMath.Struct.inComp.ScienceASystemofInteractionandStructureV:TheExponentialsandSplittingAlessioGuglielmi1†andLutzStraßburger2‡1DepartmentofComputerScienceUniversityofBathBathBA27AYUnitedKingdomhttp://alessio.guglielmi.name/2INRIASaclay–Iˆle-de-FranceandE´colePolytechniqueLaboratoired’Informatique(LIX)RuedeSaclay91128PalaiseauCedexFrancehttp://www.lix.polytechnique.fr/~lutz/Received22January2004;Revised3December2010SystemNEListhemixedcommutative/non-commutativelinearlogicBVaugmentedwithlinearlogic’sexponentials,or,equivalently,itisMELLaugmentedwiththenon-commutativeself-dualconnectiveseq.NELispresentedindeepinference,becausenoGentzenformalismcanexpressitinsuchawaythatthecutruleisadmissible.Other,recentworks,showthatsystemNELisTuring-complete,itisabletodirectlyexpressprocessalgebrasequentialcompositionanditfaithfullymodelscausalquantumevolution.Inthispaper,weshowcuteliminationforNEL,basedonatechniquethatwecallsplitting.Thesplittingtheoremshowshowandtowhatextentwecanrecoverasequent-likestructureinNELproofs.Togetherwitha‘decomposition’theorem,provedinthepreviouspaperofthisseries,splittingyieldsacut-eliminationprocedureforNEL.1.IntroductionThisistheﬁfthinaseriesofpapersdedicatedtotheprooftheoryofaself-dual,non-commutative,linearconnective,calledseq,inthecontextoflinearlogic.TheadditionofseqtomultiplicativelinearlogicyieldsalogicthatwecallBV.Thislogicisthemainsubjectofstudyofthisseriesofpapers.BVisconjecturedtobethesameaspomsetlogic,studiedbyRetore´in(Ret97)andotherpapers.†oGfuPglrioeolfms’iiasnsdupbpyotrtheedIbNyRaInAAANRRCS‘eRnEioDrOC:hRaierdeesdi’gEnxicneglleLnocgiectailtlSeydn‘tIadxe’.ntityandGeometricEssence‡StraßburgerissupportedbytheANRproject‘INFER:TheoryandApplicationofDeepInference’andbytheINRIAARC‘REDO:RedesigningLogicalSyntax’.

A.GuglielmiandL.Straßburger2BVhasbeendeﬁnedin(Gug07)(theﬁrstpaperofthisseries),whereasound,completeandcut-freesystemforBVisgiven,togetherwithacut-eliminationprocedure.TheproofsystemofBVradicallydepartsfromthetraditionalsequentcalculusmethodology,andadoptsinsteaddeepinferenceasthedesignprinciple.Inshort,thismeansthatproofscanbefreelycomposedbythesameconnectivesusedforformulae,or,equivalently,inferencerulescanbeappliedarbitrarilydeepinsideformulae.Thecitedpaperprovidesanintroductiontodeepinference,which,asamatteroffact,hasbeenoriginallyconceivedpreciselyforcapturingBV.Theformalismadoptedinthepapersoftheseriessofar,includingthisone,iscalledthecalculusofstructures,orCoS.Thisis,conceptually,thesimplestformalismindeepinference,beingjustaspecialformoftermrewriting.Moresophisticatedformalismsindeepinferenceareemerging,inparticularopendeduction(GGP10).ThisformalismimprovesonCoSbecauseithasanincreasedalgebraicﬂavourandallowsforaspeed-upinthesizeofproofs.However,thesediﬀerencesdonotaﬀectcut-eliminationprocedures,inthesensethatfromacut-eliminationprocedureinCoS,onecantriviallyobtainacut-eliminationprocedureinopendeduction.Forthisreason,theresultsinthispaperarebroadlyvalidinsidethedeep-inferenceparadigm.Theuseofdeepinferenceisnecessary:AlwenTiushowedin(Tiu06)(thesecondpaperofthisseries)thatitisimpossibleforthesequentcalculustoprovideasound,completeandcut-freeproofsystemforBV.ThisisprovedbyexhibitinganinﬁnitesetofBVtautologieswithacleverlydesignedstructure,suchthatanybounded-depth,cut-freeinferencesystem(inparticular,anysequentcalculussystem)iseitherunsoundorincompleteonthesetoftautologies.Thedesignofthesetautologiesexploitstheabilityoftheseqconnective,togetherwiththeusual‘par’disjunctionoflinearlogic,toburyatarbitrarydepthsinsideformulaecertainkeystructuresthathavetobe‘unlocked’,byinference,beforeanyotherpartsoftheformulaaretouched.Westressthefactthatthisbehaviourisindependentofthelogicalformalismemployedtodescribeit.So,deepinferenceappearstobethemostnaturalchoiceofproof-systemdesignmethodology,becauseofitsabilitytoapplyinferenceatarbitrarydepthsinsideformulae.BVmightbeconsideredexoticasalogic,butithasaverynaturalalgebraicnature,thatalreadyfoundapplicationsindiverseﬁelds.Wementionhere:1)itsabilitytocaptureverypreciselythesequentialconnectiveofMilner’sCCS(andsoofotherprocessalgebras)(Bru02);2)abetteraxiomatisationofcausalquantumcomputationthanlinearlogicprovides(BPS08;BGI+10);and3)anewclassofcategoricalmodels(BPS09).WeknowthattheproofsystemBVisNP-complete(Kah07),anditsfeasibilityforproofsearchhasbeenstudied(Kah04).Thisﬁfthpaper,togetherwiththefourthpaper(SG09)intheseries,isdevotedtotheprooftheoryofsystemBVwhenitisenrichedwithlinearlogic’sexponentials.WecallNEL(non-commutativeexponentiallinearlogic)theresultingsystem.WecanalsoconsiderNELasMELL(multiplicativeexponentiallinearlogic(Gir87))augmentedwithseq.NEL,whichwasﬁrstpresentedin(GS02),isconservativeoverbothBVandoverMELLaugmentedbythemixandnullarymixrules(FR94;Ret93;AJ94).LikeBV,NELcannotbeexpressedwithacut-freeproofsystemoutsideofdeepinference,becauseof

Univers
Ebooks
Livres audio
Presse
Podcasts
BD
Documents

Under consideration for publication in Math Struct in Comp Science

Kingdom

École polytechnique

Connective

Linear logic

YouScribe

Le catalogue

Le service

Les conditions