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 是左结合的,f x x等于(f x) x, 这显然是行不通的。

使用正确的定义，我们得到

YK := (λ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