Is the Choice operator implementable on $\pi$-calculus?
-
04-11-2019 - |
Question
I was reading about $\pi$-calculus, and some authors include in the basic operations a Choice operator $P \oplus Q$ which means that either $P$ or $Q$ will be executed, but not both.
On page 8 of "Applied $\pi$ - an introduction" (available on http://www.cl.cam.ac.uk/~pes20/apppi.ps ), the author says that the coice operator is not necessary because it can be implemented as:
$$ P \oplus Q \triangleq \textbf{new} \ x \ \textbf{in} \ ( \bar{x}z.0 | xz.P | xz.Q ) $$
But it did not convince me. For example, taking $P=ab.0$ and $Q=cd.0$:
$$ \bar{a}y.0 | (ab.0 \oplus cd.0) \rightarrow 0 | 0 \rightarrow 0 $$
but
$$ \bar{a}y.0 |(\textbf{new} \ x \ \textbf{in} \ ( \bar{x}z.0 | xz.ab.0 | xz.cd.0 )) \rightarrow $$ may reduce to $$ \bar{a}y.0 |0|ab.0|(\textbf{new} \ x \ \textbf{in} \ xz.cd.0 ) \rightarrow 0 | (\textbf{new} \ x \ \textbf{in} \ xz.cd.0 ) $$ but it may also reduce to $$ \bar{a}y.0 |0|cd.0|(\textbf{new} \ x \ \textbf{in} \ xz.ab.0 ) $$
which will deadlock without ever sending $y$ through $a$. My question is: where are the mistakes? Is my reasoning wrong? Is this implementation of the choice operator wrong? Is the $\pi$-calculus required to backtrack and find the path with the most reductions?
I'm really sorry if my question makes no sense, I have very little formal training on this subject it is mostly curiosity so that I can implement a $\pi$-calculus simulator.
No correct solution