From ee659ed0921805be0db5de5658290b6dc1222eee Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sun, 3 Oct 2010 13:35:05 -0400 Subject: [PATCH] week4 debugging more Signed-off-by: Jim Pryor --- week4.mdwn | 28 ++++++++++++++++++++++++++-- 1 file changed, 26 insertions(+), 2 deletions(-) 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. + + -- 2.11.0