X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week3.mdwn;h=477284245c5f48b88919c6b2a24ee18d9bd7d57d;hp=26760eb0c1c360fa5d49139b7220ddc14c3b85c2;hb=aaadc20de94685e29c35abbd865e5f35d194e7b9;hpb=fb0fff30796bbcb9a393638b684bac82d25a3ffe diff --git a/week3.mdwn b/week3.mdwn index 26760eb0..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 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 @@ -134,9 +137,9 @@ 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(3,y) = 2^(y+3) -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 ... @@ -146,11 +149,90 @@ But functions like the Ackermann function require us to develop a more general t ##How to do recursion with lower-case omega## -... +Recall our initial, abortive attempt above to define the `get_length` function in the lambda calculus. We said "What we really want to do is something like this: + + \lst. (isempty lst) zero (add one (... (extract-tail lst))) + +where this very same formula occupies the `...` position." + +We are not going to exactly that, at least not yet. But we are going to do something close to it. + +Consider a formula of the following form (don't worry yet about exactly how we'll fill the `...`s): + + \h \lst. (isempty lst) zero (add one (... (extract-tail lst))) + +Call that formula `H`. Now what would happen if we applied `H` to itself? Then we'd get back: + + \lst. (isempty lst) zero (add one (... (extract-tail lst))) + +where any occurrences of `h` inside the `...` were substituted with `H`. Call this `F`. `F` looks pretty close to what we're after: a function that takes a list and returns zero if it's empty, and so on. And `F` is the result of applying `H` to itself. But now inside `F`, the occurrences of `h` are substituted with the very formula `H` we started with. So if we want to get `F` again, all we have to do is apply `h` to itself---since as we said, the self-application of `H` is how we created `F` in the first place. + +So, the way `F` should be completed is: + + \lst. (isempty lst) zero (add one ((h h) (extract-tail lst))) + +and our original `H` is: + + \h \lst. (isempty lst) zero (add one ((h h) (extract-tail lst))) + +The self-application of `H` will give us `F` with `H` substituted in for its free variable `h`. + +Instead of writing out a long formula twice, we could write: + + (\x. x x) LONG-FORMULA + +and the initial `(\x. x x)` is just what we earlier called the `ω` combinator (lower-case omega, not the non-terminating `Ω`). So the self-application of `H` can be written: + +
``ω (\h \lst. (isempty lst) zero (add one ((h h) (extract-tail lst))))``
``Ψ (\self. body)``
``Ψ (\self. BODY)``
using some fixed-point combinator `Ψ`. @@ -254,14 +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 combinators, 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))
-Θ′ 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′`? @@ -270,9 +352,9 @@ Indeed you can, getting the simpler:
``````Θ ≡ (\u f. f (u u f)) (\u f. f (u u f))
-I stated the more complex formulas for the following reason: in a language whose evaluation order is *call-by-value*, the evaluation of `Θ (\self. body)` and `Y (\self. body)` will in general not terminate. But evaluation of the eta-unreduced primed versions will. +I stated the more complex formulas for the following reason: in a language whose evaluation order is *call-by-value*, the evaluation of `Θ (\self. BODY)` and `Y (\self. BODY)` will in general not terminate. But evaluation of the eta-unreduced primed versions will. -Of course, if you define your `\self. body` stupidly, your formula will never terminate. For example, it doesn't matter what fixed point combinator you use for `Ψ` in: +Of course, if you define your `\self. BODY` stupidly, your formula will never terminate. For example, it doesn't matter what fixed point combinator you use for `Ψ` in:
``Ψ (\self. \n. self n)``