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 that takes the true
11 function (the fixed point) as an argument, then calls that argument.
13 <pre>
14 let true = \y n . y in
15 let false = \y n . n in
16 let Y = \f. (\h. f (h h)) (\h. f (h h))  in
17 let iszero = \n. n (\x. false) true  in
18 let pred = \n s z. n (\u v. v (u s)) (K z) I  in
19 let protomonoeven = \e n . iszero n true (iszero (pred n) false (e (pred (pred n)))) in
20 Y protomonoeven 3
21 ~~> false
22 </pre>
24 So in the equation `X = Y T`, `X`, the function that computes whether
25 a number is even or not, is the fixed point of the protoeven function,
26 i.e., `X = Y protoeven`.
28 Obviously, we don't need mutual recursion to define the "even"
29 function (since we just defined it without mutual recursion).
30 But we *can* define it using mutual recursion, as shown in assignment
31 4:
33      even = \n . iszero n true (odd (pred n))
34      odd = \n . iszero n false (even (pred n))
36 Since we have two functions, we'll need two fixed points (`X1` and
37 `X2`), and therefore two fixed point combinators to compute them (`Y1`
38 and `Y2`), and two protofunction (`protoeven` and `protoodd`) to feed
39 to the combinators.  Furthermore, since the fixed points depend on
40 both the even function and the odd function, the combinators will need
41 to take two arguments, namely, both of the protofunctions:
43       even = X1 = Y1 protoeven protoodd
44       odd = X2 = Y2 protoeven protoodd
46 Writing protoeven and protoodd is easy.  Analogously to the ordinary
47 case, they will take arguments that we want to find fixed points for:
49       protoeven = \e o n . iszero n true (o (pred n))
50       protoodd = \e o n . iszero n false (e (pred n))
52 Notice that protoeven doesn't make use of its first argument (the one
53 that will eventually correspond to the even function itself).  This is
54 an expository weakness in the choice of the example, which is
55 particularly simple.
57 To convince yourself that these definitions of protoeven and protoodd
58 are correct, note that, for instance, `protoodd (Y protomonoeven) I 3
59 ~~> false`.  (We can get away with using `I` as one of the arguments,
60 since `protoeven` ignores its first argument.)
62 Ok, all that remains is writing `Y1` and `Y2`.  Let's look at ordinary
63 `Y` again:
65 <pre>
66 let Y = \f. (\h. f (h h)) (\h. f (h h))  in
67 </pre>
69 We know that `Y1` takes two argments, not just one, so we need to
70 start like this:
72     let Y1 = \pe po ...
74 where `pe` will be the protoeven function and `po` will be the
75 protoodd function.  Since everything in this excercise gets split into
76 two parts, let's guess that we'll need to versions of `h` as well,
77 `h1` and `h2`:
79     let Y1 = \pe po . (\h1 h2 . ...) (\h1 h2 . ...) (\h1 h2 . ...)
81 In the original, `h` was somehow *half* of the fixed point, so that `h
82 h` computed the fixed point.  In the schema here, `h1` had better be a
83 function which, when you give it suitable arguments, computes the
84 first fixed point `X1` (likewise for `h2` wrt the second fixed point
85 `X2`).  Then we can arrange for our definition to return the desired
86 fixed point like this:
88     let Y1 = \pe po . (\h1 h2 . pe (h1 [blah])(h2 [blah]))
89                       (\h1 h2 . ...)
90                       (\h1 h2 . ...)
92 The term in the middle line is going in for `h1`, so it had better
93 be the kind of thing which, when you give it suitable arguments,
94 computes a fixed point for `pe`:
96     let Y1 = \pe po . (\h1 h2 . pe (h1 [blah]) (h2 [blah]))
97                       (\h1 h2 . pe (h1 [blah]) (h2 [blah]))
98                       (\h1 h2 . po (h1 [blah]) (h2 [blah]))
100 But the third line must help compute a fixed point for `po`.
102 All we need to do is figure out what the arguments to `h1` and `h2`
103 ought to be.  Final guess: in the original, `h` took one argument (a
104 copy of itself), so once again, we'll need two arguments.  Here's
105 where the mutual recursion comes in: the two arguments to `h1` are a
106 copy of itself, and a copy of `h2` (symmetrically for `h2`).  So the
107 complete definition is
109     let Y1 = \pe po . (\h1 h2 . pe (h1 h1 h2) (h2 h1 h2))
110                       (\h1 h2 . pe (h1 h1 h2) (h2 h1 h2))
111                       (\h1 h2 . po (h1 h1 h2) (h2 h1 h2))
113 Naturally, `Y2` is the same except for the first line:
115     let Y2 = \pe po . (\h1 h2 . po (h1 h1 h2) (h2 h1 h2))
116                       (\h1 h2 . pe (h1 h1 h2) (h2 h1 h2))
117                       (\h1 h2 . po (h1 h1 h2) (h2 h1 h2))
119 Sure enough,
121     Y1 protoeven protoodd 3 ~~> false
123 So: what's a natural example in which both protofunctions need to call
124 both of their arguments?