Kleene fixed-point theorem

Remarks

Proof idea: $\bot \le f(\bot)$, and monotonicity gives $f^n(\bot) \le f^{n+1}(\bot)$ by induction, so the iterates form an increasing sequence with supremum $x$. Continuity gives $f(x) = \sup_n f^{n+1}(\bot) = x$. If $y$ is any fixed point, then $\bot \le y$ and induction gives $f^n(\bot) \le f^n(y) = y$, so $x \le y$. The same statement holds for a directed-complete partial order with least element and a Scott-continuous $f$. Example: on the power set of $\N$, the map $f(S) = \set{0} \cup \set{n + 2 : n \in S}$ preserves unions of increasing sequences. Its iterates from $\emptyset$ are $\set{0}$, $\set{0, 2}$, $\set{0, 2, 4}$, and so on, and their union, the even numbers, is the least fixed point. Continuity cannot be dropped from the formula: on the chain $\N \cup \set{\omega, \omega + 1}$, the monotone map with $f(n) = n + 1$, $f(\omega) = \omega + 1$ and $f(\omega + 1) = \omega + 1$ has least fixed point $\omega + 1$, while $\sup_n f^n(0) = \omega$.

Going deeper

For a student

The theorem is the main tool of denotational semantics, where recursive definitions are interpreted as least fixed points of continuous maps on domains. Compared with the Knaster–Tarski theorem, it needs less of the order, only suprema of increasing sequences, but more of the map, namely continuity, and it gives an explicit construction. For a monotone map that is not continuous, the iteration has to continue transfinitely, through $f^\omega(\bot) = \sup_n f^n(\bot)$, $f^{\omega + 1}(\bot)$, and so on, until it stabilises. In Datalog and in dataflow analysis on finite lattices, the iteration stops after finitely many steps.