Beta normal form

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. A term is in head normal form if there is no beta-redex in head position.

In the lambda calculus, a beta redex is a term of the form

A redex ${\displaystyle r}$ is in head position in a term ${\displaystyle t}$, if ${\displaystyle t}$ t has the following shape:

A beta reduction is an application of the following rewrite rule to a beta redex contained in a term ${\displaystyle t}$:

...
Wikipedia