Reputation: 219
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 be the same as X = λa.(λx.xx)(λx.a(xx))
or X = λa.(λx.a(xx))(λx.a(xx))
.
Can Y'
be transformed to X
by β-reductions or some other way, and how ? Thanks ...
Upvotes: -1
Views: 126
Reputation: 71070
We can do this by combinators' re-writing, without appealing to their equivalent lambda expressions at all.
First, naming a part of our combinator expressions somehow for now, for convenience,
Y' = SSK(S(K(SS(S(SSK))))K)
---------H'------
= SSKH' = SH'(KH')
meaning,
Y'g = SH'(KH')g = H'g(KH'g) = H'gH'
and
H'gx = S(K(SS(S(SSK))))Kgx
= K(SS(S(SSK)))g(Kg)x
= SS(S(SSK)) (Kg)x
= S(Kg)(S(SSK)(Kg))x
= g (S(SSK)(Kg)x)
= g ( SSKx(Kgx))
= g ( SSKx g )
= g ( Sx(Kx)g )
= g ( xg(Kxg))
= g ( xg x )
Thus,
H'gx = g(x gx )
Y'g = H'gH' = g(H'gH')
= g(Y'g )
Passing H'
as one of the arguments to H'
itself, it becomes available to construct the "next" computation step g(H'gH')
. H'
itself is not recursive, but it is able to "use itself" since it itself was passed as an argument to itself, by the top "jump-starting" call Y'g = H'gH'
.
So Y'
achieves the same fix-point equation as your -- well known -- X = λa.(λx.a(xx))(λx.a(xx))
(usually called Y
):
Xg = (λx.g(xx))(λx.g(xx)) = g((λx.g(xx))(λx.g(xx))) = g(Xg)
Xg = (λx.xx)(λx.g(xx)) = U(Hg) = BUHg = BU(CBU)g <---.
(* -- where -- *) |
Ux = xx |
Hgx = g(xx) = g(Ux) = BgUx = CBUgx -----*
Now your question of how to get from Y'
to X
definition becomes, how to get the X
definition from the recursive equation, Xg = g(Xg)
.
Using some speculation,(*) we can conclude that Xg
must involve some self-application, giving us
1. Xg = g(Xg) -- some self-application is called for:
2. Hg(Hg) = g(Hg(Hg)) -- (must have g to use g) what is this H, then?
3. Hgx = g(x x ) -- this is what! ... thus,
4. Xg = Hg(Hg) -- 1. = 2.
which is what you had.
So actually, what we see here is that we have two different definitions, Y' and X, which, both, are non-recursive yet fulfill the same recursive equation for Y combinator.
So, no, they are not "the same", but both achieve the same result i.e. both are solutions to the same problem, namely, how to define a non-recursive fixpoint combinator, i.e. such that satisfies the recursive equation Yg = g(Yg)
.
And thus we actually see the general way to derive other such definitions, however many we might want, with the chosen H definition entailing the corresponding Y definition to correctly jump-start it, like
Hxg = g(xxg)
Yg = HHg
which is the original Alan Turing's fixpoint combinator Θ, or e.g. this totally arbitrary definition:
Hsomething = g(hsomething)
Yg = HgHHgHHgHg
etc. Well, it's almost arbitrary. It still must take care to pass around the things it needs – the h
and the g
– in the correct argument spots: H
for h
and g
for g
! And that's how it's done.
In a way, the Y
equation is solved by introducing an intermediary, the H
combinator, thus serving somewhat as another instance of the old computer science maxim, "there's no problem that cannot be solved by another level of indirection" (or something like that).
Writing Yg = g(Yg)
, one might ask, but what is that Yg
? Substituting it, = g(g(Yg))
and again = g(g(g(Yg)))
, it never ends... And thus it is not true that we end up with an infinite expression here – we do not end up with anything at all since the substitution process never ends! ... if we insist on having it all done upfront.
Instead, introducing the intermediary achieves postponement, so that the next computation step expression is created when and if it is needed to be called.
(*) it goes like this: we can't refer to it by global name, but we can pass it as an argument to some other thing which will be able to refer to it by the name of that argument inside its body; so, let's pass it as argument to itself, and it'll be able to refer to (a copy of) itself. hence, self-application: Ux = xx
.
Upvotes: 2
Reputation: 219
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 ...)
Upvotes: 2