Słaba czołowa postać normalna
Z Wikipedii
Słaba czołowa postać normalna to wyrażenie w rachunku lambda w którym główne wyrażenie nie jest redukowalne.
Każde λ-wyrażenie w czołowej postaci normanej jest λ-wyrażeniem w słabej czołowej postaci normanej.
Przykład wyrażenia w słabej czołowej postaci normalnej, które nie jest wyrażeniem w czołowej postaci normalnej:
- λ x . ((λ y . y) x )
Wyrażenie to nie jest w czołowej postaci normalnej ponieważ ciało λ-abstrakcji - (λ y . y) x - jest redukowalne do x.