add Unreliable Guide OCaml Modules
[lambda.git] / topics / week4_fixed_point_combinators.mdwn
index ed22cff..a8d1a74 100644 (file)
@@ -178,6 +178,27 @@ Many simpler functions always *could* be defined using the resources we've so fa
 
 But functions like the Ackermann function require us to develop a more general technique for doing recursion --- and having developed it, it will often be easier to use it even in the cases where, in principle, we didn't have to.
 
+The example used to illustrate this in Chapter 9 of *The Little Schemer* is a function `looking` where:
+
+    (looking '(6 2 4 caviar 5 7 3))
+
+returns `#t`, because if we follow the path from the head of the list argument, `6`, to the sixth element of the list, `7` (the authors of that book count positions starting from 1, though generally Scheme follows the convention of counting positions starting from 0), and then proceed to the seventh element of the list, `3`, and then proceed to the third element of the list, `4`, and the proceed to the fourth element of the list, we find the `'caviar` we are looking for. On other hand, if we say:
+
+    (looking '(6 2 grits caviar 5 7 3))
+
+our path will take us from `6` to `7` to `3` to `grits`, which is not a number but not the `'caviar` we were looking for either. So this returns `#f`. It's not clear how to define such functions without recourse to something like `letrec` or `define`, or the techniques developed below (and also in that chapter of *The Little Schemer*).
+
+*The Little Schemer* also mentions the Ackermann function, as well as the interesting [[!wikipedia Collatz conjecture]]. They also point out that functions like their `looking` never return any value --- neither `#t` nor `#f` --- for some arguments, as in the example:
+
+    (looking '(7 1 2 caviar 5 6 3))
+
+Here our path takes us from `7` to `3` to `2` to `1` back to `7`, and the cycle repeats. So in this case, the `looking` function never returns any value.
+
+We've already tacitly been dealing with functions that we assumed to be defined only for expressions representing booleans, or only for expressions representing numbers. But in all such cases we could specify in advance what the intended domain of the function was. With examples like the above, it's not clear how to specify the domain in advance, in such a way that our function will still give a definite result for every argument in the domain. Instead, the capacity for fully general recursion brings with it also the downside that some functions will be only **partially defined**, even over restricted domains we're able to define in advance. We will see more extreme examples of this below.
+
+(Being only definable with the power of fully general recursion doesn't by itself render you only partially defined: the Ackermann function is total. The downside is rather that there's no way to let fully general recursion in, while limiting its use to just the cases where a definite value will be returned for every argument.)
+
+
 ## Using fixed-point combinators to define recursive functions ##
 
 ### Fixed points ###
@@ -258,6 +279,7 @@ it's not complete, since we don't know what value to use for the
 symbol `LENGTH`.  Technically, it has the status of an unbound
 variable.
 
+<a id=little-h></a>
 Imagine now binding the mysterious variable, and calling the resulting
 term `h`:
 
@@ -281,7 +303,7 @@ saying that we are looking for a fixed point for `h`:
 
     h LENGTH <~~> LENGTH
 
-Replacing `h` with its definition, we have
+Replacing `h` with its definition, we have:
 
     (\xs. (empty? xs) 0 (succ (LENGTH (tail xs)))) <~~> LENGTH
 
@@ -289,7 +311,17 @@ If we can find a value for `LENGTH` that satisfies this constraint, we'll
 have a function we can use to compute the length of an arbitrary list.
 All we have to do is find a fixed point for `h`.
 
-The strategy we will present will turn out to be a general way of
+Let's reinforce this. The left-hand side has the form:
+
+    (\body. Φ[...body...]) LENGTH
+
+which beta-reduces to:
+
+    Φ[...LENGTH...]
+
+where that whole formula is convertible with the term `LENGTH` itself. In other words, the term `Φ[...LENGTH...]` contains (a term that convertible with) itself --- despite being only finitely long. (If it had to contain a term *syntactically identical to* itself, this could not be achieved.)
+
+The key to achieving all this is finding a fixed point for `h`. The strategy we will present will turn out to be a general way of
 finding a fixed point for any lambda term.
 
 
@@ -304,7 +336,7 @@ work, but examining the way in which it fails will lead to a solution.
 
     h h <~~> \xs. (empty? xs) 0 (succ (h (tail xs)))
 
-The problem is that in the subexpression `h (tail list)`, we've
+The problem is that in the subexpression `h (tail xs)`, we've
 applied `h` to a list, but `h` expects as its first argument the
 length function.
 
@@ -319,7 +351,7 @@ to discuss generalizations of this strategy.)
 
 Shifting to `H` is the key creative step.  Instead of applying `u` to a list, as happened
 when we self-applied `h`, `H` applies its argument `u` first to *itself*: `u u`.
-After `u` gets an argument, the *result* is ready to apply to a list, so we've solved the problem noted above with `h (tail list)`.
+After `u` gets an argument, the *result* is ready to apply to a list, so we've solved the problem noted above with `h (tail xs)`.
 We're not done yet, of course; we don't yet know what argument `u` to give
 to `H` that will behave in the desired way.
 
@@ -487,6 +519,7 @@ Many fixed-point combinators have been discovered. (And as we've seen, some
 fixed-point combinators give us models for building infinitely many
 more, non-equivalent fixed-point combinators.)
 
+<a id=primed></a>
 Two of the simplest:
 
     Θ′ ≡ (\u h. h (\n. u u h n)) (\u h. h (\n. u u h n))
@@ -519,7 +552,7 @@ where `BODY` is equivalent to the very formula `\n. BODY n` that contains it. So
     BODY M <~~>
     ...
 
-You've written an infinite loop!
+You've written an infinite loop! (This is like the function `eternity` in Chapter 9 of *The Little Schemer*.)
 
 However, when we evaluate the application of our:
 
@@ -563,7 +596,7 @@ returns itself (a copy of `sink`); if the argument is boolean false
     sink true true false <~~> I
     sink true true true false <~~> I
 
-Evidently, then, `sink true <~~> sink`. So we want `sink` to be the fixed point
+To get this behavior, we want `sink` to be the fixed point
 of `\sink. \b. b sink I`. That is, `sink ≡ Y (\sb.bsI)`:
 
     1. sink false