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

1 Definition 1.1 Syntax 1.2 Reduction rules 1.3 Variants 2 Properties 2.1 Turing completeness 2.2 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

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