Looking into pi-calculus (or -calculus, π-calculus) recently because it is likely to be my day job soon. There are some basic questions while looking into it, and one of them is regarding the scope extrusion. I'll assume the reader is familiar with the basic definitions of pi-calculus. If not, you man consult the wikipedia article on pi-calculus and many other materials freely available online.
In standard formulations of the pi-calculus a fresh channel name is created by -binder as where is the new name bound in process . This informal description in English is already confusing because is mentioned as a fresh channel name, suggesting that is a globally unique identifier, but is also described as a bound variable with a scope restriction within . IMHO, this confusion is not merely because one is not used to pi-calculus but there is a good reason to have such confusion. In addition, I think there is a rather well-known way of describing this without such confusion. In a nutshell, the -binder is not really a binder, rather it is an action that creates a fresh channel identifier, which should be treated analogous to the
ref expression that creates a fresh reference in ML. It really is exactly like that. I really wonder why they had to define pi-calculus like this. What's strange is that pi-calculus was created by Robin Miler, the same famous person who designed ML. Now, let me give some more details below.
Scope extrusion is a "feature" of the pi-calculus that sets the pi-calculus aside from earlier process calculi CSP and CCS (Abadi & Gordon 1996). This "improvement" provided by scope extrusion allows the channel name freshly created by the -binder to escape its scope, more precisely, the scope can change according the axiom that relates restriction () and parallel composition ():
where does not appear free in . On the left hand side, is bound in only in . One the right hand side, is bound in both and . So, why do we extend the scope of $x$? It is because may send to and may then appear free in after certain number of reductions. Parallel processes and in can send and receive terms including variables. In pi-calculus, the matching pair of send and receive on the same channel by two parallel processes is a redex. The reduction rule in pi-calculus captures this idea:
The send action before is not a binder.
Both the channel name and are free variables. On the other hand, the receive action before binds
in . That is, is a local variable whose scope is within .
Consider, the process, or a composition of two parallel processes:
Here, is only bound in the left-hand side of the parallel composition but not the right-hand side. Therefore, sending from left-hand side to the right-hand side without any preparation will introduce a suddenly new free variable on the right-hand side. To remedy this problem, we use the axiom mentioned earlier on to pre-process the process syntax as follows, and then the reduction step can happen:
where the scope of extends to the left-hand side of the parallel composition. In contrast to the local variable binding of the receive , which is a true binder analogous to in the lambda calculus, the -binder is a fake binder, or at least a very strange one, somewhat like dynamic scoping. The scope extends as it is needed by the reduction semantics. FYI, the send action does not introduce any bound variables both and are free in because it is sending alreadly known term .
This is just so unnatural to me. Instead, we can make as a true binder just like in the send action, and make the reduction semantics to reduce the binder by substituting the bound variable with a fresh channel name like this:
where is a fresh channel name. As simple as that, just like allocating fresh locations (or addresses) for reference cells in ML. Then, everything became quite clear to me. The -action is a simple command that creates a globally fresh channel and binds it to the variable following . So, what we need is a clear distinction of variables and channel names, which is originally not present the calculus. This messy confusion, I think, is because of abusing variables for both local variable binding and global channel names in pi-calculus.
I am not the first to observe the need for the distinction between In fact, several people who worked on variations of pi-calculus have made a distinction between channel names and variables. For instance, in the spi-calculus (Abadi & Gordon 1996), processes can send and receive terms and within the term there is a distinction between variables and channel names. However, Abadi and Gordon's spi-calculus still rely on scope extrusion of pi-calculus and builds upon it, and several other variations of pi-calculus seems to be designed similarly; the distinction of variables and names were to make certain proofs of properties easier, but didn't seem to have any problems are strange feelings against the -binder itself like I have. FYI, the scoping of -bound variable have nothing to do with channel access rights or anything like security information flow purposes. The scope extrusion just makes all the parallel processes around the -binder have access to the new channel. In fact, that is exactly the motivation of spi-calculus trying to restrict channel access to certain processes.
So, my concluding question in this post is that what is the real benefit of having this strange scope extrusion in pi-calculus, which makes a very strange binder and needs an extra axiom to manage its scope manually? It really seems much more understandable and closer to the real implantation considering as a free channel initiation just like reference cells in ML. Is there really any benefit of manually extending the scope before reduction, or are we simply formulating it this way because of backwards compatibility with prior literature on pi-calculus?
P.S. also posted a question on cs theory stack exchange