Kleene fixed-point theorem explained

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. Suppose

(L,\sqsubseteq)

is a directed-complete partial order (dcpo) with a least element, and let

f:L\toL

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

\bot\sqsubseteqf(\bot)\sqsubseteqf(f(\bot))\sqsubseteq … \sqsubseteqf^n(\bot)\sqsubseteq …

obtained by iterating f on the least element ⊥ of L. Expressed in a formula, the theorem states that

rm{lfp}(f)=\sup\left(\left\{f^n(\bot)\midn\inN\right\}\right)

where

rm{lfp}

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]

Proof^[3]

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

f:L\toL

is Scott-continuous, then

f^n(\bot)\sqsubseteqfⁿ⁺¹(\bot),n\inN₀

Proof. We use induction:

Assume n = 0. Then

f^0(\bot)=\bot\sqsubseteqf^1(\bot),

since

\bot

is the least element.

Assume n > 0. Then we have to show that

f^n(\bot)\sqsubseteqfⁿ⁺¹(\bot)

. By rearranging we get

f(f^n-1(\bot))\sqsubseteqf(f^n(\bot))

. By inductive assumption, we know that

f^n-1(\bot)\sqsubseteqf^n(\bot)

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:

M=\{\bot,f(\bot),f(f(\bot)),\ldots\}.

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

f(m)=m

. Because

is Scott-continuous,

f(\sup(M))=\sup(f(M))

, that is

f(m)=\sup(f(M))

. Also, since

M=f(M)\cup\{\bot\}

and because

\bot

has no influence in determining the supremum we have:

\sup(f(M))=\sup(M)

. It follows that

f(m)=m

, 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

D\subseteqL

are smaller than an element of

then also

\sup(D)

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

\foralli\inN:f^i(\bot)\sqsubseteqk

. The base of the induction

(i=0)

obviously holds:

f^0(\bot)=\bot\sqsubseteqk,

since

\bot

is the least element of

. As the induction hypothesis, we may assume that

f^i(\bot)\sqsubseteqk

. 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:

f^i(\bot)\sqsubseteqk~\implies~fⁱ⁺¹(\bot)\sqsubseteqf(k).

Now, by the assumption that

is a fixed-point of

we know that

f(k)=k,

and from that we get

fⁱ⁺¹(\bot)\sqsubseteqk.

Notes and References

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

Kleene fixed-point theorem explained

Proof[3]

See also

Notes and References

Proof^[3]