X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week3.mdwn;h=477284245c5f48b88919c6b2a24ee18d9bd7d57d;hp=a1e79f5c0538e4d913d8e3e6360f908c8590cdfc;hb=aaadc20de94685e29c35abbd865e5f35d194e7b9;hpb=e9421d05c554e8abfa13c11eb62789d6c0a19d59 diff --git a/week3.mdwn b/week3.mdwn index a1e79f5c..47728424 100644 --- a/week3.mdwn +++ b/week3.mdwn @@ -126,7 +126,10 @@ With sufficient ingenuity, a great many functions can be defined in the same way ##However...## -Some computable functions are just not definable in this way. The simplest function that *simply cannot* be defined using the resources we've so far developed is the [[!wikipedia Ackermann function]]: +Some computable functions are just not definable in this way. We can't, for example, define a function that tells us, for whatever function `f` we supply it, what is the smallest integer `x` where `f x` is `true`. + +Neither do the resources we've so far developed suffice to define the +[[!wikipedia Ackermann function]]: A(m,n) = | when m == 0 -> n + 1 @@ -333,16 +336,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′`?