π-calculus

If λ-calculus is the minimum theory of computation as function application, the π-calculus (Milner, Parrow, Walker, 1992) is the minimum theory of computation as message passing over named channels. Where λ models what is computed, π models who talks to whom — and crucially, channel names themselves can be sent over channels, so the topology of the network evolves as the program runs.

The whole language

The grammar fits on one line:

P ::=  0                  ;; nothing
    |  x⟨y⟩.P             ;; send y on channel x, then continue P
    |  x(y).P             ;; receive on x, bind into y, then continue P
    |  P | Q              ;; P and Q running in parallel
    |  (νx) P             ;; create a fresh channel x, scoped to P
    |  !P                 ;; replicate — !P = P | !P (unbounded copies)

That's it. No numbers, no functions — those are encoded.

The defining move: name mobility

In CSP and the actor model, channel (or process) identity is fixed at compile time. In π, names themselves are first-class values:

;; A sends fresh channel `c` to B; now A and B share a private channel.
(νc)( a⟨c⟩.0  |  a(x).x⟨"hi"⟩.0 )

After the send, the scope of c extends to include B — this is called scope extrusion, and it's the heart of why π can model phenomena that CCS, CSP, and actors cannot: links forming and dissolving as the system runs.

This matches reality: a load balancer hands a client a connection to a backend, then steps out. A capability is passed from one service to another. A WebRTC peer-exchange hands you a new socket. All "introduction" patterns.

Encoding the world

Because names move, π is Turing-complete — you can encode:

This is the analog of Church's "everything is a function" — but here, everything is a process exchanging channels.

Reduction: communication is the only step

There is one rule:

x⟨y⟩.P  |  x(z).Q   →   P  |  Q[y/z]

A sender and a matching receiver synchronize, the receiver's z is replaced by the sent name y, and both continue. No global state. No clock. The whole operational semantics is built on this single rewriting step plus structural congruence (rearranging parallel parts, restricting scopes, unfolding replication).

Connection to other models

• CCS (Milner's earlier calculus) lacks name mobility — channels are fixed identifiers.
• CSP (Hoare) is similar in spirit but uses named events and parallel composition over event alphabets.
• Actor model (Hewitt) sends messages to actor addresses, not values on channels — closer to asynchronous π without scope extrusion.
• π-calculus = CCS + the ability to send names. That single addition unifies the bunch.

Typed π and sessions

Plain π is dynamically untyped — you can send anything on any channel. Typed π-calculi add type discipline:

• Simple types: each channel carries values of one type.
• Linear types: each channel is used a fixed number of times — prevents resource leaks.
• Session types: a channel's type is a protocol — "first send int, then receive bool, then close." A session-typed program can't break the protocol at compile time. Used in modern languages like Rust (via crates), Scala (lchannels), and research languages like Links.

Why FP cares

The π-calculus is the theoretical foundation for:

• Modern distributed systems reasoning (you can write CSP, Go's channels, Erlang actors as π-fragments).
• Session-typed protocols (preventing protocol bugs at compile time).
• Bisimulation and behavioral equivalence (two processes are "equal" if no observer can distinguish them — a richer notion than data equality).
• Concurrency safety proofs (deadlock-freedom, race-freedom) by reduction to π and its analysis tools.

Clojure's core.async channels are operationally π-shaped — channels are values, you can put them in atoms or pass them through other channels.

Try it in Clojure: name mobility with core.async

This is the scope-extrusion pattern: a server hands a fresh private channel to a client over a public introduction channel.

You're not proving theorems, but every line above is a literal π-calculus construct: chan = ν, >!/<! = x⟨y⟩ / x(y), go = | (parallel composition), go-loop = ! (replication).

Real-world: π in production thinking

When you find yourself drawing arrows on a whiteboard and someone asks "wait, where did that connection come from?" — the honest answer is usually "scope extrusion." π gives that intuition a name and a calculus.

Check yourself

Exercise

Encode a one-shot future in π-style pseudocode: a producer computes a value once, then any number of consumers ask for it on a shared channel. You should use ! (replication) on the consumer-handler side. What goes wrong if you forget the replication?