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/07 22:48] giuliano |
sav08:tarski_s_fixpoint_theorem [2009/03/26 10:36] vkuncak |
||
|---|---|---|---|
| Line 40: | 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 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$.\\ | ||