From 7b3b1c578a8c6d50c71ab570a1a49a1c3385ca62 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sun, 3 Oct 2010 13:00:22 -0400 Subject: [PATCH 1/1] proof of fixed points: W->L, be more specific about '=' Signed-off-by: Jim Pryor --- week4.mdwn | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/week4.mdwn b/week4.mdwn index e69832fd..5e219484 100644 --- 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). -
-let W = \x.T(xx) in
-let X = WW in
-X = WW = (\x.T(xx))W = T(WW) = TX
-
+

+let L = \x. T (x x) in
+let X = L L in
+X ≡ L L ≡ (\x. T (x x)) L ~~> T (L L) ≡ T X
+
Please slow down and make sure that you understand what justified each of the equalities in the last line. -- 2.11.0