Wikipedia / Kleene fixed-point theorem
Wikipedia / Kleene fixed-point theorem
In the mathematical areas of order and lattice theory, the Kleene fixed-point theorem, named after American mathematician Stephen Cole Kleene, states the following:
Kleene Fixed-Point Theorem. is a directed-complete partial order be a Scott-continuous (and therefore monotone) function has a least fixed point, which is the supremum
The ascending Kleene chain of f is the chain
obtained by iterating f on the least element ⊥ of L. Expressed in a formula, the theorem states that
denotes the least fixed point.
Although Tarski's fixed point theorem does not consider how fixed points can be computed by iterating f from some seed (also, it pertains to monotone functions on complete lattices), this result is often attributed to Alfred Tarski who proves it for additive functions. Moreover, the Kleene fixed-point theorem can be extended to monotone functions using transfinite iterations.
Proof
Source:
. To show that, we prove the following:
Lemma.
Proof. We use induction:
is the least element.
holds, and because f is monotone (property of Scott-continuous functions), the result holds as well.
As a corollary of the Lemma we have the following directed ω-chain:
is the least fixed-point.
is Scott-continuous.
is in fact the least (because by property of supremum
See also
Other fixed-point theorems
References