From 5b4ffc8a2e702ee41d626737526d586ba5ad9b48 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sun, 19 Sep 2010 02:37:04 -0400 Subject: [PATCH] week3 tweaks Signed-off-by: Jim Pryor --- week3.mdwn | 85 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 81 insertions(+), 4 deletions(-) diff --git a/week3.mdwn b/week3.mdwn index 40bcb99c..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## -[TODO] +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,13 +251,13 @@ 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))) ) -- 2.11.0