Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:tarski_s_fixpoint_theorem [2008/04/30 10:49] vkuncak |
sav08:tarski_s_fixpoint_theorem [2008/05/06 23:44] giuliano |
||
|---|---|---|---|
| Line 46: | 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. | ||