Contextual equivalence ($M_1 \cong_{ctx} M_2$) is often defined as: $C[M_1] \Downarrow V \iff C[M_2] \Downarrow V$

Which is to say for any context $C$, $C[M_1]$ terminates with value $V$ iff $C[M_2]$ terminates with value $V$.

Is there a name for the weaker equivalence: $C[M_1] \Downarrow V_1 \wedge C[M_2] \Downarrow V_2 \Rightarrow V_1 = V_2$?

Which is to say $C[M_1]$ and $C[M_2]$ reduce to equal values iff they both terminate.


1 Answer 1


(This is an extended comment).

I may be misreading your definitions, but it seems to me that the relation you introduce, let us call it $\simeq$, is not an equivalence relation because it is not transitive.

If $V_1,V_2$ are two distinct closed normal forms (values), then obviously $V_1\not\simeq V_2$.

On the other hand, the genericity lemma (Proposition 14.3.24 in Barendregt's $\lambda$-calculus book) says that given an unsolvable term, say $\Omega$, for any context $C$, either $C[\Omega]\!\Uparrow$ or $C[M]$ has the same normal form (a value, if we assume to work with closed terms) for every term $M$ (including $\Omega$). This shows in particular that $\Omega\simeq V_1$ and $\Omega\simeq V_2$, hence the failure of transitivity.

  • $\begingroup$ Yes you've understood my definitions perfectly, and it looks like I have a "tolerance relation" rather than an equivalence. $\endgroup$
    – Will
    Apr 27, 2015 at 18:39
  • $\begingroup$ Interesting. Does anyone see what the set of "transitive" terms here looks like? $\endgroup$
    – Basil
    May 24, 2015 at 9:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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