15 Pages
English

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

-

Gain access to the library to view online
Learn more

Description

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


Subjects

Informations

Published by
Reads 6
Language English
Fromproofstofocusedproofs:amodularproofofFocalizationinLinearLogicDaleMillerandAlexisSaurinINRIA&LIX/E´colePolytechnique,Palaiseau,Francedale.milleratinria.frsaurinatlix.polytechnique.frAbstract.Probablythemostsignificantresultconcerningcut-freesequentcal-culusproofsinlinearlogicisthecompletenessoffocusedproofs.Thiscom-pletenesstheoremhasanumberofprooftheoreticapplications—e.g.ingamesemantics,Ludics,andproofsearch—andmorecomputerscienceapplications—e.g.logicprogramming,call-by-name/valueevaluation.Andreoliprovedthistheoremforfirst-orderlinearlogic15yearsago.Inthepresentpaper,wegiveanewproofofthecompletenessoffocusedproofsintermsofprooftransfor-mation.Theproofofthistheoremissimpleandmodular:itisfirstprovedforMALLandthenisextendedtofulllinearlogic.Givenitsmodularstructure,weshowhowtheproofcanbeextendedtolargersystems,suchaslogicswithinduc-tion.Ouranalysisoffocusedproofswillemployaprooftransformationmethodthatleadsustostudyhowfocusingandcuteliminationinteract.Akeycompo-nentofourproofistheconstructionofafocalizationgraphwhichprovidesanabstractionoverhowfocusingcanbeorganizedwithinagivencut-freeproof.UsingthisgraphabstractionallowsustoprovideadetailedstudyofatomicbiasassignmentinawaymorerefinedthatisgiveninAndreoli’soriginalproof.Per-mittingmoreflexibleassignmentofbiaswillallowthiscompletenesstheoremtohelpestablishthecompletenessofanumberofotherautomateddeductionproce-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].
)