FGUC Preliminary Version

Dale Miller

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

• Miller
• École polytechnique
• Pi calculus
• Free variables and bound variables
• Signature

Informations

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

Extrait

FGUC2004PreliminaryVersion AProofSearchSpecificationoftheπ-Calculus AlwenTiu 1,3 INRIA-FutursandE ´ colepolytechnique DaleMiller 2 INRIA-FutursandE ´ colepolytechnique Abstract Wepresentameta-logicthatcontainsanewquantifierr(forencoding“generic judgments”)andinferencerulesforreasoningwithinfixedpointsofagivenspeci- fication.Wethenspecifytheoperationalsemanticsandbisimulationrelationsfor thefiniteπ-calculuswithinthismeta-logic.Sincewerestricttothefinitecase, theabilityofthemeta-logictoreasonwithinfixedpointsbecomesapowerfuland completetoolsincesimpleproofsearchcancomputethisonefixedpoint.Ther quantifierhelpswiththedelicateissuessurroundingthescopeofvariableswithinπ- calculusexpressionsandtheirexecutions(proofs).Weshallillustrateseveralmerits ofthelogicalspecificationswewrite:theyarenaturalanddeclarative;theycontain nosideconditionsconcerningnamesofvariableswhilemaintainingacompletely formaltreatmentofsuchvariables;differencesbetweenlateandopenbisimulation relationsareeasytoseedeclaratively;andproofsearchinvolvingtheapplicationof inferencerules,unification,andbacktrackingcanprovidecompleteproofsystems forbothone-steptransitionsandforbisimulation. Keywords:π-calculus,names,meta-logic,proofsearch, bisimulation. 1Introduction Inordertotreatabstractionswithinexpressionsandcomputationdeclara- tively,weshallworkwithinameta-logicwhichcontainsawellunderstood notionofabstraction:inparticular,weshallworkwithalogicinspiredby Church’sSimpleTheoryofTypes[4],wheretermsareactuallysimplytyped 1 Email:[e-mail] 2 Email:[e-mail] 3 ThisworkwaspartlydonewhentheauthorwasastudentatPennsylvaniaStateUniver- .ytis Thisisapreliminaryversion.Thefinalversionwillbepublishedin ElectronicNotesinTheoreticalComputerScience URL:www.elsevier.nl/locate/entcs

TiuandMiller λ-terms.Justasitiscommontouselogic-levelapplicationtorepresentobject- levelapplication(forexample,theencodingofP+Qisviathemeta-level applicationoftheencodingforplustotheencodingofitstwoarguments),we shalluselogic-levelabstractions(viaλ-abstractions)toencodeobject-level abstractions.Theλ-termsinoursettingarethussimplytypedandsatisfy theusualrulesforα,β,andη-conversion.Thisstyleofsyntacticencoding hasbeencalledλ-treesyntax[24].Thetermhigher-orderabstractsyntax[34] wasoriginallyappliedtothiskindofencoding,butinmorerecentyears, HOAShascometoencompasstheuseofarbitraryhigher-orderfunctionsto encodeabstractionsinsyntax.Whatevertermonewishestousetoclassify ourapproachhere,itisimportanttounderstandthatλ-abstractionsareonly intendedtoformabstractionsoversyntaxandtheirfunctionalinterpretation islimitedtoprovidingobject-levelsubstitutionviaβ-reduction. Wemakeuseofther-quantifier,firstintroducedinthelogicFOλ Δr [26],tohelpencodethenotionof“genericjudgment”thatoccurscommonly whenreasoningwithλ-treesyntax.Therquantifierisusedtointroduce newelementsintoatypewithinagivenscope.Inparticular,areadingofthe truthconditionforrx γ .Bxissomethinglike:ifgivenanewelement,sayc,of typeγ,thencheckthetruthofBc.Noticethatthisishypotheticalreasoning aboutthedatatypeγanditdoesnotrequireknowingwhetherornotthis typeactuallycontainsanymembers.Thisis,ofcourse,rathercentraltothe notionofgeneric:somethingholdsgenericallyusuallymeansthatitholdsfor certain“internal”reasons(thestructureofanargument,forexample)andnot forsomeaccidentconcerningmembersofthedomain.Thisisquitedifferent fromdeterminingthetruthof∀x γ .Bx:checkthatBtistrueforalltinthe typeγ.Ifthetypeisempty,thisconditionisvacuouslytrueandifthetype isinfinite,wehaveaninfinitenumberofcheckstomakeinprinciple. Itisusefultoprovidehereahigh-levelcomparisonbetweenther-quantifier andthe“new”quantifierofGabbayandPitts[10].Intheirsettheoryfoun- dations,adomaincontaininganinfinitenumberofnamesisassumedgiven. Todealwithnotionsoffreshness,renamingofboundvariables,substitution, etc,theyprovideaseriesofprimitivesbetweennamesandtermsthatcan beusedtoguaranteethatanamedoesnotoccurwithinaterm,thatone namecanbeswappedforanother,etc.Basedontheseconcepts,theycan defineanewquantifierthatguaranteestheselectionofa“fresh”namefor somespecificcontext.Inourapproachhere,thereisnoparticularclassof names:therquantifierwillworkatanytype.(Later,whenwediscussthe π-calculusexplicitly,weshallassumeatypefornamessincethisisrequiredby thisparticularapplication.)Also,heretypesdonotneedtobeinfiniteoreven non-empty.Instead,themeaningofrx γ .Bxisoneofexplicitlyintroducinga newobjectoftypeγwithinacertainscope.Thus,theGabbay-Pittsapproach assumesthatthetypeofnamesisfixedandclosed,whilethetypeusedwith risopen,inthesensethatnewmembersofthattypecanbeconstructedby themeta-logicforusewithinar-boundscope.Morespecifically,thesetof 2