International π day was this month. (It was the middle Tuesday. Get it? 3/14 almost looks like 3.14, which is almost π. This isn’t just pandering to the United States’ month/day date format—there is no 31 April, so we can’t have it on 31/4. But why not have it on 22 July? 22/7 approximates π more closely than 3.14 does.)
To celebrate international π day let’s write a compiler for the π-calculus. π-calculus is a system of terms and equations of concurrent, message-passing processes. It’s good for modeling distributed systems and a lot of other things besides.
Here’s a simple variant: there are processes, let’s call write them P and Q; there’s the process that does nothing, we write 0 for that; there’s two concurrent processes, written P | Q; there’s sending a message y on the channel named x and continuing with P, written x<y>.P; there’s receiving a message y on channel x and continuing with P, written x(y).P. But what are x and y? x and y are names, and you make new name x in P by going (ν x).P. (That— ν— is nu; just think new.)
Here’s a brief summary of what we have so far:
P, Q ::= processes
0 do nothing
P | Q concurrent composition
x(y).P message receive
x<y>.P message send
(ν x).P name creation
!P replication
Did you notice I snuck !P in there? I did. !P means an infinite number of Ps; just think P | P | P | …
Let’s go ahead and give!P a formal definition. We’re going to write equations like P → P′, which means P reduces to P′. You can read the arrow as reduces to; just think of it as our π-calculus computer executing an instruction:
!P → P | !P
You can see how we can keep reducing the !P to get our infinite concurrent Ps.
Let’s go ahead and see the operational semantics of the whole calculus. When we can write something ⇒ something else; read ⇒ as implies. Let’s start with P | Q:
P → P′ , Q → Q′ ⇒ P | Q → P′ | Q′
This shows that P and Q make reduction steps at the same time. But at some point, P might finish and go away:
0 | Q = Q
Here we’re saying that these two things are the same. And the order around | doesn’t matter either:
P | Q = Q | P
Now for sending and receiving a message:
x<y>.P | x(z).Q → P | Q[y/z]
These square brackets are new syntax, they mean replace z with y in Q. This reduction rule is rather profound. It implies is that if there’s a x<y>.P without a matching x(z) to receive the value, then the process waits until there is— it waits to send before continuing with P.
Now we must also worry about the meaning of x<y>.P | x(z).Q | x(w).R. We can send y, but does Q or R get it? We make the rule that either Q or R can get y (though not both.) We have just made the leap into non-determinism! Let’s worry about that next time, when we model something in π-calculus.
Comments:
Very good introduction to Pi-Calculus and F# parsing. — Eric Lindahl
