Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:tarski_s_fixpoint_theorem [2008/04/30 09:51] vkuncak |
sav08:tarski_s_fixpoint_theorem [2008/05/06 23:44] giuliano |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Tarski's fixed point theorem ====== | ====== Tarski's fixed point theorem ====== | ||
| - | |||
| - | **Definition** A complete lattice is a [[Lattices|lattice]] where every set of elements $S$ has the least upper bound $\sqcup S$ and the greatest lower bound $\sqcap S$ | ||
| - | (this implies that there is top and bottom as $\sqcup \emptyset = \bot$ and $\sqcap \emptyset = \top$). | ||
| - | |||
| - | (Note: if you know that you have least upper bounds for all sets, it follows that you also have greatest lower bounds, by taking the least upper bound of the lower bounds. Converse also holds, dually.) | ||
| Let $(A,\sqsubseteq)$ be a complete lattice and $G : A \to A$ a monotonic function. | Let $(A,\sqsubseteq)$ be a complete lattice and $G : A \to A$ a monotonic function. | ||
| Line 51: | Line 46: | ||
| \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$. |
| 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. | ||