From 1bac07d66d424599f9a06d374cde4e2b904847a2 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sun, 3 Oct 2010 13:34:11 -0400 Subject: [PATCH 1/1] week4 debugging Signed-off-by: Jim Pryor --- week4.mdwn | 539 +------------------------------------------------------------ 1 file changed, 2 insertions(+), 537 deletions(-) diff --git a/week4.mdwn b/week4.mdwn index 11eea4cd..077884cc 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -6,7 +6,8 @@ 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

@@ -33,540 +34,4 @@ Y Y ≡ \T. (\x. T (x x)) (\x. T (x x)) Y
~~> Y (Y ((\x. Y (x x)) (\x. Y (x x))))
~~> 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)``````
```-A(m,n) =
-    | when m == 0 -> n + 1
-    | else when n == 0 -> A(m-1,1)
-    | else -> A(m-1, A(m,n-1))
-
-let A = Y (\A m n. iszero m (succ n) (iszero n (A (pred m) 1) (A (pred m) (A m (pred n))))) in
-```
``extract_fst ≡ \pair. pair (\x y. x)``