7
$\begingroup$

What is the real benefit of scope extrusion in the Pi-calculus? I read that it adds more flexiblity to the overly restrictive prior process algebra where the scope of a newly created channel was limited. However, taking a first serious look into Pi-calculus, I came to think that this $\nu$-binder is a source of confusion between channel names and bound variables, which should be considered separately.

There are two binders in pi-calculus. One is a normal binder (just like the one in lambda calculus) in the receive $c(x).Q$ where $x$ is bound in $Q$. However, $(\nu x).P$ is a very strange binder because the scope of $x$ can extend over other parallel processes by an axiom, which is just strange, reminding me of dynamic scoping.

IMHO, this is all due to overloading variables and channel names. If we separate the notion of channel names from variables, we can make the $\nu$-binder a true binder where the variable following $\nu$ is a normal bound variable and we only need to add a reduction rule for it, which is just like the reference cell allocation in ML: $$ (\nu x)P \longrightarrow P[c/x] $$ where $c$ is a globally fresh channel name. Then, everything made sense to me.

So, what is the benefit of having this strange axiom for scope extrusion when we can simply model it as new channel creation, which to me is much more intuitive and also closer to real implementations.

$\endgroup$
1
  • $\begingroup$ There is a more elaborative version of this question (which does not add much to this post but states basic facts about pi-calculus) here: kyagrd.logdown.com/posts/… $\endgroup$ – kyagrd Jul 4 '16 at 9:30
10
$\begingroup$

If we separate the notion of channel names from variables, we can make the ν-binder a true binder where the variable following ν is a normal bound variable and we only need to add a reduction rule for it, which is just like the reference cell allocation in ML:

(νx)P ⟶ P[c/x]

where c is a globally fresh channel name. Then, everything made sense to me.

You are basically correct.

The reason most people don't do this is that to model your side condition "where $c$ is a globally fresh channel name", you need to give an operational semantics for the $\pi$-calculus which tracks the set of names $\Sigma$ allocated so far. I.e., the rule above would become:

\begin{array}{lcll} \langle\Sigma; \nu x.P\rangle & \to & \langle\Sigma \uplus \{c\}; P[c/x]\rangle & \mbox{where } c \notin \Sigma \end{array}

Then you'd also need a condition that a configuration is well-formed if the set of names $\Sigma$ is bigger than the free names in $P$, and you'd also need to prove some equivariance/permutation lemmas that configurations and reduction sequences are stable under finite permutations of names.

  1. You get this all for free from the $\alpha$-equivalence of $\pi$-calculus terms, at the price of introducing the (admittedly somewhat ugly) scope extrusion rule.

  2. However, if you don't like it, you're in good company. Bob Harper does things the way you suggest in his book Practical Foundations for Programming Languages.

$\endgroup$
3
  • $\begingroup$ Au contraire, the scope extrusion rule $P^{\text{-}x}|(\nu x)Q \equiv (\nu x)(P|Q)$ is beautiful, and its ubiquity in all forms of computation is one of the deepest insights in all of computer science. $\endgroup$ – Martin Berger Jul 4 '16 at 10:38
  • $\begingroup$ Actually, I think the same thing about explicit names -- but I also suspect it's déformation professionnelle in both cases! :-) $\endgroup$ – Neel Krishnaswami Jul 4 '16 at 10:53
  • $\begingroup$ I'm not sure it's as simple as that. With explicit names you still have to consider what it means for constants to be fresh at the meta level, for example when you compose programs from smaller fragments. The axioms that you use for the (usually informal) reasoning about this at the meta-level are ... what Milner gives you with scope extrusion. $\endgroup$ – Martin Berger Jul 4 '16 at 12:11
10
$\begingroup$

Scope extrusion is the key advance of $\pi$-calculus over earlier calculi such as CCS. Scope extrusion is the source of $\pi$-calculus' power of expressing (in a succint and compositional way) other forms of computation.

You are correct that there are two forms of binders, one for variable to be substituted for, and one for names whose scope can be extruded. It is possible to separate the two. Indeed Honda's original presentations of the asynchronous $\pi$-calculus [1, 2, 3] does exactly that. However, that defines the same calculus in the sense that you can map one to the other in a compositional and fully abstract way. Identifying variables and names makes the calculus more succinct as there are fewer syntactic categories required.

Your suggestion, as Neel also points out, works in a technical sense, but looses the key feature of $\pi$-calculus, which is compositionality. The $\nu$-binder is the key innovation of $\pi$-calculus. I recommend that you play with encoding some calculi into $\pi$-calculus (starting e.g. with [4]) to see just how much more succinct the encoding is if you keep the $\nu$-operator, in comparison with global constants.

Summary: both, identifying names and variables, as well as explicit scoping of names leads to more succinct description of computation.


[1] K. Honda, M. Tokoro, On Asynchronous Communication Semantics.

[2] K. Honda, M. Tokoro, An Object Calculus for Asynchronous Communication.

[3] K. Honda, Two bisimilarities in ν-calculus.

[4] R. Milner, Functions as Processes.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.