<p>I don't know &quot;exactly&quot; how it changes the calculus, in the sense that I don't have a formal statement measuring the difference (and I am not aware that there exists one), but allowing reduction under prefixes does change the semantics of the calculus &quot;non-trivially&quot;, as the following example shows.</p>
<p>Let</p>
<p><span class="math-container">$\qquad P\ :=\ \nu(x,y,z)(x(w).(w \mathrel| \overline w.a \mathrel| \overline{y}.b) \mathrel| \overline{x}y \mathrel| \overline xz.c)$</span></p>
<p><span class="math-container">$\qquad S\ :=\ \tau.(\tau.a+\tau.b)+\tau.(\tau.a\mathrel|c)$</span></p>
<p><span class="math-container">$\qquad S'\ :=\ \tau.(\tau.a+\tau.(a\mathrel|c))+S$</span></p>
<p>Whatever definition of reduction you choose, <span class="math-container">$S$</span> and <span class="math-container">$S'$</span> are <em>not</em> bisimilar. Now, in Milner's calculus, <span class="math-container">$P$</span> is bisimilar to <span class="math-container">$S$</span>. If you allow reduction under prefix, <span class="math-container">$P$</span> becomes bisimilar to <span class="math-container">$S'$</span>.</p>
<p>(Intuitively, the difference between <span class="math-container">$S$</span> and <span class="math-container">$S'$</span> is that <span class="math-container">$S'$</span> may &quot;lose&quot; the barb on <span class="math-container">$b$</span> without necessarily exposing a barb on <span class="math-container">$c$</span>, which is what <span class="math-container">$S$</span> must do instead.</p>
<p>Technically, <span class="math-container">$S$</span> and <span class="math-container">$S'$</span> are not weakly barbed bisimilar, which implies that they are not weakly barbed congruent, which implies that they are not weakly bisimilar, or anything stroger.  Indeed, opponent can always win the barbed bisimilarity game against me (player) by starting with the reduction
<span class="math-container">$$S'\to \tau.a+\tau.(a\mathrel|c)\ =:\ S_1'.$$</span>
To respond, I need to reduce <span class="math-container">$S$</span> (arbitrarily many times, including none) ending up on a term having the same weak barbs as <span class="math-container">$S_1'$</span>, which are <span class="math-container">$a$</span> and <span class="math-container">$c$</span>. Now, the reducts of <span class="math-container">$S$</span> having exactly <span class="math-container">$a$</span> and <span class="math-container">$c$</span> as weak barbs are <span class="math-container">$\tau.a\mathrel|c$</span> and its immediate reduct <span class="math-container">$a\mathrel| c$</span>. Whichever I choose, opponent's next move is going to select the reduction <span class="math-container">$S_1'\to a$</span>, ending on a process whose only barb is <span class="math-container">$a$</span>. There is no way for me to match this reduction, because any process I may reduce to will have barbs on both <span class="math-container">$a$</span> and <span class="math-container">$c$</span>, and so I'm toast).</p>
<p>Forbidding reduction under input prefixes corresponds to the fact that read/receive operations are blocking, which is quite natural in programming languages.  When we are waiting for some information to be received and we decide to proceed without, we might make &quot;bad&quot; choices.  In the example, we proceed as if <span class="math-container">$w$</span> could not become equal to <span class="math-container">$y$</span>.  If you think about passing values other than names (for example, integers), the phenomenon should become even more apparent intuitively.</p>
<p>In a deterministic context (like the <span class="math-container">$\lambda$</span>-calculus), proceeding without knowing the value of an input parameter (like reducing <span class="math-container">$M$</span> in <span class="math-container">$\lambda x.\!M$</span>) is fine, but in a concurrent context it is not a good idea.</p>
<p>The story is different for output prefixes and, in fact, many do consider them to be non-blocking, to the point that they force <span class="math-container">$\mathbf 0$</span> (the inactive process) to be the only process allowed under an output prefix.  This is known as the <em>asynchronous <span class="math-container">$\pi$</span>-calculus</em> and its expressiveness with respect to the synchronous version is well understood, in the sense that there are synchronous processes which may be simulated asynchronously only introducing divergence (see especially the work by Catuscia Palamidessi about this).</p>

