From: Chris Barker Date: Sat, 2 Oct 2010 19:23:05 +0000 (-0400) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=276c8f5fcba4ed0b79225eece8fb3f269e98c385 edits --- diff --git a/week4.mdwn b/week4.mdwn index 47d9c34b..06581f01 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -9,9 +9,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 W = \x.T(xx) in
+let X = WW in
+X = WW = (\x.T(xx))W = T(WW) = TX
+
Q: How do you know that for any term T, YT is a fixed point of T?