Diamo innanzitutto la definizione informale di un lambda termine in Normal Form:

Un lambda termine è in forma normale se non esiste
alcun suo sottotermine che possa essere ß-ridotto

Sappiamo anche che la ß-riduzione è possibile se e solo se nel termine c'è un sottotermine che è un ß-redex, ovvero è della forma:

(\x.M)N.

Var sottoinsieme di NF.

x in Var, M in NF

(\x.M) in NF

x in Var, N in NF

(xN) in NF

(LM) in NF, N in NF

((LM)N) in NF