From: Jim Pryor Date: Sat, 18 Sep 2010 23:33:55 +0000 (-0400) Subject: tweaked week3 X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=03909143dfb0d0c4729ffde0f59a5cc7d470c9ad tweaked week3 Signed-off-by: Jim Pryor --- diff --git a/week3.mdwn b/week3.mdwn index c9e26757..40bcb99c 100644 --- 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: -
Ψ (\self. body)
+
Ψ (\self. BODY)
using some fixed-point combinator Ψ. @@ -272,9 +272,9 @@ Indeed you can, getting the simpler: 
Θ ≡ (\u f. f (u u f)) (\u f. f (u u f))
 Y ≡ \f. (\u. f (u u)) (\u. f (u u))
-I stated the more complex formulas for the following reason: in a language whose evaluation order is *call-by-value*, the evaluation of Θ (\self. body) 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 Θ (\self. BODY) 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 Ψ 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 Ψ in: 
Ψ (\self. \n. self n)