Mixing Finite Success and Finite Failure in an Automated Prover

pages

English

Documents

Lire un extrait

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

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

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

Publié par

chaeh

Nombre de lectures

Langue

English

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

Voir

Publié par

chaeh

Nombre de lectures

Langue

English

MixingFiniteSuccessandFiniteFailureinanAutomatedProverAlwenTiu1,GopalanNadathur2,andDaleMiller31INRIALorraine/LORIA2DigitalTechnologyCenterandDeptofCS,UniversityofMinnesota3INRIA&LIX,E´colePolytechniqueAbstract.Theoperationalsemanticsandtypingjudgementsofmod-ernprogrammingandspeciﬁcationlanguagesareoftendeﬁnedusingre-lationsandproofsystems.Insimplesettings,logicprogramminglan-guagescanbeusedtoprovideratherdirectandnaturalinterpretersforsuchoperationalsemantics.Morecomplexfeaturesofspeciﬁcationssuchasnamesandtheirbindings,proofruleswithnegativepremises,andtheexhaustiveenumerationofstatespaces,allposesigniﬁcantchallengestoconventionallogicprogrammingsystems.Inthispaper,wedescribeasimplearchitecturefortheimplementationofdeductionsystemsthatallowsaspeciﬁcationtointerleavebetweenﬁnitesuccessandﬁnitefail-ure.Theimplementationtechniquesforthisproverarelargelycommononesfromhigher-orderlogicprogramming,i.e.,logicvariables,(higher-orderpattern)uniﬁcation,backtracking(usingstream-basedcomputa-tion),andabstractsyntaxbasedonsimplytypedλ-terms.Wepresentaparticularinstanceofthisprover’sarchitectureanditsprototypeimple-mentation,Level0/1,basedonthedualinterpretationof(ﬁnite)successandﬁnitefailureinproofsearch.WeshowhowLevel0/1providesahigh-levelanddeclarativeimplementationofmodelcheckingandbisimulationcheckingforthe(ﬁnite)π-calculus.1IntroductionTheoperationalsemanticsandtypingjudgementsofmodernprogrammingandspeciﬁcationlanguagesareoftendeﬁnedusingrelationsandproofsystems,e.g.,inthestyleofPlotkin’sstructuraloperationalsemantics.Insimplesettings,higher-orderlogicprogramminglanguages,suchasλPrologandTwelf,canbeusedtoprovideratherdirectandnaturalinterpretersforoperationalseman-tics.However,suchlogicprogramminglanguagescanprovidelittlemorethananimationofsemanticdescriptions:inparticular,reasoningaboutspeciﬁedlan-guageshastobedoneoutsidethesystem.Forinstance,checkingbisimulationinprocesscalculineedsanalyzingallthetransitionpathsaprocesscanpoten-tiallygothrough.Toaddtothecomplication,modernlanguagespeciﬁcationsoftenmakeuseofcomplexfeaturessuchasvariablebindingsandthenotionofnames(asintheπ-calculus[MPW92]),whichinterferesinanon-trivialwaywithcaseanalyses.Thesecaseanalysescannotbedonedirectlyinsidethelogic

programmingsystem,notinapurelylogicalwayatleast,eventhoughtheyaresimplyenumerationsofanswersubstitutions.Inthispaper,wedescribeanex-tensiontologicprogrammingwithlogicallysoundfeatureswhichallowustodosomemodestautomatedreasoningaboutspeciﬁcationsofoperationalsemantics.Thisextensionismoreconceptualthantechnical,thatis,theimplementationoftheextendedlogicprogramminglanguageusesonlyimplementationtechniquesthatarecommontologicprogramming,i.e.,logicvariables,higher-orderpatternuniﬁcation,backtracking(usingstream-basedcomputation)andabstractsyntaxbasedontypedλ-calculus.TheimplementationdescribedinthispaperisbasedonthelogicFOλΔr[MT03],whichisalogicbasedonasubsetofChurch’sSimpleTheoryofTypesbutextendedwithﬁxedpointsandtherquantiﬁer.InFOλΔrquantiﬁcationoverpropositionsisnotallowedbutquantiﬁerscanotherwisesrangeovervari-ablesofhigher-types.Thusthetermsofthelogiccanbesimplytypedterms,whichcanbeusedtoencodetheλ-treesyntaxofencodedobjectsinanopera-tionalsemanticsspeciﬁcation.Thisstyleofencodingisavariantofhigher-orderabstractsyntaxinwhichmeta-levelλ-abstractionsareusedtoencodeobject-levelvariablebinding.Thequantiﬁerrisﬁrstintroducedin[MT03]tohelpencodethenotionof“genericjudgment”thatoccurscommonlywhenreasoningwithλ-treesyntax.Thelogicalextensiontoallowﬁxedpointsisdonethroughaprooftheoreticalnotionofdeﬁnitions[SH93,Eri91,Gir92,Sta¨94,MM00].Inalogicwithdeﬁnitions,anatomicpropositionmaybedeﬁnedbyanotherformula(whichmaycontaintheatomicpropositionitself).Proofsearchforadeﬁnedatomicformulaisdonebyunfoldingthedeﬁnitionoftheformula.Aprovableformulalike∀X.pX⊃qX,wherepandqaresomedeﬁnedpredicates,expressesthefactthatforeverytermtforwhichthereisasuccessfulcomputation(proof)ofpt,thereisacomputation(proof)ofqt.Towardsestablishingthetruthofthisformula,ifthecomputationtreeassociatedwithpisﬁnite,wecaneﬀectivelyenumerateallitscomputationpathsandchecktheprovabilityofqtforeachpath.Notethatifthecomputationtreeforpisempty(ptisnotprovableforanyt)then∀X.pX⊃qXis(vacuously)true.Inotherwords,failureinproofsearchforpXentailssuccessinproofsearchforpX⊃qX.Theanalogywithnegation-as-failureinlogicprogrammingisobvious:ifwetakeqXtobe⊥(false),thenprovabilityofpX⊃⊥correspondstosuccessinproofsearchfornot(pX)inlogicprogramming.Thisrelationbetweennegation-as-failureinlogicprogrammingandnegationinlogicwithdeﬁnitionshasbeenobservedin[HSH91,Gir92].IntheimplementationofFOλΔr,theaboveobservationleadstoaneutralviewonproofsearch:IfproofsearchforagoalAreturnsanon-emptysetofanswersubstitutions,thenwehavefoundaproofofA.Ontheotherhand,ifproofsearchforAreturnsanemptyanswerset,thenwehavefoundaprooffor¬A.Answersubstitutionscanthusbeinterpretedinadualwaydependingonthecontextofproofsearch;seeSection3formoredetails.Therestofthepaperisorganizedasfollows.InSection2,wegiveanoverviewofthelogicFOλΔr.Section3describesanimplementationofafragmentof

Voir

Univers
Ebooks
Livres audio
Presse
Podcasts
BD
Documents

Mixing Finite Success and Finite Failure in an Automated Prover

YouScribe

Le catalogue

Le service

Les conditions