X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week3.mdwn;h=d9c536112218408d951f817641c7d8a5d45ac08f;hp=0129f2a957e3ef073760d70804d42afc8c7a33d4;hb=70fdac4d0a4db28dc391e3ea13b9c590b6ef9760;hpb=4d04ec1d56a71cce8cfce3aef6e39ef824ee63d8 diff --git a/week3.mdwn b/week3.mdwn index 0129f2a9..d9c53611 100644 --- a/week3.mdwn +++ b/week3.mdwn @@ -134,8 +134,8 @@ Some computable functions are just not definable in this way. The simplest funct | else -> A(m-1, A(m,n-1)) A(0,y) = y+1 - A(1,y) = y+2 - A(2,y) = 2y + 3 + A(1,y) = 2+(y+3) - 3 + A(2,y) = 2(y+3) - 3 A(3,y) = 2^(y+3) - 3 A(4,y) = 2^(2^(2^...2)) [where there are y+3 2s] - 3 ... @@ -333,16 +333,14 @@ Isn't that cool? ##Okay, then give me a fixed-point combinator, already!## -Many fixed-point combinators have been discovered. (And given a fixed-point combinator, there are ways to use it as a model to build infinitely many more, non-equivalent fixed-point combinators.) +Many fixed-point combinators have been discovered. (And some fixed-point combinators give us models for building infinitely many more, non-equivalent fixed-point combinators.) 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′`?