Mixing Finite Success and Finite Failure in an Automated Prover
20 pages
English

Mixing Finite Success and Finite Failure in an Automated Prover

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

Description

Niveau: Supérieur
Mixing Finite Success and Finite Failure in an Automated Prover Alwen Tiu1, Gopalan Nadathur2, and Dale Miller3 1 INRIA Lorraine/LORIA 2 Digital Technology Center and Dept of CS, University of Minnesota 3 INRIA & LIX, Ecole Polytechnique Abstract. The operational semantics and typing judgements of mod- ern programming and specification languages are often defined using re- lations and proof systems. In simple settings, logic programming lan- guages can be used to provide rather direct and natural interpreters for such operational semantics. More complex features of specifications such as names and their bindings, proof rules with negative premises, and the exhaustive enumeration of state spaces, all pose significant challenges to conventional logic programming systems. In this paper, we describe a simple architecture for the implementation of deduction systems that allows a specification to interleave between finite success and finite fail- ure. The implementation techniques for this prover are largely common ones from higher-order logic programming, i.e., logic variables, (higher- order pattern) unification, backtracking (using stream-based computa- tion), and abstract syntax based on simply typed ?-terms. We present a particular instance of this prover's architecture and its prototype imple- mentation, Level 0/1, based on the dual interpretation of (finite) success and finite failure in proof search. We show how Level 0/1 provides a high- level and declarative implementation of model checking and bisimulation checking for the (finite) pi-calculus.

  • pi calculus

  • specification languages

  • scoped generic constants

  • typed ?-terms

  • bound variable

  • can thus

  • generic judgment

  • higher-order abstract

  • order pattern

  • logic programming


Sujets

Informations

Publié par
Nombre de lectures 3
Langue English

Exrait

