Słaba czołowa postać normalna

Ten artykuł od 2011-06 wymaga zweryfikowania podanych informacji.

Należy podać wiarygodne źródła w formie przypisów bibliograficznych.
Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte.
Sprawdź w źródłach: Encyklopedia PWN • Google Books • Google Scholar • Federacja Bibliotek Cyfrowych • BazHum • BazTech • RCIN • Internet Archive (texts / inlibrary)
Dokładniejsze informacje o tym, co należy poprawić, być może znajdują się w dyskusji tego artykułu.
Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

Słaba czołowa postać normalna – wyrażenie w rachunku lambda, w którym główne wyrażenie nie jest redukowalne.

Każde λ-wyrażenie w czołowej postaci normalnej 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.