From 756f43f2529e362fdaab6831aa11cfa1c4beeaa5 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sat, 2 Oct 2010 22:41:39 -0400 Subject: [PATCH] start lambda_advanced Signed-off-by: Jim Pryor --- lambda_advanced.mdwn | 99 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 99 insertions(+) create mode 100644 lambda_advanced.mdwn diff --git a/lambda_advanced.mdwn b/lambda_advanced.mdwn new file mode 100644 index 00000000..dbdf9c89 --- /dev/null +++ b/lambda_advanced.mdwn @@ -0,0 +1,99 @@ +#Miscellaneous challenges and advanced topics, for untyped lambda calculus# + +1. How would you define an operation to reverse a list? (Don't peek at the +[[lambda_library]]! Try to figure it out on your own.) Choose whichever +implementation of list you like. Even then, there are various strategies you +can use. + + +2. An advantage of the v3 lists and v3 (aka "Church") numerals is that they + have a recursive capacity built into their skeleton. So for many natural + operations on them, you won't need to use a fixed point combinator. Why is + that an advantage? Well, if you use a fixed point combinator, then the terms + you get + won't be strongly normalizing: whether their reduction stops at a normal form + will depend on what evaluation order you use. Our online [[lambda evaluator]] + uses normal-order reduction, so it finds a normal form if there's one to be + had. But if you want to build lambda terms in, say, Scheme, and you wanted to + roll your own recursion as we've been doing, rather than relying on Scheme's + native `let rec` or `define`, then you can't use the fixed-point combinators + `Y` or `Θ`. Expressions using them will have non-terminating + reductions, with Scheme's eager/call-by-value strategy. There are other + fixed-point combinators you can use with Scheme (in the [[week 3]] notes they + were `Y′` and `Θ′`. But even with + those evaluation order still matters: for some (admittedly unusual) + evaluation strategies, expressions using them will also be non-terminating. + + The fixed-point combinators may be the conceptual heros. They are cool and + mathematically elegant. But for efficiency and implementation elegance, it's + best to know how to do as much as you can without them. (Also, that knowledge + could carry over to settings where the fixed point combinators are in + principle unavailable.) + + This is why the v3 lists and numbers are so lovely. However, one disadvantage + to them is that it's relatively inefficient to extract a list's tail, or get a + number's predecessor. To get the tail of the list [a;b;c;d;e], one will + basically be performing some operation that builds up the tail afresh: at + different stages, one will have built up [e], then [d;e], then [c;d;e], and + finally [b;c;d;e]. With short lists, this is no problem, but with longer lists + it takes longer and longer. And it may waste more of your computer's memory + than you'd like. Similarly for obtaining a number's predecessor. + + The v1 lists and numbers on the other hand, had the tail and the predecessor + right there as an element, easy for the taking. The problem was just that the + v1 lists and numbers didn't have recursive capacity built into them, in the + way the v3 implementations do. + + A clever approach would marry these two strategies. + + Version 3 makes the list [a; b; c; d; e] look like this: + + \f z. f a (f b (f c (f d (f e z)))) + + or in other words: + + \f z. f a + + Instead we could make it look like this: + + \f z. f a + + That is, now f is a function expecting *three* arguments: the head of the + current list, the tail of the current list, and the result of continuing to + fold f over the tail, with a given base value z. + + Call this a **version 4** list. The empty list could be the same: + + empty === \f z. z + + The list constructor would be: + + make_list === \h t. \f z. f h t (t f z) + + It differs from the version 3 `make_list` only in adding the extra argument + `t` to the new, outer application of `f`. + + Similarly, 5 as a v3 or Church numeral looks like this: + + \s z. s (s (s (s (s z)))) + + or in other words: + + \s z. s + + Instead we could make it look like this: + + \s z. s + + That is, now s is a function expecting *two* arguments: the predecessor of the + current number, and the result of continuing to apply s to the base value z + predecessor-many times. + + Jim had the pleasure of "inventing" these implementations himself. However, + unsurprisingly, he wasn't the first to do so. See for example [Oleg's report + on P-numerals](http://okmij.org/ftp/Computation/lambda-calc.html#p-numerals). + + +3. Implementing (self-balancing) trees + + -- 2.11.0