World Library  
Flag as Inappropriate
Email this Article

Kleene fixpoint theorem

Article Id: WHEBN0020928817
Reproduction Date:

Title: Kleene fixpoint theorem  
Author: World Heritage Encyclopedia
Language: English
Subject: Stephen Cole Kleene, Knaster–Tarski theorem, Complete partial order, Fixed-point theorem
Publisher: World Heritage Encyclopedia

Kleene fixpoint 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:

Let L be a complete partial order, and let f : L → L be a Scott-continuous (and therefore monotone) function. Then f has a least fixed point, which is the supremum of the ascending Kleene chain of f.

The ascending Kleene chain of f is the chain

\bot \; \le \; f(\bot) \; \le \; f\left(f(\bot)\right) \; \le \; \dots \; \le \; f^n(\bot) \; \le \; \dots

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

\textrm{lfp}(f) = \sup \left(\left\{f^n(\bot) \mid n\in\mathbb{N}\right\}\right)

where \textrm{lfp} denotes the least fixed point.

This result is often attributed to Alfred Tarski, but Tarski's fixed point theorem pertains to monotone functions on complete lattices.


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

Lemma 1:If L is CPO, and f : L → L is a Scott-continuous, then f^n(\bot) \le f^{n+1}(\bot), n \in \mathbb{N}_0

Proof by induction:

  • Assume n = 0. Then f^0(\bot) = \bot \leq f^1(\bot), since ⊥ is the least element.
  • Assume n > 0. Then we have to show that f^n(\bot) \leq f^{n+1}(\bot). By rearranging we get f(f^{n-1}(\bot)) \leq f(f^n(\bot)). By inductive assumption, we know that f^{n-1}(\bot) \leq f^n(\bot) holds, and because f is monotone (property of Scott-continuous functions), the result holds as well.

Immediate corollary of Lemma 1 is the existence of the chain.

Let \mathbb{M} be the set of all elements of the chain: \mathbb{M} = \{ \bot, f(\bot), f(f(\bot)), \ldots\}. This set is clearly directed due to Lemma 1. From definition of CPO follows that this set has a supremum, we will 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. That is, we have to show that f(m) = m. Because f is Scott-continuous, f(\sup(\mathbb{M})) = \sup(f(\mathbb{M})), that is f(m) = \sup(f(\mathbb{M})). Also, \sup(f(\mathbb{M})) = \sup(\mathbb{M}) (from the property of the chain) and from 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 \mathbb{M} is smaller than any fixed-point of f. This is done by induction: Assume k is some fixed-point of f. We now proof by induction over i that \forall i \in \mathbb{N}\colon f^i(\bot) \sqsubseteq k. For the induction start, we take i = 0: f^0(\bot) = \bot \sqsubseteq k obviously holds, since \bot is the smallest element of L. As the induction hypothesis, we may assume that f^i(\bot) \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(\bot) \sqsubseteq k ~\implies~ f^{i+1}(\bot) \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}(\bot) \sqsubseteq k.

See also

This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.

Copyright © World Library Foundation. All rights reserved. eBooks from Project Gutenberg are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.