Back to π-Calculus: a better introduction

Now that things are settling down a little bit, I wanted to get back to the stuff I was writing about π-calculus. But looking back at what I've already written, I think I did a terrible job of introducing it. So I'm going to start over, and try to be more clear.

I'll start with a basic refresher of what π-calculus is for, and a bit of history for where it came from.

When computer networks first appeared and came into relatively widespread use, one of the problems that smart people recognized quite quickly is that communicating systems are fundamentally different from the kinds of computing systems that most of us are familiar with. The tools that we use to model conventional computing systems fail to capture many of the relevant properties of computation in a distributed world; and in fact, worse than just not capturing things, they often get things actively wrong.

So - some people started looking at more useful and/or realistic ways of describing
communicating systems - things called process calculi. The first major process calculus that I know of that's still used today is CSP (Communicating Sequential Processes), first described in 1978 by C. A. R. Hoare. CSP became the basis of a
system called the transputer, and its programming language, Occam.

Just two years later, in 1980, Robin Milner proposed something similar
to CSP called CCS - the calculus of communicating systems. The CCS had a stronger formal
basis than CSP, and was somewhat more flexible in some ways. It was a very widely respected and widely used tool - in particular, it became the basis of a major tool for the formal description of network communication protocols, called LOTOS. But it had one
major problem: it was limited to static communication structures. What that means
is that it described communication over a specific, static network of communication
channels. Using the CCS, you could not add channels, remove channels, or rearrange the
interconnections of communication channels in a system.

The π-calculus is an extension of the CCS that addresses that limitation, by
replacing static communication channels with channel names. Instead of using a
predefined network of communication channels, the π-calculus introduced the notion of a
dynamic system of named channels, and communication instructions in the π-calculus work
in terms of channel names, not specific channels. Channel names can be created
dynamically, assigned to variables, and passed in messages. With the addition of channel
names, π-calculus could be used to describe many more kinds of communicating systems
much more easily than could be done in the systems that preceded it.

So, finally, let's get down to some syntax. There are only a small number of
basic forms in π-calculus. I'm not going to use Milner's syntax - it's too hard to write in HTML. But I'm going to try to be more consistent than last time around. A π-calculus expression is called a process. Processes are written using the following forms:

Send Message: !name(values).Process

If there is a matching receiver waiting, send the values as a message on the channel named by the value of the name.

Receive Message: ?name(values).Process

If there is a matching sender, receive the values that it's sending as a message on the channel named by the value of name.

Create Name: new(vars).Process

Create a new channel set of channel name, and assign them to the variables. The variables names are scoped to the rest of the process definition.

Parallel Composition: Process1 | Process2

Run both Process₁ and Process₂ at the same
time.

Choice Composition:Process1 + Process2

Non-deterministically choose to run either Process₁ or Process₂.

Replication: *(Process)

Spawn as many copies of a process as necessary. "*(P)" is equivalent to "P | *(P)".

Null: ∅

An empty process. The null process is mainly used to express process termination.

In addition to those basic structures, I'll also use "{}"s for grouping.

As usual for a calculus, we also need to look at reduction rules, the rules by which steps in a π-calculus process get evaluated. In π-calculus, reduction is written using →: "A" is reducible to "B" in one step is written "A → B". The reduction rules are:

• The Fundamental Rule: ( !x(z).P | ?x(y).Q ) → P|(Q[z/y]). This rule basically says that given a matching pair of message send and message receive in parallel processes, both the send and the receive can be executed in one step, and the values in the message replace the parameters named in the receiver. (Q[z/y] means "The process Q with every reference to name "z" replaced with a reference to name "y".)
• The Choice Rule: If P→Q, then (P+R)→Q. This one is a little bit tricky. What it says is: if you have a choice between either process P or process R, and there is a one-step reduction of P to Q, then you can choose P, and do that reduction.
• The Parallelism Rule: If P→Q, then (P|R)→(Q|R). All this says is that if there's two processes running in
  parallel, you can do a one-step reduction of one of the parallel processes without
  affecting the other.
• The Replication Rule: If P→Q, then *(P)→Q|*(P). This is just a restatement of what I said earlier about the
  meaning of replication.
• Name Binding Rule: If P→Q, then new(x).P→new(x).Q. This just says that introducing a new name around
  a process doesn't change the reduceability of the processes inside of it.

For today, we'll just do one simple example. Suppose that we've got a communication channel named "out", and any message received by "out" is printed to the standard output. Then we can write a hello world process:

 
new(in).( *(?in(x).!out(x).∅) 
           | !in(hello).!in(world).∅ )

There are two processes composed in parallel. One is a replicated process - so there are conceptually an infinite number of copies of this instantiated. Each instantiated copy receives one message on the channel named "in", and then sends it to out. The other process in here sends two messages to "in": "hello", and "world".

Here's an exercise for interested readers. What's wrong with this process?