proof of fixed points: W->L, be more specific about '='

[lambda.git] / week4.mdwn

diff --git a/week4.mdwn b/week4.mdwn
index e69832f..5e21948 100644 (file)
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -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.