Вызов по имени vs нормальный порядок

Question

Я знаю, что эта тема обсуждалась несколько раз, но для меня все еще неясно. Я прочитал этот вопрос applicative-order/call-by-value and normal-order/call-by-name differences и есть что-то я бы прояснить раз и навсегда:

Вызов по имени

В обычном порядке, но никаких сокращений не производится внутри абстракций. Например, λx. (Λx.x) x находится в нормальной форме в соответствии с этой стратегией, хотя в нем содержится redex (λx.x) x.

При вызове по имени выражение λx. (Λx.x) x называется нормальным; это потому, что «(λx.x) x" считается телом (поскольку область λ продолжается как можно дальше справа)? И так с другой стороны, если я применяю обычный порядок, каков будет результат?

Answer 1

При вызове по имени выражение λx. (Λx.x) x называется нормальным; это потому, что «(λx.x) x" считается телом (поскольку область λ продолжается как можно дальше справа)?

Да, вы правы.

И так, с другой стороны, если я применяю обычный порядок, каков будет результат?

Вы делаете сокращение внутри тела: (λx.x)x -> x, так что все сводится к тождественной функции:

λx.(λx.x)x -> λx.x 

Чтобы прояснить это немного дальше, позвольте мне сделать это еще раз, renaming переменные для соответствия Barendregt variable convention: λx.(λx.x)x =α λx.(λy.y)x:

λx.(λy.y)x -> λx.[y := x](y) = λx.x