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/05/06 23:44] giuliano |
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_* = \bigsqcup_{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. | ||