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 |
|
2 Properties 3 See also 4 References 5 External links |
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
The main reduction rule which captures the ability of processes to communicate through channels is the following:
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
The polyadic π-calculus allows communicating more than one name in a single action: x
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. Invokation 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 invokation.
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
This article is a stub. You can help Wikipedia by expanding it.
Definition
Syntax
Reduction rules
The concept of free names is of fundamental importance in Pi-Calculi.
It can be defined inductivly as follows.Variants
Properties
Turing completeness
Bisimulations
See also
References
External links