Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

August 15, 2009

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:

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:

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:

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.

Posted at August 15, 2009 11:05 PM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2037



16 Comments & 2 Trackbacks

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.

Posted by: Ruud Koot on August 16, 2009 4:55 AM | Permalink | Reply to this

Re: The Pi Calculus

Ruud wrote:

As it happened, I was reading up on concurrent computation and the pi-calculus myself, yesterday.

Interesting! How many people world-wide are struggling this very moment to understand this stuff?

The Wikipedia article refers to Sangiorgi and Walker’s The π-Calculus: A Theory of Mobile Processes and Milner’s Communicating and Mobile Systems: the π-Calculus. Indeed Robin Milner is the one who invented the pi-calculus, so his book seems like a natural place to start. But I need to hike down to the library to get these books… maybe I can do it on Monday.

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.

Oh, good! It takes an honest writer to admit when a subject hasn’t found its proper foundation. When I first started going to theoretical computer science conferences back in the mid-1990s, everyone was talking about the need for a good theory of concurrency. Sangiorgi and Walker’s book dates to around 2001. I wonder if experts feel they’ve found this fundamental theory by now, or not. It sounds like a fun challenge.

Posted by: John Baez on August 16, 2009 5:44 AM | Permalink | Reply to this

Re: The Pi Calculus

I beg to differ: the lambda calculus is not “a complete theory for sequential computation”. There are many aspects of sequential computation that are not captured by the lambda calculus. In fact, lambda calculus by itself does not provide any notion of sequentiality because it is an equational theory, and as such does not say anything at all about how things get computed (rather it just says which things are equal). Only when combined with a particular evaluation strategy to normal form and observable side effects (non-termination, I/O) can one meaningfully discuss the order of evaluation.

Posted by: Andrej Bauer on August 16, 2009 10:21 AM | Permalink | Reply to this

Re: The Pi Calculus

Andrej wrote:

I beg to differ: the lambda calculus is not “a complete theory for sequential computation”.

I agree with you here; my quoting Ruud Koot was not meant to express agreement with the bold claim that the lambda calculus is a “complete theory for sequential computation”.

In fact, lambda calculus by itself does not provide any notion of sequentiality because it is an equational theory, and as such does not say anything at all about how things get computed (rather it just says which things are equal).

Here I think you’re being a bit unfair to the lambda calculus. This calculus contains rewrite rules, and I don’t think it’s the fault of the lambda calculus that some people have chosen to interpret these rules as equations. Indeed my LICS talk emphasized that to treat the rewrite rules fairly we need, at the very least, to study the lambda calculus using cartesian closed 2-categories instead of cartesian closed categories.

Only when combined with a particular evaluation strategy to normal form and observable side effects (non-termination, I/O) can one meaningfully discuss the order of evaluation.

I would like to study evaluation strategies using the 2-categorical approach. I would also like to see what normalization by evaluation looks like from the 2-categorical viewpoint.

I don’t know much about the formal theory of ‘observable side-effects’…

Posted by: John Baez on August 16, 2009 4:35 PM | Permalink | Reply to this

Re: The Pi Calculus

Since you’re familiar with some of Paul-André Melliès’s work, you might find his take on concurrency interesting. For example, a relatively recent paper with Samuel Mimram, “Asynchronous games: innocence without alternation”.

Posted by: Noam Zeilberger on August 16, 2009 5:39 AM | Permalink | Reply to this

Re: The Pi Calculus

I’ll check it out. I should also ask his opinion about these matters! Whenever we talk, the conversation tends to focus on our research project.

Posted by: John Baez on August 16, 2009 11:20 PM | Permalink | Reply to this

Re: The Pi Calculus

Hello John,

I think you should have a look at Milner’s most recent work, Bigraphs. Bigraphs are a generalization of Milner’s earlier work on CCS and the Pi-calculus, enriched with categorical ideas and a nice graphical formalism. Milner explicitly states that he hopes to investigate links with natural sciences, including physics.

A recent book offers a gentle introduction to the theory. An electronic version was previously available on Milner’s web-page ; copies could still be available somewhere on the internet (Google or e-mail me for more).

Posted by: Adrien Guatto on August 16, 2009 11:45 AM | Permalink | Reply to this

Re: The Pi Calculus

Thanks, Adrien! I’ll check out bigraphs. Here’s what Milner says about them:

