<p>(This is an extended comment).</p>

<p>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.</p>

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

<p>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.</p>

CC BY-SA 3.0
2015-04-27T18:39:54.933Z
Yes you've understood my definitions perfectly, and it looks like I have a "tolerance relation" rather than an equivalence.
Will
CC BY-SA 3.0
2015-05-24T09:37:04.027Z
Interesting. Does anyone see what the set of ["transitive" terms](http://mathoverflow.net/questions/171665/do-you-have-examples-of-such-transitive-elements) here looks like?
Basil
CC BY-SA 3.0
2015-04-26T07:53:31.623Z
2015-04-26T07:53:31.623Z
Damiano Mazza
<p>Contextual equivalence ($M_1 \cong_{ctx} M_2$) is often defined as: 
$C[M_1] \Downarrow V \iff C[M_2] \Downarrow V$</p>

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

<p>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$?</p>

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

<lambda-calculus><denotational-semantics><operational-semantics>
What is contextual equivalence ignoring non-termination called?
Will
# What is contextual equivalence ignoring non-termination called?

(Asked by: username_0 on 2015-04-25)

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.

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

---

## 1 answers

### Answer by username_1 on 2015-04-26. Score: 3 | Accepted answer

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

> **Comments:**
> **username_0**: Yes you've understood my definitions perfectly, and it looks like I have a "tolerance relation" rather than an equivalence.  
> **username_2**: Interesting. Does anyone see what the set of ["transitive" terms](http://mathoverflow.net/questions/171665/do-you-have-examples-of-such-transitive-elements) here looks like?  

---

