Kleene fixed-point theorem

<h2 id="proof">Proof</h2>
<p>Source:<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a>
</p><p>We first have to show that the ascending Kleene chain of 
  
    
      
        f
      
    
    {\displaystyle f}
  
 exists in 
  
    
      
        L
      
    
    {\displaystyle L}
  
. To show that, we prove the following:
</p>
Lemma. If 
  
    
      
        L
      
    
    {\displaystyle L}
  
 is a dcpo with a least element, and 
  
    
      
        f
        :
        L
        →
        L
      
    
    {\displaystyle f:L\to L}
  
 is Scott-continuous, then 
  
    
      
        
          f
          
            n
          
        
        (
        ⊥
        )
        ⊑
        
          f
          
            n
            +
            1
          
        
        (
        ⊥
        )
        ,
        n
        ∈
        
          
            N
          
          
            0
          
        
      
    
    {\displaystyle f^{n}(\bot )\sqsubseteq f^{n+1}(\bot ),n\in \mathbb {N} _{0}}

Proof. We use induction:
<ul><li>Assume n = 0. Then 
  
    
      
        
          f
          
            0
          
        
        (
        ⊥
        )
        =
        ⊥
        ⊑
        
          f
          
            1
          
        
        (
        ⊥
        )
        ,
      
    
    {\displaystyle f^{0}(\bot )=\bot \sqsubseteq f^{1}(\bot ),}
  
 since 
  
    
      
        ⊥
      
    
    {\displaystyle \bot }
  
 is the least element.</li>
<li>Assume n > 0. Then we have to show that 
  
    
      
        
          f
          
            n
          
        
        (
        ⊥
        )
        ⊑
        
          f
          
            n
            +
            1
          
        
        (
        ⊥
        )
      
    
    {\displaystyle f^{n}(\bot )\sqsubseteq f^{n+1}(\bot )}
  
. By rearranging we get 
  
    
      
        f
        (
        
          f
          
            n
            −
            1
          
        
        (
        ⊥
        )
        )
        ⊑
        f
        (
        
          f
          
            n
          
        
        (
        ⊥
        )
        )
      
    
    {\displaystyle f(f^{n-1}(\bot ))\sqsubseteq f(f^{n}(\bot ))}
  
. By inductive assumption, we know that 
  
    
      
        
          f
          
            n
            −
            1
          
        
        (
        ⊥
        )
        ⊑
        
          f
          
            n
          
        
        (
        ⊥
        )
      
    
    {\displaystyle f^{n-1}(\bot )\sqsubseteq f^{n}(\bot )}
  
 holds, and because f is monotone (property of Scott-continuous functions), the result holds as well.</li></ul>
<p>As a corollary of the Lemma we have the following directed ω-chain:
</p>

M
        
        =
        {
        ⊥
        ,
        f
        (
        ⊥
        )
        ,
        f
        (
        f
        (
        ⊥
        )
        )
        ,
        …
        }
        .
      
    
    {\displaystyle \mathbb {M} =\{\bot ,f(\bot ),f(f(\bot )),\ldots \}.}

<p>From the definition of a dcpo it follows that 
  
    
      
        
          M
        
      
    
    {\displaystyle \mathbb {M} }
  
 has a supremum, call it 
  
    
      
        m
        .
      
    
    {\displaystyle m.}
  
 What remains now is to show that 
  
    
      
        m
      
    
    {\displaystyle m}
  
 is the least fixed-point.
</p><p>First, we show that 
  
    
      
        m
      
    
    {\displaystyle m}
  
 is a fixed point, i.e. that 
  
    
      
        f
        (
        m
        )
        =
        m
      
    
    {\displaystyle f(m)=m}
  
. Because 
  
    
      
        f
      
    
    {\displaystyle f}
  
 is <a href="/facts/Scott_continuity/7CqoURj0">Scott-continuous</a>, 
  
    
      
        f
        (
        sup
        (
        
          M
        
        )
        )
        =
        sup
        (
        f
        (
        
          M
        
        )
        )
      
    
    {\displaystyle f(\sup(\mathbb {M} ))=\sup(f(\mathbb {M} ))}
  
, that is 
  
    
      
        f
        (
        m
        )
        =
        sup
        (
        f
        (
        
          M
        
        )
        )
      
    
    {\displaystyle f(m)=\sup(f(\mathbb {M} ))}
  
. Also, since 
  
    
      
        
          M
        
        =
        f
        (
        
          M
        
        )
        ∪
        {
        ⊥
        }
      
    
    {\displaystyle \mathbb {M} =f(\mathbb {M} )\cup \{\bot \}}
  
 and because 
  
    
      
        ⊥
      
    
    {\displaystyle \bot }
  
 has no influence in determining the supremum we have: 
  
    
      
        sup
        (
        f
        (
        
          M
        
        )
        )
        =
        sup
        (
        
          M
        
        )
      
    
    {\displaystyle \sup(f(\mathbb {M} ))=\sup(\mathbb {M} )}
  
