Мне сказали, что термин
(z (λy.z x) (λy.y z))
уже в нормальной форме - но я не понимаю, почему. Нельзя ли сделать еще одну бета-редукцию в этом состоянии и заменить все вхождения y в терме (λy.z x) на (λy.y z), чтобы оно оценивалось как:
(z (λy.z x) (λy.y z)) ==> (z z x)
