Home > 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).1 Definition
1.1 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<y>.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, 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.
1.2 Reduction rules
The main reduction rule which captures the ability of processes to communicate through channels is the following:
x<y>.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 ≡ 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 inductively as follows.
- The 0 process has no free names.
- The process x<y>.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 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.
1.3 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:
x<y1,y2,...,yn>.P denotes νw.x<w>.w<y1>.w<y2>...w<yn>.P
x(y1,y2,...,yn).P denotes x(w).w(y1).w(y2)...w(yn).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.
