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 that takes the true
-function (the fixed point) as an argument, then calls that argument.
+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:
<pre>
let true = \y n . y in
</pre>
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 protoeven function,
-i.e., `X = Y protoeven`.
+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).
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 protofunction (`protoeven` and `protoodd`) to feed
+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:
odd = X2 = Y2 protoeven protoodd
Writing protoeven and protoodd is easy. Analogously to the ordinary
-case, they will take arguments that we want to find fixed points for:
+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 (the one
-that will eventually correspond to the even function itself). This is
+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.
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
+`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 . ...)
The term in the middle line is going in for `h1`, so it had better
-be the kind of thing which, when you give it suitable arguments,
+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]))
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, we'll need two arguments. Here's
+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