Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
sav08:tarski_s_fixpoint_theorem [2008/05/07 22:48] giuliano |
sav08:tarski_s_fixpoint_theorem [2008/05/07 22:50] giuliano |
||
|---|---|---|---|
| Line 50: | Line 50: | ||
| **Proof:**\\ | **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.\\ | 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.\\ | + | 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.\\ | 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$.\\ | 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$.\\ | ||