X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=bd3d8e5c6e0deac02d0954379f67b4d393ab2bc8;hp=edf9552d041ee41a2f1580a7a4987478c5e74cb5;hb=ee659ed0921805be0db5de5658290b6dc1222eee;hpb=1f5422bb82c42ac01506c66e21faea79e4872af3 diff --git a/week4.mdwn b/week4.mdwn index edf9552d..bd3d8e5c 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -1,167 +1,61 @@ [[!toc]] -#These notes return to the topic of fixed point combiantors for one more return to the topic of fixed point combinators# - -Q: How do you know that every term in the untyped lambda calculus has -a fixed point? +#Q: How do you know that every term in the untyped lambda calculus has a fixed point?# 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 L = \x. T (x x) in
+let X = L L in
+X ≡ L L ≡ (\x. T (x x)) L ~~> T (L L) ≡ T X
+``````
Please slow down and make sure that you understand what justified each of the equalities in the last line. -Q: How do you know that for any term `T`, `YT` is a fixed point of `T`? +#Q: How do you know that for any term `T`, `Y T` is a fixed point of `T`?# A: Note that in the proof given in the previous answer, we chose `T` -and then set `X = WW = (\x.T(xx))(\x.T(xx))`. If we abstract over -`T`, we get the Y combinator, `\T.(\x.T(xx))(\x.T(xx))`. No matter -what argument `T` we feed Y, it returns some `X` that is a fixed point +and then set `X = L L = (\x. T (x x)) (\x. T (x x))`. If we abstract over +`T`, we get the Y combinator, `\T. (\x. T (x x)) (\x. T (x x))`. No matter +what argument `T` we feed `Y`, it returns some `X` that is a fixed point of `T`, by the reasoning in the previous answer. -Q: So if every term has a fixed point, even `Y` has fixed point. +#Q: So if every term has a fixed point, even `Y` has fixed point.# A: Right: - let Y = \T.(\x.T(xx))(\x.T(xx)) in - Y Y = \T.(\x.T(xx))(\x.T(xx)) Y - = (\x.Y(xx))(\x.Y(xx)) - = Y((\x.Y(xx))(\x.Y(xx))) - = Y(Y((\x.Y(xx))(\x.Y(xx)))) - = Y(Y(Y(...(Y(YY))...))) +
``````let Y = \T. (\x. T (x x)) (\x. T (x x)) in
+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))...)))``````
```-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
-```
- -For instance, - - A 1 2 - = A 0 (A 1 1) - = A 0 (A 0 (A 1 0)) - = A 0 (A 0 (A 0 1)) - = A 0 (A 0 2) - = A 0 3 - = 4 - -A 1 x is to A 0 x as addition is to the successor function; -A 2 x is to A 1 x as multiplication is to addition; -A 3 x is to A 2 x as exponentiation is to multiplication--- -so A 4 x is to A 3 x as hyper-exponentiation is to exponentiation... +
``````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. +