Pi Calculus

Origin. Milner, Parrow, Walker (1992). Mobile processes. Channel passing. Name binding. Foundation for mobile computation.

Models. Processes exchange channel names. Dynamic reconfiguration. Name scope extrusion. Bisimulation over mobile systems.

Formalism.

Syntax: P ::= 0 | x̄⟨y⟩.P | x(z).P | P | Q | (νx)P | !P | P + Q

Output: x̄⟨y⟩.P: send y on x, then P. Channel x, message y.

Input: x(z).P: receive on x, bind to z. z bound in P.

Parallel: P | Q: concurrent.

Restriction: (νx)P: fresh private name x. Scope of x is P.

Replication: !P = P | P | P | ... Unbounded copies.

Communication: x̄⟨y⟩.P | x(z).Q →τ P | Q[y/z] Synchronous.

Scope extrusion: (νx)(x̄⟨x⟩.P | R) | x(z).Q →τ (νx)(P | R | Q[x/z]) Private name escapes scope.

Structural congruence: P | 0 ≡ P P | Q ≡ Q | P (νx)0 ≡ 0 (νx)(νy)P ≡ (νy)(νx)P

Bisimulation: Late vs early. Open bisimulation. Congruence properties.

Symbols.

Symbol	Unicode	Name	Meaning
x̄⟨y⟩	—	Output	Send y on x
x(z)	—	Input	Receive on x, binding z
ν	U+03BD	Nu	Restriction binder: (νx)P makes x private to P
!	—	Replication	Unboundedly many copies
\|	—	Parallel	Concurrent composition
τ	U+03C4	Tau	The silent action a communication produces
≡	U+2261	Identical to	Structural congruence

Metatheory. The second part of Milner, Parrow and Walker (1992) is the theory of bisimulation, and the delicate point is that passing names makes equivalence sensitive to substitution. Early and late bisimilarity differ over when the received name is instantiated, and neither is preserved by input prefix; the corresponding congruences require closure under substitution, while Sangiorgi's open bisimilarity (1996), defined relative to distinctions, is a congruence outright and is strictly finer. Reduction-closed barbed congruence recovers an equivalence from reduction and observability alone, and for image-finite processes early bisimilarity characterizes it. The calculus is Turing complete: Milner's encoding of the lazy λ-calculus is sound, and Sangiorgi showed it identifies exactly those λ-terms with the same Lévy–Longo trees. Palamidessi (1997) proved there is no uniform encoding of the π-calculus with mixed choice into its asynchronous fragment, so asynchrony is a genuine loss of expressive power.

Applies to. Mobile systems. Web services. Security protocols. Concurrent objects. Distributed systems.

Limitations. Bisimilarity comes as a family rather than a canonical relation — early, late, open, ground, barbed, each with a congruence variant — because input prefix fails to preserve the naive definitions, and which one to use is a modelling decision the calculus does not settle. Behavioural equivalence is undecidable for the full calculus, and replication alone yields infinite state spaces, so automated checking reaches only restricted fragments. Structural congruence, which must be applied before any reduction can be read off, includes α-conversion and permutation of parallel components; Khomenko and Meyer (2009) showed deciding it is graph-isomorphism complete. Communication is synchronous, unordered and reliable, so loss, latency, failure and location fall outside the model — the reason distributed variants such as the join calculus and Dπ exist. Mixed choice, the source of the calculus's expressive power, has no distributed implementation.