Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
tarski_fixed_point_theorem [2007/04/15 18:20] vkuncak |
tarski_fixed_point_theorem [2007/05/11 17:32] ghid.maatouk |
||
|---|---|---|---|
| Line 12: | Line 12: | ||
| $\mbox{Post} = \{x \mid G(x) \sqsubseteq x \}$ the set of postfix points of $G$ (e.g. $\top$ is a postfix point) | $\mbox{Post} = \{x \mid G(x) \sqsubseteq x \}$ the set of postfix points of $G$ (e.g. $\top$ is a postfix point) | ||
| - | $\mbox{Fix} = \{x \mid G(x) = x\}$ the set of fixed points of $G$ | + | $\mbox{Fix} = \{x \mid G(x) = x\}$ the set of fixed points of $G$. Note that $\mbox{Fix} \subseteq \mbox{Post}$. |
| **Theorem**: Let $a = \sqcap \mbox{Post}$. Then $a$ is the least element of $\mbox{Fix}$. | **Theorem**: Let $a = \sqcap \mbox{Post}$. Then $a$ is the least element of $\mbox{Fix}$. | ||