Beta normal form

Remarks

The terms in $\beta$-normal form are exactly the terms of the shape $$\lambda x_1.\, \cdots \lambda x_n.\, y\, N_1 \cdots N_k,$$ with $n, k \ge 0$, a variable $y$, and terms $N_1, \ldots, N_k$ in $\beta$-normal form.

Example: $\lambda f.\, \lambda x.\, f\, (f\, x)$ is in $\beta$-normal form. Each application in it has the variable $f$ in function position, so no subterm is a redex.

Non-example: $\lambda x.\, (\lambda y.\, y)\, x$ is not in $\beta$-normal form, since it contains the redex $(\lambda y.\, y)\, x$. It has the $\beta$-normal form $\lambda x.\, x$.

The term $\Omega = (\lambda x.\, x\, x)(\lambda x.\, x\, x)$ reduces in one step to itself and to nothing else, so it has no $\beta$-normal form.