0
$\begingroup$

A term is is normal form, if there are no more redexes. But I'm confused as to what that means.

E.g. $\lambda x. f x$ isn't in normal form, obviously, because it contains an $\eta$-redex. But is $\lambda x. f$ in a normal form? Because applying any kind of term, would always result in the same term.

And even one step beyond, can a lambda term even be in normal form if it is a lambda abstraction? Because I know of pointfree programming, which tries to remove any kind of lambda abstraction, and people say that that has its origin in $\eta$-reduction. But pointfree usually implies applying combinators (which lead us to combinatory logic).

As I see it currently, the only "reduction" $\eta$-reduction can do, is the kind, where the a bound variable appears once in the body, and that is at the end at the same position as the parameter itself, e.g.:

$\lambda x y z. x f g x y z = \lambda x. x f g x$

Is this correct?

$\endgroup$
1
$\begingroup$

In the lambda calculus, a term is in beta normal form if no beta reduction is possible. A term is in beta-eta normal form if neither a beta reduction nor an eta reduction is possible.

So, $\lambda x. f x$ is in beta normal form but not in beta-eta normal form.

But is λx.f in a normal form?

Yes, it is in both beta and beta-eta normal forms.

Because applying any kind of term, would always result in the same term.

Yes, you are right, but this term does not match the $\lambda x.fx$ format, so it cannot be eta-reduced.

the only "reduction" η-reduction can do, is the kind, where the a bound variable appears once in the body, and that is at the end at the same position as the parameter itself

You're correct. Eta-reduction expresses the idea of extensionality, which in this context is that two functions are the same if and only if they give the same result for all arguments. Eta-reductions converts $\lambda x.f x$ into $f$ whenever $x$ does not appear free in $f$.

$\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.