Lab 04: QE, Lattices and Fixed points

Exercise 1

Recall the algorithm for quantifier elimination for Presburger arithmetic.

Use this algorithm to eliminate quantifiers in the following formula in Presburger arithmetic.

$\begin{equation*} \exists y. \exists x. x < -2 \wedge 1 - 5y < x \wedge 1 + y < 13x \end{equation*}$

Exercise 2

Prove the following:

$(x \sqcup y) \sqcup z = x \sqcup (y \sqcup z)$

$\sqcup A \sqsubseteq \sqcap B \ \Leftrightarrow \ \forall x \in A. \forall y \in B. x \sqsubseteq y$

Exercise 3

Let $(A,\sqsubseteq)$ be a partial order such that every set $S \subseteq A$ has the greatest lower bound.
Prove that then every set $S \subseteq A$ has the least upper bound.

Exercise 4

Let $C[0, 1]$ be the set of continuous functions from $[0, 1]$ to the reals. Define $\le$ on $C[0, 1]$ by $f \le g$ if and only if $f(a) \le g(a)$ for all $a \in [0, 1]$ . Show that $\le$ is a partial order and that $C[0, 1]$ with this order forms a lattice.

Exercise 5

Let $A = [0,1] = \{ x \in \mathbb{R} \mid 0 \le x \le 1 \}$ be the interval of real numbers. Recall that, by definition of real numbers and complete lattice, $(A,\le)$ is a complete lattice with least lattice element $0$ and greatest lattice element $1$ . Here $\sqcup$ is the least upper bound operator on sets of real numbers, also called supremum and denoted sup in real analysis.

Let function $f : A \to A$ be given by

$\begin{equation*} f(x) = \left\{\begin{array}{l} \frac{1}{2} + \frac{1}{4}x, \mbox{ if } x \in [0,\frac{2}{3}) \\ \ \\ \frac{3}{5} + \frac{1}{5}x, \mbox{ if } x \in [\frac{2}{3},1] \end{array}\right. \end{equation*}$

(It may help you to try to draw $f$ .)

Part a)

Prove that $f$ is monotonic and injective (so it is strictly monotonic).

Part b)

Compute the set of fixpoints of $f$ .

Part c)

Define $iter(x) = \sqcup \{ f^n(x) \mid n \in \{0,1,2,\ldots \}\}$ . (This is in fact equal to $\lim_{n\to\infty} f^n(x)$ when $f$ is a monotonic bounded function.)

Compute $iter(0)$ (prove that the computed value is correct by definition of $iter$ , that is, that the value is indeed $\sqcup$ of the set of values). Is $iter(0)$ a fixpoint of $f$ ? Is $iter(iter(0))$ a fixpoint of $f$ ? Is $f$ an $\omega$ -continuous function?