Фиксированная точка 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 (xx)) (λx.f (xx))) K
       (λx.K (xx)) (λx.K (xx))
       K ((λx.K (xx)) (λx.K (xx)))
       K (YK)

Поскольку YK не сводится к 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