<p>It took me a while to realize, but, at least for the standard <span class="math-container">$\lambda$</span>-calculus, those two should actually coincide. I'm not sure if there's any reference to this (I'd like to see it if there is!), but a proof for this would be as follow:</p>
<p>Given that <span class="math-container">$\subset$</span> is antisymetric, we can show that the sets coincide if each is a subset from the other:</p>
<ol>
<li><p>To show <span class="math-container">${\approx_M}\subset{\approx_A}$</span>, assume terms <span class="math-container">$a$</span> and <span class="math-container">$b$</span> such that <span class="math-container">$a \approx_M b$</span>, and a context <span class="math-container">$C$</span>. As we have a bi-implication, we can assume either:</p>
<ul>
<li><p><span class="math-container">$C[a] \Downarrow$</span>, which means there is a <span class="math-container">$v$</span> such that <span class="math-container">$C[a] \Downarrow v$</span>. Due to our hypothesis, we also have that <span class="math-container">$C[b] \Downarrow v$</span>, and, thus, <span class="math-container">$C[b] \Downarrow$</span> as needed.</p>
</li>
<li><p>Same as above.</p>
</li>
</ul>
</li>
<li><p>To show <span class="math-container">${\approx_A}\subset{\approx_M}$</span>, assume terms <span class="math-container">$a$</span> and <span class="math-container">$b$</span> such that <span class="math-container">$a \approx_A b$</span>, a context <span class="math-container">$C$</span>, and a value <span class="math-container">$v$</span>. As we have a bi-implication, we can assume either:</p>
<ul>
<li><span class="math-container">$C[a] \Downarrow v$</span>, from which we can derive that <span class="math-container">$C[a] \Downarrow$</span>, and, from our hypothesis, <span class="math-container">$C[b] \Downarrow$</span>. This means that there exists an <span class="math-container">$u$</span> such that <span class="math-container">$C[b] \Downarrow u$</span>. We have that either <span class="math-container">$v = u$</span> or <span class="math-container">$v \neq u$</span> (recall that equality of lambda terms in normal form is decidable, so this doesn't need the excluded middle). If they are the same, we are done, as <span class="math-container">$C[b] \Downarrow v$</span> as required. However, if they are not, we have that, by Böhm's theorem (<em>here's the trick!</em>), that there exists a context <span class="math-container">$D$</span> such that <span class="math-container">$D[v] \Downarrow x$</span> and <span class="math-container">$D[u] \Downarrow y$</span> for different fresh names <span class="math-container">$x$</span> and <span class="math-container">$y$</span>. By replacing our values with our original terms, we have that <span class="math-container">$D[C[a]] \Downarrow x$</span> and <span class="math-container">$D[C[b]] \Downarrow y$</span>. Then consider the context <span class="math-container">$E$</span>, defined as <span class="math-container">$E = (\lambda x.\lambda y.D[C[\cdot]])\ I\ \Omega$</span>. So <span class="math-container">$E[a] \Downarrow$</span>, while <span class="math-container">$E[b]\Uparrow$</span> (it diverges). By our hypothesis, since <span class="math-container">$E[a]\Downarrow$</span>, we also have <span class="math-container">$E[b]\Downarrow$</span>: we have now a contradiction, and are thus finished.</li>
<li>Same as above.</li>
</ul>
</li>
</ol>
<p>If there is any reference to this result, I'd appreciate if someone could point it out. I also don't know if this will work on the call-by-value <span class="math-container">$\lambda$</span>-calculus, since we don't have a separability result as Böhm's theorem, and that by using Plotkin's reduction (the <span class="math-container">$\beta_v$</span> and <span class="math-container">$\eta_v$</span> rules) we do have different normal forms which are not separable.</p>

CC BY-SA 4.0
2023-03-28T17:46:26.287Z
2023-03-28T17:46:26.287Z
paulotorrens
<p>I've seem two different notions of operational equivalence being used for the <span class="math-container">$\lambda$</span>-lalculus, i.e., an equivalence stating that &quot;if we replace term <span class="math-container">$a$</span> with a term <span class="math-container">$b$</span> in a program, the observable behavior of the program isn't changed&quot;. The first is Morris' context equivalence, which is defined, given that <span class="math-container">$v$</span> is a value of a ground type (bool, nat, etc):</p>
<p><span class="math-container">$$a \approx_M b \iff (\forall C,\forall v,C[a]\Downarrow v \iff C[b]\Downarrow v)$$</span></p>
<p>I.e., for all possible program contexts, plugging in <span class="math-container">$a$</span> gives a constant <span class="math-container">$v$</span> iff plugging in <span class="math-container">$b$</span> does as well: the context can't tell them apart. The second definition I've seem is Abramsky's applicative bisimulation, which is a coindutive definition that &quot;looks inside abstractions&quot;:</p>
<p><span class="math-container">$$a \approx_A b\iff (\forall a',a\Downarrow \lambda x.a' \implies \exists b',b\Downarrow\lambda x.b' \land \forall c,a'[c/x] \approx_Ab'[c/x])$$</span></p>
<p>Abramsky's paper also states that the above definition can be characterizad as follows:</p>
<p><span class="math-container">$$a\approx_Ab\iff(\forall C, C[a]\Downarrow\iff C[b]\Downarrow)$$</span></p>
<p>I.e., for all possible program contexts, plugging in <span class="math-container">$a$</span> halts iff plugging in <span class="math-container">$b$</span> also halts.</p>
<p>(In the above definitions, <span class="math-container">$x \Downarrow y$</span> is the big step operational semantics, and <span class="math-container">$x\Downarrow$</span> means <span class="math-container">$\exists y,x\Downarrow y$</span>.)</p>
<p>These seems to me somewhat complementary (as Morris' equivalence checks for constants and Abramsky's equivalence checks under abstractions). My question is: in the <span class="math-container">$\lambda$</span>-calculus, are these equivalences comparable? I.e., can I derive one from the other? If so, would this be preserved for typed versions of the relations, where we would have less discriminating power on contexts?</p>
<p>(Just to give some context on my question: I'm investigating full abstraction of the simply typed lambda calculus into the simply typed CPS-calculus, where in fact the corresponding versions of Morris' and Abramsky's equivalences coincide, at least in the untyped version. Any directions for this are welcome.)</p>

<lambda-calculus><denotational-semantics><operational-semantics>
What's the relation between applicative bisimulation and context equivalence in the $\lambda$-calculus?
paulotorrens
# What's the relation between applicative bisimulation and context equivalence in the $\lambda$-calculus?

(Asked by: username_0 on 2022-02-20)

I've seem two different notions of operational equivalence being used for the $\lambda$-lalculus, i.e., an equivalence stating that "if we replace term $a$ with a term $b$ in a program, the observable behavior of the program isn't changed". The first is Morris' context equivalence, which is defined, given that $v$ is a value of a ground type (bool, nat, etc):

$$a \approx\_M b \iff (\forall C,\forall v,C[a]\Downarrow v \iff C[b]\Downarrow v)$$

I.e., for all possible program contexts, plugging in $a$ gives a constant $v$ iff plugging in $b$ does as well: the context can't tell them apart. The second definition I've seem is Abramsky's applicative bisimulation, which is a coindutive definition that "looks inside abstractions":

$$a \approx\_A b\iff (\forall a',a\Downarrow \lambda x.a' \implies \exists b',b\Downarrow\lambda x.b' \land \forall c,a'[c/x] \approx\_Ab'[c/x])$$

Abramsky's paper also states that the above definition can be characterizad as follows:

$$a\approx\_Ab\iff(\forall C, C[a]\Downarrow\iff C[b]\Downarrow)$$

I.e., for all possible program contexts, plugging in $a$ halts iff plugging in $b$ also halts.

(In the above definitions, $x \Downarrow y$ is the big step operational semantics, and $x\Downarrow$ means $\exists y,x\Downarrow y$.)

These seems to me somewhat complementary (as Morris' equivalence checks for constants and Abramsky's equivalence checks under abstractions). My question is: in the $\lambda$-calculus, are these equivalences comparable? I.e., can I derive one from the other? If so, would this be preserved for typed versions of the relations, where we would have less discriminating power on contexts?

(Just to give some context on my question: I'm investigating full abstraction of the simply typed lambda calculus into the simply typed CPS-calculus, where in fact the corresponding versions of Morris' and Abramsky's equivalences coincide, at least in the untyped version. Any directions for this are welcome.)

**Tags:** lambda-calculus, denotational-semantics, operational-semantics

---

## 1 answers

### Answer by username_0 on 2023-03-28. Score: 1 | Accepted answer

It took me a while to realize, but, at least for the standard $\lambda$-calculus, those two should actually coincide. I'm not sure if there's any reference to this (I'd like to see it if there is!), but a proof for this would be as follow:

Given that $\subset$ is antisymetric, we can show that the sets coincide if each is a subset from the other:

1. To show ${\approx\_M}\subset{\approx\_A}$, assume terms $a$ and $b$ such that $a \approx\_M b$, and a context $C$. As we have a bi-implication, we can assume either:

   * $C[a] \Downarrow$, which means there is a $v$ such that $C[a] \Downarrow v$. Due to our hypothesis, we also have that $C[b] \Downarrow v$, and, thus, $C[b] \Downarrow$ as needed.
   * Same as above.
2. To show ${\approx\_A}\subset{\approx\_M}$, assume terms $a$ and $b$ such that $a \approx\_A b$, a context $C$, and a value $v$. As we have a bi-implication, we can assume either:

   * $C[a] \Downarrow v$, from which we can derive that $C[a] \Downarrow$, and, from our hypothesis, $C[b] \Downarrow$. This means that there exists an $u$ such that $C[b] \Downarrow u$. We have that either $v = u$ or $v \neq u$ (recall that equality of lambda terms in normal form is decidable, so this doesn't need the excluded middle). If they are the same, we are done, as $C[b] \Downarrow v$ as required. However, if they are not, we have that, by Böhm's theorem (*here's the trick!*), that there exists a context $D$ such that $D[v] \Downarrow x$ and $D[u] \Downarrow y$ for different fresh names $x$ and $y$. By replacing our values with our original terms, we have that $D[C[a]] \Downarrow x$ and $D[C[b]] \Downarrow y$. Then consider the context $E$, defined as $E = (\lambda x.\lambda y.D[C[\cdot]])\ I\ \Omega$. So $E[a] \Downarrow$, while $E[b]\Uparrow$ (it diverges). By our hypothesis, since $E[a]\Downarrow$, we also have $E[b]\Downarrow$: we have now a contradiction, and are thus finished.
   * Same as above.

If there is any reference to this result, I'd appreciate if someone could point it out. I also don't know if this will work on the call-by-value $\lambda$-calculus, since we don't have a separability result as Böhm's theorem, and that by using Plotkin's reduction (the $\beta\_v$ and $\eta\_v$ rules) we do have different normal forms which are not separable.


---

