Kleene fixed-point theorem

Source:{{Cite book|title=Mathematical Theory of Domains by V. Stoltenberg-Hansen|last1=Stoltenberg-Hansen|first1=V.|last2=Lindstrom|first2=I.|last3=Griffor|first3=E. R.|publisher=Cambridge University Press|year=1994|isbn=0521383447|pages=[https://archive.org/details/mathematicaltheo0000stol/page/24 24]|language=en|doi=10.1017/cbo9781139166386|url=https://archive.org/details/mathematicaltheo0000stol/page/24}}

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

:Lemma. If $L$ is a dcpo with a least element, and $f:\; L\; \backslash to\; L$ is Scott-continuous, then $f^n(\backslash bot)\; \backslash sqsubseteq\; f^\{n+1\}(\backslash bot),\; n\; \backslash in\; \backslash mathbb\{N\}\_0$

:Proof. We use induction:

:* Assume n = 0. Then $f^0(\backslash bot)\; =\; \backslash bot\; \backslash sqsubseteq\; f^1(\backslash bot),$ since $\backslash bot$ is the least element.

:* Assume n > 0. Then we have to show that $f^n(\backslash bot)\; \backslash sqsubseteq\; f^\{n+1\}(\backslash bot)$. By rearranging we get $f(f^\{n-1\}(\backslash bot))\; \backslash sqsubseteq\; f(f^n(\backslash bot))$. By inductive assumption, we know that $f^\{n-1\}(\backslash bot)\; \backslash sqsubseteq\; f^n(\backslash 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:

:$\backslash mathbb\{M\}\; =\; \backslash \{\; \backslash bot,\; f(\backslash bot),\; f(f(\backslash bot)),\; \backslash ldots\backslash \}.$

From the definition of a dcpo it follows that $\backslash mathbb\{M\}$ has a supremum, call it $m.$ What remains now is to show that $m$ is the least fixed-point.

First, we show that $m$ is a fixed point, i.e. that $f(m)\; =\; m$. Because $f$ is Scott-continuous, $f(\backslash sup(\backslash mathbb\{M\}))\; =\; \backslash sup(f(\backslash mathbb\{M\}))$, that is $f(m)\; =\; \backslash sup(f(\backslash mathbb\{M\}))$. Also, since $\backslash mathbb\{M\}\; =\; f(\backslash mathbb\{M\})\backslash cup\backslash \{\backslash bot\backslash \}$ and because $\backslash bot$ has no influence in determining the supremum we have: $\backslash sup(f(\backslash mathbb\{M\}))\; =\; \backslash sup(\backslash mathbb\{M\})$. It follows that $f(m)\; =\; m$, making $m$ a fixed-point of $f$.

The proof that $m$ is in fact the least fixed point can be done by showing that any element in $\backslash mathbb\{M\}$ is smaller than any fixed-point of $f$ (because by property of supremum, if all elements of a set $D\; \backslash subseteq\; L$ are smaller than an element of $L$ then also $\backslash sup(D)$ is smaller than that same element of $L$). This is done by induction: Assume $k$ is some fixed-point of $f$. We now prove by induction over $i$ that $\backslash forall\; i\; \backslash in\; \backslash mathbb\{N\}:\; f^i(\backslash bot)\; \backslash sqsubseteq\; k$. The base of the induction $(i\; =\; 0)$ obviously holds: $f^0(\backslash bot)\; =\; \backslash bot\; \backslash sqsubseteq\; k,$ since $\backslash bot$ is the least element of $L$. As the induction hypothesis, we may assume that $f^i(\backslash bot)\; \backslash sqsubseteq\; k$. We now do the induction step: From the induction hypothesis and the monotonicity of $f$ (again, implied by the Scott-continuity of $f$), we may conclude the following: $f^i(\backslash bot)\; \backslash sqsubseteq\; k\; ~\backslash implies~\; f^\{i+1\}(\backslash bot)\; \backslash sqsubseteq\; f(k).$ Now, by the assumption that $k$ is a fixed-point of $f,$ we know that $f(k)\; =\; k,$ and from that we get $f^\{i+1\}(\backslash bot)\; \backslash sqsubseteq\; k.$

• Other fixed-point theorems

{{Reflist}}

Category:Order theory

Category:Fixed-point theorems