Pi calculus

The pi calculus, also written as π calculus, is a formal rewriting calculus invented by Robin Milner in 1992. It is based on channels which can be used to transmit data, and processes which determine the behavior of those channels. It is similar to lambda calculus in that there is only one first-class datatype (the process), but pi calculus also allows concurrent execution, stateful functions, and a richer structure for programs.
== Introduction ==
In the basic form of the calculus, processes are built recursively from the following commands:
Process 	Description	Read as 	Meaning
x(y).P 	Input 	 	Read from the channel x, then execute P with the result named y
x<y>.P	Output 	 	Write y to the channel x, then execute P
(v x).P 	Creation 	new x in P	Execute P with a new channel named x
Q 	Concurrency	Par 	Execute P and Q concurrently
!P 	Replication	Bang 	Execute P an infinite number of times concurrently
0 	Nil 	 	Does nothing
Commands in a process are generally separated with ., and processes are terminated with a 0 (although this is often omitted to improve readability).
Reads implement pattern-matching, meaning that the rest of the process will not execute if the current value taken from the channel does not satisfy the condition. A name acts like a wildcard, and any current value in the channel will match a name. Pattern-matches towards a literal will only be satisfied if the current value in the channel is exactly the literal specified in the read.
Importantly, both read and writes will block the current process from continuing further until they complete. In this way, communication can be used to block processes from running until particular conditions are met. Replication is often restricted to just before an input operation, as in !x(y) (termed a "replicated read"); this does not weaken the calculus.
=== Providers ===
Unlike lambda calculus, which is entirely based around functions, pi calculus does not have any primitive notion of a function. Despite this, it is possible to make a "provider", which behaves similarly to a function. Providers are processes which constantly read from a particular channel and perform some operation whenever data is transmitted. A provider is typically written like this:
 !provider(a).a(input1).a(input2). P .a<output1>.a<output2>.0
To later invoke this provider:
 (v a).provider<a>.a<input1>.a<input2>.a(output1).a(output2)
Since the provider can be invoked multiple times concurrently, each invocation uses a separate temporary communication channel a instead of transmitting the inputs and outputs directly.
== Structural Congruences ==
* P|0 = P - Executing parallel with the inert process is the same as executing without the process.
* P|Q = Q|P - Parallel composition is commutative.
* (P|Q)|R = P|(Q|R) - Parallel composition is associative.
* !P = !P|P - Infinite P in parallel is the same as adding another P in parallel.
* (v a)(v b)P = (v b)(v a)P - The definition of new channels is associative.
* (v c)(P|Q) = (v c)P|Q, if c also appears in Q
* c<x>.P|c(y).Q = P|Q, in which all y in Q is replaced with x
* (v x)0 = 0
== Examples ==
=== Cat program ===
This process endlessly copies anything read from i, and writes it to o.
!i(x).o<x>.0
Note that the above program does not guarantee that the writes to o happen in the same order as the reads to i. This can be fixed by adding some extra blocking mechanisms:
(v loop).
( !loop(y).i(x).o<x>.loop<loop>.0
| loop<loop> )
This version will block writes to i if o is not ready to receive output.
=== Thread Join ===
This process will only execute S once P, Q, and R have finished.
(v x).
( P.x<x>.0
| Q.x<x>.0
| R.x<x>.0
| x(y).x(y).x(y).S )
=== Add one provider ===
!incr(a,x).a<x+1>
== Extensions ==
The pi calculus is sometimes extended for notational convenience, or to make it easier to express certain concepts.
=== Polyadic communication ===
One common extension permits read and write operations to accept more than one argument. An example of a polyadic write operation would be f<x,y,z>, which can be interpreted as shorthand for (v a).f<a>.a<x>.a<y>.a<z>. Likewise, a polyadic read operation f(x,y,z) could be interpreted as f(a).a(x).a(y).a(z).
=== Nondeterministic choice operator ===
The nondeterministic choice operator P+Q will execute one of either P or Q, but it is unknown which. This could be modeled as (v a)(a(x).P|a(x).Q|a<a>.0).
=== Match / Mismatch ===
The operator if x=y then P behaves like P if x and y are the same. Parrow, J. .
The operator if x≠y then P behaves like P if x and y are not the same.
In some variants, if cond then P can also be written as [cond].P.
It is possible to simulate if/else via if x=y then P + if x≠y then Q. This can also be written as if x then P else Q.
If the equality comparison is made between channel names, then it is possible to simulate the comparison without match operators. For example, [x=y].Q + [x=z].R can be modeled as x<0> | (y(a).Q + z(a).R). This works because if a value is sent through the channel x, and the channel y recieves the message, then the channels x and y are the same channels; and vice versa.
=== Cryptographic primitives ===
As the pi calculus is very good at modeling communication systems, it has been extended to include primitives which cryptographically encrypt and decrypt data streams Blanchet, Bruno. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif..
=== Arithmetic and common data structures ===
Common data structures is a frequent extension, along with their related operations. This may include, but is not limited to, numbers (and arithmetic), lists(maps, filters), sets, maps, etc.
== Encoding of Lambda Calculus ==
Lambda calculus can be readily encoded using providers. As lambda calculus is functional in nature while pi calculus is procedural in nature, the lambda term must be used as a channel rather than a process. Let [f] denote a channel representing the lambda term f, and make these substitutions repeatedly:
* c<[λx.f]>.P ⇒ (v l)(!l(a).a(x).a<[f]>|c<l>.P)
* [λx.f]<c>.P ⇒ (v l)(!l(a).a(x).a<[f]>|l<c>.P)
* c<[f(x)]>.P ⇒ (v a).[f]<a>.a<[x]>.a(r).c<r>.P
* [f(x)]<c>.P ⇒ (v a).[f]<a>.a<[x]>.a(r).r<c>.P
* c<[x]>.P ⇒ c<x>.P (where x is atomic)
* [x]<c>.P ⇒ x<c>.P (where x is atomic)
Some care must be taken to ensure that the temporary variables l, a, r don't clash with any other variables created during the expansion, particularly in [f(x)] terms.
== See also ==
* Lambda calculus
* Binary Pi-calculus
== External resources ==
* Pi calculus at Wikipedia
* FAQ on Pi-Calculus
== References ==
Category:Before 1993
Category:Implemented
Category:Computational models
Category:Concepts
Category:Turing complete
Category:Concurrent programming
Category: Languages