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

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

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

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
18 pages
English
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

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


Sujets

Informations

Publié par
Nombre de lectures 15
Langue English

Extrait

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
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • Podcasts Podcasts
  • BD BD
  • Documents Documents