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?