From proofs to focused proofs: a modular proof of Focalization in Linear Logic

pages

English

Documents

Écrit par
Alexis Saurin

Publié par
chaeh

Lire un extrait

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

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

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

Publié par

chaeh

Nombre de lectures

Langue

English

Niveau: Supérieur
From proofs to focused proofs: a modular proof of Focalization in Linear Logic Dale Miller and Alexis Saurin INRIA & LIX/Ecole Polytechnique, Palaiseau, France dale.miller at inria.fr saurin at lix.polytechnique.fr Abstract. Probably the most significant result concerning cut-free sequent cal- culus proofs in linear logic is the completeness of focused proofs. This com- pleteness theorem has a number of proof theoretic applications — e.g. in game semantics, Ludics, and proof search — and more computer science applications — e.g. logic programming, call-by-name/value evaluation. Andreoli proved this theorem for first-order linear logic 15 years ago. In the present paper, we give a new proof of the completeness of focused proofs in terms of proof transfor- mation. The proof of this theorem is simple and modular: it is first proved for MALL and then is extended to full linear logic. Given its modular structure, we show how the proof can be extended to larger systems, such as logics with induc- tion. Our analysis of focused proofs will employ a proof transformation method that leads us to study how focusing and cut elimination interact. A key compo- nent of our proof is the construction of a focalization graph which provides an abstraction over how focusing can be organized within a given cut-free proof.

inference rules

mall

linear logic

focused proof

can account

cut-free sequent

consider cut

sequent ?

no cut-free

focused proofs

Voir

Publié par

chaeh

Nombre de lectures

Langue

English

Fromproofstofocusedproofs:amodularproofofFocalizationinLinearLogicDaleMillerandAlexisSaurinINRIA&LIX/E´colePolytechnique,Palaiseau,Francedale.milleratinria.frsaurinatlix.polytechnique.frAbstract.Probablythemostsigniﬁcantresultconcerningcut-freesequentcal-culusproofsinlinearlogicisthecompletenessoffocusedproofs.Thiscom-pletenesstheoremhasanumberofprooftheoreticapplications—e.g.ingamesemantics,Ludics,andproofsearch—andmorecomputerscienceapplications—e.g.logicprogramming,call-by-name/valueevaluation.Andreoliprovedthistheoremforﬁrst-orderlinearlogic15yearsago.Inthepresentpaper,wegiveanewproofofthecompletenessoffocusedproofsintermsofprooftransfor-mation.Theproofofthistheoremissimpleandmodular:itisﬁrstprovedforMALLandthenisextendedtofulllinearlogic.Givenitsmodularstructure,weshowhowtheproofcanbeextendedtolargersystems,suchaslogicswithinduc-tion.Ouranalysisoffocusedproofswillemployaprooftransformationmethodthatleadsustostudyhowfocusingandcuteliminationinteract.Akeycompo-nentofourproofistheconstructionofafocalizationgraphwhichprovidesanabstractionoverhowfocusingcanbeorganizedwithinagivencut-freeproof.UsingthisgraphabstractionallowsustoprovideadetailedstudyofatomicbiasassignmentinawaymorereﬁnedthatisgiveninAndreoli’soriginalproof.Per-mittingmoreﬂexibleassignmentofbiaswillallowthiscompletenesstheoremtohelpestablishthecompletenessofanumberofotherautomateddeductionproce-dures.Focalizationgraphscanbeusedtojustifytheintroductionofaninferenceruleformultifocusderivation:arulethatshouldhelpusbetterunderstandtherelationsbetweensequentialityandconcurrencyinlinearlogic.1IntroductionLinearLogicwasintroduced20yearsagobyGirardandsincethenithasledtomanydevelopmentsinprooftheory,computationallogic,andprogramminglanguagetheory.Muchprooftheoreticanalysesandapplicationsoflinearlogichaveconcentratedonthenatureanddynamicsofcut-eliminationviathegeometryofinteractions,gamese-mantics,interactions,etc.Lesshasbeenstudiedaboutthestructureofcut-freeproofsthemselves:themainresultinthatareaisprobablythecompletenessoffocusedproofsduetoAndreoli[3,4].Thiscompletenesstheoremhasanumberofapplicationsincom-puterscience:forexample,focusedproofshavebeenusedtodesignandformalizelogicprogramminglanguages[2,20],toformalizeproofsystemsthatallowforbothforward-chainingandbackward-chaining[15,19],andshouldbebehindthedualitiesbetweencall-by-nameandcall-by-valueevaluationintheλ-calculus[6].Thestructureoffo-cusedproofsisalsoakeyingredientinthedevelopmentofPolarizedLogic[17,18]andLudics[13].

Voir