From: Jim Pryor Date: Sun, 19 Sep 2010 23:37:17 +0000 (-0400) Subject: week3 tweak X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=c595c61a3fc33a2343e3ef906a382652c655d518 week3 tweak Signed-off-by: Jim Pryor --- diff --git a/week3.mdwn b/week3.mdwn index 5d05c700..d9c53611 100644 --- a/week3.mdwn +++ b/week3.mdwn @@ -340,9 +340,7 @@ Two of the simplest: 
Θ′ ≡ (\u f. f (\n. u u f n)) (\u f. f (\n. u u f n))
 Y′ ≡ \f. (\u. f (\n. u u n)) (\u. f (\n. u u n))
-Θ′ has the advantage that f (Θ′ f) really *reduces to* Θ′ f. - -f (Y′ f) is only convertible with Y′ f; that is, there's a common formula they both reduce to. For most purposes, though, either will do. +Θ′ has the advantage that f (Θ′ f) really *reduces to* Θ′ f. Whereas f (Y′ f) is only *convertible with* Y′ f; that is, there's a common formula they both reduce to. For most purposes, though, either will do. You may notice that both of these formulas have eta-redexes inside them: why can't we simplify the two `\n. u u f n` inside Θ′ to just `u u f`? And similarly for Y′?