Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
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.