CC BY-SA 4.0
2022-05-26T23:22:18.477Z
Thank you for your example. I've checked the reductions and indeed it seems correct. But, wouldn't that be the case just for strong bisimilarity? I mean, wouldn't $S$ and $S'$ be weakly bisimilar? It also appears to me that, e.g., if $a\rightarrow b$ by reducing a redex under a prefix, $a$ and $b$ would still be barbed bisimilar (I assume that allowing inner reductions doesn't change the observational power of barbed bisimilarity either). That's why I'm seeking a reference about reductions inside prefixes on the $\pi$-calculus (I'd actually like to cite it on a draft I'm working on).
paulotorrens
CC BY-SA 4.0
2022-05-27T07:11:36.547Z
Actually, $S$ and $S'$ are not weakly bisimilar.  I edited the answer to add an explanation about this.
Damiano Mazza
CC BY-SA 4.0
2022-05-27T07:31:26.123Z
About references, unfortunately I don't have any off of the top of my head.  Like I said in my answer, the fact that input prefixes are "blocking" is so natural that, I think, hardly anyone ever considered doing otherwise.
Damiano Mazza
CC BY-SA 4.0
2022-05-27T07:57:33.847Z
Ohh, I get it. I was ignoring silent transitions, instead seeing $S$ as if it were (up to $\equiv$) simply $a + b + (a\ |\ c)$, in which you'd have to pick one of the three options right away (which appear to be the same options given in $S'$). That's why I assumed $S$ and $S'$ could be weakly bisimilar (and perhaps they'd be in a calculus with only input and output as prefixes, without explicit silent actions, but I'd have to check). Thank you, your example was really helpful.
paulotorrens
CC BY-SA 4.0
2022-05-26T21:03:53.103Z
2022-05-27T07:25:39.033Z
2022-05-27T07:25:39.033Z
Damiano Mazza
<p>Interesting question.</p>
<p>As Damiano says, while syntactically trivial a change, the π-calculus with non-blocking inputs is a different model of computing. (A <em>very</em> different one, and an extremely interesting one that has not, so far, received the attention it deserves.) How computation changes if you can reduce under an input is subtle, and depends in detail on the rest of the model of computing we are talking about. My intuition is that without input prefixing, sequential behaviour becomes difficult to implement.</p>
<p>About 20 years ago, people studied π-like calculi, called Solos [1] that can reduce under inputs. See [2] for some related work.</p>
<p>The <em>&quot;Strong normalisation ...&quot;</em> paper you mention does <strong>not</strong> remove blocking input prefixing from the underlying π-calculus (simplifying a bit, the typing system in that paper has type erasure), but rather proves that non-blocking input is semantically
sound against the chosen (and natural) notion of process equivalence (for which we give a bisimulation characterisation). This means <strong>no well-typed observer</strong> can distinguish a process that did 'reduce' under input from one that did not. To phrase this in yet another way, the equations between processes that come from reduction under input are in the bisimulation.  This all holds because of the
strong restriction linearity places on what is typable. Basically: if
you have a linear output, potentially suppressed under a blocking
input, somewhere in a well-typed process, then this output is guaranteed eventually to synchronise with its corresponding input, since the (linear) input that blocks the linear output will eventually also be unblocked (by linearity). As soon as you loose linearity (e.g. by moving to an affine setting), this stops being true. The <em>&quot;Strong normalisation ...&quot;</em> paper gives a full-abstraction result for a compilation of the simply-typed λ-calculus into the π-calculus, and you can reduce under a λ so,  it order to get a precise model of the SLTC in π we must restrict the latter to an unusually small fragment of the calculus.</p>
<hr />
<ol>
<li><p>C. Laneve, B. Victor, Solos in Concert. <a href="https://user.it.uu.se/%7Evictor/tr/solos-final.pdf" rel="nofollow noreferrer">https://user.it.uu.se/~victor/tr/solos-final.pdf</a></p>
</li>
<li><p>L. Wischik, Fusions - overview. <a href="http://wischik.com/lu/research/fusions.html" rel="nofollow noreferrer">http://wischik.com/lu/research/fusions.html</a></p>
</li>
</ol>

