X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week3.mdwn;h=39e472bf9a644c1bdac774790ed134f26ab7cf31;hp=f83d377c90296d304bacae0175c8459391bf8fdd;hb=399197e0af7c4b80f326be60ff2c0caae74b3687;hpb=7ee83a5cebdf94623bfce3edc2dfad4f93c79c9a diff --git a/week3.mdwn b/week3.mdwn index f83d377c..39e472bf 100644 --- a/week3.mdwn +++ b/week3.mdwn @@ -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. @@ -582,3 +591,50 @@ See Barwise and Etchemendy's 1987 OUP book, [The Liar: an essay on 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 +these results. Thinking again of the truth-teller paradox, yes, +Ω 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 (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 + + X <~~> I X + +for any choice of X whatsoever. + +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 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? + +One obstacle to thinking this through is the fact that a sentence +normally has only two truth values. We might consider instead a noun +phrase such as + +(3) the entity that this noun phrase refers to + +The reference of (3) depends on the reference of the embedded noun +phrase *this noun phrase*. It's easy to see that any object is a +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.