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