Звонок по имени против обычного порядка

Question

Я знаю, что эта тема обсуждалась несколько раз, но кое-что мне все еще неясно. Я прочитал этот вопрос о различиях между аппликативным порядком / вызовом по значению и обычным порядком / вызовом по имени, и есть кое-что, что я хотел бы уточнить раз и навсегда:

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

В обычном порядке, но никакие сокращения не выполняются внутри абстракций. Например, λx. (Λx.x)x находится в нормальной форме в соответствии с этой стратегией, хотя и содержит переопределение (λ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

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

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