The Pi Calculus
Posted by John Baez
After years of suffering, I finally feel I understand the lambda calculus — a programming language so simple that it’s ideal for theoretical computer science, with beautiful connections to category theory. Now I’m ready to move on down the Greek alphabet, and ask:
What’s the pi calculus?
It’s a famous example of a process calculus. Process begins with ‘p’. That explains the ‘pi’.
But what’s a ‘process calculus’?
Well, I know that process calculi are a way of trying to formalize computations where a bunch of stuff goes on simultaneously — or as they prefer to say, ‘concurrently’. Concurrency became a big thing in computer science as soon as distributed systems like the internet became important. The all-knowing Wikipedia tells us:
In computer science, the ‘process calculi’ (or ‘process algebras’) are a diverse family of related approaches to formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and synchronizations between a collection of independent agents or processes. They also provide algebraic laws that allow process descriptions to be manipulated and analyzed, and permit formal reasoning about equivalences between processes (e.g., using bisimulation).
That sounds cool — and I can roughly imagine what ‘bisimulation’ means: something like two processes that are isomorphic, in that each can simulate the other. But then:
Leading examples of process calculi include CSP, CSS, ACP, and LOTOS. More recent additions to the family include the π-calculus, the ambient calculus, PEPA and the fusion calculus.
Mike Stay also likes the blue calculus.
This is a bit disheartening! Imagine you’re about to sign up for a class in calculus, and then they ask you: “So, what brand do you want to learn?” Now I know how people feel when they’re just getting started learning about $n$-categories!
In fact, if you read this review article:
- J.C.M. Baeten, A brief history of process algebra, Rapport CSR 04-02, Vakgroep Informatica, Technische Universiteit Eindhoven, 2004.
you’ll see the problem is worse, in a sense, for process calculi, because people have really different ideas of precisely what these calculi should achieve. They are not all equivalent.
But I should just knuckle down and learn one: for example, the pi calculus. I can start with the Wikipedia article, or these:
- Jeannette M. Wing, FAQ on pi-calculus, 2002.
- Mark Chu-Carroll, Pi calculus entries from his blog Good Math, Bad Math.
They’re not bad! The pi calculus has a shortish axiomatic description, and the sources above provide intuitive explanations of what the axioms mean.
But I can’t help wanting to ‘cheat’ and find some sort of category that captures the essence of the pi calculus, in the same way that cartesian closed categories are supposed to capture the essence of the lambda calculus.
(I say “supposed to”, because this is an oversimplification! But anyway…)
Mike Stay has given me a list of papers that may help me cheat:
- Gian Luca Cattani and Ian Stark and Glynn Winskel, Presheaf models for the pi-calculus.
- Roberto Bruni and Ugo Montanari, Cartesian closed double categories, their lambda-notation, and the pi-calculus.
- Ian Stark, Free-algebra models of the pi calculus.
- Ian Stark, A fully abstract domain model for the pi-calculus.
But it seems to me that a really good formalism for dealing with concurrent processes should have a lot in common with the applications of monoidal categories to physics. After all, doing processes in ‘series’ is just like composing morphisms, and doing them in ‘parallel’ is a bit like tensoring them.
In short, this stuff should be something I can understand!
Maybe someday…
Any help would be appreciated.
Re: The Pi Calculus
As it happened, I was reading up on concurrent computation and the pi-calculus myself, yesterday. I’ve had “The pi-calculus: A Theory of Mobile Processes” by Sangiorgi and Walker standing on my bookshelf for some years, but never started reading as seemed to require a deeper understanding of concurrent computation than I possesed. In fact, in the introduction they suggest “Communicating and Mobile Systems: the pi-Calculus” by Robin Milner as a good introduction into the field of concurrent computation and hope their book will form a good complement.
Sangiorgi and Walker also note that neither the pi-calculus, nor currently any other process calculus, forms a complete theory of mobile systems (like lambda-calculus is for sequential computation), but is only a stepping-stone on the road to a more fundamental theory.
They assume something basic underlies the various theories. It would be interesting to see if category theory could help in shedding some light on this currently unknown theory.