Content deleted Content added
More specific hatnote |
Loewenheim (talk | contribs) f(M) = M \ {⊥} is not equivalent to M = f(M) ∪ {⊥} (consider the case of f = ⊥ const.) |
||
Line 34:
From the definition of a dcpo it follows that <math>\mathbb{M}</math> has a supremum, call it <math>m.</math> What remains now is to show that <math>m</math> is the least fixed-point.
First, we show that <math>m</math> is a fixed point, i.e. 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, since <math>
The proof that <math>m</math> is in fact the ''least'' fixed point can be done by showing that any element in <math>\mathbb{M}</math> is smaller than any fixed-point of <math>f</math> (because by property of [[supremum]], if all elements of a set <math>D \subseteq L</math> are smaller than an element of <math>L</math> then also <math>\sup(D)</math> is smaller than that same element of <math>L</math>). This is done by induction: Assume <math>k</math> is some fixed-point of <math>f</math>. We now prove by induction over <math>i</math> that <math>\forall i \in \mathbb{N}: f^i(\bot) \sqsubseteq k</math>. The base of the induction <math>(i = 0)</math> obviously holds: <math>f^0(\bot) = \bot \sqsubseteq k,</math> since <math>\bot</math> is the least element of <math>L</math>. As the induction hypothesis, we may assume that <math>f^i(\bot) \sqsubseteq k</math>. We now do the induction step: From the induction hypothesis and the monotonicity of <math>f</math> (again, implied by the Scott-continuity of <math>f</math>), we may conclude the following: <math>f^i(\bot) \sqsubseteq k ~\implies~ f^{i+1}(\bot) \sqsubseteq f(k).</math> Now, by the assumption that <math>k</math> is a fixed-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>
| |||