--- /dev/null
+This hint works all the way through constructing fixed-point
+combinators that deliver fixed points for a pair of mutually-recursive
+functions. So if you want to solve the problem yourself, as soon as
+you begin to see what's going on, stop reading and work through the
+rest on your own.
+
+Let's remind ourselves of how the ordinary Y combinator works, since
+we're going to attack mutual recursion in the same way.
+
+First, we define a recursive proto-function called `protomonoeven`
+that takes the true even function (the fixed point) as an argument,
+then calls that argument:
+
+<pre>
+let true = \y n . y in
+let false = \y n . n in
+let Y = \f. (\h. f (h h)) (\h. f (h h)) in
+let iszero = \n. n (\x. false) true in
+let pred = \n s z. n (\u v. v (u s)) (K z) I in
+let protomonoeven = \e n . iszero n true (iszero (pred n) false (e (pred (pred n)))) in
+Y protomonoeven 3
+~~> false
+</pre>
+
+So in the equation `X = Y T`, `X`, the function that computes whether
+a number is even or not, is the fixed point of the `protomonoeven` function,
+i.e., `X = Y protomonoeven`.
+
+Obviously, we don't need mutual recursion to define the "even"
+function (since we just defined it without mutual recursion).
+But we *can* define it using mutual recursion, as shown in assignment
+4:
+
+ even = \n . iszero n true (odd (pred n))
+ odd = \n . iszero n false (even (pred n))
+
+Since we have two functions, we'll need two fixed points (`X1` and
+`X2`), and therefore two fixed point combinators to compute them (`Y1`
+and `Y2`), and two protofunctions (`protoeven` and `protoodd`) to feed
+to the combinators. Furthermore, since the fixed points depend on
+both the even function and the odd function, the combinators will need
+to take two arguments, namely, both of the protofunctions:
+
+ even = X1 = Y1 protoeven protoodd
+ odd = X2 = Y2 protoeven protoodd
+
+Writing protoeven and protoodd is easy. Analogously to the ordinary
+case, they will take as arguments the very fixed points we're looking for:
+
+ protoeven = \e o n . iszero n true (o (pred n))
+ protoodd = \e o n . iszero n false (e (pred n))
+
+Notice that `protoeven` doesn't make use of its first argument.
+Likewise, `protoodd` doesn't make use of its second argument. This is
+an expository weakness in the choice of the example, which is
+particularly simple.
+
+To convince yourself that these definitions of protoeven and protoodd
+are correct, note that, for instance, `protoodd (Y protomonoeven) I 3
+~~> false`. (We can get away with using `I` as one of the arguments,
+since `protoeven` ignores its first argument.)
+
+Ok, all that remains is writing `Y1` and `Y2`. Let's look at ordinary
+`Y` again:
+
+<pre>
+let Y = \f. (\h. f (h h)) (\h. f (h h)) in
+</pre>
+
+We know that `Y1` takes two argments, not just one, so we need to
+start like this:
+
+ let Y1 = \pe po ...
+
+where `pe` will be the protoeven function and `po` will be the
+protoodd function. Since everything in this excercise gets split into
+two parts, let's guess that we'll need to versions of `h` as well,
+`h1` and `h2`:
+
+ let Y1 = \pe po . (\h1 h2 . ...) (\h1 h2 . ...) (\h1 h2 . ...)
+
+In the original, `h` was somehow *half* of the fixed point, so that `h
+h` computed the fixed point. In the schema here, `h1` had better be a
+function which, when you give it suitable arguments, computes the
+first fixed point `X1` (likewise for `h2` wrt the second fixed point
+`X2`).
+
+Then we can arrange for our definition to return the desired
+fixed point like this:
+
+ let Y1 = \pe po . (\h1 h2 . pe (h1 [blah])(h2 [blah]))
+ (\h1 h2 . ...)
+ (\h1 h2 . ...)
+
+The term in the middle line is going in for `h1`, so it had better
+also be the kind of thing which, when you give it suitable arguments,
+computes a fixed point for `pe`:
+
+ let Y1 = \pe po . (\h1 h2 . pe (h1 [blah]) (h2 [blah]))
+ (\h1 h2 . pe (h1 [blah]) (h2 [blah]))
+ (\h1 h2 . po (h1 [blah]) (h2 [blah]))
+
+But the third line must help compute a fixed point for `po`.
+
+All we need to do is figure out what the arguments to `h1` and `h2`
+ought to be. Final guess: in the original, `h` took one argument (a
+copy of itself), so once again, here we'll need two arguments. Here's
+where the mutual recursion comes in: the two arguments to `h1` are a
+copy of itself, and a copy of `h2` (symmetrically for `h2`). So the
+complete definition is
+
+ let Y1 = \pe po . (\h1 h2 . pe (h1 h1 h2) (h2 h1 h2))
+ (\h1 h2 . pe (h1 h1 h2) (h2 h1 h2))
+ (\h1 h2 . po (h1 h1 h2) (h2 h1 h2))
+
+Naturally, `Y2` is the same except for the first line:
+
+ let Y2 = \pe po . (\h1 h2 . po (h1 h1 h2) (h2 h1 h2))
+ (\h1 h2 . pe (h1 h1 h2) (h2 h1 h2))
+ (\h1 h2 . po (h1 h1 h2) (h2 h1 h2))
+
+Sure enough,
+
+ Y1 protoeven protoodd 3 ~~> false
+
+So: what's a natural example in which both protofunctions need to call
+both of their arguments?