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 .)
Part a)
Prove that is monotonic and injective (so it is strictly monotonic).
Part b)
Compute the set of fixpoints of .
Part c)
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
?