+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 ++ +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: + +

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