Home Home  Article Index Article Index  
GuruPedia  

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

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<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";
  • x<y>.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<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.

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<y>.0, not x<y>.P.

The polyadic π-calculus allows communicating more than one name in a single action: x<y1,y2,...>.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<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.

A higher order π-calculus can be defined where not names but processes are sent through channels.

Properties

Turing completeness

Bisimulations

This article is a stub. You can help Wikipedia by expanding it .


See also

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

Popular Topics

This article is from Wikipedia. All text is available under the terms of the GNU Free Documentation License.  For the live article, click here.

Privacy