Fixed Point Theorems

Theorem 1

Cor:
Def: A fixed pt combinator is a term such that for all

Note is a fixed point combinator. We can get fixed combinators such that

Def: Let and let .

Note

Theorem 2

Let then is a fixed pt combinator iff , i.e. is a fixed pt of .

so by def, is a fixed pt combinator.

If is a fixed pt combinator, then , so by abstraction

To see that notice that by Church-Rosser,

Since is closed, it must reduce to some and

QED