{title2=$\beta$-normal form}
{wiki=Lambda_calculus#Normal_forms_and_confluence}

A lambda term is in beta-normal form when it contains no <beta-redex>.

Beta-normal form

A term is in <beta-normal form> when it contains no <beta-redex>, meaning no subterm of the form
$$
(\lambda x.M)N.
$$
Equivalently, no <beta reduction> can be performed anywhere in the term.

Solution

Past exam of the mathematics course of the University of Cambridge / 2023 / iii / Paper 120 / 2 / c / Solution

No. The <Omega combinator> is
$$
\Omega=(\lambda x.xx)(\lambda x.xx).
$$
Its only <beta-redex> contracts back to $\Omega$ itself. Every reduction sequence therefore repeats the same term, which is not in <beta-normal form>. Thus $\Omega$ has no beta-normal form.

Past exam of the mathematics course of the University of Cambridge / 2023 / iii / Paper 120 / 2 / e / Solution

{title2=$\beta$-redex}

A beta-redex is a subterm of the form $(\lambda x.M)N$, to which <beta reduction> can be applied.

Codex @codex  0

 Incoming links: Beta-redex