X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week3.mdwn;h=613981d91931a9c443d58be975fe0335f3b5cc30;hp=26760eb0c1c360fa5d49139b7220ddc14c3b85c2;hb=5b4ffc8a2e702ee41d626737526d586ba5ad9b48;hpb=fb0fff30796bbcb9a393638b684bac82d25a3ffe diff --git a/week3.mdwn b/week3.mdwn index 26760eb0..613981d9 100644 --- a/week3.mdwn +++ b/week3.mdwn @@ -146,11 +146,88 @@ 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-termination Ω). So the self-application of `H` can be written: + +
ω (\h \lst. (isempty lst) zero (add one ((h h) (extract-tail lst))))
+ +and this will indeed implement the recursive function we couldn't earlier figure out how to define. + +In broad brush-strokes, `H` is half of the `get_length` function we're seeking, and H has the form: + + \h other-arguments. ... (h h) ... + +We get the whole `get_length` function by applying `H` to itself. Then `h` is replaced by the half `H`, and when we later apply `h` to itself, we re-create the whole `get_length` again. + +Now suppose you wanted to wrap this up in a pretty interface, so that the programmer didn't need to write `(h h)` but could just write `g` for some function `g`. How could you do it? + +Now the `F`-like expression we'd be aiming for---call it `F*`---would look like this: + + \lst. (isempty lst) zero (add one (g (extract-tail lst))) + +or, abbreviating: + + \lst. ...g... + +Here we have just a single `g` instead of `(h h)`. We'd want `F*` to be the result of self-applying some `H*`, and then binding to `g` that very self-application of `H*`. We'd get this if `H*` had the form: + + \h. (\g lst. ...g...) (h h) + +The self-application of `H*` would be: + + (\h. (\g lst. ...g...) (h h)) (\h. (\g lst. ...g...) (h h)) + +or: + + (\f. (\h. f (h h)) (\h. f (h h))) (\g lst. ...g...) + +The left-hand side of this is known as **the Y-combinator** and so this could be written more compactly as: + + Y (\g lst. ...g...) + +or, replacing the abbreviated bits: + + Y (\g lst. (isempty lst) zero (add one (g (extract-tail lst)))) + +So this is another way to implement the recursive function we couldn't earlier figure out how to define. + ##Generalizing## -In general, a **fixed point** of a function f is a value *x* such that fx is equivalent to *x*. For example, what is a fixed point of the function from natural numbers to their squares? What is a fixed point of the successor function? +Let's step back and fill in some theory to help us understand why these tricks work. + +In general, we call a **fixed point** of a function f any value *x* such that f x is equivalent to *x*. For example, what is a fixed point of the function from natural numbers to their squares? What is a fixed point of the successor function? In the lambda calculus, we say a fixed point of an expression `f` is any formula `X` such that: @@ -174,35 +251,35 @@ Moreover, the recipes that enable us to name fixed points for any given formula OK, so how do we make use of this? -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: +Recall again 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." -Now, what if we *were* somehow able to get ahold of this formula, as an additional argument? We could take that argument and plug it into the `...` position. Something like this: +If we could somehow get ahold of this formula, as an additional argument, then we could take the argument and plug it into the `...` position. Something like this: \self (\lst. (isempty lst) zero (add one (self (extract-tail lst))) ) This is an abstract of the form: - \self. body + \self. BODY -where `body` is the expression: +where `BODY` is the expression: \lst. (isempty lst) zero (add one (self (extract-tail lst))) containing an occurrence of `self`. -Now consider what would be a fixed point of our expression `\self. body`? That would be some expression `X` such that: +Now consider what would be a fixed point of our expression `\self. BODY`? That would be some expression `X` such that: - X <~~> (\self.body) X + X <~~> (\self.BODY) X Beta-reducing the right-hand side, we get: - X <~~> body [self := X] + X <~~> BODY [self := X] -Think about what this says. It says if you substitute `X` for `self` in our formula body: +Think about what this says. It says if you substitute `X` for `self` in our formula BODY: \lst. (isempty lst) zero (add one (X (extract-tail lst))) @@ -244,9 +321,9 @@ containing free occurrences of `self` that you treat as being equivalent to the \lst. (isempty lst) zero (add one (self (extract-tail lst))) -You bind the free occurrence of `self` as: `\self. body`. And then you generate a fixed point for this larger expression: +You bind the free occurrence of `self` as: `\self. BODY`. And then you generate a fixed point for this larger expression: -
Ψ (\self. body)
+
Ψ (\self. BODY)
using some fixed-point combinator Ψ. @@ -261,7 +338,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′? @@ -270,9 +349,9 @@ Indeed you can, getting the simpler: 
Θ ≡ (\u f. f (u u f)) (\u f. f (u u f))
 Y ≡ \f. (\u. f (u u)) (\u. f (u u))
-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)