## 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 that h 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 of h. 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 of us or vs. You could also use, for example (\u v. h (v u v).) You'll see that when u is bound to T and so is v, then (u u v) <~~> T T T.

• Ok, now let's tackle Y1 and Y2. Begin by trying to specify ξ1 and ξ2 directly, then worry about making operators Y1 and Y2 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 form X1 H G, for three terms X1, H, and G. Don't worry yet about what the terms H and G are.

• Second hint: ξ2 is going to have the form X2 H G.

• So evidently, X1 will be an abstract that accepts (at least) two arguments, and so too X2. 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 like even? that needs to refer to odd?, and possibly also to itself. (In the particular case of even? it doesn't need to refer to itself, but in general a mutually recursive function might.) So we can imagine h to have the form \h g. ..., and similarly, we can imagine g to have the form \h g. .... For g, the ... will presumably be different than it is for h. (We adopt the convention of always having the \h come first and the \g come second in both h and g, 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 for g.

• 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; and X2 happens also to be the lambda term that is the head of ξ2.

• Where we have H in X1 (the head of ξ1), there we could just use the bound variable u, right? Similarly for G we could just use the bound variable v, right? And similarly for X2 (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 and G? What are their relations to X1 and X2? 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 is X1 and G is X2.

• Now can you figure out how to get rid of the explicit self-referencing whereby X1 contains the free variable X1, meant to refer to the lambda abstract that contains it? If X1 is just H, also known inside the body of X1 as u, 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 just G, also known inside the body of X1 as v, 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 calling X1 and H.

• 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, where H and G 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 functions h and g. 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.