X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=f92ea169d4e09cc67c097cb104be303328dd607f;hp=78e2d37e8a4363b6ebe10e46baa2e0205148ab08;hb=9bd471a9af2e11b8490fe386f72270218333499c;hpb=21d0ff6296bd67c8828a6968b9e909078aa3aa67 diff --git a/week4.mdwn b/week4.mdwn index 78e2d37e..f92ea169 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -27,11 +27,13 @@ of `T`, by the reasoning in the previous answer. A: Right:
``````let Y = \T. (\x. T (x x)) (\x. T (x x)) in
-Y Y ≡ \T. (\x. T (x x)) (\x. T (x x)) Y
+Y Y
+≡   \T. (\x. T (x x)) (\x. T (x x)) Y
~~> (\x. Y (x x)) (\x. Y (x x))
~~> Y ((\x. Y (x x)) (\x. Y (x x)))
~~> Y (Y ((\x. Y (x x)) (\x. Y (x x))))
-~~> Y (Y (Y (...(Y (Y Y))...)))``````
+~~> Y (Y (Y (...(Y (Y Y))...))) + #Q: Ouch! Stop hurting my brain.# @@ -51,9 +53,9 @@ 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 ( (\x. succ (x x)) (\x. succ (x x)) )
~~> succ (succ ( (\x. succ (x x)) (\x. succ (x x)) ))
-≡ succ (succ X)
+≡   succ (succ X)
``````
You should see the close similarity with `Y Y` here. @@ -66,12 +68,12 @@ numeral:
``````[same definitions]
succ X
-≡ (\n s z. s (n s z)) X
-~~> \s z. s (X s z)
+≡    (\n s z. s (n s z)) X
+~~>  \s z. s (X s z)
<~~> succ (\s z. s (X s z)) ; using fixed-point reasoning
-≡ (\n s z. s (n s z)) (\s z. s (X s z))
-~~> \s z. s ((\s z. s (X s z)) s z)
-~~> \s z. s (s (X s z))
+≡    (\n s z. s (n s z)) (\s z. s (X s z))
+~~>  \s z. s ((\s z. s (X s z)) s z)
+~~>  \s z. s (s (X s z))
``````
So `succ X` looks like a numeral: it takes two arguments, `s` and `z`, @@ -109,17 +111,17 @@ endless reduction:
``````let prefact = \f n. iszero n 1 (mul n (f (pred n))) in
let fact = Y prefact in
fact 2
-≡ [(\f. (\x. f (x x)) (\x. f (x x))) prefact] 2
+≡   [(\f. (\x. f (x x)) (\x. f (x x))) prefact] 2
~~> [(\x. prefact (x x)) (\x. prefact (x x))] 2
~~> [prefact ((\x. prefact (x x)) (\x. prefact (x x)))] 2
~~> [prefact (prefact ((\x. prefact (x x)) (\x. prefact (x x))))] 2
-≡ [ (\f n. iszero n 1 (mul n (f (pred n)))) (prefact ((\x. prefact (x x)) (\x. prefact (x x))))] 2
+≡   [ (\f n. iszero n 1 (mul n (f (pred n)))) (prefact ((\x. prefact (x x)) (\x. prefact (x x))))] 2
~~> [\n. iszero n 1 (mul n ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred n)))] 2
~~> iszero 2 1 (mul 2 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred 2)))
~~> mul 2 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] 1)
...
~~> mul 2 (mul 1 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] 0))
-≡ mul 2 (mul 1 (iszero 0 1 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred 0))))
+≡   mul 2 (mul 1 (iszero 0 1 (mul 1 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred 0)))))
~~> mul 2 (mul 1 1)
~~> mul 2 1
~~> 2
``````