week4 debugging
[lambda.git] / week4.mdwn
1 [[!toc]]
2
3 #Q: How do you know that every term in the untyped lambda calculus has a fixed point?#
4
5 A: That's easy: let `T` be an arbitrary term in the lambda calculus.  If
6 `T` has a fixed point, then there exists some `X` such that `X <~~>
7 TX` (that's what it means to *have* a fixed point).
8
9 <pre><code>
10 let L = \x. T (x x) in
11 let X = L L in
12 X &equiv; L L &equiv; (\x. T (x x)) L ~~> T (L L) &equiv; T X
13 </code></pre>
14
15 Please slow down and make sure that you understand what justified each
16 of the equalities in the last line.
17
18 #Q: How do you know that for any term `T`, `Y T` is a fixed point of `T`?#
19
20 A: Note that in the proof given in the previous answer, we chose `T`
21 and then set `X = L L = (\x. T (x x)) (\x. T (x x))`.  If we abstract over
22 `T`, we get the Y combinator, `\T. (\x. T (x x)) (\x. T (x x))`.  No matter
23 what argument `T` we feed `Y`, it returns some `X` that is a fixed point
24 of `T`, by the reasoning in the previous answer.
25
26 #Q: So if every term has a fixed point, even `Y` has fixed point.#
27
28 A: Right:
29
30 <pre><code>let Y = \T. (\x. T (x x)) (\x. T (x x)) in
31 Y Y &equiv; \T. (\x. T (x x)) (\x. T (x x)) Y
32 ~~> (\x. Y (x x)) (\x. Y (x x))
33 ~~> Y ((\x. Y (x x)) (\x. Y (x x)))
34 ~~> Y (Y ((\x. Y (x x)) (\x. Y (x x))))
35 ~~> Y (Y (Y (...(Y (Y Y))...)))</code></pre>
36
37