author Jim Pryor Sun, 3 Oct 2010 17:35:05 +0000 (13:35 -0400) committer Jim Pryor Sun, 3 Oct 2010 17:35:05 +0000 (13:35 -0400)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>
 week4.mdwn patch | blob | history

index 077884c..bd3d8e5 100644 (file)
@@ -6,8 +6,7 @@ A: That's easy: let `T` be an arbitrary term in the lambda calculus.  If
`T` has a fixed point, then there exists some `X` such that `X <~~>
TX` (that's what it means to *have* a fixed point).

`T` has a fixed point, then there exists some `X` such that `X <~~>
TX` (that's what it means to *have* a fixed point).

-<pre><code>
-let L = \x. T (x x) in
+<pre><code>let L = \x. T (x x) in
let X = L L in
X &equiv; L L &equiv; (\x. T (x x)) L ~~> T (L L) &equiv; T X
</code></pre>
let X = L L in
X &equiv; L L &equiv; (\x. T (x x)) L ~~> T (L L) &equiv; T X
</code></pre>
@@ -35,3 +34,28 @@ Y Y &equiv; \T. (\x. T (x x)) (\x. T (x x)) Y
~~> Y (Y (Y (...(Y (Y Y))...)))</code></pre>

~~> Y (Y (Y (...(Y (Y Y))...)))</code></pre>

+#Q: Ouch!  Stop hurting my brain.#
+
+A: Is that a question?
+
+Let's come at it from the direction of arithmetic.  Recall that we
+claimed that even `succ`---the function that added one to any
+number---had a fixed point.  How could there be an X such that X = X+1?
+That would imply that
+
+    X <~~> succ X <~~> succ (succ X) <~~> succ (succ (succ (X))) <~~> succ (... (succ X)...)
+
+In other words, the fixed point of `succ` is a term that is its own
+successor.  Let's just check that `X = succ X`:
+
+<pre><code>let succ = \n s z. s (n s z) in
+let X = (\x. succ (x x)) (\x. succ (x x)) in
+succ X
+&equiv; succ ( (\x. succ (x x)) (\x. succ (x x)) )
+~~> succ (succ ( (\x. succ (x x)) (\x. succ (x x))))
+&equiv; succ (succ X)
+</code></pre>
+
+You should see the close similarity with `Y Y` here.
+
+