LARA

Tarski's fixed point theorem

A complete lattice is a lattice where every set of elements $S$ has the least upper bound $\sqcup S$ and the greatest lower bound $\sqcap S$ (this implies that there is top and bottom as $\sqcup \emptyset = \bot$ and $\sqcap \emptyset = \top$.

(Note: if you know that you have least upper bounds for all sets, it follows that you also have greatest lower bounds, by taking the least upper bound of the lower bounds. Converse also holds, dually.)

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

Define

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

$\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}$.

Proof is amusing. Let $x$ range over elements of $\mbox{Post}$.

  • applying monotonic $G$ from $a \sqsubseteq x$ we get $G(a) \sqsubseteq G(x) \sqsubseteq x$
  • so $G(a)$ is a lower bound on $\mbox{Post}$, but $a$ is the greatest lower bound, so $G(a) \sqsubseteq a$
  • therefore $a \in \mbox{Post}$
  • $\mbox{Post}$ is closed under $G$, by monotonicity, so $G(a) \in \mbox{Post}$
  • $a$ is a lower bound on $\mbox{Post}$, so $a \sqsubseteq G(a)$
  • from $a \sqsubseteq G(a)$ and $G(a) \sqsubseteq a$ we have $a = G(a)$, so $a \in \mbox{Fix}$
  • $a$ is a lower bound on $\mbox{Post}$ so it is also a lower bound on a smaller set $\mbox{Fix}$

Dually, if $\mbox{Pre} = \{x \mid x \sqsubseteq G(x) \}$ the set of prefix points of $G$, then $\sqcup \mbox{Pre}$ is the largest element of $\mbox{Fix}$.

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}$.
To find this fixed point, we can start from $\bot$. Then the sequence $\bot \sqsubseteq G(\bot) \sqsubseteq G^2(\bot) \sqsubseteq \cdots$ will converge to the least fixed point if $G$ is $\omega$-continuous, i.e. if $G(\sqcup_{n \geq 0}x_n)=\sqcup_{n \geq 0}G(x_n)$.
In order to converge faster, we can use techniques such as widening.

More information: