hints/assignment_4_hint_3_alternate_2.mdwn

   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.
   6
   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.
   9
  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:
  13
  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>
  24
  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`.
  28
  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:
  33
  34      even = \n . iszero n true (odd (pred n))
  35      odd = \n . iszero n false (even (pred n))
  36
  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:
  43
  44       even = X1 = Y1 protoeven protoodd
  45       odd = X2 = Y2 protoeven protoodd
  46
  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:
  49
  50       protoeven = \e o n . iszero n true (o (pred n))
  51       protoodd = \e o n . iszero n false (e (pred n))
  52
  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.
  57
  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.)
  62
  63 Ok, all that remains is writing `Y1` and `Y2`.  Let's look at ordinary
  64 `Y` again:
  65
  66 <pre>
  67 let Y = \f. (\h. f (h h)) (\h. f (h h))  in
  68 </pre>
  69
  70 We know that `Y1` takes two argments, not just one, so we need to
  71 start like this:
  72
  73     let Y1 = \pe po ...
  74
  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`:
  79
  80     let Y1 = \pe po . (\h1 h2 . ...) (\h1 h2 . ...) (\h1 h2 . ...)
  81
  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`).
  87
  88 Then we can arrange for our definition to return the desired
  89 fixed point like this:
  90
  91     let Y1 = \pe po . (\h1 h2 . pe (h1 [blah])(h2 [blah]))
  92                       (\h1 h2 . ...)
  93                       (\h1 h2 . ...)
  94
  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`:
  98
  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]))
 102
 103 But the third line must help compute a fixed point for `po`.
 104
 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
 111
 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))
 115
 116 Naturally, `Y2` is the same except for the first line:
 117
 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))
 121
 122 Sure enough,
 123
 124     Y1 protoeven protoodd 3 ~~> false
 125
 126 So: what's a natural example in which both protofunctions need to call
 127 both of their arguments?