<p>The key to understanding scope management in $\pi$-calculi is to look at the <strong>structural congruence</strong> $P \equiv Q$ and at the notions of <strong>free name</strong> $\newcommand{\FN}[1]{\text{fn}(#1)}\FN{P}$ and <strong>free variable</strong> $\newcommand{\FV}[1]{\text{fv}(#1)}\FV{P}$. The great novelty that distinguishes $\pi$-calculi from its predecessors is the ability to <strong>extrude scope</strong>. It is guided by the following law.</p>

<p>$$
   P \ |\ (\nu x)Q \ \equiv\ (\nu x)(P\ |\ Q) \qquad \text{if $x \notin \FN{P} \cup \FV{P}$}.
$$</p>

<p>This rule is also at the heart of the applied $\pi$-calculus, otherwise it would not be a $\pi$-calculus. In order to understand the scope of active substitution in the applied $\pi$-calculus, we need to understand the free names and variables of an active substitution. This is defined in Section 2.1 of "<a href="http://crysys.hu/members/tvthong/pispi/applied.pdf" rel="nofollow">Mobile values, new names, and secure communication</a>", the paper that introduces the applied $\pi$-calculus:</p>

<ul>
<li>$\FV{\{M/x\}} = \FV{M} \cup \{x\}$.</li>
<li>$\FN{\{M/x\}} = \FN{M}$.</li>
</ul>

<p>The full definition of structural congruence in applied $\pi$ is a bit more elaborate because the calculus parameterises the definition of structural congruence with application-specific equations that define cryptographic primitives, e.g. $\text{decode}_k(\text{encode}_k(msg)) \equiv msg$. In other words, the algebraic laws that give the (formal) cryptography are embedded in the structural congruence. In addition, active substitution itself has associated structural congruence laws:</p>

<ul>
<li>$(\nu x)\{M/x\} \equiv 0$.</li>
<li>$\{M/x\} | P \equiv \{M/x\} | P\{M/x\}$.</li>
<li>$\{M/x\} \equiv \{N/x\}$ whenever the equation $M = N$ holds in the paramterisation. </li>
</ul>

<p>None of these additional structural congruences does anything 'unusual' with extrusion, so, as Damiano says, whether $M$ substitutes for $x$ in $N$ has nothing to do with restrictions 'on the outside' in $(\nu \vec{n})(\{M/x\} | N)$, but only with $x$ occurring in $N$ or not.</p>

CC BY-SA 3.0
2015-10-23T09:39:50.363Z
2015-10-23T09:44:50.603Z
2015-10-23T09:44:50.603Z
Martin Berger
<p>As I have seen a few questions on calculi floating around, I figure this is the right place to ask. Suppose we have an extended process $P \equiv \nu \tilde{n}.\left( \{M/x\} \mid N \right)$ where $\{M/x\}$ denotes an active substitutions and $M$ and $N$ are some terms.</p>

<p>The question i ask myself is, whether we generally substitute $x$ for $M$ in $N$ if $x \in N$, or whether it depends on if $x \in \tilde{n}$ such that it is bound by $\nu \tilde{n}$. In other words, are processes computing in parallel in scope of active substitutions, and if yes, on what conditions?</p>

<p>Despite skimming through several papers, i did not manage to get a clear cut answer.</p>

CC BY-SA 3.0
2015-10-21T09:03:03.820Z
Can you define (or give a reference to the definition of) "active substitution"?
Damiano Mazza
CC BY-SA 3.0
2015-10-21T10:01:15.200Z
Sure. Ben Smyth wrote an introductory paper on the applied $\pi$-calculus which includes the definition of active substitutions. Simply [click.](http://www.bensmyth.com/files/Smyth10-applied-pi-calculus.pdf)
foobar
CC BY-SA 3.0
2015-10-21T12:55:05.270Z
I skimmed through the definitions, I think it is pretty clear that {M/x} | N is structurally equivalent to {M/x} | N' where N' is N in which every free occurrence of x is replaced by M.  This behavior is the expected one and I did not see anything in the text contradicting it.  In particular, it does not matter whether x is bound by the restriction or not.  So, if I correctly understood your question, the answer is yes, the scope of an active substitution {M/x} extends to every parallel process which "knows" x (e.g., in ($\nu$x.{M/x}) | P, the process P is out of scope).
Damiano Mazza
CC BY-SA 3.0
2015-10-22T19:27:55.553Z
What is the variable $x_1$?
Martin Berger
CC BY-SA 3.0
2015-10-22T20:00:50.657Z
I edited the post and forgot to remove the index. Just fixed it.
foobar
<pi-calculus>
Scope of active substitutions in the applied $\pi$-calculus
foobar
# Scope of active substitutions in the applied $\pi$-calculus

(Asked by: username_0 on 2015-10-20)

As I have seen a few questions on calculi floating around, I figure this is the right place to ask. Suppose we have an extended process $P \equiv \nu \tilde{n}.\left( \{M/x\} \mid N \right)$ where $\{M/x\}$ denotes an active substitutions and $M$ and $N$ are some terms.

The question i ask myself is, whether we generally substitute $x$ for $M$ in $N$ if $x \in N$, or whether it depends on if $x \in \tilde{n}$ such that it is bound by $\nu \tilde{n}$. In other words, are processes computing in parallel in scope of active substitutions, and if yes, on what conditions?

Despite skimming through several papers, i did not manage to get a clear cut answer.

**Tags:** pi-calculus
> **Comments:**
> **username_1**: Can you define (or give a reference to the definition of) "active substitution"?  
> **username_0**: Sure. Ben Smyth wrote an introductory paper on the applied $\pi$-calculus which includes the definition of active substitutions. Simply [click.](http://www.bensmyth.com/files/Smyth10-applied-pi-calculus.pdf)  
> **username_1**: I skimmed through the definitions, I think it is pretty clear that {M/x} | N is structurally equivalent to {M/x} | N' where N' is N in which every free occurrence of x is replaced by M.  This behavior is the expected one and I did not see anything in the text contradicting it.  In particular, it does not matter whether x is bound by the restriction or not.  So, if I correctly understood your question, the answer is yes, the scope of an active substitution {M/x} extends to every parallel process which "knows" x (e.g., in ($\nu$x.{M/x}) | P, the process P is out of scope).  
> **username_2**: What is the variable $x_1$?  
> **username_0**: I edited the post and forgot to remove the index. Just fixed it.  

---

## 1 answers

### Answer by username_2 on 2015-10-23. Score: 3

The key to understanding scope management in $\pi$-calculi is to look at the **structural congruence** $P \equiv Q$ and at the notions of **free name** $\newcommand{\FN}[1]{\text{fn}(#1)}\FN{P}$ and **free variable** $\newcommand{\FV}[1]{\text{fv}(#1)}\FV{P}$. The great novelty that distinguishes $\pi$-calculi from its predecessors is the ability to **extrude scope**. It is guided by the following law.

$$
P \ |\ (\nu x)Q \ \equiv\ (\nu x)(P\ |\ Q) \qquad \text{if $x \notin \FN{P} \cup \FV{P}$}.
$$

This rule is also at the heart of the applied $\pi$-calculus, otherwise it would not be a $\pi$-calculus. In order to understand the scope of active substitution in the applied $\pi$-calculus, we need to understand the free names and variables of an active substitution. This is defined in Section 2.1 of "[Mobile values, new names, and secure communication](http://crysys.hu/members/tvthong/pispi/applied.pdf)", the paper that introduces the applied $\pi$-calculus:

* $\FV{\{M/x\}} = \FV{M} \cup \{x\}$.
* $\FN{\{M/x\}} = \FN{M}$.

The full definition of structural congruence in applied $\pi$ is a bit more elaborate because the calculus parameterises the definition of structural congruence with application-specific equations that define cryptographic primitives, e.g. $\text{decode}\_k(\text{encode}\_k(msg)) \equiv msg$. In other words, the algebraic laws that give the (formal) cryptography are embedded in the structural congruence. In addition, active substitution itself has associated structural congruence laws:

* $(\nu x)\{M/x\} \equiv 0$.
* $\{M/x\} | P \equiv \{M/x\} | P\{M/x\}$.
* $\{M/x\} \equiv \{N/x\}$ whenever the equation $M = N$ holds in the paramterisation.

None of these additional structural congruences does anything 'unusual' with extrusion, so, as Damiano says, whether $M$ substitutes for $x$ in $N$ has nothing to do with restrictions 'on the outside' in $(\nu \vec{n})(\{M/x\} | N)$, but only with $x$ occurring in $N$ or not.


---

