ну, правильно воспроизвела - это одно, а не сможет остановиться при проверке - это другое. В чём смысл проверки на альфа-эквивалентность двух шагов редукции? Чтобы ловить зацикленную проверялку или ещё что-то?
Я так понимаю, что
f x y = y x f f f f
будет редуцироваться так:
(upd: ~> наверное, что-то своё означают, напишу-ка, как знаю)
(x -> y -> y x f) f f (y -> y f f) f f f f = (x -> y -> y x f) f f (y -> y f f) f ...
Поскольку проверялка будет сравнивать (x -> y -> y x f) f f и (y -> y f f) f, она просто никогда не остановится.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2013-03-28 10:22 am (UTC)Я так понимаю, что
f x y = y x f
f f f
будет редуцироваться так:
(upd: ~> наверное, что-то своё означают, напишу-ка, как знаю)
(x -> y -> y x f) f f
(y -> y f f) f
f f f = (x -> y -> y x f) f f
(y -> y f f) f
...
Поскольку проверялка будет сравнивать (x -> y -> y x f) f f и (y -> y f f) f, она просто никогда не остановится.