From a8f9da95c22c7bf21df81404cd9c3f5b2e73e6a7 Mon Sep 17 00:00:00 2001
From: Chris Barker
Date: Sun, 26 Sep 2010 17:59:24 -0400
Subject: [PATCH 1/1] edits
---
lambda_evaluator.mdwn | 2 +-
week3.mdwn | 58 +++++++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 59 insertions(+), 1 deletion(-)
diff --git a/lambda_evaluator.mdwn b/lambda_evaluator.mdwn
index 26de7109..4a5b9dc0 100644
--- a/lambda_evaluator.mdwn
+++ b/lambda_evaluator.mdwn
@@ -85,7 +85,7 @@ Object.prototype.error = function (message, t) {
// string = expr.to_string() + "\n\n~~>\n\n";
string = '';
eta = document.getElementById('ETA').checked;
- string = string + reduce(expr, eta, 1).to_string();
+ string = string + reduce(expr, eta, false).to_string();
} catch (e) {
string = JSON.stringify(e, ['name', 'message', 'from', 'to', 'key',
'value', 'arity', 'first', 'second', 'third', 'fourth'], 4);
diff --git a/week3.mdwn b/week3.mdwn
index 892a055a..45aa5b3d 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,
+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 (\fb.bfI):
+
+ 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.
+
--
2.11.0