What's the relation between applicative bisimulation and context equivalence in the $\lambda$-calculus?

Question

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.)

Answer 1

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.