# What is contextual equivalence ignoring non-termination called?

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.

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

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