author Jim Pryor Sat, 18 Sep 2010 23:33:55 +0000 (19:33 -0400) committer Jim Pryor Sat, 18 Sep 2010 23:33:55 +0000 (19:33 -0400)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>
 week3.mdwn patch | blob | history

index c9e2675..40bcb99 100644 (file)
@@ -186,23 +186,23 @@ Now, what if we *were* somehow able to get ahold of this formula, as an addition

This is an abstract of the form:

-       \self. body
+       \self. BODY

-where `body` is the expression:
+where `BODY` is the expression:

\lst. (isempty lst) zero (add one (self (extract-tail lst)))

containing an occurrence of `self`.

-Now consider what would be a fixed point of our expression `\self. body`? That would be some expression `X` such that:
+Now consider what would be a fixed point of our expression `\self. BODY`? That would be some expression `X` such that:

-       X <~~> (\self.body) X
+       X <~~> (\self.BODY) X

Beta-reducing the right-hand side, we get:

-       X <~~> body [self := X]
+       X <~~> BODY [self := X]

-Think about what this says. It says if you substitute `X` for `self` in our formula body:
+Think about what this says. It says if you substitute `X` for `self` in our formula BODY:

\lst. (isempty lst) zero (add one (X (extract-tail lst)))

@@ -244,9 +244,9 @@ containing free occurrences of `self` that you treat as being equivalent to the

\lst. (isempty lst) zero (add one (self (extract-tail lst)))

-You bind the free occurrence of `self` as: `\self. body`. And then you generate a fixed point for this larger expression:
+You bind the free occurrence of `self` as: `\self. BODY`. And then you generate a fixed point for this larger expression:

-<pre><code>&Psi; (\self. body)</code></pre>
+<pre><code>&Psi; (\self. BODY)</code></pre>

using some fixed-point combinator <code>&Psi;</code>.

@@ -272,9 +272,9 @@ Indeed you can, getting the simpler:
<pre><code>&Theta; &equiv; (\u f. f (u u f)) (\u f. f (u u f))
Y &equiv; \f. (\u. f (u u)) (\u. f (u u))</code></pre>

-I stated the more complex formulas for the following reason: in a language whose evaluation order is *call-by-value*, the evaluation of <code>&Theta; (\self. body)</code> and `Y (\self. body)` will in general not terminate. But evaluation of the eta-unreduced primed versions will.
+I stated the more complex formulas for the following reason: in a language whose evaluation order is *call-by-value*, the evaluation of <code>&Theta; (\self. BODY)</code> and `Y (\self. BODY)` will in general not terminate. But evaluation of the eta-unreduced primed versions will.

-Of course, if you define your `\self. body` stupidly, your formula will never terminate. For example, it doesn't matter what fixed point combinator you use for <code>&Psi;</code> in:
+Of course, if you define your `\self. BODY` stupidly, your formula will never terminate. For example, it doesn't matter what fixed point combinator you use for <code>&Psi;</code> in:

<pre><code>&Psi; (\self. \n. self n)</code></pre>