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


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

  • $\begingroup$ Welcome to Computer Science! The title you have chosen is not well suited to representing your question. Please take some time to improve it; we have collected some advice here. Thank you! $\endgroup$ – Raphael Nov 6 '17 at 6:45

The issue is that you are manipulating $\oplus$ but you don't have any rules (besides its definition) telling you what reductions you can do. The whole point of the paragraph that presents this definition is that there are multiple notions of choice and some but not all are encodable.

Many process calculi have explicit choice or summation operators for nondeterminism, allowing for example $P+Q$ which can behave either as $P$ or as $Q$ (this is imprecise – in fact several different operators are possible). [...] In some cases a form of choice is encodable in a choice-free calculus – for example a purely internal choice can be encoded in the π-calculus given in Section 1.1 above by [expression from question] but in other cases non-encodability results can be proved [...].

| cite | improve this answer | |
  • $\begingroup$ Great answer, you have highlighted a few points I had not understood correctly. But the text in plain english says that the choice operator can behave either as $P$ or as $Q$, and the example makes it possible to behave as neither. $\endgroup$ – Pufe Nov 6 '17 at 13:27
  • $\begingroup$ Another complexity of the $\pi$-calculus (and concurrent calculi in general) is that there's also a variety of (distinct) notions of "behave the same". $\endgroup$ – Derek Elkins left SE Nov 6 '17 at 13:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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