X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week3.mdwn;h=c9e26757dfac9cac8e94e7b8391f2045f8ed0cb0;hp=26760eb0c1c360fa5d49139b7220ddc14c3b85c2;hb=410a9889c779d960e4570c056833f7b3ba12a94a;hpb=fb0fff30796bbcb9a393638b684bac82d25a3ffe 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′
?