Introductory Example for Fixpoints
Let be the interval of real numbers. Recall that, by definition of real numbers and complete lattice, is a complete lattice with least lattice element and greatest lattice element . Here is the least upper bound operator on sets of real numbers, also called supremum and denoted sup in real analysis.
Let function be given by
(It may help you to try to draw .)
Prove that is monotonic and injective (so it is strictly monotonic).
Compute the set of fixpoints of .
Define . (This is in fact equal to when is a monotonic bounded function.)
Compute (prove that the computed value is correct by definition of , that is, that the value is indeed of the set of values). Is a fixpoint of ? Is a fixpoint of ?