18 Pages
English

The pi calculus as a theory in linear logic: Preliminary results

Gain access to the library to view online
Learn more

Description

Niveau: Supérieur, Doctorat, Bac+8
The pi-calculus as a theory in linear logic: Preliminary results ? Dale Miller Computer Science Department University of Pennsylvania Philadelphia, PA 19104-6389 USA October 29, 1992 Abstract The agent expressions of the pi-calculus can be translated into a theory of linear logic in such a way that the reflective and transitive closure of pi-calculus (unlabeled) reduction is identified with “entailed-by”. Under this translation, parallel composition is mapped to the multiplicative disjunct (“par”) and restriction is mapped to universal quantification. Prefixing, non-deterministic choice (+), replication (!), and the match guard are all represented using non-logical constants, which are specified using a simple form of axiom, called here a process clause. These process clauses resemble Horn clauses except that they may have multiple conclu- sions; that is, their heads may be the par of atomic formulas. Such multiple conclusion clauses are used to axiomatize communications among agents. Given this translation, it is nature to ask to what extent proof theory can be used to understand the meta-theory of the pi-calculus. We present some preliminary results along this line for pi0, the “propositional” fragment of the pi-calculus, which lacks restriction and value passing (pi0 is a subset of CCS).

  • pi calculus

  • conclusion sequents

  • single-conclusion sequent

  • into

  • differences between

  • right-introduction rules can

  • logic programming

  • such

  • sequent calculus


Subjects

Informations

Published by
Reads 15
Language English
Theπ-calculusasatheoryinlinearlogic:PreliminaryresultsDaleMillerComputerScienceDepartmentUniversityofPennsylvaniaPhiladelphia,PA19104-6389USAdale@cis.upenn.eduOctober29,1992AbstractTheagentexpressionsoftheπ-calculuscanbetranslatedintoatheoryoflinearlogicinsuchawaythatthereflectiveandtransitiveclosureofπ-calculus(unlabeled)reductionisidentifiedwith“entailed-by”.Underthistranslation,parallelcompositionismappedtothemultiplicativedisjunct(“par”)andrestrictionismappedtouniversalquantification.Prefixing,non-deterministicchoice(+),replication(!),andthematchguardareallrepresentedusingnon-logicalconstants,whicharespecifiedusingasimpleformofaxiom,calledhereaprocessclause.TheseprocessclausesresembleHornclausesexceptthattheymayhavemultipleconclu-sions;thatis,theirheadsmaybetheparofatomicformulas.Suchmultipleconclusionclausesareusedtoaxiomatizecommunicationsamongagents.Giventhistranslation,itisnaturetoasktowhatextentprooftheorycanbeusedtounderstandthemeta-theoryoftheπ-calculus.Wepresentsomepreliminaryresultsalongthislineforπ0,the“propositional”fragmentoftheπ-calculus,whichlacksrestrictionandvaluepassing(π0isasubsetofCCS).Usingideasfromproof-theory,weintroduceco-agentsandshowthattheycanspecifysometestingequivalencesforπ0.Ifnegation-as-failure-to-proveispermittedasaco-agentcombinator,thentestingequiv-alencebasedonco-agentsyieldsobservationalequivalenceforπ0.Thislatterresultfollowsfromobservingthatco-agentsdirectlyrepresentformulasintheHennessy-Milnermodallogic.1IntroductionInthispaperweaddressthequestion“Canweviewagivenprocesscalculusasalogic?”Thisisdifferent(althoughcertainlyrelated)tothequestion“Canlogicbeusedtocharacterizeagivenprocesscalculus?”Suchaquestionwouldviewlogicasanauxiliarylanguagetothatoftheprocesscalculus:forexample,theHennessy-MilnerlogichassucharelationshiptoCCS.Ourapproachherewillbetouselogicmoreimmediatelybytryingtomatchcombinatorsofthegivenprocesscalculusdirectlytologicalconnectivesand,ifacombinatorfailstomatch,tryingtoaxiomatizeditdirectlyanduniformlyinlogic.Forourpurposeshere,weshallconsideraformalsystemtobealogicifithasasequentcalculuspresentationthatadmitsacut-eliminationtheorem.Ofcourse,thisdefinitionoflogicisnotformalunlessformaldefinitionsofsequentcalculiandcut-eliminationareprovided.WeshallnotattemptThispaperappearsintheProceedingsofthe1992WorkshoponExtensionstoLogicProgramming,editedbyE.LammaandP.Mello,LectureNotesinComputerScience,Springer-Verlag.1