FGUC Preliminary Version
21 pages
English

FGUC Preliminary Version

-

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

Description

Niveau: Supérieur
FGUC 2004 Preliminary Version A Proof Search Specification of the pi-Calculus Alwen Tiu 1,3 INRIA-Futurs and Ecole polytechnique Dale Miller 2 INRIA-Futurs and Ecole polytechnique Abstract We present a meta-logic that contains a new quantifier ? (for encoding “generic judgments”) and inference rules for reasoning within fixed points of a given speci- fication. We then specify the operational semantics and bisimulation relations for the finite pi-calculus within this meta-logic. Since we restrict to the finite case, the ability of the meta-logic to reason within fixed points becomes a powerful and complete tool since simple proof search can compute this one fixed point. The ? quantifier helps with the delicate issues surrounding the scope of variables within pi- calculus expressions and their executions (proofs). We shall illustrate several merits of the logical specifications we write: they are natural and declarative; they contain no side conditions concerning names of variables while maintaining a completely formal treatment of such variables; differences between late and open bisimulation relations are easy to see declaratively; and proof search involving the application of inference rules, unification, and backtracking can provide complete proof systems for both one-step transitions and for bisimulation. Key words: pi-calculus, names, meta-logic, proof search, bisimulation. 1 Introduction In order to treat abstractions within expressions and computation declara- tively, we shall work within a meta-logic which contains a well understood notion of abstraction: in particular, we shall work with a logic inspired by Church's Simple Theory

  • pi calculus

  • logic

  • free variable

  • empty

  • differences between

  • signature

  • open bisimulation

  • fo?∆?

  • free names


Sujets

Informations

Publié par
Nombre de lectures 9
Langue English

Exrait

FGUC2004PreliminaryVersionAProofSearchSpecificationoftheπ-CalculusAlwenTiu1,3INRIA-FutursandE´colepolytechniqueDaleMiller2INRIA-FutursandE´colepolytechniqueAbstractWepresentameta-logicthatcontainsanewquantifierr(forencoding“genericjudgments”)andinferencerulesforreasoningwithinfixedpointsofagivenspeci-fication.Wethenspecifytheoperationalsemanticsandbisimulationrelationsforthefiniteπ-calculuswithinthismeta-logic.Sincewerestricttothenitecase,theabilityofthemeta-logictoreasonwithinfixedpointsbecomesapowerfulandcompletetoolsincesimpleproofsearchcancomputethisonefixedpoint.Therquantifierhelpswiththedelicateissuessurroundingthescopeofvariableswithinπ-calculusexpressionsandtheirexecutions(proofs).Weshallillustrateseveralmeritsofthelogicalspecificationswewrite:theyarenaturalanddeclarative;theycontainnosideconditionsconcerningnamesofvariableswhilemaintainingacompletelyformaltreatmentofsuchvariables;differencesbetweenlateandopenbisimulationrelationsareeasytoseedeclaratively;andproofsearchinvolvingtheapplicationofinferencerules,unification,andbacktrackingcanprovidecompleteproofsystemsforbothone-steptransitionsandforbisimulation.Keywords:π-calculus,names,meta-logic,proofsearch,bisimulation.1IntroductionInordertotreatabstractionswithinexpressionsandcomputationdeclara-tively,weshallworkwithinameta-logicwhichcontainsawellunderstoodnotionofabstraction:inparticular,weshallworkwithalogicinspiredbyChurch’sSimpleTheoryofTypes[4],wheretermsareactuallysimplytyped1Email:tiu@lix.polytechnique.fr2Email:dale.miller@inria.fr3ThisworkwaspartlydonewhentheauthorwasastudentatPennsylvaniaStateUniver-.ytisThisisapreliminaryversion.ThefinalversionwillbepublishedinElectronicNotesinTheoreticalComputerScienceURL:www.elsevier.nl/locate/entcs
TiuandMillerλ-terms.Justasitiscommontouselogic-levelapplicationtorepresentobject-levelapplication(forexample,theencodingofP+Qisviathemeta-levelapplicationoftheencodingforplustotheencodingofitstwoarguments),weshalluselogic-levelabstractions(viaλ-abstractions)toencodeobject-levelabstractions.Theλ-termsinoursettingarethussimplytypedandsatisfytheusualrulesforα,β,andη-conversion.Thisstyleofsyntacticencodinghasbeencalledλ-treesyntax[24].Thetermhigher-orderabstractsyntax[34]wasoriginallyappliedtothiskindofencoding,butinmorerecentyears,HOAShascometoencompasstheuseofarbitraryhigher-orderfunctionstoencodeabstractionsinsyntax.Whatevertermonewishestousetoclassifyourapproachhere,itisimportanttounderstandthatλ-abstractionsareonlyintendedtoformabstractionsoversyntaxandtheirfunctionalinterpretationislimitedtoprovidingobject-levelsubstitutionviaβ-reduction.Wemakeuseofther-quantifier,firstintroducedinthelogicFOλΔr[26],tohelpencodethenotionof“genericjudgment”thatoccurscommonlywhenreasoningwithλ-treesyntax.Therquantifierisusedtointroducenewelementsintoatypewithinagivenscope.Inparticular,areadingofthetruthconditionforrxγ.Bxissomethinglike:ifgivenanewelement,sayc,oftypeγ,thencheckthetruthofBc.Noticethatthisishypotheticalreasoningaboutthedatatypeγanditdoesnotrequireknowingwhetherornotthistypeactuallycontainsanymembers.Thisis,ofcourse,rathercentraltothenotionofgeneric:somethingholdsgenericallyusuallymeansthatitholdsforcertain“internal”reasons(thestructureofanargument,forexample)andnotforsomeaccidentconcerningmembersofthedomain.Thisisquitedifferentfromdeterminingthetruthofxγ.Bx:checkthatBtistrueforalltinthetypeγ.Ifthetypeisempty,thisconditionisvacuouslytrueandifthetypeisinfinite,wehaveaninfinitenumberofcheckstomakeinprinciple.Itisusefultoprovidehereahigh-levelcomparisonbetweenther-quantifierandthe“new”quantifierofGabbayandPitts[10].Intheirsettheoryfoun-dations,adomaincontaininganinfinitenumberofnamesisassumedgiven.Todealwithnotionsoffreshness,renamingofboundvariables,substitution,etc,theyprovideaseriesofprimitivesbetweennamesandtermsthatcanbeusedtoguaranteethatanamedoesnotoccurwithinaterm,thatonenamecanbeswappedforanother,etc.Basedontheseconcepts,theycandefineanewquantifierthatguaranteestheselectionofa“fresh”nameforsomespecificcontext.Inourapproachhere,thereisnoparticularclassofnames:therquantifierwillworkatanytype.(Later,whenwediscusstheπ-calculusexplicitly,weshallassumeatypefornamessincethisisrequiredbythisparticularapplication.)Also,heretypesdonotneedtobeinfiniteorevennon-empty.Instead,themeaningofrxγ.Bxisoneofexplicitlyintroducinganewobjectoftypeγwithinacertainscope.Thus,theGabbay-Pittsapproachassumesthatthetypeofnamesisfixedandclosed,whilethetypeusedwithrisopen,inthesensethatnewmembersofthattypecanbeconstructedbythemeta-logicforusewithinar-boundscope.Morespecifically,thesetof2
  • Accueil Accueil
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • BD BD
  • Documents Documents