π-calculus

Process constructs

Central to the π-calculus is the notion of name. The simplicity of the calculus lies in the dual role that names play as communication channels and variables.

The process constructs available in the calculus are the following^[3] (a precise definition is given in the following section):

• concurrency, written ${\displaystyle P\mid Q}$, where ${\displaystyle P}$ and ${\displaystyle Q}$ are two processes or threads executed concurrently.
• communication, where
  • input prefixing ${\displaystyle c\left(x\right).P}$ is a process waiting for a message that was sent on a communication channel named ${\displaystyle c}$ before proceeding as ${\displaystyle P}$, binding the name received to the name x. Typically, this models either a process expecting a communication from the network or a label c usable only once by a goto c operation.
  • output prefixing ${\displaystyle {\overline {c}}\langle y\rangle .P}$ describes that the name ${\displaystyle y}$ is emitted on channel ${\displaystyle c}$ before proceeding as ${\displaystyle P}$. Typically, this models either sending a message on the network or a goto c operation.
• replication, written ${\displaystyle$ !\,P} , which may be seen as a process which can always create a new copy of ${\displaystyle P}$. Typically, this models either a network service or a label c waiting for any number of goto c operations.
• creation of a new name, written ${\displaystyle \left(\nu x\right)P}$, which may be seen as a process allocating a new constant x within ${\displaystyle P}$. The constants of π-calculus are defined by their names only and are always communication channels. Creation of a new name in a process is also called restriction.
• the nil process, written ${\displaystyle 0}$, is a process whose execution is complete and has stopped.

Although the minimalism of the π-calculus prevents us from writing programs in the normal sense, it is easy to extend the calculus. In particular, it is easy to define both control structures such as recursion, loops and sequential composition and datatypes such as first-order functions, truth values, lists and integers. Moreover, extensions of the π-calculus have been proposed which take into account distribution or public-key cryptography. The applied π-calculus due to Abadi and Fournet put these various extensions on a formal footing by extending the π-calculus with arbitrary datatypes.

A small example

Below is a tiny example of a process which consists of three parallel components. The channel name x is only known by the first two components.

${\displaystyle {\begin{aligned}(\nu x)&\;(\;{\overline {x}}\langle z\rangle .\;0\\&\;|\;x(y).\;{\overline {y}}\langle x\rangle .\;x(y).\;0\;)\\&\;|\;z(v).\;{\overline {v}}\langle v\rangle .0\end{aligned}}}$

The first two components are able to communicate on the channel x, and the name y becomes bound to z. The next step in the process is therefore

${\displaystyle {\begin{aligned}(\nu x)&\;(\;0\\&\;|\;{\overline {z}}\langle x\rangle .\;x(y).\;0\;)\\&\;|\;z(v).\;{\overline {v}}\langle v\rangle .\;0\end{aligned}}}$

Note that the remaining y is not affected because it is defined in an inner scope. The second and third parallel components can now communicate on the channel name z, and the name v becomes bound to x. The next step in the process is now

${\displaystyle {\begin{aligned}(\nu x)&\;(\;0\\&\;|\;x(y).\;0\\&\;|\;{\overline {x}}\langle x\rangle .\;0\;)\end{aligned}}}$

Note that since the local name x has been output, the scope of x is extended to cover the third component as well. Finally, the channel x can be used for sending the name x. After that all concurrently executing processes have stopped

${\displaystyle {\begin{aligned}(\nu x)&\;(\;0\\&\;|\;0\\&\;|\;0\;)\end{aligned}}}$

Syntax

Let Χ be a set of objects called names. The abstract syntax for the π-calculus is built from the following BNF grammar (where x and y are any names from Χ):^[4]

${\displaystyle {\begin{aligned}P,Q::=&\;x(y).P\,\,\,\,\,&{\text{Receive on channel }}x{\text{, bind the result to }}y{\text{, then run }}P\\&\;|\;{\overline {x}}\langle y\rangle .P\,\,\,\,\,&{\text{Send the value }}y{\text{ over channel }}x{\text{, then run }}P\\&\;|\;P|Q\,\,\,\,\,\,\,\,\,&{\text{Run }}P{\text{ and }}Q{\text{ simultaneously}}\\&\;|\;(\nu x)P\,\,\,&{\text{Create a new channel }}x{\text{ and run }}P\\&\;|\;!P\,\,\,&{\text{Repeatedly spawn copies of }}P\\&\;|\;0&{\text{Terminate the process}}\end{aligned}}}$

