1
$\begingroup$

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.

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

1 Answer 1

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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