LARA

Tarski's fixed point theorem

Let $(A,\sqsubseteq)$ be a complete lattice and $G : A \to A$ a monotonic function.

Definition:

$\mbox{Post} = \{x \mid G(x) \sqsubseteq x \}$ - the set of postfix points of $G$ (e.g. $\top$ is a postfix point)

$\mbox{Pre} = \{x \mid x \sqsubseteq G(x) \}$ - the set of prefix points of $G$

$\mbox{Fix} = \{x \mid G(x) = x\}$ - the set of fixed points of $G$. Note that $\mbox{Fix} \subseteq \mbox{Post}$.

Theorem: Let $a = \sqcap \mbox{Post}$. Then $a$ is the least element of $\mbox{Fix}$ (dually, $\sqcup \mbox{Pre}$ is the largest element of $\mbox{Fix}$).

Proof.

In fact, the set of all fixpoints $\mbox{Fix}$ is a lattice itself.

Tarski's Fixed Point theorem shows that in a complete lattice with a monotonic function $G$ on this lattice, there is at least one fixed point of $G$, namely the least fixed point $\sqcap \mbox{Post}$.

Iterating Sequences and Omega Continuity

Tarski's theorem guarantees fixpoints in complete lattices, but the above proof does not say how to find them.

How difficult it is to find fixpoints depends on the structure of the lattice.

Let $G$ be a monotonic function on a lattice. Let $a_0 = \bot$ and $a_{n+1}=G(a_n)$. We obtain a sequence $\bot \sqsubseteq G(\bot) \sqsubseteq G^2(\bot) \sqsubseteq \cdots$. Let $a_* = \bigsqcup_{n \ge 0} a_n$.

Lemma: The value $a_*$ is a prefix point.

Observation: $a_*$ need not be a fixpoint (example in exercises, e.g. on lattice [0,1] of real numbers).

Definition: A function $G$ is $\omega$-continuous if for every chain $x_0 \sqsubseteq x_1 \sqsubseteq \ldots \sqsubseteq x_n \sqsubseteq \ldots$ we have

\begin{equation*} G(\bigsqcup_{i \ge 0} x_i) = \bigsqcup_{i \ge 0} G(x_i) \end{equation*}

Lemma: For an $\omega$-continuous function $G$, the value $a_* = \bigsqcup_{n \ge 0} G^n(\bot)$ is the least fixpoint of $G$.
Proof:
By definition of $\omega$-continuous we have $G(\bigsqcup_{n \ge 0} G^n(\bot)) = \bigsqcup_{n \ge 0} G^{n+1}(\bot)=\bigsqcup_{n \ge 1} G^n(\bot)$.
But $\bigsqcup_{n \ge 0} G^n(\bot) = \bigsqcup_{n \ge 1} G^n(\bot) \sqcup \bot = \bigsqcup_{n \ge 1} G^n(\bot)$ because $\bot$ is the least element of the lattice.
Thus $G(\bigsqcup_{n \ge 0} G^n(\bot)) = \bigsqcup_{n \ge 0} G^n(\bot)$ and $a_*$ is a fixpoint.
Now let's prove it is the least.
Let $c$ be such that $G(c)=c$. We want $\bigsqcup_{n \ge 0} G^n(\bot) \sqsubseteq c$. This is equivalent to $\forall n \in \mathbb N . G^n(\bot) \sqsubseteq c$.
We can prove this by induction : $\bot \sqsubseteq c$ and if $G^n(\bot) \sqsubseteq c$, then by monotonicity of $G$ and by definition of $c$ we have $G^{n+1}(\bot) \sqsubseteq G(c) \sqsubseteq c$.

When the function is not $\omega$-continuous, then we obtain $a_*$ as above (we jump over a discontinuity) and then continue iterating. We then take the limit of such sequence, and the limit of limits etc., ultimately we obtain the fixpoint.

References