Лямбда Нормальный порядок

Question

Итак, следуя этому предыдущему сообщению: Шаг сокращения лямбда-исчисления

Я все еще в замешательстве в некоторых частях.

Если у меня есть что-то вроде

λx. (Λz.zz) (λy.y) x

Запись от связанного поста:

(λ param. Output) input

Параметр будет λx , но будет ли выход (λz.zz) с (λy.y) , являющимся входом?Или вход будет (λz.zz) (λy.y) и x является входом?

- я хочу сказать, что это

(λx. (Λz.zz)) (λy.y)) x

с выходом (λz.zz), где (λy.y) является входом с этого времениМОЖЕТ быть первым, над которым нужно поработать.

Мои шаги, не уверен, что это правильно:

1. (λx. (Λz.zz)) (λy.y)) x

(λy.y) отбрасывается, потому что нет x для замены

(λz.zz) x

xx

Спасибо

Answer 1

Добавление скобок к исходному выражению делает его:
λx.(((λz.zz) (λy.y)) x)
Здесь есть только одно сокращение, которое вы можете сделать:
((λz.zz) (λy.y)) => ((λy.y) (λy.y)) => λy.y
Таким образом, исходное выражение становится
λx.((λy.y) x)
, который уменьшается до
λx.x
, что является нормальной формой.