Bigraphs are a rigorous generic model for systems of autonomous agents that interact and move among each other, or within each other. They can be specialised to very different applications. In particular, they offer a unified platform for ubiquitous systems. They are proposed as a Ubiquitous Abstract Machine, playing the foundational role for ubiquitous computing that the von Neumann machine has played for sequential computing.

Bigraphs have evolved from process calculi, especially the calculus of Mobile Ambients (invented by L Cardelli and A Gordon) and the Pi calculus. Over-simplifying a little, the Ambient calculus models spatial reconfiguration, while the Pi calculus models reconfiguration of connectivity. Ubiquitous systems need both. Bigraphs allow agents to be structured simultaneously in these two ways (hence the `bi’ prefix); the two structures are independent, so that where you are does not dictate whom you talk to. This independence has led to an elegant theory.

To specialise Bigraphs to a particular family of systems, we impose a sorting discipline. This declares specific sorts of nodes and edges for the graphs, and may also impose a formation rule that limits the admissible graphs. By this means, Bigraphs have been specialised to represent existing process calculi, recovering their specific theories by means of its generic theory. Bigraphs can also be specialised to such different applications as the movement of agents (e.g. humans) in a built environment and the behaviour of cells and molecules in biology.

Through their graphical presentation, Bigraphs can make it easy for non-experts to visualise their system and assemble them geometrically. Through their algebraic representation they allow the derivation of languages for programming and simulation.

It would be nice to see a formalism that can be specialized to obtain other existing process calculi — it might speed up the process of learning all these process calculi! I also love graphical methods.

Posted by: John Baez on August 16, 2009 4:57 PM | Permalink | Reply to this

Re: The Pi Calculus

Yes, I think I’m going to like these ‘bigraphs’. Here’s a sample from a draft of Milner’s book The Space and Motion of Communicating Agents:


Posted by: John Baez on August 16, 2009 11:15 PM | Permalink | Reply to this

Re: The Pi Calculus

To get a quick feel of bigraphs if you already know symmetric monoidal closed categories (smcc): they are smc theories, almost.

Namely, they form a symmetric monoidal (pre)category which is closely related to the free smcc generated by:

  • two sorts: p for processes and n for names,
  • plus operations making:
    • p into a commutative monoid object,
    • n into a commutative comonoid object,
    • plus a name generation operation I→n,
plus additional operations, according to the process calculus you want to model.

For example, a signature for the π-calculus would include a send operation n⊗n⊗p→p, and a get operation n⊗(n⊸p)→p (and possibly more). Send(a,b,P), usually written b⟨a⟩.P is “send name a on channel b and then do P”. Get(a,(b↦P)), usually written a(b).P, is “receive a name b on channel a and then do P.

Milner’s category of bigraphs is obtained via an ad hoc construction, which faithfully embeds into this free smcc (and is not closed).

There is a standard description of the free smcc, largely due to Todd Trimble himself, which is based on linear logic proof nets, and comes surprisingly close to Milner’s definition.

If you want to understand more, there is this paper (with Richard Garner and Aurélien Pardon): Variable binding, symmetric monoidal closed theories, and bigraphs.

But that is just bigraphical syntax: then you have to throw in reduction rules, and there you start seeing the less satisfactory aspects of bigraphs.

Posted by: Tom Hirschowitz on August 17, 2009 3:06 PM | Permalink | Reply to this

Re: The Pi Calculus

One way to understand Pi-calculus is to compare and contrast Pi-calculus composition with categorical composition.

Categories are about things (morphisms and their attached domain and codomain) and how to compose them. If we compose

   f : A -> B
with 
   g : B -> C
we get 
  
   (g o f) : A -> C
What’s interesting here is that the intermediate thing (B) that enables the composition, has disappeared.

Pi-calculus is also about composition, this time of processes. A process is a thing with a finite number of connection points (like domain and codomain for morphisms, except that there can be any finite number of connection points, including 0). Let’s write P(x1, …, xn) for a process with n connection points x1, …, xn. Composing say

   P(abcx)
with 
   
   Q(axyz)
gives a process 
   P|Q
with connection points abcxyz. In other words, the shared connection points (in this example a and x) have not disappeared and remains available for further composition.

This is also what happens when you connect your computer with Google’s by making a search query: the parallel composition of your machine with Google does not prevent others from also interacting with Google.

Of course sometimes we want to prevent further composition at some composition points. The Pi-calculus enables this by providing an explicit hiding operation (nu x): given P(abc), the process

   (nu a)P
has connection points b and c only.

So in some sense this aspect of Pi-calculus can be seen as decomposing the usual functional/categorical composition into two distinct parts: the pure connection aspect and the hiding aspect, both of which are given as one basic operation in category theory.

A paper that looks at this generalised form of composition in some detail is Elementary structures in process theory (1) by K. Honda.

This is not the full story of the Pi-calculus, because processes have dynamics, they evolve over time, and the connection structure can change over time.

I don’t recommend the Sangiorgi, Walker book as an introduction to the field. Good as it is, it’s too full of technical detail for an introduction.

Posted by: Martin Berger on August 16, 2009 12:59 PM | Permalink | Reply to this

Re: The Pi Calculus

Thanks, Martin, for explaining the idea of processes with more ‘connection points’ than just source and target. The image I get is of a string of beads

•→•→•→•

instead of a mere arrow

•→•

I can imagine a binary ‘composition’ operation that attaches two strings of bead end to end, and also unary ‘hiding’ operations that eliminate a given bead on a string.

Such general ways of ‘gluing things together’ are nicely described by operads, and Tom Leinster’s book studies massive generalizations of category theory based on operads and monads. I don’t know if this could be helpful here.

I’ll check out Honda’s paper.

Posted by: John Baez on August 16, 2009 4:51 PM | Permalink | Reply to this

Re: The Pi Calculus

Good, you’re getting into process algebras. That should increase the chances of my understanding them. I have had some contact with systems biology people in Kent, and I know there’s some interest there. We read an introduction by Luca Cardelli. Certainly an ambitious program.

Mind you, Samson Abramsky is looking to physics rather than biology for inspiration.

Posted by: David Corfield on August 16, 2009 1:07 PM | Permalink | Reply to this

Re: The Pi Calculus

Neat. Another tantalizing subject I wish I understood.

This one, i.e. process calculus, seems particularly close to my heart because, from my very naive understanding, it seems similar in spirit to what I was trying to do with discrete calculus.

The intersecting theme I guess is physics as a process of computation.

Posted by: Eric Forgy on August 16, 2009 5:26 PM | Permalink | Reply to this

Networks of Intelligent Agents, Some of Whom Are Liars

Claude Shannon sharpened the notion of building reliably systems from unreliable components. I’ve been working for some time on the model theory of systems of intelligent agents (not a spacial model) who are all interconnected in that any “announcement” is a public announcement that all agents can hear. The problem is how can one prove theorems about the way that agents revise their belief sets as they determine that certain other agents are certain kinds of liars. First, I have formally proved some of Raymond Smullyan’s (verbal) examples of Knights and Knaves. More importantly, what if there are conspiracies of strategic liars? There is some dispute in the Logic and Philosophy literature as to what is the proper definition of “lying and deception.” I recommend: The Definition of Lying and Deception, James Edwin Mahon. As the Global Recession suggests, markets of “intelligent agents” behave differently if some agents are trying to defraud others. This is a process logic issue, but I’m not clear how Pi Calculus refines the approach. My coauthor and I have been pushing for about 7 years to extend Information Theory into Disinformation Theory.

Posted by: Jonathan vos Post on August 16, 2009 11:10 PM | Permalink | Reply to this

Re: Networks of Intelligent Agents, Some of Whom Are Liars

Mingsheng Ying has been working on combining Pi-calculus with Shannon-style information theory. See for example:

Pi-Calculus with Noisy Channels.

There are a couple of follow-up papers. I don’t think this theory tradition fully solves the problem of generalising process calculus commiunication to noisy channels because of a naive treatement of the free/bound name distinction. However, it’s an interesting start.

Posted by: Martin Berger on August 18, 2009 2:16 PM | Permalink | Reply to this
Read the post Coalgebraic Modal Logic
Weblog: The n-Category Café
Excerpt: Putting together ideas of modal logic and coalgebra with ways of modelling first-order theories.
Tracked: September 7, 2009 12:50 PM
Read the post The Pi Calculus II
Weblog: The n-Category Café
Excerpt: Mike Stay begins to explain the pi calculus.
Tracked: September 8, 2009 4:52 PM

Post a New Comment