How far does $\eta$-reduction go?

Question

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?

Answer 1

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