From: Jim Pryor Date: Sun, 29 May 2011 17:58:39 +0000 (-0400) Subject: assignment 4 hint 3 alt 2: how did this get deleted? X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=4a272d8c5fb04cb46905851c88b46bdb73dff415;hp=-c assignment 4 hint 3 alt 2: how did this get deleted? Signed-off-by: Jim Pryor --- 4a272d8c5fb04cb46905851c88b46bdb73dff415 diff --git a/hints/assignment_4_hint_3_alternate_2.mdwn b/hints/assignment_4_hint_3_alternate_2.mdwn new file mode 100644 index 00000000..a0ed78dc --- /dev/null +++ b/hints/assignment_4_hint_3_alternate_2.mdwn @@ -0,0 +1,127 @@ +This hint works all the way through constructing fixed-point +combinators that deliver fixed points for a pair of mutually-recursive +functions. So if you want to solve the problem yourself, as soon as +you begin to see what's going on, stop reading and work through the +rest on your own. + +Let's remind ourselves of how the ordinary Y combinator works, since +we're going to attack mutual recursion in the same way. + +First, we define a recursive proto-function called `protomonoeven` +that takes the true even function (the fixed point) as an argument, +then calls that argument: + +
+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?