Моя ~> означает "редуцируется к". Рекурсивных определений у нас нет, см. определение data Term = ..., однако любое рекурсивное определение можно свести к использованию комбинатору неподвижной точки над подходящим термом. Вот цепочка выкладок для получения нерекурсивного определения f:
f x y = y x f
f = \x y -> y x f
f = (\z x y -> y x z) f
То что в скобках теперь неподвижная точка для f, используя, например, Y-комбинатор fixY = \p -> (\q -> p (q q)) (\q -> p (q q)) имеем:
f = fixY (\z x y -> y x z)
То есть f и, следовательно, f f f будут термами фиксированной конечной длины, поэтому проблема не в зависании проверялки.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2013-03-28 01:51 pm (UTC)То что в скобках теперь неподвижная точка для f, используя, например, Y-комбинатор fixY = \p -> (\q -> p (q q)) (\q -> p (q q)) имеем:
То есть f и, следовательно, f f f будут термами фиксированной конечной длины, поэтому проблема не в зависании проверялки.