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 ~~> falseSo 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:

let Y = \f. (\h. f (h h)) (\h. f (h h)) inWe 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?