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
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.
10 First, we define a recursive proto-function that takes the true
11 function (the fixed point) as an argument, then calls that argument.
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
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`.
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
33 even = \n . iszero n true (odd (pred n))
34 odd = \n . iszero n false (even (pred n))
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:
43 even = X1 = Y1 protoeven protoodd
44 odd = X2 = Y2 protoeven protoodd
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:
49 protoeven = \e o n . iszero n true (o (pred n))
50 protoodd = \e o n . iszero n false (e (pred n))
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
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.)
62 Ok, all that remains is writing `Y1` and `Y2`. Let's look at ordinary
66 let Y = \f. (\h. f (h h)) (\h. f (h h)) in
69 We know that `Y1` takes two argments, not just one, so we need to
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,
79 let Y1 = \pe po . (\h1 h2 . ...) (\h1 h2 . ...) (\h1 h2 . ...)
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:
88 let Y1 = \pe po . (\h1 h2 . pe (h1 [blah])(h2 [blah]))
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`:
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]))
100 But the third line must help compute a fixed point for `po`.
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
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))
113 Naturally, `Y2` is the same except for the first line:
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))
121 Y1 protoeven protoodd 3 ~~> false
123 So: what's a natural example in which both protofunctions need to call
124 both of their arguments?