Differences

This shows you the differences between two versions of the page.

--- sav08:tarski_s_fixpoint_theorem [2008/05/06 23:44]
giuliano
+++ sav08:tarski_s_fixpoint_theorem [2008/05/07 22:50]
giuliano
@@ 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}$.
 ===== Iterating Sequences and Omega Continuity =====
@@ Line 46: / Line 47: @@
 \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.