Are there stronger notions of equivalence over lambda terms than beta equivalence?

Question

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!

Answer 1

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 for models of system $F$ and the classic Barendregt chapters 5 and 10.