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 that takes the true
  11 function (the fixed point) as an argument, then calls that argument.
  12
  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>
  23
  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`.
  27
  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:
  32
  33      even = \n . iszero n true (odd (pred n))
  34      odd = \n . iszero n false (even (pred n))
  35
  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:
  42
  43       even = X1 = Y1 protoeven protoodd
  44       odd = X2 = Y2 protoeven protoodd
  45
  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:
  48
  49       protoeven = \e o n . iszero n true (o (pred n))
  50       protoodd = \e o n . iszero n false (e (pred n))
  51
  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.
  56
  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.)
  61
  62 Ok, all that remains is writing `Y1` and `Y2`.  Let's look at ordinary
  63 `Y` again:
  64
  65 <pre>
  66 let Y = \f. (\h. f (h h)) (\h. f (h h))  in
  67 </pre>
  68
  69 We know that `Y1` takes two argments, not just one, so we need to
  70 start like this:
  71
  72     let Y1 = \pe po ...
  73
  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`:
  78
  79     let Y1 = \pe po . (\h1 h2 . ...) (\h1 h2 . ...) (\h1 h2 . ...)
  80
  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:
  87
  88     let Y1 = \pe po . (\h1 h2 . pe (h1 [blah])(h2 [blah]))
  89                       (\h1 h2 . ...)
  90                       (\h1 h2 . ...)
  91
  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`:
  95
  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]))
  99
 100 But the third line must help compute a fixed point for `po`.
 101
 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
 108
 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))
 112
 113 Naturally, `Y2` is the same except for the first line:
 114
 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))
 118
 119 Sure enough,
 120
 121     Y1 protoeven protoodd 3 ~~> false
 122
 123 So: what's a natural example in which both protofunctions need to call
 124 both of their arguments?