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)?


  • $\begingroup$ This question is probably more suited for http://cs.stackexchange.com/. $\endgroup$ – cody Jun 10 '14 at 13:25
  • $\begingroup$ Can it be migrated? I made an account there. $\endgroup$ – Jake Jun 10 '14 at 15:25
  • 1
    $\begingroup$ @cody Why should it be more suited for CS rather than TCS? Just trying to understand. $\endgroup$ – babou Jun 10 '14 at 21:55
  • $\begingroup$ 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. $\endgroup$ – cody Jun 10 '14 at 22:49
  • $\begingroup$ 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. $\endgroup$ – Jake Jun 11 '14 at 2:14

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.

  • $\begingroup$ 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? $\endgroup$ – Jake Jun 11 '14 at 21:10
  • $\begingroup$ 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. $\endgroup$ – cody Jun 11 '14 at 21:26
  • $\begingroup$ Perfect! You have answered my question and then some! Thanks! $\endgroup$ – Jake Jun 11 '14 at 22:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.