Pi calculus

pi calculus

Designed by	Robin Milner
Appeared in	1992
Computational class	Turing-complete
Reference implementation	Unimplemented
File extension(s)	{{{files}}}

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

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 .

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