Lab 04: QE, Lattices and Fixed points
Recall the algorithm for quantifier elimination for Presburger arithmetic.
Use this algorithm to eliminate quantifiers in the following formula in Presburger arithmetic.
Prove the following:
Let be a partial order such that every set has the greatest lower bound.
Prove that then every set has the least upper bound.
Let be the set of continuous functions from to the reals. Define on by if and only if for all . Show that is a partial order and that with this order forms a lattice.
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 ? Is an -continuous function?