MixingFiniteSuccessandFiniteFailureinanAutomatedProverAlwenTiu1,GopalanNadathur2,andDaleMiller31INRIALorraine/LORIA2DigitalTechnologyCenterandDeptofCS,UniversityofMinnesota3INRIA&LIX,E´colePolytechniqueAbstract.Theoperationalsemanticsandtypingjudgementsofmod-ernprogrammingandspecificationlanguagesareoftendefinedusingre-lationsandproofsystems.Insimplesettings,logicprogramminglan-guagescanbeusedtoprovideratherdirectandnaturalinterpretersforsuchoperationalsemantics.Morecomplexfeaturesofspecificationssuchasnamesandtheirbindings,proofruleswithnegativepremises,andtheexhaustiveenumerationofstatespaces,allposesignificantchallengestoconventionallogicprogrammingsystems.Inthispaper,wedescribeasimplearchitecturefortheimplementationofdeductionsystemsthatallowsaspecificationtointerleavebetweenfinitesuccessandfinitefail-ure.Theimplementationtechniquesforthisproverarelargelycommononesfromhigher-orderlogicprogramming,i.e.,logicvariables,(higher-orderpattern)unification,backtracking(usingstream-basedcomputa-tion),andabstractsyntaxbasedonsimplytypedλ-terms.Wepresentaparticularinstanceofthisprover’sarchitectureanditsprototypeimple-mentation,Level0/1,basedonthedualinterpretationof(finite)successandfinitefailureinproofsearch.WeshowhowLevel0/1providesahigh-levelanddeclarativeimplementationofmodelcheckingandbisimulationcheckingforthe(finite)π-calculus.1IntroductionTheoperationalsemanticsandtypingjudgementsofmodernprogrammingandspecificationlanguagesareoftendefinedusingrelationsandproofsystems,e.g.,inthestyleofPlotkin’sstructuraloperationalsemantics.Insimplesettings,higher-orderlogicprogramminglanguages,suchasλPrologandTwelf,canbeusedtoprovideratherdirectandnaturalinterpretersforoperationalseman-tics.However,suchlogicprogramminglanguagescanprovidelittlemorethananimationofsemanticdescriptions:inparticular,reasoningaboutspecifiedlan-guageshastobedoneoutsidethesystem.Forinstance,checkingbisimulationinprocesscalculineedsanalyzingallthetransitionpathsaprocesscanpoten-tiallygothrough.Toaddtothecomplication,modernlanguagespecificationsoftenmakeuseofcomplexfeaturessuchasvariablebindingsandthenotionofnames(asintheπ-calculus[MPW92]),whichinterferesinanon-trivialwaywithcaseanalyses.Thesecaseanalysescannotbedonedirectlyinsidethelogic
programmingsystem,notinapurelylogicalwayatleast,eventhoughtheyaresimplyenumerationsofanswersubstitutions.Inthispaper,wedescribeanex-tensiontologicprogrammingwithlogicallysoundfeatureswhichallowustodosomemodestautomatedreasoningaboutspecificationsofoperationalsemantics.Thisextensionismoreconceptualthantechnical,thatis,theimplementationoftheextendedlogicprogramminglanguageusesonlyimplementationtechniquesthatarecommontologicprogramming,i.e.,logicvariables,higher-orderpatternunification,backtracking(usingstream-basedcomputation)andabstractsyntaxbasedontypedλ-calculus.TheimplementationdescribedinthispaperisbasedonthelogicFOλΔr[MT03],whichisalogicbasedonasubsetofChurch’sSimpleTheoryofTypesbutextendedwithfixedpointsandtherquantifier.InFOλΔrquantificationoverpropositionsisnotallowedbutquantifierscanotherwisesrangeovervari-ablesofhigher-types.Thusthetermsofthelogiccanbesimplytypedterms,whichcanbeusedtoencodetheλ-treesyntaxofencodedobjectsinanopera-tionalsemanticsspecification.Thisstyleofencodingisavariantofhigher-orderabstractsyntaxinwhichmeta-levelλ-abstractionsareusedtoencodeobject-levelvariablebinding.Thequantifierrisfirstintroducedin[MT03]tohelpencodethenotionof“genericjudgment”thatoccurscommonlywhenreasoningwithλ-treesyntax.Thelogicalextensiontoallowfixedpointsisdonethroughaprooftheoreticalnotionofdefinitions[SH93,Eri91,Gir92,Sta¨94,MM00].Inalogicwithdefinitions,anatomicpropositionmaybedefinedbyanotherformula(whichmaycontaintheatomicpropositionitself).Proofsearchforadefinedatomicformulaisdonebyunfoldingthedefinitionoftheformula.AprovableformulalikeX.pXqX,wherepandqaresomedefinedpredicates,expressesthefactthatforeverytermtforwhichthereisasuccessfulcomputation(proof)ofpt,thereisacomputation(proof)ofqt.Towardsestablishingthetruthofthisformula,ifthecomputationtreeassociatedwithpisfinite,wecaneffectivelyenumerateallitscomputationpathsandchecktheprovabilityofqtforeachpath.Notethatifthecomputationtreeforpisempty(ptisnotprovableforanyt)thenX.pXqXis(vacuously)true.Inotherwords,failureinproofsearchforpXentailssuccessinproofsearchforpXqX.Theanalogywithnegation-as-failureinlogicprogrammingisobvious:ifwetakeqXtobe(false),thenprovabilityofpX⊃⊥correspondstosuccessinproofsearchfornot(pX)inlogicprogramming.Thisrelationbetweennegation-as-failureinlogicprogrammingandnegationinlogicwithdefinitionshasbeenobservedin[HSH91,Gir92].IntheimplementationofFOλΔr,theaboveobservationleadstoaneutralviewonproofsearch:IfproofsearchforagoalAreturnsanon-emptysetofanswersubstitutions,thenwehavefoundaproofofA.Ontheotherhand,ifproofsearchforAreturnsanemptyanswerset,thenwehavefoundaprooffor¬A.Answersubstitutionscanthusbeinterpretedinadualwaydependingonthecontextofproofsearch;seeSection3formoredetails.Therestofthepaperisorganizedasfollows.InSection2,wegiveanoverviewofthelogicFOλΔr.Section3describesanimplementationofafragmentof
  • Accueil Accueil
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • BD BD
  • Documents Documents