Słaba czołowa postać normalna

Słaba czołowa postać normalna

Słaba czołowa postać normalna (weak head normal form) to termin w rachunku lambda, odnoszący się do wyrażenia, w którym główne elementy nie mogą być dalej redukowane. Każde wyrażenie w czołowej postaci normalnej (head normal form) automatycznie spełnia kryteria słabej czołowej postaci normalnej.

Przykład wyrażenia

Przykładem słabej czołowej postaci normalnej, która nie jest czołową postacią normalną, jest:

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

To wyrażenie nie znajduje się w czołowej postaci normalnej, gdyż jego ciało λ-abstrakcji – (λ y . y) x – jest redukowalne do x.

Podsumowanie

• Słaba czołowa postać normalna oznacza wyrażenie, które nie jest redukowalne.
• Każde wyrażenie w czołowej postaci normalnej jest również w słabej czołowej postaci normalnej.
• Przykład ilustruje, jak wyrażenie może być w słabej czołowej postaci, ale nie w czołowej.

Kategoria: Rachunek lambda