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:

Computation of the least fixpoint of f(x) = 1/10x2+atan(x)+1 using Kleene's theorem in the real interval [0,7] with the usual order
Kleene Fixed-Point Theorem. Suppose is a directed-complete partial order (dcpo) with a least element, and let be a Scott-continuous (and therefore monotone) function. Then has a least fixed point, which is the supremum of the ascending Kleene chain of

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

where 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 [1] Moreover, Kleene Fixed-Point Theorem can be extended to monotone functions using transfinite iterations.[2]


We first have to show that the ascending Kleene chain of   exists in  . To show that, we prove the following:

Lemma. If   is a dcpo with a least element, and   is Scott-continuous, then  
Proof. We use induction:
  • Assume n = 0. Then   since   is the least element.
  • Assume n > 0. Then we have to show that  . By rearranging we get  . By inductive assumption, we know that   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:


From the definition of a dcpo it follows that   has a supremum, call it   What remains now is to show that   is the least fixed-point.

First, we show that   is a fixed point, i.e. that  . Because   is Scott-continuous,  , that is  . Also, since   and because   has no influence in determining the supremum we have:  . It follows that  , making   a fixed-point of  .

The proof that   is in fact the least fixed point can be done by showing that any element in   is smaller than any fixed-point of   (because by property of supremum, if all elements of a set   are smaller than an element of   then also   is smaller than that same element of  ). This is done by induction: Assume   is some fixed-point of  . We now prove by induction over   that  . The base of the induction   obviously holds:   since   is the least element of  . As the induction hypothesis, we may assume that  . We now do the induction step: From the induction hypothesis and the monotonicity of   (again, implied by the Scott-continuity of  ), we may conclude the following:   Now, by the assumption that   is a fixed-point of   we know that   and from that we get  

See alsoEdit


  1. ^ Alfred Tarski (1955). "A lattice-theoretical fixpoint theorem and its applications". Pacific Journal of Mathematics. 5:2: 285–309., page 305.
  2. ^ Patrick Cousot and Radhia Cousot (1979). "Constructive versions of Tarski's fixed point theorems". Pacific Journal of Mathematics. 82:1: 43–57.
  3. ^ Stoltenberg-Hansen, V.; Lindstrom, I.; Griffor, E. R. (1994). Mathematical Theory of Domains by V. Stoltenberg-Hansen. Cambridge University Press. pp. 24. doi:10.1017/cbo9781139166386. ISBN 0521383447.