lambda-calculus - 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-combinator 的正确定义开始.它应该是 Y := λf.(λx.f (x x)) (λx.f (x x))(注意 x x 两边的括号)。自 lambda-calculus is left-associative , 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)

Since Y K doesn't reduce to I, the following substitution is not allowed.

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