Kleene fixed-point theorem: Difference between revisions

Content deleted Content added
Line 32:
First, we show that <math>m</math> is a fixed point. That is, we have to show that <math>f(m) = m</math>. Because <math>f</math> is [[Scott continuity|Scott-continuous]], <math>f(\sup(\mathbb{M})) = \sup(f(\mathbb{M}))</math>, that is <math>f(m) = \sup(f(\mathbb{M}))</math>. Also, <math>\sup(f(\mathbb{M})) = \sup(\mathbb{M})</math> (from the property of the chain) and from that <math>f(m) = m</math>, making <math>m</math> a fixed-point of <math>f</math>.
 
The proof that <math>m</math> is in fact the ''least'' fixed point can be done by contradiction.showing Assumethat any Element in <math>k\mathbb{M}</math> is asmaller than any fixed-point andof <math>kf</math>. This is done by induction: Assume <math>k</math> mis some fixed-point of <math>f</math>. ThenWe therenow hasproof toby beinduction anover <math>i</math> such that <math>k\forall =i \in \mathbb{N}\colon f^i(\bot) \sqsubseteq k</math>. For the induction start, we take <math>i = f(0</math>: <math>f^i0(\bot)) = \bot \sqsubseteq k</math>. Butobviously thanholds, for allsince <math>j \bot</math> iis the smallest element of <math>L</math>. As the resultinduction wouldhypothesis, neverwe bemay greaterassume thanthat <math>f^i(\bot) \sqsubseteq k</math>. We now do the induction step: From the induction hypothesis and sothe monotonicity of <math>mf</math> cannot(again, beimplied aby supremumthe Scott-continuity of <math>f</math>), we may conclude the following: <math>f^i(\mathbbbot) \sqsubseteq k ~\implies~ f^{Mi+1}(\bot) \sqsubseteq f(k)</math>. Now, whichby the assumption that <math>k</math> is a contradictionfixed-point of <math>f</math>, we know that <math>f(k) = k</math>, and from that we get <math>f^{i+1}(\bot) \sqsubseteq k</math>.
 
== See also ==