In the concrete syntax below, the prefixes bind more tightly than the parallel composition (|), and parentheses are used to disambiguate.

Names are bound by the restriction and input prefix constructs. Formally, the set of free names of a process in π–calculus are defined inductively by the table below. The set of bound names of a process are defined as the names of a process that are not in the set of free names.

Construct	Free names
${\displaystyle x(y).P}$	x; free names of P except for y
${\displaystyle {\overline {x}}\langle y\rangle .P}$	x; y; all free names of P
${\displaystyle P|Q}$	All free names of P and Q
${\displaystyle (\nu x)P}$	Free names of P except for x
${\displaystyle !P}$	All free names of P
${\displaystyle 0}$	None

Structural congruence

Central to both the reduction semantics and the labelled transition semantics is the notion of structural congruence. Two processes are structurally congruent, if they are identical up to structure. In particular, parallel composition is commutative and associative.

More precisely, structural congruence is defined as the least equivalence relation preserved by the process constructs and satisfying:

Alpha-conversion:

• ${\displaystyle P\equiv Q}$ if ${\displaystyle Q}$ can be obtained from ${\displaystyle P}$ by renaming one or more bound names in ${\displaystyle P}$.

Axioms for parallel composition:

• ${\displaystyle P|Q\equiv Q|P}$
• ${\displaystyle (P|Q)|R\equiv P|(Q|R)}$
• ${\displaystyle P|0\equiv P}$

Axioms for restriction:

• ${\displaystyle (\nu x)(\nu y)P\equiv (\nu y)(\nu x)P}$
• ${\displaystyle (\nu x)0\equiv 0}$

Axiom for replication:

• ${\displaystyle !P\equiv P|!P}$

Axiom relating restriction and parallel:

• ${\displaystyle (\nu x)(P|Q)\equiv (\nu x)P|Q}$ if x is not a free name of ${\displaystyle Q}$.

This last axiom is known as the "scope extension" axiom. This axiom is central, since it describes how a bound name x may be extruded by an output action, causing the scope of x to be extended. In cases where x is a free name of ${\displaystyle Q}$, alpha-conversion may be used to allow extension to proceed.

Reduction semantics

We write ${\displaystyle P\rightarrow P'}$ if ${\displaystyle P}$ can perform a computation step, following which it is now ${\displaystyle P'}$. This reduction relation ${\displaystyle \rightarrow }$ is defined as the least relation closed under a set of reduction rules.

The main reduction rule which captures the ability of processes to communicate through channels is the following:

• ${\displaystyle {\overline {x}}\langle z\rangle .P|x(y).Q\rightarrow P|Q[z/y]}$

where ${\displaystyle Q[z/y]}$ denotes the process ${\displaystyle Q}$ in which the free name ${\displaystyle z}$ has been substituted for the free occurrences of ${\displaystyle y}$. If a free occurrence of ${\displaystyle y}$ occurs in a location where ${\displaystyle z}$ would not be free, alpha-conversion may be required.

There are three additional rules:

• If ${\displaystyle P\rightarrow Q}$ then also ${\displaystyle P|R\rightarrow Q|R}$.

This rule says that parallel composition does not inhibit computation.

• If ${\displaystyle P\rightarrow Q}$, then also ${\displaystyle (\nu x)P\rightarrow (\nu x)Q}$.

This rule ensures that computation can proceed underneath a restriction.

• If ${\displaystyle P\equiv P'}$ and ${\displaystyle P'\rightarrow Q'}$ and ${\displaystyle Q'\equiv Q}$, then also ${\displaystyle P\rightarrow Q}$.

The latter rule states that processes that are structurally congruent have the same reductions.

The example revisited

Consider again the process

