X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=bd3d8e5c6e0deac02d0954379f67b4d393ab2bc8;hp=077884cc0df70cfb962f2b03ffad70f121ca1f32;hb=ee659ed0921805be0db5de5658290b6dc1222eee;hpb=1bac07d66d424599f9a06d374cde4e2b904847a2
diff --git a/week4.mdwn b/week4.mdwn
index 077884cc..bd3d8e5c 100644
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -6,8 +6,7 @@ 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 L = \x. T (x x) in
+
``````
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
```

@@ -35,3 +34,28 @@ Y Y ≡ \T. (\x. T (x x)) (\x. T (x x)) Y
~~> Y (Y (Y (...(Y (Y Y))...)))

+#Q: Ouch! Stop hurting my brain.#
+
+A: Is that a question?
+
+Let's come at it from the direction of arithmetic. Recall that we
+claimed that even `succ`---the function that added one to any
+number---had a fixed point. How could there be an X such that X = X+1?
+That would imply that
+
+ X <~~> succ X <~~> succ (succ X) <~~> succ (succ (succ (X))) <~~> succ (... (succ X)...)
+
+In other words, the fixed point of `succ` is a term that is its own
+successor. Let's just check that `X = succ X`:
+
+```
let succ = \n s z. s (n s z) in
+let X = (\x. succ (x x)) (\x. succ (x x)) in
+succ X
+≡ succ ( (\x. succ (x x)) (\x. succ (x x)) )
+~~> succ (succ ( (\x. succ (x x)) (\x. succ (x x))))
+≡ succ (succ X)
+
```

+
+You should see the close similarity with `Y Y` here.
+
+