. It follows that 
  
    
      
        f
        (
        m
        )
        =
        m
      
    
    {\displaystyle f(m)=m}
  
, making 
  
    
      
        m
      
    
    {\displaystyle m}
  
 a fixed-point of 
  
    
      
        f
      
    
    {\displaystyle f}
  
.
</p><p>The proof that 
  
    
      
        m
      
    
    {\displaystyle m}
  
 is in fact the <i>least</i> fixed point can be done by showing that any element in 
  
    
      
        
          M
        
      
    
    {\displaystyle \mathbb {M} }
  
 is smaller than any fixed-point of 
  
    
      
        f
      
    
    {\displaystyle f}
  
 (because by property of <a href="/facts/Supremum/oXCKVopz">supremum</a>, if all elements of a set 
  
    
      
        D
        ⊆
        L
      
    
    {\displaystyle D\subseteq L}
  
 are smaller than an element of 
  
    
      
        L
      
    
    {\displaystyle L}
  
 then also 
  
    
      
        sup
        (
        D
        )
      
    
    {\displaystyle \sup(D)}
  
 is smaller than that same element of 
  
    
      
        L
      
    
    {\displaystyle L}
  
). This is done by induction: Assume 
  
    
      
        k
      
    
    {\displaystyle k}
  
 is some fixed-point of 
  
    
      
        f
      
    
    {\displaystyle f}
  
. We now prove by induction over 
  
    
      
        i
      
    
    {\displaystyle i}
  
 that 
  
    
      
        ∀
        i
        ∈
        
          N
        
        :
        
          f
          
            i
          
        
        (
        ⊥
        )
        ⊑
        k
      
    
    {\displaystyle \forall i\in \mathbb {N} :f^{i}(\bot )\sqsubseteq k}
  
. The base of the induction 
  
    
      
        (
        i
        =
        0
        )
      
    
    {\displaystyle (i=0)}
  
 obviously holds: 
  
    
      
        
          f
          
            0
          
        
        (
        ⊥
        )
        =
        ⊥
        ⊑
        k
        ,
      
    
    {\displaystyle f^{0}(\bot )=\bot \sqsubseteq k,}
  
 since 
  
    
      
        ⊥
      
    
    {\displaystyle \bot }
  
 is the least element of 
  
    
      
        L
      
    
    {\displaystyle L}
  
. As the induction hypothesis, we may assume that 
  
    
      
        
          f
          
            i
          
        
        (
        ⊥
        )
        ⊑
        k
      
    
    {\displaystyle f^{i}(\bot )\sqsubseteq k}
  
. We now do the induction step: From the induction hypothesis and the monotonicity of 
  
    
      
        f
      
    
    {\displaystyle f}
  
 (again, implied by the Scott-continuity of 
  
    
      
        f
      
    
    {\displaystyle f}
  
), we may conclude the following: 
  
    
      
        
          f
          
            i
          
        
        (
        ⊥
        )
        ⊑
        k
         
        
        ⟹
        
         
        
          f
          
            i
            +
            1
          
        
        (
        ⊥
        )
        ⊑
        f
        (
        k
        )
        .
      
    
    {\displaystyle f^{i}(\bot )\sqsubseteq k~\implies ~f^{i+1}(\bot )\sqsubseteq f(k).}
  
 Now, by the assumption that 
  
    
      
        k
      
    
    {\displaystyle k}
  
 is a fixed-point of 
  
    
      
        f
        ,
      
    
    {\displaystyle f,}
  
 we know that 
  
    
      
        f
        (
        k
        )
        =
        k
        ,
      
    
    {\displaystyle f(k)=k,}
  
 and from that we get 
  
    
      
        
          f
          
            i
            +
            1
          
        
        (
        ⊥
        )
        ⊑
        k
        .
      
    
    {\displaystyle f^{i+1}(\bot )\sqsubseteq k.}

</p>
<h2 id="see-also">See also</h2>
<ul><li>Other <a href="/facts/Fixed-point_theorem/Jvkz4SUu">fixed-point theorems</a></li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>Alfred Tarski (1955). "A lattice-theoretical fixpoint theorem and its applications". Pacific Journal of Mathematics. 5:2: 285–309., page 305. <a href="http://projecteuclid.org/Dienst/UI/1.0/Summarize/euclid.pjm/1103044538" target="_blank">http://projecteuclid.org/Dienst/UI/1.0/Summarize/euclid.pjm/1103044538</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>Patrick Cousot and Radhia Cousot (1979). "Constructive versions of Tarski's fixed point theorems". Pacific Journal of Mathematics. 82:1: 43–57. <a href="https://projecteuclid.org/euclid.pjm/1102785059" target="_blank">https://projecteuclid.org/euclid.pjm/1102785059</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
<li id="fn:3"><p>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. <a href="0521383447" target="_blank">0521383447</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li>
</ol>

Kleene fixed-point theorem open-in-new

Kleene fixed-point theorem