author jim Sun, 22 Feb 2015 21:39:30 +0000 (16:39 -0500) committer Linux User Sun, 22 Feb 2015 21:39:30 +0000 (16:39 -0500)

index ca9ab64..41a5273 100644 (file)
@@ -297,7 +297,7 @@ which beta-reduces to:

Φ[...LENGTH...]

Φ[...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.)
+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.

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.
@@ -314,7 +314,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)))

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.

applied `h` to a list, but `h` expects as its first argument the
length function.

@@ -329,7 +329,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`.

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.

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.

@@ -573,7 +573,7 @@ returns itself (a copy of `sink`); if the argument is boolean false
sink true true false <~~> I
sink true true true false <~~> I

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
of `\sink. \b. b sink I`. That is, `sink ≡ Y (\sb.bsI)`:

1. sink false