3
$\begingroup$

Wikipedia lists the following algorithm for normalizing a lambda calculus term $t$:

  • If $t$ is not in head normal form, beta reduce the beta redex in the head position to get $t'$. Then normalize $t'$ to get $t''$. $t''$ is the normal form of $t$.
  • If $t$ is in head normal form, normalize each of its subterms to get $t'$. $t'$ is the normal form of $t$.

The implied base case is if $t$ is in head normal form but has no subterms, in which case it is in normal form already. If $t$ has a normal form, the above algorithm is guaranteed to find it.

The problem I'm having is that it does not seem that the algorithm ever eta-reduces.

For example given the algorithm normalizes $\lambda y.\lambda x.y x$ to itself (since it is already in head normal form, and $x$ is also in head normal form). It should normalize to $\lambda y. y$ though.

It seems apparent that you need to add eta-reduction steps at some point. The problem is I'm not sure where to put them and preserve the property that the algorithm is guaranteed to find the normal form.

When and where do you eta-reduce to achieve this?

$\endgroup$
  • $\begingroup$ The Wikipedia page is talking about beta normal form. $\lambda y.\lambda x.yx$ is in beta normal form. There are no beta redexes anywhere. It also fits the explicit description of what normal forms look like given on that page. It's not in beta-eta normal form though. $\endgroup$ – Derek Elkins left SE Dec 14 '18 at 21:13
2
$\begingroup$

$\eta$ conversion is not a mean to reduce a term to $\beta$-normal form, but a tool to show equivalence regarding the (future) application; to express that 2 terms “are the same function”; that they will reduce to the same term when applied to arbitrary term(s).

If you want to also do $\eta$ conversions, you can do it anytime because you still have the same term (application-wise) after performing it. Having $\eta$ conversion in the theory will not enrich nor deplete the theory regarding existence of $\beta$($\eta$)-normal forms.

| cite | improve this answer | |
$\endgroup$
1
$\begingroup$

Here are some crucial properties about $\beta$ and $\eta$ reductions that explain the strategies for computing normal forms.

We write $\rightarrow_\beta, \rightarrow_\eta$ for a single step of $\beta$ resp. $\eta$, $\rightarrow^*_{\beta},\rightarrow^*_\eta$ for 0 or more steps, and $\rightarrow^{\mathrm{hd}}_\beta$ for head $\beta$-reductions.

Lemma 1: If $t\rightarrow^*_\beta t'\rightarrow^{\mathrm{hd}}_\beta t''$, then there is some $u$ such that $$ t\rightarrow^{\mathrm{hd}}_\beta u\rightarrow^*_\beta t''$$

So head reduction can always be done right up front, and they always must happen, i.e. they can never "disappear" after a (non-head) $\beta$ reduction. A more subtle result (that relies on this one) is that if there is a normal form, then starting with the head reductions is a complete strategy to find it.

Lemma 2: If $t\rightarrow_\eta t' \rightarrow^*_\beta t''$ then there is some $u$ such that $$ t\rightarrow^*_\beta u\rightarrow^*_\eta t''$$

That is, $\eta$ reductions can be "postponed", though they may disappear, e.g. as in $(\lambda x. t\ x)\ u$.

Finally:

Lemma 3: if $t$ is a $\beta$ normal form, and $t\rightarrow_\eta t'$, then $t'$ is also a $\beta$ normal form.

These 2 lemmas imply that it never hurts to push all the $\eta$ reductions to the very end. So simply adding to the $\beta$ normalization strategy: "And then $\eta$ normalize" is a strategy for finding $\beta\eta$ normal forms.

| cite | improve this answer | |
$\endgroup$

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.