From c595c61a3fc33a2343e3ef906a382652c655d518 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sun, 19 Sep 2010 19:37:17 -0400 Subject: [PATCH] week3 tweak Signed-off-by: Jim Pryor --- week3.mdwn | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) 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′? -- 2.11.0