CC BY-SA 4.0
2023-05-02T03:08:59.490Z
I just came back to this, as I'm writing about it now, and shamefully only now I've noticed _who_ had written this answer (one of the authors!), sorry about that. Anyway, your remark that you don't actually extend the reduction relation, but rather show it is sound within the type system, is very helpful. So thank you.
paulotorrens
CC BY-SA 4.0
2023-05-02T07:13:14.137Z
@paulotorrens No worries. About 99% of that paper's readers thought we changed the reduction relation. We should have made this more clear. Semantically defining such relations is a very powerful proof technique and works in more contexts when you have linear types.
Martin Berger
CC BY-SA 4.0
2023-05-02T07:30:57.747Z
I had written this question precisely because of the relation you had used on that paper, as I was very curious about it. I thought I'd came up with it at first, for a different calculus (Thielecke's CPS-calculus), then I found it out in your paper. Later I found out the _exact_ same rules as compiler optimizations in another paper, and then again in a paper about explicit substitution, only to later realize these rules are justified by cut elimination rules on linear proof nets. They seem to have a deep connection (which I'm writing about now).
paulotorrens
CC BY-SA 4.0
2023-05-02T08:31:21.933Z
There is a deep connection, which Kohei and Olivier wrote about in http://perso.ens-lyon.fr/olivier.laurent/picppn.pdf (there was some more unpublished work along those lines, but it never got published because of Kohei's untimely death). Regarding Thielecke's CPS-calculus, you might find my work https://martinfriedrichberger.net/fsen09.html which started from  Thielecke's work, although I then drove it in a different direction (Hoare logic).
Martin Berger
CC BY-SA 4.0
2023-05-02T08:32:58.893Z
What is the compiler optimisation work you mention? (A lot of techniques are discovered by logicians, and, independently, by compiler research.)
Martin Berger
CC BY-SA 4.0
2023-05-02T08:43:35.657Z
I've read the former paper (which uses the same reduction as well), and I'll check the latter, thanks. The rewriting rules also appear here, https://www.microsoft.com/en-us/research/wp-content/uploads/2007/10/compilingwithcontinuationscontinued.pdf, namely as function inlining and dead code elimination (and are mentioned in Appel's book, on his CPS datatype).
paulotorrens
CC BY-SA 4.0
2023-05-02T09:10:41.117Z
Interestingly, compilation by CPS transform, despite its many nice theoretical properties, has fallen out of favour, because it introduces a great many non-local jumps which are hard/impossible to predict well by the branch predictors in modern processors, hence produce slow code. I think an interesting research direction would be to design branch-prediction-friendly CPS transforms (or, branch predictors that handle CPS-transformed code well).
Martin Berger
CC BY-SA 4.0
2022-05-27T09:10:11.353Z
2023-05-02T07:14:12.737Z
2023-05-02T07:14:12.737Z
Martin Berger
<p>The reduction relation given for the <span class="math-container">$\pi$</span>-caculus is usually <em>not</em> compatible (i.e., it's not preserved under arbitrary contexts). Quoting Milner's <a href="https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.6277&amp;rep=rep1&amp;type=pdf" rel="nofollow noreferrer">The Polyadic <span class="math-container">$\pi$</span>-Calculus: A Tutorial</a>:</p>
<blockquote>
<p>It is important to see what the rules do <em>not</em> allow. First, they do not allow reductions underneath prefix, or sum; for example we have
<span class="math-container">$$u(v).(x(y)\ |\ \bar{x}z )\not\rightarrow$$</span>
Thus prefixing imposes an order upon reduction. This constraint is not necessary. However, the calculus changes non-trivially if we relax it, and we shall not consider
the possibility further in this paper.</p>
</blockquote>
<p>I haven't seem yet a reference discussing the possibility of a compatible reduction relation (though one is used in Yoshida's <a href="https://www.doc.ic.ac.uk/research/technicalreports/2003/DTR03-1.pdf" rel="nofollow noreferrer">Strong Normalisation in the <span class="math-container">$\pi$</span>-Calculus</a>). So, my question is: how exactly does having a compatible relation change the calculus, as Milner puts it? Are there any references that study this possibility I could refer to?</p>
<p>(I do assume one of Milner's papers must mention this, but I couldn't find which one, if any.)</p>

<reference-request><concurrency><pi-calculus>
How exactly does a compatible reduction relation change the $\pi$-calculus?
paulotorrens
# How exactly does a compatible reduction relation change the $\pi$-calculus?

(Asked by: username_0 on 2022-05-26)

The reduction relation given for the $\pi$-caculus is usually *not* compatible (i.e., it's not preserved under arbitrary contexts). Quoting Milner's [The Polyadic $\pi$-Calculus: A Tutorial](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.6277&rep=rep1&type=pdf):

> It is important to see what the rules do *not* allow. First, they do not allow reductions underneath prefix, or sum; for example we have
> $$u(v).(x(y)\ |\ \bar{x}z )\not\rightarrow$$
> Thus prefixing imposes an order upon reduction. This constraint is not necessary. However, the calculus changes non-trivially if we relax it, and we shall not consider
> the possibility further in this paper.

I haven't seem yet a reference discussing the possibility of a compatible reduction relation (though one is used in Yoshida's [Strong Normalisation in the $\pi$-Calculus](https://www.doc.ic.ac.uk/research/technicalreports/2003/DTR03-1.pdf)). So, my question is: how exactly does having a compatible relation change the calculus, as Milner puts it? Are there any references that study this possibility I could refer to?

(I do assume one of Milner's papers must mention this, but I couldn't find which one, if any.)

**Tags:** reference-request, concurrency, pi-calculus


---

## 2 answers

### Answer by username_1 on 2022-05-26. Score: 3 | Accepted answer

I don't know "exactly" how it changes the calculus, in the sense that I don't have a formal statement measuring the difference (and I am not aware that there exists one), but allowing reduction under prefixes does change the semantics of the calculus "non-trivially", as the following example shows.

Let

$\qquad P\ :=\ \nu(x,y,z)(x(w).(w \mathrel| \overline w.a \mathrel| \overline{y}.b) \mathrel| \overline{x}y \mathrel| \overline xz.c)$

$\qquad S\ :=\ \tau.(\tau.a+\tau.b)+\tau.(\tau.a\mathrel|c)$

$\qquad S'\ :=\ \tau.(\tau.a+\tau.(a\mathrel|c))+S$

Whatever definition of reduction you choose, $S$ and $S'$ are *not* bisimilar. Now, in Milner's calculus, $P$ is bisimilar to $S$. If you allow reduction under prefix, $P$ becomes bisimilar to $S'$.

(Intuitively, the difference between $S$ and $S'$ is that $S'$ may "lose" the barb on $b$ without necessarily exposing a barb on $c$, which is what $S$ must do instead.

Technically, $S$ and $S'$ are not weakly barbed bisimilar, which implies that they are not weakly barbed congruent, which implies that they are not weakly bisimilar, or anything stroger. Indeed, opponent can always win the barbed bisimilarity game against me (player) by starting with the reduction
$$S'\to \tau.a+\tau.(a\mathrel|c)\ =:\ S\_1'.$$
To respond, I need to reduce $S$ (arbitrarily many times, including none) ending up on a term having the same weak barbs as $S\_1'$, which are $a$ and $c$. Now, the reducts of $S$ having exactly $a$ and $c$ as weak barbs are $\tau.a\mathrel|c$ and its immediate reduct $a\mathrel| c$. Whichever I choose, opponent's next move is going to select the reduction $S\_1'\to a$, ending on a process whose only barb is $a$. There is no way for me to match this reduction, because any process I may reduce to will have barbs on both $a$ and $c$, and so I'm toast).

Forbidding reduction under input prefixes corresponds to the fact that read/receive operations are blocking, which is quite natural in programming languages. When we are waiting for some information to be received and we decide to proceed without, we might make "bad" choices. In the example, we proceed as if $w$ could not become equal to $y$. If you think about passing values other than names (for example, integers), the phenomenon should become even more apparent intuitively.

In a deterministic context (like the $\lambda$-calculus), proceeding without knowing the value of an input parameter (like reducing $M$ in $\lambda x.\!M$) is fine, but in a concurrent context it is not a good idea.

The story is different for output prefixes and, in fact, many do consider them to be non-blocking, to the point that they force $\mathbf 0$ (the inactive process) to be the only process allowed under an output prefix. This is known as the *asynchronous $\pi$-calculus* and its expressiveness with respect to the synchronous version is well understood, in the sense that there are synchronous processes which may be simulated asynchronously only introducing divergence (see especially the work by Catuscia Palamidessi about this).

> **Comments:**
> **username_0**: Thank you for your example. I've checked the reductions and indeed it seems correct. But, wouldn't that be the case just for strong bisimilarity? I mean, wouldn't $S$ and $S'$ be weakly bisimilar? It also appears to me that, e.g., if $a\rightarrow b$ by reducing a redex under a prefix, $a$ and $b$ would still be barbed bisimilar (I assume that allowing inner reductions doesn't change the observational power of barbed bisimilarity either). That's why I'm seeking a reference about reductions inside prefixes on the $\pi$-calculus (I'd actually like to cite it on a draft I'm working on).  
> **username_1**: Actually, $S$ and $S'$ are not weakly bisimilar.  I edited the answer to add an explanation about this.  
> **username_1**: About references, unfortunately I don't have any off of the top of my head.  Like I said in my answer, the fact that input prefixes are "blocking" is so natural that, I think, hardly anyone ever considered doing otherwise.  
> **username_0**: Ohh, I get it. I was ignoring silent transitions, instead seeing $S$ as if it were (up to $\equiv$) simply $a + b + (a\ |\ c)$, in which you'd have to pick one of the three options right away (which appear to be the same options given in $S'$). That's why I assumed $S$ and $S'$ could be weakly bisimilar (and perhaps they'd be in a calculus with only input and output as prefixes, without explicit silent actions, but I'd have to check). Thank you, your example was really helpful.  

---

### Answer by username_2 on 2022-05-27. Score: 3

Interesting question.

As Damiano says, while syntactically trivial a change, the π-calculus with non-blocking inputs is a different model of computing. (A *very* different one, and an extremely interesting one that has not, so far, received the attention it deserves.) How computation changes if you can reduce under an input is subtle, and depends in detail on the rest of the model of computing we are talking about. My intuition is that without input prefixing, sequential behaviour becomes difficult to implement.

About 20 years ago, people studied π-like calculi, called Solos [1] that can reduce under inputs. See [2] for some related work.

The *"Strong normalisation ..."* paper you mention does **not** remove blocking input prefixing from the underlying π-calculus (simplifying a bit, the typing system in that paper has type erasure), but rather proves that non-blocking input is semantically
sound against the chosen (and natural) notion of process equivalence (for which we give a bisimulation characterisation). This means **no well-typed observer** can distinguish a process that did 'reduce' under input from one that did not. To phrase this in yet another way, the equations between processes that come from reduction under input are in the bisimulation. This all holds because of the
strong restriction linearity places on what is typable. Basically: if
you have a linear output, potentially suppressed under a blocking
input, somewhere in a well-typed process, then this output is guaranteed eventually to synchronise with its corresponding input, since the (linear) input that blocks the linear output will eventually also be unblocked (by linearity). As soon as you loose linearity (e.g. by moving to an affine setting), this stops being true. The *"Strong normalisation ..."* paper gives a full-abstraction result for a compilation of the simply-typed λ-calculus into the π-calculus, and you can reduce under a λ so, it order to get a precise model of the SLTC in π we must restrict the latter to an unusually small fragment of the calculus.

---

1. C. Laneve, B. Victor, Solos in Concert. [https://user.it.uu.se/~victor/tr/solos-final.pdf](https://user.it.uu.se/%7Evictor/tr/solos-final.pdf)
2. L. Wischik, Fusions - overview. <http://wischik.com/lu/research/fusions.html>

> **Comments:**
> **username_0**: I just came back to this, as I'm writing about it now, and shamefully only now I've noticed _who_ had written this answer (one of the authors!), sorry about that. Anyway, your remark that you don't actually extend the reduction relation, but rather show it is sound within the type system, is very helpful. So thank you.  
> **username_2**: @username_0 No worries. About 99% of that paper's readers thought we changed the reduction relation. We should have made this more clear. Semantically defining such relations is a very powerful proof technique and works in more contexts when you have linear types.  
> **username_0**: I had written this question precisely because of the relation you had used on that paper, as I was very curious about it. I thought I'd came up with it at first, for a different calculus (Thielecke's CPS-calculus), then I found it out in your paper. Later I found out the _exact_ same rules as compiler optimizations in another paper, and then again in a paper about explicit substitution, only to later realize these rules are justified by cut elimination rules on linear proof nets. They seem to have a deep connection (which I'm writing about now).  
> **username_2**: There is a deep connection, which Kohei and Olivier wrote about in http://perso.ens-lyon.fr/olivier.laurent/picppn.pdf (there was some more unpublished work along those lines, but it never got published because of Kohei's untimely death). Regarding Thielecke's CPS-calculus, you might find my work https://martinfriedrichberger.net/fsen09.html which started from  Thielecke's work, although I then drove it in a different direction (Hoare logic).  
> **username_2**: What is the compiler optimisation work you mention? (A lot of techniques are discovered by logicians, and, independently, by compiler research.)  
> **username_0**: I've read the former paper (which uses the same reduction as well), and I'll check the latter, thanks. The rewriting rules also appear here, https://www.microsoft.com/en-us/research/wp-content/uploads/2007/10/compilingwithcontinuationscontinued.pdf, namely as function inlining and dead code elimination (and are mentioned in Appel's book, on his CPS datatype).  
> **username_2**: Interestingly, compilation by CPS transform, despite its many nice theoretical properties, has fallen out of favour, because it introduces a great many non-local jumps which are hard/impossible to predict well by the branch predictors in modern processors, hence produce slow code. I think an interesting research direction would be to design branch-prediction-friendly CPS transforms (or, branch predictors that handle CPS-transformed code well).  

---

