3 #Q: How do you know that every term in the untyped lambda calculus has a fixed point?#
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).
9 <pre><code>let L = \x. T (x x) in
11 X ≡ L L ≡ (\x. T (x x)) L ~~> T (L L) ≡ T X
14 Please slow down and make sure that you understand what justified each
15 of the equalities in the last line.
17 #Q: How do you know that for any term `T`, `Y T` is a fixed point of `T`?#
19 A: Note that in the proof given in the previous answer, we chose `T`
20 and then set `X = L L = (\x. T (x x)) (\x. T (x x))`. If we abstract over
21 `T`, we get the Y combinator, `\T. (\x. T (x x)) (\x. T (x x))`. No matter
22 what argument `T` we feed `Y`, it returns some `X` that is a fixed point
23 of `T`, by the reasoning in the previous answer.
25 #Q: So if every term has a fixed point, even `Y` has fixed point.#
29 <pre><code>let Y = \T. (\x. T (x x)) (\x. T (x x)) in
30 Y Y ≡ \T. (\x. T (x x)) (\x. T (x x)) Y
31 ~~> (\x. Y (x x)) (\x. Y (x x))
32 ~~> Y ((\x. Y (x x)) (\x. Y (x x)))
33 ~~> Y (Y ((\x. Y (x x)) (\x. Y (x x))))
34 ~~> Y (Y (Y (...(Y (Y Y))...)))</code></pre>
37 #Q: Ouch! Stop hurting my brain.#
39 A: Is that a question?
41 Let's come at it from the direction of arithmetic. Recall that we
42 claimed that even `succ`---the function that added one to any
43 number---had a fixed point. How could there be an X such that X = X+1?
46 X <~~> succ X <~~> succ (succ X) <~~> succ (succ (succ (X))) <~~> succ (... (succ X)...)
48 In other words, the fixed point of `succ` is a term that is its own
49 successor. Let's just check that `X = succ X`:
51 <pre><code>let succ = \n s z. s (n s z) in
52 let X = (\x. succ (x x)) (\x. succ (x x)) in
54 ≡ succ ( (\x. succ (x x)) (\x. succ (x x)) )
55 ~~> succ (succ ( (\x. succ (x x)) (\x. succ (x x))))
59 You should see the close similarity with `Y Y` here.