How could this Y' same as this Y combinator itself?

31 Views Asked by At

I see this in wiki:

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

And I understand why it corresponds to this lambda expression Y' = (λab.aba) (λab.a(bab))

But I don't know how can this same as X = λa.(λx.xx)(λx.a(xx)) or X = λa.(λx.a(xx))(λx.a(xx)).

Can Y' trans to X by β-reduces or some other way and how ? Thanks ...

1

There are 1 best solutions below

0
ypa y yhm On

I know it !

We can make this:

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

So

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)

So

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)

(I don't know did that correct ...)