Scope of active substitutions in the applied $\pi$-calculus 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.
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", 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.