<blockquote>
  <p>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:</p>

<pre><code>(νx)P ⟶ P[c/x]
</code></pre>
  
  <p>where c is a globally fresh channel name. Then, everything made sense to me.</p>
</blockquote>

<p>You are basically correct. </p>

<p>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:</p>

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

<p>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. </p>

<ol>
<li><p>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.</p></li>
<li><p>However, if you don't like it, you're in good company. Bob Harper does things the way you suggest in his book <a href="http://www.cs.cmu.edu/~rwh/pfpl.html"><em>Practical Foundations for Programming Languages</em></a>.</p></li>
</ol>

CC BY-SA 3.0
2016-07-04T10:38:57.423Z
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.
Martin Berger
CC BY-SA 3.0
2016-07-04T10:53:30.157Z
Actually, I think the same thing about explicit names -- but I also suspect it's *déformation professionnelle* in both cases! :-)
Neel Krishnaswami
CC BY-SA 3.0
2016-07-04T12:11:17.387Z
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.
Martin Berger
CC BY-SA 3.0
2016-07-04T10:09:27.443Z
2016-07-04T10:09:27.443Z
Neel Krishnaswami
<p>Scope extrusion is <strong>the</strong> key advance of <span class="math-container">$\pi$</span>-calculus over earlier calculi
such as CCS. Scope extrusion is the source of <span class="math-container">$\pi$</span>-calculus' power of
expressing (in a succinct and
compositional way) other forms of computation.</p>
<p>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 <span class="math-container">$\pi$</span>-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.</p>
<p>Your suggestion, as Neel also points out, works in a technical sense,
but looses the key feature of <span class="math-container">$\pi$</span>-calculus, which is
compositionality.  The <span class="math-container">$\nu$</span>-binder is the key innovation of
<span class="math-container">$\pi$</span>-calculus. I recommend that you play with encoding some calculi
into <span class="math-container">$\pi$</span>-calculus (starting e.g. with [4]) to see just how much more succinct the encoding is
if you keep the <span class="math-container">$\nu$</span>-operator, in comparison with global constants.</p>
<p><strong>Summary</strong>: both, identifying names and variables, as well as explicit
scoping of names leads to more succinct description of computation.</p>
<hr>
<sup>
[1] K. Honda, M. Tokoro, On Asynchronous Communication Semantics.
<p>[2] K. Honda, M. Tokoro, An Object Calculus for Asynchronous Communication.</p>
<p>[3] K. Honda, Two bisimilarities in ν-calculus.</p>
<p>[4] R. Milner, Functions as Processes.
</sup></p>

CC BY-SA 4.0
2016-07-04T10:17:36.217Z
2024-12-05T14:48:27.753Z
2024-12-05T14:48:27.753Z
Martin Berger
<p>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.</p>

<p>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.</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2016-07-04T09:30:18.507Z
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:
http://kyagrd.logdown.com/posts/748618-about-scope-extrusion-of-pi-calculus
kyagrd
<pi-calculus>
Is scope extrusion necessary in the Pi-calculus?
kyagrd
# Is scope extrusion necessary in the Pi-calculus?

(Asked by: username_0 on 2016-07-04)

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.

**Tags:** pi-calculus

> **Comments:**
> **username_0**: 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: http://username_0.logdown.com/posts/748618-about-scope-extrusion-of-pi-calculus  

---

## 2 answers

### Answer by username_1 on 2016-07-04. Score: 10

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. 

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.
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.

> **Comments:**
> **username_2**: 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.  
> **username_1**: Actually, I think the same thing about explicit names -- but I also suspect it's *déformation professionnelle* in both cases! :-)  
> **username_2**: 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.  

---

### Answer by username_2 on 2016-07-04. Score: 10

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 succinct 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.


---

