Pi-calculus

In theoretical computer science, the π-calculus is a notation originally developed by Robin Milner, Joachim Parrow and David Walker to model concurrency (like λ-calculus; is a simple model of sequential programming languages).

Table of contents

1 Definition

1.1 Syntax
1.2 Reduction rules
1.3 Variants

2 Properties

2.4 Turing completeness
2.5 Bisimulations

3 See also
4 References
5 External links

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

P :: = x(y).P | x.P | P|Q | νx.P | !P | 0 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";

x.P, which binds the name y in P, means "output the name y on the channel named x";

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 z 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 cannot do anything. 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:

x.P | x(z).Q → P | Q[y/z] 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 If P → Q then also P|E → Q|E. It says that parallel composition does not inhibit computation. Similarly, the rule If P → Q then also (ν x)P → (ν x)Q ensures that computation can proceed underneath a restriction. Finally we have the structural rule If P ≡ P' → Q' ≡ Q, then also P → Q . Here ≡ is the structural congruence, which equates processes that should be regarded as essentially the same. It is the least congruence such that

P | Q ≡ Q|P, P|(Q|R) ≡ (P|Q)|R and P|0 ≡.
(ν x)(ν y)P ≡ (ν y)(ν x)P.
(ν x)(P|Q) ≡ P|(ν x)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 inductivly as follows.

The 0 process has no free names.
The process x.P has x and y and all of Ps free names as its own free names.
The free names of x(v).P are all of Ps free names except for v. In addition x is a free names 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 of Ps, 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 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.0, not x.P.

The polyadic π-calculus allows communicating more than one name in a single action: x.P and x(y1,y2,...).P. It can be simulated in the monadic calculus by passing the name of a private channel though 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

x.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. Invokation 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 invokation.

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.P | x(v).Q → P | Q[R/v].

In this case, the process x.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.

References

Robin Milner: Communicating and Mobile Systems: the Pi-Calculus, Springer Verlag, ISBN 0521658691
Davide Sangiorgi and David Walker: The Pi-calculus: A Theory of Mobile Processes, Cambridge University Press, ISBN 0521781779

External links

Citations from CiteSeer