Mixing Finite Success and Finite Failure in an Automated Prover

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

• École polytechnique
• Pi calculus
• Free variables and bound variables
• Logic programming

Informations

• Publié par: chaeh
• Nombre de lectures: 3
• Langue: English

Extrait

MixingFiniteSuccessandFiniteFailure inanAutomatedProver AlwenTiu 1 ,GopalanNadathur 2 ,andDaleMiller 3 1 INRIALorraine/LORIA 2 DigitalTechnologyCenterandDeptofCS,UniversityofMinnesota 3 INRIA&LIX,E ´ colePolytechnique Abstract. Theoperationalsemanticsandtypingjudgementsofmod- ernprogrammingandspecificationlanguagesareoftendefinedusingre- lationsandproofsystems.Insimplesettings,logicprogramminglan- guagescanbeusedtoprovideratherdirectandnaturalinterpretersfor suchoperationalsemantics.Morecomplexfeaturesofspecificationssuch asnamesandtheirbindings,proofruleswithnegativepremises,andthe exhaustiveenumerationofstatespaces,allposesignificantchallenges toconventionallogicprogrammingsystems.Inthispaper,wedescribe asimplearchitecturefortheimplementationofdeductionsystemsthat allowsaspecificationtointerleavebetweenfinitesuccessandfinitefail- ure.Theimplementationtechniquesforthisproverarelargelycommon onesfromhigher-orderlogicprogramming,i.e.,logicvariables,(higher- orderpattern)unification,backtracking(usingstream-basedcomputa- tion),andabstractsyntaxbasedonsimplytypedλ-terms.Wepresenta particularinstanceofthisprover’sarchitectureanditsprototypeimple- mentation,Level0/1,basedonthedualinterpretationof(finite)success andfinitefailureinproofsearch.WeshowhowLevel0/1providesahigh- levelanddeclarativeimplementationofmodelcheckingandbisimulation checkingforthe(finite)π-calculus. 1Introduction Theoperationalsemanticsandtypingjudgementsofmodernprogrammingand specificationlanguagesareoftendefinedusingrelationsandproofsystems,e.g., inthestyleofPlotkin’sstructuraloperationalsemantics.Insimplesettings, higher-orderlogicprogramminglanguages,suchasλPrologandTwelf,canbe usedtoprovideratherdirectandnaturalinterpretersforoperationalseman- tics.However,suchlogicprogramminglanguagescanprovidelittlemorethan animationofsemanticdescriptions:inparticular,reasoningaboutspecifiedlan- guageshastobedoneoutsidethesystem.Forinstance,checkingbisimulation inprocesscalculineedsanalyzingallthetransitionpathsaprocesscanpoten- tiallygothrough.Toaddtothecomplication,modernlanguagespecifications oftenmakeuseofcomplexfeaturessuchasvariablebindingsandthenotion ofnames(asintheπ-calculus[MPW92]),whichinterferesinanon-trivialway withcaseanalyses.Thesecaseanalysescannotbedonedirectlyinsidethelogic

programmingsystem,notinapurelylogicalwayatleast,eventhoughtheyare simplyenumerationsofanswersubstitutions.Inthispaper,wedescribeanex- tensiontologicprogrammingwithlogicallysoundfeatureswhichallowustodo somemodestautomatedreasoningaboutspecificationsofoperationalsemantics. Thisextensionismoreconceptualthantechnical,thatis,theimplementationof theextendedlogicprogramminglanguageusesonlyimplementationtechniques thatarecommontologicprogramming,i.e.,logicvariables,higher-orderpattern unification,backtracking(usingstream-basedcomputation)andabstractsyntax basedontypedλ-calculus. TheimplementationdescribedinthispaperisbasedonthelogicFOλ Δr [MT03],whichisalogicbasedonasubsetofChurch’sSimpleTheoryofTypes butextendedwithfixedpointsandtherquantifier.InFOλ Δr quantification overpropositionsisnotallowedbutquantifierscanotherwisesrangeovervari- ablesofhigher-types.Thusthetermsofthelogiccanbesimplytypedterms, whichcanbeusedtoencodetheλ-treesyntaxofencodedobjectsinanopera- tionalsemanticsspecification.Thisstyleofencodingisavariantofhigher-order abstractsyntaxinwhichmeta-levelλ-abstractionsareusedtoencodeobject- levelvariablebinding.Thequantifierrisfirstintroducedin[MT03]tohelp encodethenotionof“genericjudgment”thatoccurscommonlywhenreasoning withλ-treesyntax. Thelogicalextensiontoallowfixedpointsisdonethroughaprooftheoretical notionofdefinitions[SH93,Eri91,Gir92,Sta¨94,MM00].Inalogicwithdefinitions, anatomicpropositionmaybedefinedbyanotherformula(whichmaycontain theatomicpropositionitself).Proofsearchforadefinedatomicformulaisdone byunfoldingthedefinitionoftheformula.Aprovableformulalike∀X.pX⊃qX, wherepandqaresomedefinedpredicates,expressesthefactthatforeveryterm tforwhichthereisasuccessfulcomputation(proof)ofpt,thereisacomputation (proof)ofqt.Towardsestablishingthetruthofthisformula,ifthecomputation treeassociatedwithpisfinite,wecaneffectivelyenumerateallitscomputation pathsandchecktheprovabilityofqtforeachpath.Notethatifthecomputation treeforpisempty(ptisnotprovableforanyt)then∀X.pX⊃qXis(vacuously) true.Inotherwords,failureinproofsearchforpXentailssuccessinproofsearch forpX⊃qX.Theanalogywithnegation-as-failureinlogicprogrammingis obvious:ifwetakeqXtobe⊥(false),thenprovabilityofpX⊃⊥correspondsto successinproofsearchfornot(pX)inlogicprogramming.Thisrelationbetween negation-as-failureinlogicprogrammingandnegationinlogicwithdefinitions hasbeenobservedin[HSH91,Gir92].IntheimplementationofFOλ Δr ,the aboveobservationleadstoaneutralviewonproofsearch:Ifproofsearchfora goalAreturnsanon-emptysetofanswersubstitutions,thenwehavefounda proofofA.Ontheotherhand,ifproofsearchforAreturnsanemptyanswerset, thenwehavefoundaprooffor¬A.Answersubstitutionscanthusbeinterpreted inadualwaydependingonthecontextofproofsearch;seeSection3formore details. Therestofthepaperisorganizedasfollows.InSection2,wegiveanoverview ofthelogicFOλ Δr .Section3describesanimplementationofafragmentof