Merge branch 'pryor'
[lambda.git] / week3.mdwn
index a55659c..39e472b 100644 (file)
@@ -1,3 +1,12 @@
+[[!toc]]
+
+##More on evaluation strategies##
+
+Here are notes on [[evaluation order]] that make the choice of which
+lambda to reduce next the selection of a route through a network of
+links.
+
+
 ##Computing the length of a list##
 
 How could we compute the length of a list? Without worrying yet about what lambda-calculus implementation we're using for the list, the basic idea would be to define this recursively:
@@ -415,7 +424,7 @@ to *the tail* of the list we were evaluating its application to at the previous
 
 ##Fixed-point Combinators Are a Bit Intoxicating##
 
-![tatoo](/y-combinator.jpg)
+![tatoo](/y-combinator-fixed.jpg)
 
 There's a tendency for people to say "Y-combinator" to refer to fixed-point combinators generally. We'll probably fall into that usage ourselves. Speaking correctly, though, the Y-combinator is only one of many fixed-point combinators.
 
@@ -583,11 +592,14 @@ truth and circularity](http://tinyurl.com/2db62bk) for an approach
 that is similar, but expressed in terms of non-well-founded sets
 rather than recursive functions.
 
-HOWEVER, you should be cautious about feeling too comfortable with
+##However...##
+
+You should be cautious about feeling too comfortable with
 these results.  Thinking again of the truth-teller paradox, yes,
-<code>&omega;</code> is *a* fixed point for `I`, and perhaps it has
+<code>&Omega;</code> is *a* fixed point for `I`, and perhaps it has
 some a privileged status among all the fixed points for `I`, being the
-one delivered by Y and all.
+one delivered by Y and all (though it is not obvious why Y should have
+any special status).
 
 But one could ask: look, literally every formula is a fixed point for
 `I`, since
@@ -600,7 +612,8 @@ So the Y combinator is only guaranteed to give us one fixed point out
 of infinitely many---and not always the intuitively most useful
 one. (For instance, the squaring function has zero as a fixed point,
 since 0 * 0 = 0, and 1 as a fixed point, since 1 * 1 = 1, but `Y
-(\x. mul x x)` doesn't give us 0 or 1.) So why in the reasoning we've
+(\x. mul x x)` doesn't give us 0 or 1.) So with respect to the
+truth-teller paradox, why in the reasoning we've
 just gone through should we be reaching for just this fixed point at
 just this juncture?
 
@@ -616,6 +629,12 @@ fixed point for this referential function: if this pen cap is the
 referent of *this noun phrase*, then it is the referent of (3), and so
 for any object.
 
+The chameleon nature of (3), by the way (a description that is equally
+good at describing any object), makes it particularly well suited as a
+gloss on pronouns such as *it*.  In the system of 
+[Jacobson 1999](http://www.springerlink.com/content/j706674r4w217jj5/),
+pronouns denote (you guessed it!) identity functions...
+
 Ultimately, in the context of this course, these paradoxes are more
 useful as a way of gaining leverage on the concepts of fixed points
 and recursion, rather than the other way around.