${\displaystyle (\nu x)({\overline {x}}\langle z\rangle .0|x(y).{\overline {y}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0}$

Applying the definition of the reduction semantics, we get the reduction

${\displaystyle (\nu x)({\overline {x}}\langle z\rangle .0|x(y).{\overline {y}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0\rightarrow (\nu x)(0|{\overline {z}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0}$

Note how, applying the reduction substitution axiom, free occurrences of ${\displaystyle y}$ are now labeled as ${\displaystyle z}$.

Next, we get the reduction

${\displaystyle (\nu x)(0|{\overline {z}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0\rightarrow (\nu x)(0|x(y).0|{\overline {x}}\langle x\rangle .0)}$

Note that since the local name x has been output, the scope of x is extended to cover the third component as well. This was captured using the scope extension axiom.

Next, using the reduction substitution axiom, we get

${\displaystyle (\nu x)(0|0|0)}$

Finally, using the axioms for parallel composition and restriction, we get

${\displaystyle 0}$

Labelled semantics

Alternatively, one may give the pi-calculus a labelled transition semantics (as has been done with the Calculus of Communicating Systems).
In this semantics, a transition from a state ${\displaystyle P}$ to some other state ${\displaystyle P'}$ after an action ${\displaystyle \alpha }$ is notated as:

• ${\displaystyle P\,{\xrightarrow {\overset {}{\alpha }}}P'}$

Where states ${\displaystyle P}$ and ${\displaystyle P'}$ represent processes and ${\displaystyle \alpha }$ is either an input action ${\displaystyle a(x)}$, an output action ${\displaystyle {\overline {a}}\langle x\rangle }$, or a silent action τ.^[5]

A standard result about the labelled semantics is that it agrees with the reduction semantics up to structural congruence, in the sense that ${\displaystyle P\rightarrow P'}$ if and only if ${\displaystyle P\,\xrightarrow {\overset {}{\tau }} \equiv P'}$ ^[6]

Turing completeness

The π-calculus is a universal model of computation. This was first observed by Milner in his paper "Functions as Processes",^[10] in which he presents two encodings of the lambda-calculus in the π-calculus. One encoding simulates the eager (call-by-value) evaluation strategy, the other encoding simulates the normal-order (call-by-name) strategy. In both of these, the crucial insight is the modeling of environment bindings – for instance, "x is bound to term ${\textstyle M}$" – as replicating agents that respond to requests for their bindings by sending back a connection to the term ${\displaystyle M}$.

The features of the π-calculus that make these encodings possible are name-passing and replication (or, equivalently, recursively defined agents). In the absence of replication/recursion, the π-calculus ceases to be Turing-complete. This can be seen by the fact that bisimulation equivalence becomes decidable for the recursion-free calculus and even for the finite-control π-calculus where the number of parallel components in any process is bounded by a constant.^[11]

Early and late bisimilarity

Early and late bisimilarity were both formulated by Milner, Parrow and Walker in their original paper on the π-calculus.^[12]

A binary relation ${\displaystyle R}$ over processes is an early bisimulation if for every pair of processes ${\displaystyle (p,q)\in R}$,

• whenever ${\displaystyle p\,{\xrightarrow {a(x)}}\,p'}$ then for every name ${\displaystyle y}$ there exists some ${\displaystyle q'}$ such that ${\displaystyle q\,{\xrightarrow {a(x)}}\,q'}$ and ${\displaystyle (p'[y/x],q'[y/x])\in R}$;
• for any non-input action ${\displaystyle \alpha }$, if ${\displaystyle {p{\xrightarrow {\overset {}{\alpha }}}p'}}$ then there exists some ${\displaystyle q'}$ such that ${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$ and ${\displaystyle (p',q')\in R}$;
• and symmetric requirements with ${\displaystyle p}$ and ${\displaystyle q}$ interchanged.

Processes ${\displaystyle p}$ and ${\displaystyle q}$ are said to be early bisimilar, written ${\displaystyle p\sim _{e}q}$ if the pair ${\displaystyle (p,q)\in R}$ for some early bisimulation ${\displaystyle R}$.

In late bisimilarity, the transition match must be independent of the name being transmitted. A binary relation ${\displaystyle R}$ over processes is a late bisimulation if for every pair of processes ${\displaystyle (p,q)\in R}$,

• whenever ${\displaystyle p{\xrightarrow {a(x)}}p'}$ then for some ${\displaystyle q'}$ it holds that ${\displaystyle q{\xrightarrow {a(x)}}q'}$ and ${\displaystyle (p'[y/x],q'[y/x])\in R}$ for every name y;
• for any non-input action ${\displaystyle \alpha }$, if ${\displaystyle p{\xrightarrow {\overset {}{\alpha }}}p'}$ implies that there exists some ${\displaystyle q'}$ such that ${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$and ${\displaystyle (p',q')\in R}$;
• and symmetric requirements with ${\displaystyle p}$ and ${\displaystyle q}$ interchanged.

Processes ${\displaystyle p}$ and ${\displaystyle q}$ are said to be late bisimilar, written ${\displaystyle p\sim _{l}q}$ if the pair ${\displaystyle (p,q)\in R}$ for some late bisimulation ${\displaystyle R}$.

Both ${\displaystyle \sim _{e}}$ and ${\displaystyle \sim _{l}}$ suffer from the problem that they are not congruence relations in the sense that they are not preserved by all process constructs. More precisely, there exist processes ${\displaystyle p}$ and ${\displaystyle q}$ such that ${\displaystyle p\sim _{e}q}$ but ${\displaystyle a(x).p\not \sim _{e}a(x).q}$. One may remedy this problem by considering the maximal congruence relations included in ${\displaystyle \sim _{e}}$ and ${\displaystyle \sim _{l}}$, known as early congruence and late congruence, respectively.

Open bisimilarity

Fortunately, a third definition is possible, which avoids this problem, namely that of open bisimilarity, due to Sangiorgi.^[13]

A binary relation ${\displaystyle R}$ over processes is an open bisimulation if for every pair of elements ${\displaystyle (p,q)\in R}$ and for every name substitution ${\displaystyle \sigma }$ and every action ${\displaystyle \alpha }$, whenever ${\displaystyle p\sigma {\xrightarrow {\overset {}{\alpha }}}p'}$ then there exists some ${\displaystyle q'}$ such that ${\displaystyle q\sigma {\xrightarrow {\overset {}{\alpha }}}q'}$ and ${\displaystyle (p',q')\in R}$.

Processes ${\displaystyle p}$ and ${\displaystyle q}$ are said to be open bisimilar, written ${\displaystyle p\sim _{o}q}$ if the pair ${\displaystyle (p,q)\in R}$ for some open bisimulation ${\displaystyle R}$.

Barbed equivalence

Alternatively, one may define bisimulation equivalence directly from the reduction semantics. We write ${\displaystyle p\Downarrow a}$ if process ${\displaystyle p}$ immediately allows an input or an output on name ${\displaystyle a}$.

A binary relation ${\displaystyle R}$ over processes is a barbed bisimulation if it is a symmetric relation which satisfies that for every pair of elements ${\displaystyle (p,q)\in R}$ we have that

(1) ${\displaystyle p\Downarrow a}$ if and only if ${\displaystyle q\Downarrow a}$ for every name ${\displaystyle a}$

and

(2) for every reduction ${\displaystyle p\rightarrow p'}$ there exists a reduction ${\displaystyle q\rightarrow q'}$

such that ${\displaystyle (p',q')\in R}$.

We say that ${\displaystyle p}$ and ${\displaystyle q}$ are barbed bisimilar if there exists a barbed bisimulation ${\displaystyle R}$ where ${\displaystyle (p,q)\in R}$.

Defining a context as a π term with a hole [] we say that two processes P and Q are barbed congruent, written ${\displaystyle P\sim _{b}Q\,\!}$, if for every context ${\displaystyle C[]}$ we have that ${\displaystyle C[P]}$ and ${\displaystyle C[Q]}$ are barbed bisimilar. It turns out that barbed congruence coincides with the congruence induced by early bisimilarity.