<p>Alright I'll give it a crack. It seems what you are describing is close to <em>contextual equivalence</em>, which is defined in the following manner $t$ and $t'$ ($t\simeq t'$) are contextually equivalent iff:</p>

<p>$$\forall E, E[t]\!\downarrow\ \Leftrightarrow\ E[t']\!\downarrow $$
where $E$ ranges over the set of <em>term contexts</em> (terms with one "hole") and $t\!\downarrow$ means $t$ is normalizing. Now this definition works for all untyped $\lambda$-terms and it is possible to show that if $t$ and $t'$ are normalizing, then
$$ t\simeq t'\ \Leftrightarrow\ t=_{\beta\eta}t'$$</p>

<p>Here $\beta$ is the usual $\beta$-conversion and $\eta$ is the equality
$$ \lambda x.t\ x = t$$
if $x\not\in \mathrm{FV}(t)$</p>

<p>This shows that $\beta+\eta$ is a rather strong form of equivalence for normalizing terms <em>in the untyped setting</em>. However in general the statement
$$ \forall v:T,\ t\ v=_{\beta\eta} t'\ v\qquad (1)$$
in some (normalizing) typed calculus is significatnly stronger than $t=_{\beta\eta}t'$: the first one is usually undecidable, and the second is not.</p>

<hr>

<p>If You take as a starting point $\beta+\eta$ equality at non-functional types and $(1)$ at functional types, what you get is <em>extensional equality of terms</em>, and it holds in most "natural" models. See e.g. <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.9878" rel="nofollow">Berardi <em>et al</em></a> for models of system $F$ and the classic <a href="http://rads.stackoverflow.com/amzn/click/0444875085" rel="nofollow">Barendregt</a> chapters 5 and 10.</p>

CC BY-SA 3.0
2014-06-11T21:10:51.253Z
I'm trying to understand that last paragraph. what is meant by "holds"? (btw, thanks! this is awesome). Also in the first paper $\beta\eta$-completeness is mentioned. What does that mean?
Jake
CC BY-SA 3.0
2014-06-11T21:26:52.453Z
I mean "holds" as in "if terms are equal by (1), then they are equal in the model". $\beta\eta$-completeness of a model is the following fact: *if 2 terms are equal in the model, then they are $\beta\eta$-equal*. This is considered to be an important measure of the power of your model-building technique.
cody
CC BY-SA 3.0
2014-06-11T22:40:01.603Z
Perfect! You have answered my question and then some! Thanks!
Jake
CC BY-SA 3.0
2014-06-11T20:58:03.893Z
2014-06-11T20:58:03.893Z
cody
<p>I should add the context that I am concerned with strongly normalizing systems like System-F.</p>

<p>I have what I consider a very strong notion of equivalence for lambda terms that goes something like the following (not super formal)</p>

<ol>
<li>if $E_1$ and $E_2$ have WHNFs $\lambda x:t.E_1'$ and $\lambda x:t.E_2'$ then $E_1 = E_2$ if $\forall x:t. E_1' = E_2'$</li>
<li>if $E_1$ and $E_2$ have WHNFs that are not $\lambda$s then they must be constructively equivalent. If $\lambda$s are elements of $E_1$ and $E_2$ they must be in the same structural locations and be equivalent by 1.</li>
</ol>

<p>Is this notation of equivalence stronger than beta equivalence for strongly normalizing systems? If not is it equivalent? Are there stronger kinds of equivalence (or perhaps ones in the same spirit but more formal)?</p>

<p>Thanks!</p>

CC BY-SA 3.0
2014-06-10T13:25:29.127Z
This question is probably more suited for [http://cs.stackexchange.com/](http://cs.stackexchange.com/).
cody
CC BY-SA 3.0
2014-06-10T15:25:26.373Z
Can it be migrated? I made an account there.
Jake
CC BY-SA 3.0
2014-06-10T21:55:13.703Z
@cody Why should it be more suited for CS rather than TCS? Just trying to understand.
babou
CC BY-SA 3.0
2014-06-10T22:49:43.240Z
My feeling was that it was not a *research-level* question, since such notions of equivalence are rather well studied. I've changed my mind now though.
cody
CC BY-SA 3.0
2014-06-11T02:14:09.647Z
I wasn't able to find anything (but then again I don't know the right terms) in searching for this. Beta equivalence seems to be the strongest notion of equivalence I can find but I don't see anything that says how it relates to my notation equivalence. Certainly my notation is at least as strong as beta equivalence but perhaps it considers more things equal.
Jake
CC BY-SA 3.0
2014-06-11T06:47:14.867Z
I don't understand clause (1) of the definition: what do you mean by $\forall x:t.E_1'=E_2'$? What does the equality symbol mean there? You are suggesting a recursive definition for your equivalence? And where is $x$ used in $E_1',E_2'$?
Damiano Mazza
CC BY-SA 3.0
2014-06-11T13:03:32.730Z
$=$ is my equality definition so yes this is a recursive definition. x is potentially free in $E_1'$ and $E_2'$. In other fields you might write $E_1'(x)$ to make it clear that the expression may depend on x. I don't see that used ever when describing things like this however. Take a typing judgment for abstraction for instance; $(\Gamma, x:t \vdash e:t')\Rightarrow(\Gamma \vdash \lambda x:t. e : t \rightarrow t')$ it is implied that x possibly be free in e. Frankly it is assumed that anything can be free in these expressions
Jake
CC BY-SA 3.0
2014-06-11T13:14:16.253Z
What does $\forall x : t$ mean? All closed terms of type $t$? All terms in the current context? Or did you mean to say that $E_1' = E_2'$ where $x$ is a free variable?
Andrej Bauer
CC BY-SA 3.0
2014-06-11T13:37:54.753Z
$\forall x : t. P$ means "forall x of type t P is true". Sorry about that; I could have been a bit clearer on that one.
Jake
<pl.programming-languages><lambda-calculus><functional-programming>
Are there stronger notions of equivalence over lambda terms than beta equivalence?
Jake
# Are there stronger notions of equivalence over lambda terms than beta equivalence?

(Asked by: username_0 on 2014-06-10)

I should add the context that I am concerned with strongly normalizing systems like System-F.

I have what I consider a very strong notion of equivalence for lambda terms that goes something like the following (not super formal)

1. if $E\_1$ and $E\_2$ have WHNFs $\lambda x:t.E\_1'$ and $\lambda x:t.E\_2'$ then $E\_1 = E\_2$ if $\forall x:t. E\_1' = E\_2'$
2. if $E\_1$ and $E\_2$ have WHNFs that are not $\lambda$s then they must be constructively equivalent. If $\lambda$s are elements of $E\_1$ and $E\_2$ they must be in the same structural locations and be equivalent by 1.

Is this notation of equivalence stronger than beta equivalence for strongly normalizing systems? If not is it equivalent? Are there stronger kinds of equivalence (or perhaps ones in the same spirit but more formal)?

Thanks!

**Tags:** pl.programming-languages, lambda-calculus, functional-programming

> **Comments:**
> **username_1**: This question is probably more suited for [http://cs.stackexchange.com/](http://cs.stackexchange.com/).  
> **username_0**: Can it be migrated? I made an account there.  
> **username_2**: @username_1 Why should it be more suited for CS rather than TCS? Just trying to understand.  
> **username_1**: My feeling was that it was not a *research-level* question, since such notions of equivalence are rather well studied. I've changed my mind now though.  
> **username_0**: I wasn't able to find anything (but then again I don't know the right terms) in searching for this. Beta equivalence seems to be the strongest notion of equivalence I can find but I don't see anything that says how it relates to my notation equivalence. Certainly my notation is at least as strong as beta equivalence but perhaps it considers more things equal.  
> **username_3**: I don't understand clause (1) of the definition: what do you mean by $\forall x:t.E_1'=E_2'$? What does the equality symbol mean there? You are suggesting a recursive definition for your equivalence? And where is $x$ used in $E_1',E_2'$?  
> **username_0**: $=$ is my equality definition so yes this is a recursive definition. x is potentially free in $E_1'$ and $E_2'$. In other fields you might write $E_1'(x)$ to make it clear that the expression may depend on x. I don't see that used ever when describing things like this however. Take a typing judgment for abstraction for instance; $(\Gamma, x:t \vdash e:t')\Rightarrow(\Gamma \vdash \lambda x:t. e : t \rightarrow t')$ it is implied that x possibly be free in e. Frankly it is assumed that anything can be free in these expressions  
> **username_4**: What does $\forall x : t$ mean? All closed terms of type $t$? All terms in the current context? Or did you mean to say that $E_1' = E_2'$ where $x$ is a free variable?  
> **username_0**: $\forall x : t. P$ means "forall x of type t P is true". Sorry about that; I could have been a bit clearer on that one.  

---

## 1 answers

### Answer by username_1 on 2014-06-11. Score: 3 | Accepted answer

Alright I'll give it a crack. It seems what you are describing is close to *contextual equivalence*, which is defined in the following manner $t$ and $t'$ ($t\simeq t'$) are contextually equivalent iff:

$$\forall E, E[t]\!\downarrow\ \Leftrightarrow\ E[t']\!\downarrow $$
where $E$ ranges over the set of *term contexts* (terms with one "hole") and $t\!\downarrow$ means $t$ is normalizing. Now this definition works for all untyped $\lambda$-terms and it is possible to show that if $t$ and $t'$ are normalizing, then
$$ t\simeq t'\ \Leftrightarrow\ t=\_{\beta\eta}t'$$

Here $\beta$ is the usual $\beta$-conversion and $\eta$ is the equality
$$ \lambda x.t\ x = t$$
if $x\not\in \mathrm{FV}(t)$

This shows that $\beta+\eta$ is a rather strong form of equivalence for normalizing terms *in the untyped setting*. However in general the statement
$$ \forall v:T,\ t\ v=\_{\beta\eta} t'\ v\qquad (1)$$
in some (normalizing) typed calculus is significatnly stronger than $t=\_{\beta\eta}t'$: the first one is usually undecidable, and the second is not.

---

If You take as a starting point $\beta+\eta$ equality at non-functional types and $(1)$ at functional types, what you get is *extensional equality of terms*, and it holds in most "natural" models. See e.g. [Berardi *et al*](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.9878) for models of system $F$ and the classic [Barendregt](http://rads.stackoverflow.com/amzn/click/0444875085) chapters 5 and 10.

> **Comments:**
> **username_0**: I'm trying to understand that last paragraph. what is meant by "holds"? (btw, thanks! this is awesome). Also in the first paper $\beta\eta$-completeness is mentioned. What does that mean?  
> **username_1**: I mean "holds" as in "if terms are equal by (1), then they are equal in the model". $\beta\eta$-completeness of a model is the following fact: *if 2 terms are equal in the model, then they are $\beta\eta$-equal*. This is considered to be an important measure of the power of your model-building technique.  
> **username_0**: Perfect! You have answered my question and then some! Thanks!  

---

