[[!toc]]
#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 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`, `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 = 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 (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))...)))
```