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)))
\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>Ψ (\self. body)</code></pre>
+<pre><code>Ψ (\self. BODY)</code></pre>
using some fixed-point combinator <code>Ψ</code>.
<pre><code>Θ ≡ (\u f. f (u u f)) (\u f. f (u u f))
Y ≡ \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>Θ (\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>Θ (\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>Ψ</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>Ψ</code> in:
<pre><code>Ψ (\self. \n. self n)</code></pre>