Pi-calculus
|
|
In theoretical computer science, the π-calculus is a notation originally developed by Robin Milner, Joachim Parrow and David Walker to model concurrency (just as the λ-calculus is a simple model of sequential programming languages).
| Contents |
Informal definition
The π-calculus is a process calculus, a mathematical formalism for describing and analyzing properties of concurrent computation. In fact, the π-calculus, just as the λ-calculus, is so minimal that it does not contain primitives such as arithmetics (no numbers, no operations), booleans, usual flow control statements (no if... then...else, no while...), data structures, variables or functions.
Central to the π-calculus is the notion of name. Names play the double part of communication channels and variables.
The process constructs available in the calculus are the following:
- concurrency, written <math>P \mid Q<math>, where <math>P<math> and <math>Q<math> are two processes or threads executed concurrently
- communication, where
- input prefixing <math>c(x).P<math> is a process waiting for a message to be sent on a communication channel named <math>c<math> before proceeding as <math>P<math>, binding the name received to the name <math>x<math>. Typically, this models either a process expecting a communication from the network or a label
cusable only once by agoto coperation. - output prefixing <math>c \langle y \rangle.P<math> describes that the name <math>y<math> is emitted on channel <math>c<math> before proceeding as <math>P<math>. Typically, this models either sending a message on the network or a
goto coperation.
- input prefixing <math>c(x).P<math> is a process waiting for a message to be sent on a communication channel named <math>c<math> before proceeding as <math>P<math>, binding the name received to the name <math>x<math>. Typically, this models either a process expecting a communication from the network or a label
- replication, written <math>! P<math>, which may be seen as a process which can always create a new copy of <math>P<math>. Typically, this models either a network service or a label
cwaiting for any number ofgoto coperations. - creation of a new name, written <math>(\nu x)P<math>, which may be seen as a process allocating a new constant <math>x<math> within <math>P<math>. As opposed to functional programming's
let x=... in...operation, the constants of π-calculus are defined by their name only and are always communication channels. - the nil process, written 0, is a process whose execution is complete and has stopped.
(note that the formal definition underneath is more complete than this informal outline)
Although this minimality prevents us from writing actual programs in the naked π-calculus, it is relatively easy to extend the calculus with using either macros or ad-hoc mechanisms. In particular, it is easy to define first-order functions, and not much harder to define recursivity, lists, integers, and forall control statements.
The applied π-calculus due to Abadi and Fournet tries to put such ad-hoc extensions on a formal footing by extending th π-calculus with arbitrary signatures.
The minimality serves several purposes:
- the number of definition is small (compare this page to the hundreds of pages of the Java Language specifications)
- the concepts are kept orthogonal, which means that every operation unambiguously only has one implementation
- it is possible to extend the calculus without breaking it, as there are few aspects to check. For instance, several simple extensions of the π-calculus have been proposed which take into account distribution or public-key cryptography.
- writing an unoptimised virtual machine for the language and many of its extensions is relatively easy, as it will have extremely few opcodes (i.e. basic instructions)
- isolating fragments of the language which respect some given properties is relatively simple. In particular, many type systems have been developed to guarantee statically (i.e. at compile time) that a process respects primitive types, that some information will be kept secret, that some information will be used only once, that a process will not use unavailable resources (such as memory), that some network protocol is respected...
Formal definition
Syntax
Let Χ = {x, y, z, ...} be a set of objects called names which can be seen as names of channels of communication. The processes of π-calculus are built from names by the syntax
which have the following meaning:
- x(y).P, which binds the name y in P, means "input some name – call it y – on the channel named x, and use it in P";
- x<y>.P means "output the name y on the channel named x, and then do P";
- P|Q means that the processes P and Q are concurrently active (this is the construction which really gives the power to model concurrency to the π-calculus);
- νx.P, which binds the name x in P, means that the usage of x is "restricted" to the process P;
- !P means that there are infinitely many processes P concurrently active (this construction might not be present in the definition of the π-calculus but it is needed for the π-calculus to be turing complete), formally !P → P | !P;
- 0 is the null process which does nothing. Its purpose is to serve as basis upon which one builds other processes.
Reduction rules
The main reduction rule which captures the ability of processes to communicate through channels is the following:
where Q[y/z] is the process Q where the name y has been substituted to the name z. There are 3 more rules, one of which is
It says that parallel composition does not inhibit computation. Similarly, the rule
ensures that computation can proceed underneath a restriction. Finally we have the structural rule
Here ≡ is the structural congruence, which says that concurrency is commutative and associative. It is the least congruence such that
- P|Q ≡ Q|P, P|(Q|R) ≡ (P|Q)|R and P|0 ≡ P.
- νx.νy.P ≡ νy.νx.P.
- νx.(P|Q) ≡ νx.P|Q, provided x is not a free name in P.
The concept of free names is of fundamental importance in Pi-Calculi. It can be defined inductively as follows.
- The 0 process has no free names.
- The process x<y>.P has x and y and all of P's free names as its own free names.
- The free names of x(v).P are all of P's free names except for v. In addition x is a free name of this process.
- The free names of P|Q are those of P together with those of Q.
- The free names of νx.P are those of P, except for x.
- The free names of !P are those of P.
Variants
A sum (P + Q) can be added to the syntax. It behaves like a nondeterministic choice between P and Q.
A test for name equality (if x=y then P else Q) can be added to the syntax. Similarly, one may add name inequality.
The asynchronous π-calculus allows only x<y>.0, not x<y>.P.
The polyadic π-calculus allows communicating more than one name in a single action: x<y1,y2,...,yn>.P and x(y1,y2,...,yn).P. It can be simulated in the monadic calculus by passing the name of a private channel through which the multiple arguments are then passed in sequence:
Replication !P is not usually needed for arbitrary processes P. One can replace !P with replicated or lazy input !x(y).P without loss of expressive power. The corresponding reduction rule is
Processes like !x(y).P can be understood as servers, waiting on channel x to be invoked by clients. Invocation of a server spawns a new copy of the process P[a/y], where a is the name passed by the client to the server, during the latter's invocation.
A higher order π-calculus can be defined where not names but processes are sent through channels. The key reduction rule for the higher order case is
In this case, the process x<R>.P sends the process R to x(v).Q. Sangiorgi established the surprising result that the ability to pass processes does not increase the expressivity of the π-calculus: passing a process P can be simulated by just passing a name that points to P instead.
Properties
Turing completeness
The π-calculus is a universal model of computation. This was first observed by Milner in his paper "Functions as Processes" ( Mathematical Structures in Computer Science, Vol. 2, pp. 119-141, 1992), in which he presents two encodings of the lambda-calculus in the π-calculus. One encoding simulates the call-by-value reduction strategy, the other encoding simulates the lazy (call-by-name) strategy.
The features of the π-calculus that make these encodings possible are name-passing and replication (or, equivalently, recursively defined agents). In the absence of replication/recursion, the π-calculus ceases to be Turing-powerful. This can be seen by the fact the bisimulation equivalence becomes decidable for the recursion-free calculus and even for the finite-control π-calculus where the number of parallel components in any process is bounded by a constant (Mads Dam: On the Decidability of Process Equivalences for the pi-Calculus. Theoretical Computer Science 183, 1997, pp. 215-228.)
Bisimulations in the π-calculus
See also article: Bisimulation
There are (at least) three different ways of defining bisimulation equivalence (aka bisimilarity) in the π-calculus: Early, late and open bisimilarity. This stems from the fact that the π-calculus is a value-passing process calculus.
Early and late bisimilarity
Early and late bisimilarity were both discovered by Milner, Parrow and Walker in their original paper on the π-calculus (R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, Information and Computation, 100:1--40, 1992.)
A binary relation <math>R<math> over processes is an early bisimulation if for every pair of elements <math>(p, q) \in R<math>, whenever
- <math>
\begin{matrix}
& a(x) & \\
p & \rightarrow & p' \\ \end{matrix}
<math>
then for every name <math>y<math> there exists some <math>q' \in R<math> such that
- <math>
\begin{matrix}
& a(x) & \\
q & \rightarrow & q' \\ \end{matrix}
<math>
and <math>(p'[y/x],q'[y/x]) \in R<math> , and for any other kind of action <math>\alpha<math>:
<math> \begin{matrix}
& \alpha & \\
p & \rightarrow & p' \\ \end{matrix}
<math>
implies that there exists some <math>q' \in R<math> such that
- <math>
\begin{matrix}
& \alpha & \\
q & \rightarrow & q' \\ \end{matrix}
<math>
and <math>(p',q') \in R<math> Processes <math>p<math> and <math>q<math> are said to be early bisimilar, written <math>p \sim_e q<math> if the pair <math>(p,q) \in R<math> for some early bisimulation <math>R<math>. <math>\sim_e<math>
In late bisimilarity, the transition match must be independent of the name being transmitted. A binary relation <math>R<math> over processes is a late bisimulation if for every pair of elements <math>(p, q) \in R<math>, whenever
<math> \begin{matrix}
& a(x) & \\
p & \rightarrow & p' \\ \end{matrix}
<math>
then for some <math>q' \in R<math> it holds that
- <math>
\begin{matrix}
& a(x) & \\
q & \rightarrow & q' \\ \end{matrix}
<math>
and <math>(p'[y/x],q'[y/x]) \in R<math> for every name y, and for any other kind of action <math>\alpha<math>:
<math> \begin{matrix}
& \alpha & \\
p & \rightarrow & p' \\ \end{matrix}
<math>
implies that there exists some <math>q' \in R<math> such that
- <math>
\begin{matrix}
& \alpha & \\
q & \rightarrow & q' \\ \end{matrix}
<math>
and <math>(p',q') \in R<math>
Processes <math>p<math> and <math>q<math> are said to be late bisimilar, written <math>p \sim_l q<math> if the pair <math>(p,q) \in R<math> for some late bisimulation <math>R<math>. <math>\sim_e<math>
Both <math>\sim_e<math> and <math>\sim_l<math> suffer from the problem that they are not congruence relations in the sense that they are not preserved by all process constructs. More precisely, there exist processes <math>p<math> and <math>q<math> such that <math>p \sim_e q<math> but <math>a(x)p \not \sim_e a(x).q<math>.
Open bisimilarity
Fortunately, a third definition is possible, which avoids this problem, namely that of open bisimilarity, due to Sangiorgi (D. Sangiorgi. A theory of bisimulation for the π-calculus. Acta Informatica, Volume 33 , Issue 1, 1996.)
A binary relation <math>R<math> over processes is an open bisimulation if for every pair of elements <math>(p, q) \in R<math> and for every name substitution <math>\sigma<math> and every action <math>\alpha<math>, whenever
- <math>
\begin{matrix}
& \alpha & \\
p\sigma & \rightarrow & p' \\ \end{matrix}
<math>
then there exists some <math>q' \in R<math> such that
- <math>
\begin{matrix}
& \alpha & \\
q\sigma & \rightarrow & q' \\ \end{matrix}
<math>
and <math>(p',q') \in R<math>
Processes <math>p<math> and <math>q<math> are said to be open bisimilar, written <math>p \sim_o q<math> if the pair <math>(p,q) \in R<math> for some early bisimulation <math>R<math>. <math>\sim_e<math>
Early, late and open bisimilarity are in fact all distinct. The containments are proper, so <math>\sim_o \subsetneq \sim_l \subsetneq \sim_e<math>.
In certain subcalculi such as the asynchronous pi-calculus, late, early and open bisimilarity are known to coincide. However, in this setting a more appropriate notion is that of asynchronous bisimilarity.
Implementations
The following programming languages are implementations either of the π-calculus or of its variants:
- Acute
- BPML (Business Process Modeling Language)
- JoCaml
- The Kell machine
- Nomadic Pict
- Polyphonic C#
See also
- Calculus of Communicating Systems
- Communicating sequential processes
- Calculus of Broadcasting Systems
- Ambient calculus
- Join calculus
- Actor model
References
- Robin Milner: Communicating and Mobile Systems: the Pi-Calculus, Springer Verlag, ISBN 0521658691
- Robin Milner: The Polyadic π-Calculus: A Tutorial (http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-180/ECS-LFCS-91-180.ps). Logic and Algebra of Specification, 1993.
- Davide Sangiorgi and David Walker: The Pi-calculus: A Theory of Mobile Processes, Cambridge University Press, ISBN 0521781779
External links
- Citations from CiteSeer (http://citeseer.org/cs?q=Communicating+and+Pi-Calculus)
- PiCalculus (http://c2.com/cgi/wiki?PiCalculus) on the C2 wiki
- Calculi for Mobile Processes (http://move.to/mobility)