X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=week3.mdwn;h=c18048797f9a3874603fa8b3446e776c3e1ef166;hb=0075435e792b4c2ef1b718b695aebd016d2929a4;hp=892a055a39fa4b193c91914bd8442de1c0c0eac9;hpb=007ff95aa566224781dc275c590efec56cd53c96;p=lambda.git

diff --git a/week3.mdwn b/week3.mdwn
index 892a055a..c1804879 100644
--- a/week3.mdwn
+++ b/week3.mdwn
@@ -268,6 +268,8 @@ In the lambda calculus, we say a fixed point of an expression `f` is any formula
 
 What is a fixed point of the identity combinator I?
 
+What is a fixed point of the false combinator, KI?
+
 It's a theorem of the lambda calculus that every formula has a fixed point. In fact, it will have infinitely many, non-equivalent fixed points. And we don't just know that they exist: for any given formula, we can name many of them.
 
 Yes, even the formula that you're using the define the successor function will have a fixed point. Isn't that weird? Think about how it might be true.
@@ -427,3 +429,59 @@ then this is a fixed-point combinator:
 	L L L L L L L L L L L L L L L L L L L L L L L L L L
 
 
+##Watching Y in action##
+
+For those of you who like to watch ultra slow-mo movies of bullets
+piercing apples, here's a stepwise computation of the application of a
+recursive function.  We'll use a function `sink`, which takes one
+argument.  If the argument is boolean true (i.e., `\x y.x`), it
+returns itself (a copy of `sink`); if the argument is boolean false
+(`\x y. y`), it returns `I`.  That is, we want the following behavior:
+
+    sink false ~~> I
+    sink true false ~~> I
+    sink true true false ~~> I
+    sink true true true false ~~> I
+
+So we make `sink = Y (\f b. b f I)`: 
+
+    1. sink false 
+    2. Y (\fb.bfI) false
+    3. (\f. (\h. f (h h)) (\h. f (h h))) (\fb.bfI) false
+    4. (\h. [\fb.bfI] (h h)) (\h. [\fb.bfI] (h h)) false
+    5. [\fb.bfI] ((\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))) false
+    6. (\b.b[(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))]I)  false
+    7. false [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] I
+             --------------------------------------------
+    8. I
+
+So far so good.  The crucial thing to note is that as long as we
+always reduce the outermost redex first, we never have to get around
+to computing the underlined redex: because `false` ignores its first
+argument, we can throw it away unreduced.
+
+Now we try the next most complex example:
+
+    1. sink true false 
+    2. Y (\fb.bfI) true false
+    3. (\f. (\h. f (h h)) (\h. f (h h))) (\fb.bfI) true false
+    4. (\h. [\fb.bfI] (h h)) (\h. [\fb.bfI] (h h)) true false
+    5. [\fb.bfI] ((\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))) true false
+    6. (\b.b[(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))]I)  true false
+    7. true [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] I false
+    8. [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] false
+
+We've now arrived at line (4) of the first computation, so the result
+is again I.
+
+You should be able to see that `sink` will consume as many `true`s as
+we throw at it, then turn into the identity function after it
+encounters the first `false`. 
+
+The key to the recursion is that, thanks to Y, the definition of
+`sink` contains within it the ability to fully regenerate itself as
+many times as is necessary.  The key to *ending* the recursion is that
+the behavior of `sink` is sensitive to the nature of the input: if the
+input is the magic function `false`, the self-regeneration machinery
+will be discarded, and the recursion will stop.
+