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

index e69832f..5e21948 100644 (file)
@@ -6,11 +6,11 @@ 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>
-let W = \x.T(xx) in
-let X = WW in
-X = WW = (\x.T(xx))W = T(WW) = TX
-</pre>
+<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.

Please slow down and make sure that you understand what justified each
of the equalities in the last line.