1 This hint works all the way through constructing fixed-point
2 combinators that deliver fixed points for a pair of mutually-recursive
3 functions.  So if you want to solve the problem yourself, as soon as
4 you begin to see what's going on, stop reading and work through the
5 rest on your own.
7 Let's remind ourselves of how the ordinary Y combinator works, since
8 we're going to attack mutual recursion in the same way.
10 First, we define a recursive proto-function called `protomonoeven`
11 that takes the true even function (the fixed point) as an argument,
12 then calls that argument:
14 <pre>
15 let true = \y n . y in
16 let false = \y n . n in
17 let Y = \f. (\h. f (h h)) (\h. f (h h))  in
18 let iszero = \n. n (\x. false) true  in
19 let pred = \n s z. n (\u v. v (u s)) (K z) I  in
20 let protomonoeven = \e n . iszero n true (iszero (pred n) false (e (pred (pred n)))) in
21 Y protomonoeven 3
22 ~~> false
23 </pre>
25 So in the equation `X = Y T`, `X`, the function that computes whether
26 a number is even or not, is the fixed point of the `protomonoeven` function,
27 i.e., `X = Y protomonoeven`.
29 Obviously, we don't need mutual recursion to define the "even"
30 function (since we just defined it without mutual recursion).
31 But we *can* define it using mutual recursion, as shown in assignment
32 4:
34      even = \n . iszero n true (odd (pred n))
35      odd = \n . iszero n false (even (pred n))
37 Since we have two functions, we'll need two fixed points (`X1` and
38 `X2`), and therefore two fixed point combinators to compute them (`Y1`
39 and `Y2`), and two protofunctions (`protoeven` and `protoodd`) to feed
40 to the combinators.  Furthermore, since the fixed points depend on
41 both the even function and the odd function, the combinators will need
42 to take two arguments, namely, both of the protofunctions:
44       even = X1 = Y1 protoeven protoodd
45       odd = X2 = Y2 protoeven protoodd
47 Writing protoeven and protoodd is easy.  Analogously to the ordinary
48 case, they will take as arguments the very fixed points we're looking for:
50       protoeven = \e o n . iszero n true (o (pred n))
51       protoodd = \e o n . iszero n false (e (pred n))
53 Notice that `protoeven` doesn't make use of its first argument.
54 Likewise, `protoodd` doesn't make use of its second argument.  This is
55 an expository weakness in the choice of the example, which is
56 particularly simple.
58 To convince yourself that these definitions of protoeven and protoodd
59 are correct, note that, for instance, `protoodd (Y protomonoeven) I 3
60 ~~> false`.  (We can get away with using `I` as one of the arguments,
61 since `protoeven` ignores its first argument.)
63 Ok, all that remains is writing `Y1` and `Y2`.  Let's look at ordinary
64 `Y` again:
66 <pre>
67 let Y = \f. (\h. f (h h)) (\h. f (h h))  in
68 </pre>
70 We know that `Y1` takes two argments, not just one, so we need to
71 start like this:
73     let Y1 = \pe po ...
75 where `pe` will be the protoeven function and `po` will be the
76 protoodd function.  Since everything in this excercise gets split into
77 two parts, let's guess that we'll need to versions of `h` as well,
78 `h1` and `h2`:
80     let Y1 = \pe po . (\h1 h2 . ...) (\h1 h2 . ...) (\h1 h2 . ...)
82 In the original, `h` was somehow *half* of the fixed point, so that `h
83 h` computed the fixed point.  In the schema here, `h1` had better be a
84 function which, when you give it suitable arguments, computes the
85 first fixed point `X1` (likewise for `h2` wrt the second fixed point
86 `X2`).
88 Then we can arrange for our definition to return the desired
89 fixed point like this:
91     let Y1 = \pe po . (\h1 h2 . pe (h1 [blah])(h2 [blah]))
92                       (\h1 h2 . ...)
93                       (\h1 h2 . ...)
95 The term in the middle line is going in for `h1`, so it had better
96 also be the kind of thing which, when you give it suitable arguments,
97 computes a fixed point for `pe`:
99     let Y1 = \pe po . (\h1 h2 . pe (h1 [blah]) (h2 [blah]))
100                       (\h1 h2 . pe (h1 [blah]) (h2 [blah]))
101                       (\h1 h2 . po (h1 [blah]) (h2 [blah]))
103 But the third line must help compute a fixed point for `po`.
105 All we need to do is figure out what the arguments to `h1` and `h2`
106 ought to be.  Final guess: in the original, `h` took one argument (a
107 copy of itself), so once again, here we'll need two arguments.  Here's
108 where the mutual recursion comes in: the two arguments to `h1` are a
109 copy of itself, and a copy of `h2` (symmetrically for `h2`).  So the
110 complete definition is
112     let Y1 = \pe po . (\h1 h2 . pe (h1 h1 h2) (h2 h1 h2))
113                       (\h1 h2 . pe (h1 h1 h2) (h2 h1 h2))
114                       (\h1 h2 . po (h1 h1 h2) (h2 h1 h2))
116 Naturally, `Y2` is the same except for the first line:
118     let Y2 = \pe po . (\h1 h2 . po (h1 h1 h2) (h2 h1 h2))
119                       (\h1 h2 . pe (h1 h1 h2) (h2 h1 h2))
120                       (\h1 h2 . po (h1 h1 h2) (h2 h1 h2))
122 Sure enough,
124     Y1 protoeven protoodd 3 ~~> false
126 So: what's a natural example in which both protofunctions need to call
127 both of their arguments?