+++ /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?