(λx. (λy. y x) (λz. x z)) (λy. y y)
Как отмечает @ymonad, один из параметров y необходимо переименовать, чтобы избежать захвата (объединяя разные переменные, которые совпадают только с одним и тем же именем).Здесь я переименовываю последний экземпляр (используя α -эквивалентность):
(λx. (λy. y x) (λz. x z)) (λm. m m)
Следующий шаг - β -reduce.В этом выражении мы можем сделать это в одном из двух мест: мы можем уменьшить либо внешнее приложение (λx), либо внутреннее приложение (λy).Я собираюсь сделать последнее, в основном по произвольной прихоти / потому что я немного подумал и думаю, что это приведет к более коротким промежуточным выражениям:
(λx. (λz. x z) x) (λm. m m)
Еще больше β -сокращение, чтобы сделать.Опять же, я собираюсь выбрать внутреннее выражение, потому что я могу видеть, куда это идет, но в данном случае это не имеет значения, я получу один и тот же окончательный ответ независимо от:
(λx. x x) (λm. m m)
Сторонапримечание: эти два лямбда-выражения (которые также известны как «Пересмешник» (согласно Раймонду Смулляну)) на самом деле α -эквивалентны, и все выражение является (в) известным Ω-комбинатором.Однако, если мы проигнорируем все это и применим другое β -среднение:
(λm. m m) (λm. m m)
Ах, это все еще β -редуцируемое.Либо это?Это выражение α -эквивалентно предыдущему.О, дорогой, мы, кажется, оказались в бесконечном цикле, как это всегда возможно в языках, полных по Тьюрингу (или мы должны сказать, что Лямбда-полные?).Можно было бы обозначить это как наше оригинальное выражение, равное «дну» (на языке Хаскеля), обозначенное ⊥:
(λx. (λy. y x) (λz. x z)) (λy. y y) = ⊥
Является ли это ошибкой?Что ж, есть хорошая теория ЛК, которую нужно знать:
- если выражение имеет β -нормальную форму, то оно будет таким же β -нормальная форма независимо от того, какой порядок сокращений был использован для ее достижения, и
- , если выражение имеет β -нормальную форму, тогда нормальный порядок оценка гарантированно найдет его.
Так что же такое нормальный порядок ?Короче говоря, это β - сокращение внешнего выражения на каждом шаге.Давайте возьмем это выражение для еще одного вращения!
(λx. (λy. y x) (λz. x z)) (λm. m m)
(λy. y (λm. m m)) (λz. (λm. m m) z)
(λz. (λm. m m) z) (λm. m m)
(λm. m m) (λm. m m)
Черт.Похоже, это выражение не имеет нормальной формы - оно расходится (не заканчивается).