Czołowa postać normalna

Czołowa postać normalna to wyrażenie w rachunku lambda w którym główne wyrażenie nie jest redukowalne, oraz nie jest lambda-wyrażeniem o redukowalnym ciele.

λ-wyrażenie w postaci normalnej jest λ-wyrażeniem w czołowej postaci normanej. λ-wyrażenie w czołowej postaci normanej jest λ-wyrażeniem w słabej czołowej postaci normanej.

Przykład wyrażenia w czołowej postaci normalnej które nie jest wyrażeniem w postaci normalnej:

λ x . (x ((λ y . y) x))

Wyrażenie to redukuje się do λ x . (x x).

Mówiąc inaczej, wyrażenie jest w czołowej postaci normalnej jeśli ma wyrażenia redukowalne co najwyżej jako argumenty.