这个Y'怎么会和这个Y组合器本身一样呢？

Question

我在wiki中看到了这个：

Y' = SSK(S(K(SS(S(SSK))))K)

我理解为什么它对应于这个lambda表达式

Y' = (λab.aba) (λab.a(bab))

但我不知道这怎么能与

X = λa.(λx.xx)(λx.a(xx))

或

X = λa.(λx.a(xx))(λx.a(xx))

相同。

可以通过

β-reduces

或其他方式将

Y'

转换为 X 以及如何进行？谢谢...

Answer 1

我知道！

我们可以做这个：

🤔 = S(K(SS(S(SSK))))K = λab.a(bab)

所以

Y' 
 = (λb'.(λab.a(bab))b'(λab.a(bab)))
 = λx.(λab.a(bab))x(λab.a(bab))
 = λx.🤔x🤔

Y' 
 = SSK(S(K(SS(S(SSK))))K)
 = (λb'.(λab.a(bab))b'(λab.a(bab)))
 = (λb'.(b'((λab.a(bab))b'(λab.a(bab)))))
 = (λb'.(b'(b'((λab.a(bab))b'(λab.a(bab))))))
 = (λb'.(b'(b'(b'((λab.a(bab))b'(λab.a(bab)))))))
 = (λb'.(b'(b'(b'(b'((λab.a(bab))b'(λab.a(bab))))))))
 = ...

Y' 
 = λx.🤔x🤔
 = λx.x(🤔x🤔)
 = λx.x(x(🤔x🤔))
 = ...

Y' f 
 = 🤔f🤔
 = f(🤔f🤔)
 = f(f(🤔f🤔))
 = ...

Y' f = f (Y' f)

所以

Y 
 = S(K(SII))(S(S(KS)K)(K(SII)))
 = λa.(λb.a(bb))(λc.a(cc))

Y f 
 = (λb.f(bb)) (λc.f(cc))
 = f ((λb.f(bb)) (λc.f(cc)))
 = f (Y f)
 = f (f (Y f))
 = f (f (f (Y f)))
 = ...

Y f = f (Y f)
Y' f = f (Y' f)

Y = Y'

S(K(SII))(S(S(KS)K)(K(SII))) = SSK(S(K(SS(S(SSK))))K)

（我不知道这是否正确......）