From 410a9889c779d960e4570c056833f7b3ba12a94a Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sat, 18 Sep 2010 19:32:14 -0400 Subject: [PATCH] tweaked week3 Signed-off-by: Jim Pryor --- week3.mdwn | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/week3.mdwn b/week3.mdwn index 26760eb0..c9e26757 100644 --- a/week3.mdwn +++ b/week3.mdwn @@ -146,7 +146,7 @@ But functions like the Ackermann function require us to develop a more general t ##How to do recursion with lower-case omega## -... +[TODO] ##Generalizing## @@ -261,7 +261,9 @@ 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`. + +`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