From: Jim Pryor
Date: Sun, 3 Oct 2010 02:41:39 +0000 (-0400)
Subject: start lambda_advanced
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=756f43f2529e362fdaab6831aa11cfa1c4beeaa5;hp=97ac6ce93d149beb471ad64da9e47e0416efbe82
start lambda_advanced
Signed-off-by: Jim Pryor
---
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
+
+