Фиксированная точка K комбинатора

Question

Комбинатор K равен K := (λxy.x), а комбинатор с фиксированной точкой - Y := λf.(λx.f x x) (λx.f x x).Я попытался вычислить YK:

YK = (λx.Kxx)(λx.Kxx) = (λx.x)(λx.x) = (λx.x) = I

Так как YK является фиксированной точкой K:

K(YK) = YK
KI = I
KIe = Ie = e

для любого e.Но KIe должно быть равно I!

Answer 1

Вы не начинаете с правильного определения Y-комбинатора . Это должно быть Y := λf.(λx.f (x x)) (λx.f (x x)) (обратите внимание на круглые скобки x x). Поскольку лямбда-исчисление является левоассоциативным , f x x равно (f x) x, что, очевидно, не работает.

Используя правильное определение, получаем

Y K := (λf.(λx.f (x x)) (λx.f (x x))) K
       (λx.K (x x)) (λx.K (x x))
       K ((λx.K (x x)) (λx.K (x x)))
       K (Y K)

Поскольку Y K не сводится к I, следующая замена не допускается.

K (Y K) = Y K
K I = I

Итак, K I e - это просто

K I e := (K I) e
         ((λx.λy.x) I) e
         (λy.I) e
         I