Редекс — это составной терм, оператором которого служит абстракция, т.е. терм с λ.
| (λx.x x) (λy.y) z → (λy.y) (λy.y) z → (λy.y) z |
; сворачиваемый ; бета-редекс ; выделен фоном |
| → z | ; нф |
| (λx.x x) (λx.x x) → (λx.x x) (λx.x x) → ... |
; не имеет нф ; редукционная цепочка ; бесконечна |