Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:tarski_s_fixpoint_theorem [2008/04/30 10:49] vkuncak |
sav08:tarski_s_fixpoint_theorem [2009/03/26 10:36] vkuncak |
||
---|---|---|---|
Line 28: | Line 28: | ||
Tarski's Fixed Point theorem shows that in a complete lattice with a monotonic function $G$ on this lattice, there is at least one fixed point of $G$, namely the least fixed point $\sqcap \mbox{Post}$. | Tarski's Fixed Point theorem shows that in a complete lattice with a monotonic function $G$ on this lattice, there is at least one fixed point of $G$, namely the least fixed point $\sqcap \mbox{Post}$. | ||
+ | |||
===== Iterating Sequences and Omega Continuity ===== | ===== Iterating Sequences and Omega Continuity ===== | ||
Line 39: | Line 40: | ||
**Lemma:** The value $a_*$ is a prefix point. | **Lemma:** The value $a_*$ is a prefix point. | ||
- | Observation: $a_*$ need not be a fixpoint. | + | Observation: $a_*$ need not be a fixpoint (example in exercises, e.g. on lattice [0,1] of real numbers). |
**Definition:** A function $G$ is $\omega$-continuous if for every chain $x_0 \sqsubseteq x_1 \sqsubseteq \ldots \sqsubseteq x_n \sqsubseteq \ldots$ we have | **Definition:** A function $G$ is $\omega$-continuous if for every chain $x_0 \sqsubseteq x_1 \sqsubseteq \ldots \sqsubseteq x_n \sqsubseteq \ldots$ we have | ||
Line 46: | Line 47: | ||
\end{equation*} | \end{equation*} | ||
- | **Lemma:** For an $\omega$-continuous function $G$, the value $a_* = \bigcup_{n \ge 0} G^n(\bot)$ is the least fixpoint of $G$. | + | **Lemma:** For an $\omega$-continuous function $G$, the value $a_* = \bigsqcup_{n \ge 0} G^n(\bot)$ is the least fixpoint of $G$.\\ |
+ | **Proof:**\\ | ||
+ | By definition of $\omega$-continuous we have $G(\bigsqcup_{n \ge 0} G^n(\bot)) = \bigsqcup_{n \ge 0} G^{n+1}(\bot)=\bigsqcup_{n \ge 1} G^n(\bot)$.\\ But $\bigsqcup_{n \ge 0} G^n(\bot) = \bigsqcup_{n \ge 1} G^n(\bot) \sqcup \bot = \bigsqcup_{n \ge 1} G^n(\bot)$ because $\bot$ is the least element of the lattice.\\ | ||
+ | Thus $G(\bigsqcup_{n \ge 0} G^n(\bot)) = \bigsqcup_{n \ge 0} G^n(\bot)$ and $a_*$ is a fixpoint.\\ | ||
+ | Now let's prove it is the least.\\ | ||
+ | Let $c$ be such that $G(c)=c$. We want $\bigsqcup_{n \ge 0} G^n(\bot) \sqsubseteq c$. This is equivalent to $\forall n \in \mathbb N . G^n(\bot) \sqsubseteq c$.\\ | ||
+ | We can prove this by induction : $\bot \sqsubseteq c$ and if $G^n(\bot) \sqsubseteq c$, then by monotonicity of $G$ and by definition of $c$ we have $G^{n+1}(\bot) \sqsubseteq G(c) \sqsubseteq c$. | ||
When the function is not $\omega$-continuous, then we obtain $a_*$ as above (we jump over a discontinuity) and then continue iterating. We then take the limit of such sequence, and the limit of limits etc., ultimately we obtain the fixpoint. | When the function is not $\omega$-continuous, then we obtain $a_*$ as above (we jump over a discontinuity) and then continue iterating. We then take the limit of such sequence, and the limit of limits etc., ultimately we obtain the fixpoint. |