LARA

This is an old revision of the document!

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

More information: