Noname manuscript No will be inserted by the editor
23 pages
English

Noname manuscript No will be inserted by the editor

-

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

Description

Niveau: Supérieur, Doctorat, Bac+8
ar X iv :0 91 1. 29 93 v2 [ cs .L O] 1 Se p 2 01 0 Noname manuscript No. (will be inserted by the editor) A two-level logic approach to reasoning about computations Andrew Gacek · Dale Miller · Gopalan Nadathur the date of receipt and acceptance should be inserted later Abstract Relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, typing, and acceptance by non-deterministic machines. We therefore propose a (restricted) logical theory over relations as a language for specifying such notions. Our specification logic is further characterized by an ability to explicitly treat binding in object languages. Once such a logic is fixed, a natural next question is how we might prove theorems about specifications written in it. We propose to use a second logic, called a reasoning logic, for this purpose. A satisfactory reasoning logic should be able to completely encode the specification logic. Associated with the specification logic are various notions of binding: for quantifiers within formulas, for eigenvariables within sequents, and for abstractions within terms. To provide a natural treatment of these aspects, the reasoning logic must encode binding structures as well as their associated notions of scope, free and bound variables, and capture-avoiding substitution. Further, to support arguments about provability, the reasoning logic should possess strong mechanisms for constructing proofs by induction and co-induction.

  • logic

  • nominal constant

  • capture

  • can therefore

  • using ?-abstraction

  • rule

  • specification language

  • clause can

  • clause

  • rules


Sujets

Informations

Publié par
Nombre de lectures 27
Langue English

Exrait

NonamemanuscriptNo.(willbeinsertedbytheeditor)Atwo-levellogicapproachtoreasoningaboutcomputationsAndrewGacekDaleMillerGopalanNadathurthedateofreceiptandacceptanceshouldbeinsertedlaterAbstractRelationaldescriptionshavebeenusedinformalizingdiversecomputationalnotions,including,forexample,operationalsemantics,typing,andacceptancebynon-deterministicmachines.Wethereforeproposea(restricted)logicaltheoryoverrelationsasalanguageforspecifyingsuchnotions.Ourspecificationlogicisfurthercharacterizedbyanabilitytoexplicitlytreatbindinginobjectlanguages.Oncesuchalogicisfixed,anaturalnextquestionishowwemightprovetheoremsaboutspecificationswritteninit.Weproposetouseasecondlogic,calledareasoninglogic,forthispurpose.Asatisfactoryreasoninglogicshouldbeabletocompletelyencodethespecificationlogic.Associatedwiththespecificationlogicarevariousnotionsofbinding:forquantifierswithinformulas,foreigenvariableswithinsequents,andforabstractionswithinterms.Toprovideanaturaltreatmentoftheseaspects,thereasoninglogicmustencodebindingstructuresaswellastheirassociatednotionsofscope,freeandboundvariables,andcapture-avoidingsubstitution.Further,tosupportargumentsaboutprovability,thereasoninglogicshouldpossessstrongmechanismsforconstructingproofsbyinductionandco-induction.WeprovidethesecapabilitiesherebyusingalogiccalledGwhichrepresentsrelationsoverλ-termsviadefinitionsofatomicjudgments,containsinferencerulesforinductionandco-induction,andincludesaspecialgenericquantifier.WeshowhowprovabilityinthespecificationlogiccanbetransparentlyencodedinG.WealsodescribeaninteractivetheoremprovercalledAbellathatimplementsGandthistwo-levellogicapproachandwepresentseveralexamplesthatdemonstratetheefficacyofAbellainreasoningaboutcomputations.1IntroductionWeareinterestedinthispaperinspecifyingcomputationsandthenreasoningaboutthem.Arangeofformalismshavebeenusedasameansforrealizingthefirstoftheseobjectives.Forexample,theexecutionsemanticsofpro-gramminglanguageshavebeendescribeviatheλ-calculus[Reynolds,1972,Plotkin,1976],theπ-calculus[Milner,1992],andabstractmachines[Landin,1964].Aspecificationformalismthathasbeenparticularlysuccessfulandwidelyapplicableisoperationalsemanticsinbothits“small-step”version[Plotkin,1981]andits“big-step”ver-sion[Kahn,1987].Ofthemanymatureandflexiblechoicesthatcanbemade,wepickhererelationalspecificationsandtheirdirectencodingastheoriesinrestrictedlogics.Thischoiceallowsustotransparentlyencodeoperationalsemanticsaswellasarangeofothernotionsincluding,mostnotably,typing.Anotherconsequenceofourchoiceisthatourspecificationlanguagewill,infact,beaspecificationlogic.Morespecifically,itwillturnouttobeasimple,wellunderstoodlogicthatcanbeinterpretedasalogicprogramminglanguageinthestyleofλProlog[NadathurandMiller,1988].Afteronehaspickedalanguageforwritingspecifications,thereisstillachoicetobemadeaboutalanguageforreasoningaboutthem.Thechoicesofthesetwolanguagesareoftenrelated.Ifonehasselectedaspecificationlanguagerelyingon,say,processcalculus,thenareasoninglanguagethatexploitsbisimulationsandcongruenceswouldbeanaturalchoice:see,forexample,[Sangiorgi,1994].IfonechoosesabstractmachinesforspecificationsA.GacekandD.MillerINRIASaclay-Iˆle-de-France&LIX/E´colePolytechnique,Palaiseau,FranceE-mail:gacekatlix.polytechnique.fr,dale.milleratinria.frG.NadathurDepartmentofComputerScienceandEngineering,UniversityofMinnesota4-192EE/CSBuilding,200UnionStreetSE,Minneapolis,MN55455USAE-mail:gopalanatcs.umn.edu
theninductivedefinitionsareanaturalchoiceforareasoninglanguage.Inthispaper,ourreasoninglanguagewillbealogicthatcontainsstandardbutpowerfulmechanismsforinductionandco-inductionaswellasthe-quantifier(bothinformulasandindefinitions)[MillerandTiu,2005,Gaceketal.,2009].Ourchoiceofreasoninglogichasanumberofappealingaspects,chiefamongthembeingthatitispowerfulenoughtocapturewithinitmanyotherreasoningtechniquessuchasbisimulationandinductivedefinitions.Theapproachweshalldescribeinthispaperisthuscharacterizedbytheuseoftwologics,oneforspecifyingcomputationsandtheotherforreasoningabouttheselogicspecifications.Wepickbothoflogicstobeintuition-isticherebutotherchoicesarealsosensible:forexample,McDowellandMiller[2002]usedalinearlogicasaspecificationlanguageinordertoprovidedeclarativespecificationsforaprogramminglanguagewithstate.Thelogicalsymbolsofthesetwologicswillbeseparatedinourtreatment:infact,provabilityinthespecificationlogicwillbeaninductivelydefinedpredicateofthereasoninglogic.Althoughwedistinguishthelogicsinthisway,thetermstructuresthattheyusewillbeidentical:inparticular,theconstructionoftermsinbothlogicswillusethesameapplicationandabstractionoperations.Asaresult,termequalityinthereasoninglogicwillimmediatelyreflecttermequalityinthespecificationlogic.Inmanycommonlyusedapproaches,itisproblematictotreatspecification-languageabstractionthroughreasoning-logicabstraction.Thereasoninglogicofteninvolvesfunctiontypesthatcontainrecursivefunctions;thisisthecase,forexample,inCoqandIsabelle/HOL.Iffunctionabstractionatthetwolevelsareidentified,functiontypesinthespecificationlanguagewouldalsohavetocontainrecursivelydefinedfunctions.Sincethespecificationlanguageisintendedtotreatsyntacticexpressionsandnotgeneralfunctions,thisraisesissuesabouttheadequaterepresentationofsyntax:see,forexample,thediscussionabout“exoticterms”in[Despeyrouxetal.,1995].Inthesettingthatweshallsoonunfold,wegetaroundsuchproblemsbymakingfunctiontypesinboththespecificationandthereasoninglogicweak:whiletermequalitywillstillbegovernedbytherulesforαβη-conversion,thiswillhappenwithinthesimplytypedλ-calculusthatdoesnotincludestrongerprinciplessuchasrecursion.Torecovertheloststrength,wewilluseinductivelyandco-inductivelydefinedpredicatesforreasoningaboutcomputations.However,atthepredicatelevel,thespecificationlogicandthereasoninglogicwillbestrictlyseparated.Insummary,functiontypesinbothlogicswillbeweakandwillbeusedexclusivelytorepresentsyntaxthatmaycontainbindings.FollowingMiller[2000],weshallcallthisstyleofencodingdatawithbindingstheλ-treeapproachtoabstractsyntax.Whenwedevelopthetwo-levellogicapproachindetail,theformulasofthespecificationlogicwillbecometermsofthereasoninglogic.Thisapproachtoencodinganobjectlogicwithinasecondlogicshouldbecontrastedtotheapproachofprovabilitylogic(see,forexample,[Smorynski,2004])wherenaturalnumbersareusedtodenotesyntacticobjectsofanobject-logicandprimitiverecursivefunctionsareusedtoparseandmanipulatethoseobjects-cum-natural-numbers.Ourencodingismoredirect:bothtermsandformulasofthespecificationlogicarerepresentedbytermsinthereasoninglogic,withsimpletypesbeingusedtoseparatetermsfromformulas.Moreover,thepresenceofbindinginthetermsofthereasoninglogicmakesitpossibletorepresentquantifiedformulasinthespecificationlogicinanimmediateandnaturalmanner.Thereareanumberofadvantagestothetwo-levellogicapproachtoreasoningandtheparticularrealizationofitthatwediscussinthispaper.First,becauseofthetermstructuresusedinthereasoninglogic,onlymildencodingtechniquesareneededtoembedthespecificationlogicinit:forexample,specification-leveltermequalityisdirectlycaptured,quantificationinthespecificationlogicistreatedbyusingλ-abstractiontobindthequantifiedvariable,andtheinstantiationofquantifiersisrealizedthroughβ-conversion.Second,sincespecificationsarewritteninalogicandsincesuchalogictypicallyhasmeta-theoreticproperties(suchascut-admissibility)thatcanbeformalizedinthereasoninglogic,powerfultechniquesbecomeavailableforreasoningaboutdescriptionspresentedinthespecificationlogic.Third,asaseriesofexamplesillustrates,thistwo-levellogicapproachcanresultinnatural,readable,andcompletelyformalproofsofwell-knowntheoremsaboutcomputationalsystems.Finally,whenonemovestoimplementingtheoremproversbasedonthisarchitecture,onlyonenotionofbinding,variable,termequality,substitution,andunificationneedstobetreatedforbothlogics.InthenextsectionwedescribetheaspectsofthereasoninglogicGthatweshalluseinthispaper.Section3presentsthespecificationlanguagehH2andshowshowcut-freesequentcalculusprovabilityforitcanbegivenanadequateencodinginG.Section4describesbrieflythestructureofatheorem-provercalledAbellathatcanbeusedtointeractivelyconstructsequentcalculusproofsinG.ThisdescriptionisthenexploitedinSection5topresentexamplesoftheuseofthetwo-levellogicapproach.Section6describesrelatedworkandSection7concludeswithanindicationofsomefuturedirections.2
  • Accueil Accueil
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • BD BD
  • Documents Documents