X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=bd3d8e5c6e0deac02d0954379f67b4d393ab2bc8;hp=e01db2e857d5550eee64aa84f99860658b2fea47;hb=ee659ed0921805be0db5de5658290b6dc1222eee;hpb=72af25c790aaa979710ffc2b7fab823ffaf94b05 diff --git a/week4.mdwn b/week4.mdwn index e01db2e8..bd3d8e5c 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -6,297 +6,56 @@ 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.# 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
-```
``````let succ = \n s z. s (n s z) in