Induction and Co induction in Sequent Calculus

Alberto Momigliano1

Description

Niveau: Supérieur, Doctorat, Bac+8
Induction and Co-induction in Sequent Calculus Alberto Momigliano1,2 and Alwen Tiu3,4 1 LFCS, University of Edinburgh 2 DSI, University of Milan 3 LIX, Ecole polytechnique 4 Computer Science and Engineering Department, Penn State University Abstract. Proof search has been used to specify a wide range of computation sys- tems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof princi- ples are based on a proof theoretic notion of definition [26, 9, 13] Definitions are essentially stratified logic programs. The left and right rules for defined atoms treat the definitions as defining fixed points. The use of definitions makes it possible to rea- son intensionally about syntax, in particular enforcing free equality via unification. The full system thus allows inductive and co-inductive proofs involving higher-order abstract syntax. We extend earlier work by allowing induction and co-induction on general definitions and show that cut-elimination holds for this extension. We present some examples involving lists and simulation in the lazy ?-calculus. 1 Introduction A common approach to specifying computation systems is via deductive systems, e.g., structural operational semantics. Such specifications can be represented as logical theo- ries in a suitably expressive formal logic in which proof-search can then be used to model the computation.

• cut-elimination holds


• order proof


• can thus


• ??c ?


• corresponding defined


• clause


• ??


• co-inductive clause


• logical constants

Sujets

• École polytechnique
• Universidad Estatal de Pensilvania
• Clause
• Logical constant

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 13
• Langue: English

Extrait

InductionandCo-inductioninSequentCalculus AlbertoMomigliano 1 , 2 andAlwenTiu 3 , 4 1 LFCS,UniversityofEdinburgh 2 DSI,UniversityofMilan [e-mail] 3 LIX,E ´ colepolytechnique 4 ComputerScienceandEngineeringDepartment,PennStateUniversity [e-mail] Abstract.Proofsearchhasbeenusedtospecifyawiderangeofcomputationsys- tems.Inordertobuildaframeworkforreasoningaboutsuchspecications,wemake useofasequentcalculusinvolvinginductionandco-induction.Theseproofprinci- plesarebasedonaprooftheoreticnotionofdenition[26,9,13]Denitionsare essentiallystratiedlogicprograms.Theleftandrightrulesfordenedatomstreat thedenitionsasdeningxedpoints.Theuseofdenitionsmakesitpossibletorea- sonintensionallyaboutsyntax,inparticularenforcingfreeequalityviaunication. Thefullsystemthusallowsinductiveandco-inductiveproofsinvolvinghigher-order abstractsyntax.Weextendearlierworkbyallowinginductionandco-inductionon generaldenitionsandshowthatcut-eliminationholdsforthisextension.Wepresent someexamplesinvolvinglistsandsimulationinthelazy l -calculus. 1Introduction Acommonapproachtospecifyingcomputationsystemsisviadeductivesystems,e.g., structuraloperationalsemantics.Suchspecicationscanberepresentedaslogicaltheo- riesinasuitablyexpressiveformallogicinwhichproof-searchcanthenbeusedtomodel thecomputation.Thisuseoflogicasaspecicationlanguageisalongthelineoflogical frameworks[21].Therepresentationofthesyntaxofcomputationsystemsinsideformal logiccanbenetfromtheuseofhigher-orderabstractsyntax(HOAS),ahigh-leveland declarativetreatmentofobject-levelboundvariablesandsubstitution.Atthesametime, wewanttousesuchalogicinordertoreasonoverthemeta-theoreticalpropertiesofob- jectlanguages,forexampletypepreservationinoperationalsemantics[14],soundnessand completenessofcompilation[18]orcongruenceofbisimulationintransitionsystems[15]. Typicallythisinvolvesreasoningby(structural)inductionand,whendealingwithinnite behaviour,co-induction[5]. Theneedtosupportbothinductiveandco-inductivereasoningandsomeformofHOAS requiressomecarefuldesigndecisions,sincethetwoareprimafacienotoriouslyincompat- ible.Whileanymeta-languagebasedona l -calculuscanbeusedtospecifyandpossibly performcomputationsoverHOASencodings,meta-reasoninghastraditionallyinvolved (co)inductivespecicationsbothatthelevelofthesyntaxandofthejudgementsaswell (whichareofcourseuniedatthetype-theoreticlevel).Therstprovidescrucialfreeness propertiesfordatatypesconstructors,whilethesecondoffersprincipleofcaseanalysisand (co)induction.Thisiswell-knowntobeproblematic,sinceHOASspecicationsleadto