Pi-calculus

From Free net encyclopedia

(Redirected from Pi-Calculus)

In theoretical computer science, the π-calculus is a notation originally developed by Robin Milner, Joachim Parrow and David Walker as an advance over Calculus of Communicating Systems in order to provide mobility in modeling concurrency. The π-calculus is in the family of process calculi that have been used to model concurrent programming languages just as the λ-calculus has been used to model sequential programming languages.

1 Informal definition
2 Formal definition
3 Properties
- 3.1 Turing completeness
4 Bisimulations in the π-calculus
5 Implementations
6 See also
7 References
8 External links

[edit]

Informal definition

The π-calculus is in the family of process calculi, mathematical formalisms for describing and analyzing properties of concurrent computation. In fact, the π-calculus, like the λ-calculus, is so minimal that it does not contain primitives such as numbers, booleans, data structures, variables, functions, or even the usual flow control statements (such as if... then...else, while...).

Central to the π-calculus is the notion of name. Names play a dual role as 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\left(x\right).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 c usable only once by a goto c operation.
- 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 c operation.
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 c waiting for any number of goto c operations.
creation of a new name, written <math>\left(\nu x\right)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.

A more complete definition is given below.

Although the minimality of the π-calculus prevents us from writing programs in the normal sense, it is easy to extend the calculus. 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 puts various extensions on a formal footing by extending the π-calculus with arbitrary signatures.

The minimality serves several purposes:

the number of definitions 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, etc.

[edit]

Formal definition

[edit]

Syntax

Let Χ 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 (where x and y are any names from Χ)

<math>\begin{matrix} P ::= & x(y).P \\

   | & x \langle y \rangle.P \\
   | & P|P \\
   | & !P \\
   | & (\nu x).P \\
   | & 0

\end{matrix}</math>

the productions of which have the following meanings:

x(y).P means "input some name – call it y – on the channel named x, and bind y to 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 makes it possible to model concurrency in 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.

Names can be bound by the restriction and input prefix constructs. The sets of free and bound names of a process in π–calculus are defined inductively as follows.

The 0 process has no free names and no bound names.

The free names of <math>a\langle x \rangle.P</math> are <math>a</math>, <math>x</math>, and the free names of <math>P</math>. The bound names of <math>a\langle x \rangle.P</math> are the bound names of <math>P</math>.

The free names of <math>a(x).P</math> are <math>a</math> and the free names of <math>P</math>. The bound names of <math>a(x).P</math> are <math>x</math> and the bound names of <math>P</math>.

The free names of P|Q are those of P together with those of Q. The bound names of P|Q are those of P together with those of Q.

The free names of <math>(\nu x).P</math> are those of P, except for x. The bound names of <math>(\nu x).P</math> are <math>x</math> and the bound names of <math>P</math>.

The free names of !P are those of P. The bound names of !P are those of P.

[edit]

Reduction semantics

The pi-calculus can be given a reduction semantics.

The main reduction rule which captures the ability of processes to communicate through channels is the following:

If x<y>.P | x(z).Q, then also P | Q[y/z]

where Q[y/z] denotes the process Q in which the name y has been substituted for the name z.

There are three additional rules:

If <math>P \equiv Q</math> then also <math>P|R \equiv Q|R</math>.

This rule says that parallel composition does not inhibit computation.

If <math>P \equiv Q</math>, then also <math>\nu x.P \equiv \nu x.Q</math>.

This rule ensures that computation can proceed underneath a restriction.

If P ≡ P' and P' → Q' and Q' ≡ Q, then also P → Q.

In this rule, called the structural rule, ≡ denotes 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 Q.

[edit]

Labelled semantics

Alternatively, one may give the pi-calculus a labelled transition semantics (as has been done with the Calculus of Communicating Systems). Transitions in this semantics are of the form:

<math> \begin{matrix}

 & \alpha & \\

p & \rightarrow & p' \\ \end{matrix} </math>

This notation signifies that <math>p</math> after the action <math>\alpha</math> becomes <math>p'</math>. <math>\alpha</math> can be an input action <math>a(x)</math>, an output action <math>a\langle x \rangle</math>, or a tau-action.

[edit]

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<y₁,y₂,...,y_n>.P and x(y₁,y₂,...,y_n).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:

x<y₁,y₂,...,y_n>.P denotes νw.x<w>.w<y₁>.w<y₂>...w<y_n>.P

x(y₁,y₂,...,y_n).P denotes x(w).w(y₁).w(y₂)...w(y_n).P

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

x<y>.P | !x(z).Q → P | !x(z).Q | Q[y/z].

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

x<R>.P | x(v).Q → P | Q[R/v].

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.

[edit]

Properties

[edit]

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.)

[edit]

Bisimulations in the π-calculus

See also article: Bisimulation

The notion of bisimulation equivalence (aka bisimilarity) may be based on either the reduction semantics or on the labelled transition semantics.

There are (at least) three different ways of defining labelled bisimulation equivalence in the π-calculus: Early, late and open bisimilarity. This stems from the fact that the π-calculus is a value-passing process calculus.

[edit]

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>.

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>.

[edit]

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 open bisimulation <math>R</math>. <math>\sim_o</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.

The reader should note that, in the literature, the term open bisimulation usually refers to a more sophisticated notion, where processes and relations are indexed by distinction relations; details are in Sangiorgi's paper cited above.

[edit]

Barbed equivalence

Alternatively, one may define bisimulation equivalence using the reduction semantics. A notion of bisimilarity based solely on the reduction semantics is not particularly interesting. A better notion is that of barbed bisimilarity. Definying a context as a π term with a hole [] then two processes P and Q are barbed congruent if for all context C[] C[P] and C[Q] are observables on the same name a.

[edit]