X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=58d6bc38204bd3bcbf4afabe6d9c4306b82735de;hp=077884cc0df70cfb962f2b03ffad70f121ca1f32;hb=HEAD;hpb=1bac07d66d424599f9a06d374cde4e2b904847a2

diff --git a/week4.mdwn b/week4.mdwn
deleted file mode 100644
index 077884cc..00000000
--- a/week4.mdwn
+++ /dev/null
@@ -1,37 +0,0 @@
-[[!toc]]
-
-#Q: How do you know that every term in the untyped lambda calculus has a fixed point?#
-
-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).
-
-<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>
-
-Please slow down and make sure that you understand what justified each
-of the equalities in the last line.
-
-#Q: How do you know that for any term `T`, `Y T` is a fixed point of `T`?#
-
-A: Note that in the proof given in the previous answer, we chose `T`
-and then set `X = L L = (\x. T (x x)) (\x. T (x x))`.  If we abstract over
-`T`, we get the Y combinator, `\T. (\x. T (x x)) (\x. T (x x))`.  No matter
-what argument `T` we feed `Y`, it returns some `X` that is a fixed point
-of `T`, by the reasoning in the previous answer.
-
-#Q: So if every term has a fixed point, even `Y` has fixed point.#
-
-A: Right:
-
-<pre><code>let Y = \T. (\x. T (x x)) (\x. T (x x)) in
-Y Y &equiv; \T. (\x. T (x x)) (\x. T (x x)) Y
-~~> (\x. Y (x x)) (\x. Y (x x))
-~~> Y ((\x. Y (x x)) (\x. Y (x x)))
-~~> Y (Y ((\x. Y (x x)) (\x. Y (x x))))
-~~> Y (Y (Y (...(Y (Y Y))...)))</code></pre>
-
-