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

Informal definition

Although from the point of view of the theoretists, this is not exactly true, the π-calculus can be seen as a minimal programming language built to capture all interesting behaviors of concurrent programs. 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.

The only primitives available in the calculus are the following:

• concurrency, written P|Q, where P and Q are two processes or threads executed concurrently
• communication, written c(x).P|c<y>, where
  • c(x).P is a process waiting for a message to be sent on a communication channel named c before proceeding as P, using that value x. Typically, this models either a process expecting a communication from the network or a label c usable only once by a goto c operation.
  • c<y> is the emission of value y on a communication on channel c. Typically, this models either sending a message on the network or a goto c operation.
• input replication, written !c(x).P, which may be seen as a process waiting for any number of communications on c. After each communication of value, a new copy of process P is spawned, using that value x. Typically, this models either a network service or a label c waiting for any number of goto c operations. Often, P is actually built so as to use a return channel, hence acting as a function.
• creation of a new name, written νx.P, which may be seen as a process allocating a new constant x for P. 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 using either macros, Bisimulations (see underneath) or ad-hoc mechanisms such as the signatures formalized in the Applied π-calculus. In particular, it is trivial to define first-order functions, and not much harder to define recursivity, lists, integers, and forall control statements.

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) ≡ 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 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<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:

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

Bisimulations

See article: Bisimulation

Implementations

The following programming languages are implementations either of the π-calculus or of its variants:

• JoCaml
• Acute
• Nomadic Pict
• The Kell machine
• Polyphonic C#

See also

• Calculus of Communicating Systems
• Communicating sequential processes
• Calculus of Broadcasting Systems
• Ambient calculus
• Join calculus

References

• Robin Milner: Communicating and Mobile Systems: the Pi-Calculus, Springer Verlag, ISBN 0521658691

• Robin Milner: The Polyadic π-Calculus: A Tutorial. 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
• PiCalculus on the C2 wiki
• Calculi for Mobile Processes