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

• Can you define (or give a reference to the definition of) "active substitution"? Oct 21 '15 at 9:03
• Sure. Ben Smyth wrote an introductory paper on the applied $\pi$-calculus which includes the definition of active substitutions. Simply click. Oct 21 '15 at 10:01
• 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). Oct 21 '15 at 12:55
• What is the variable $x_1$? Oct 22 '15 at 19:27
• I edited the post and forgot to remove the index. Just fixed it. Oct 22 '15 at 20:00


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