Я пытаюсь попрактиковаться в бета-уменьшении, но я застрял в том, как уменьшить эту проблему:
(λx((λy.x)(λx.x))x)y
Чтобы выполнить первое β-сокращение, вы должны посмотреть напеременные x ограничены внешней λx, то есть
(λx((λy.x)(λx.x))x)y
^ ^
Обратите внимание, что во внутренней λx.x затеняется внешняя лямбда, поскольку она использует то же имя переменной.Таким образом, граница x здесь привязана к этой внутренней лямбде, а не к внешней.
Другая проблема состоит в том, что если вы замените y на x в λy.x, тогда y будет захваченвнешняя лямбда.Этого не может быть, поэтому вам нужно выполнить α-преобразование (переименование) на λy.x, чтобы избежать захвата.
Итак, сначала α-преобразование, β-уменьшение
(λx((λy.x)(λx.x))x)y
→ (λx((λz.x)(λx.x))x)y
→ ((λz.y)(λx.x))y
Если вы хотите продолжить, то λz.y возвращает y для любого ввода,
((λz.y)(λx.x))y
→ yy
Обратите внимание, что λ-исчисление не устанавливает стратегию сокращения, оно только устанавливает отношение эквивалентностимежду сроками.Таким образом, вы можете выбрать другой порядок сокращения.Например, вы могли бы сначала β-уменьшить внутренний β-redex (λy.x)(λx.x).
(λx((λy.x)(λx.x))x)y
→ (λx(xx)y
→ yy
Это позволило бы избежать α-преобразования.