Question

In "A Calculus of Mobile Processes, Part 1" [1], Milner et al. give an example for transmitting a pair of values $(u,v)$ from the process $P$ to either $R$ or $Q$ (see page 13). All three processes are assumed to run in parallel.

They present following solution:

$$ \begin{align} P &= (w) (\bar{x}(w).P' | \bar{w}u.\bar{w}v.0) \\ Q &= x(w).w(y).w(z).Q' \\ R &= x(w).w(y).w(z).R' \end{align} $$

They claim that "it is vital to this idea that w (...) is indeed a private name". Why is this a necessity?

Wouldn't following solution without restriction work?

$$ \begin{align*} P &= \bar{x}(w).P' | \bar{w}u.\bar{w}v.0 \\ Q &= x(\alpha).\alpha(y).\alpha(z).Q' \\ R &= x(\beta).\beta(y).\beta(z).R' \end{align*} $$

[1] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.159.363&rep=rep1&type=pdf

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top