Hint/solution for Y1, Y2
(Perhaps you might read a few bullet points to get some momentum, then stop reading and see how much further you can get on your own.)
First, the thought exercise about
T T T
. Recall thath
was of the form\body. ...body...
, and we created one fixed pointξ
like this:H ≡ \u. h (u u) ξ ≡ H H
Now we want to create another fixed point
ξ′
that works like this:T ≡ \u v. h ... ξ′ ≡ T T T ≡ (\u v. h ...) T T <~~> h (T T T)
The last line is justified because we know that
ξ′ ≡ T T T
is supposed to be a fixed point ofh
. How could you fill in the...
so that the next to last line reduced to the last line?We're going to give the answer now, so try to solve it without looking...
Answer:
T ≡ (\u v. h (u u v))
. (Really it could be three occurrences of any mix ofu
s orv
s. You could also use, for example(\u v. h (v u v)
.) You'll see that whenu
is bound toT
and so isv
, then(u u v) <~~> T T T
.Ok, now let's tackle
Y1
andY2
. Begin by trying to specifyξ1
andξ2
directly, then worry about making operatorsY1
andY2
such that:ξ1 ≡ Y1 h g ξ2 ≡ Y2 h g
later. Remember how
ξ1
andξ2
need to work:ξ1 <~~> h ξ1 ξ2 and ξ2 <~~> g ξ1 ξ2
First hint:
ξ1
is going to have the formX1 H G
, for three termsX1
,H
, andG
. Don't worry yet about what the termsH
andG
are.Second hint:
ξ2
is going to have the formX2 H G
.So evidently,
X1
will be an abstract that accepts (at least) two arguments, and so tooX2
. We can write them schematically like this:X1 ≡ \u v. ... X2 ≡ \u v. ...
(What fills in the
...
in the two cases will presumably be different.) And thus:ξ1 ≡ (\u v. ...) H G ξ2 ≡ (\u v. ...) H G
Can you solve it now?
Another hint.
h
is going to be a function likeeven?
that needs to refer toodd?
, and possibly also to itself. (In the particular case ofeven?
it doesn't need to refer to itself, but in general a mutually recursive function might.) So we can imagineh
to have the form\h g. ...
, and similarly, we can imagineg
to have the form\h g. ...
. Forg
, the...
will presumably be different than it is forh
. (We adopt the convention of always having the\h
come first and the\g
come second in bothh
andg
, just because that makes some of the patterns that will emerge easier to see. You could do it differently if you wanted. Then your answer would be different than the one we're developing here.)What
h
should be using for its\h
variable is the fixed pointξ1
; and for its\g
variable is the fixed pointξ2
. Same forg
.So
X1
will have the form:X1 ≡ \u v. h ξ1 ξ2 ≡ \u v. h (X1 H G) (X2 H G)
And
X2
will have the form:X2 ≡ \u v. g ξ1 ξ2 ≡ \u v. g (X1 H G) (X2 H G)
Thus:
ξ1 ≡ (\u v. h (X1 H G) (X2 H G)) H G ξ2 ≡ (\u v. g (X1 H G) (X2 H G)) H G
where
X1
happens also to be the lambda term that is the head ofξ1
; andX2
happens also to be the lambda term that is the head ofξ2
.Where we have
H
inX1
(the head ofξ1
), there we could just use the bound variableu
, right? Similarly forG
we could just use the bound variablev
, right? And similarly forX2
(the head ofξ2
). So:ξ1 ≡ (\u v. h (X1 u v) (X2 u v)) H G ξ2 ≡ (\u v. g (X1 u v) (X2 u v)) H G
Can you solve it yet?
Don't bring in
Y
or any other already-familiar fixed point combinator; that's a false path. You don't need it.The question you should be focusing on is: what are
H
andG
? What are their relations toX1
andX2
? These might not be four distinct lambda terms. How many lambda terms do you think those four labels collectively designate?They designate only two lambda terms.
Can you figure out what they are?
H
isX1
andG
isX2
.Now can you figure out how to get rid of the explicit self-referencing whereby
X1
contains the free variableX1
, meant to refer to the lambda abstract that contains it? IfX1
is justH
, also known inside the body ofX1
asu
, we could just writeξ1
like this, right:ξ1 ≡ (\u v. h (u u v) (X2 u v)) H G
And similarly, if
X2
is justG
, also known inside the body ofX1
asv
, we could just writeξ1
like this, right:ξ1 ≡ (\u v. h (u u v) (v u v)) H G
The lambda abstract that is the head of
ξ1
is just an ordinary, non-self-referring lambda term, and it is what we've been callingX1
andH
.Now can you write
ξ2
?Answer:
ξ2 ≡ (\u v. g (u u v) (v u v)) H G
So in short,
ξ1 ≡ H H G
andξ2 ≡ G H G
, whereH
andG
are the terms(\u v. h (u u v) (v u v))
and(\u v. g (u u v) (v u v))
, respectively. If you do the substitutions, you will see that these definitions do indeed satisfy our constraint that:ξ1 <~~> h ξ1 ξ2 and ξ2 <~~> g ξ1 ξ2
Ok, so that provides a
ξ1
and aξ2
for our specific choice of the functionsh
andg
. Now can you generalize this, so thatξ1 ≡ Y1 h g ξ2 ≡ Y2 h g
We're going to give the answer. Do you want to try again to solve it yourself? By this point you should be able to do it.
If you're confused, read this all through again until you understand it.
Ready for the answer?
Ok, here it is:
Y1 ≡ \h g. (\H G. H H G) (\u v. h (u u v) (v u v)) (\u v. g (u u v) (v u v)) Y2 ≡ \h g. (\H G. G H G) (\u v. h (u u v) (v u v)) (\u v. g (u u v) (v u v))
You can reduce those a bit further, but it makes the pattern harder to see.