tweaked week3

Signed-off-by: Jim Pryor <profjim@jimpryor.net>

diff --git a/week3.mdwn b/week3.mdwn
index c9e2675..40bcb99 100644 (file)
--- a/week3.mdwn
+++ b/week3.mdwn
@@ -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>