Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
tarski_fixed_point_theorem [2007/04/15 15:16] vkuncak |
tarski_fixed_point_theorem [2007/04/15 18:19] vkuncak |
||
|---|---|---|---|
| Line 27: | Line 27: | ||
| Dually, if $\mbox{Pre} = \{x \mid x \sqsubseteq G(x) \}$ the set of prefix points of $G$, then $\sqcup \mbox{Pre}$ is the largest element of $\mbox{Fix}$. | Dually, if $\mbox{Pre} = \{x \mid x \sqsubseteq G(x) \}$ the set of prefix points of $G$, then $\sqcup \mbox{Pre}$ is the largest element of $\mbox{Fix}$. | ||
| - | For (way) more details see J.B.Nation's notes | + | More information: |
| - | [[http://bigcheese.math.sc.edu/~mcnulty/alglatvar/lat0.pdf|0]], | + | * Constructive proof using ordinals, by Cousot & Cousot [[http://www.di.ens.fr/~cousot/COUSOTpapers/Tarski-79.shtml]] |
| - | [[http://bigcheese.math.sc.edu/~mcnulty/alglatvar/lat1.pdf|1]] | + | * A shorter constructive proof using ordinals, [[http://129.3.20.41/eps/ge/papers/0305/0305001.pdf]] |
| + | * Many more details on lattices: J.B.Nation's notes [[http://bigcheese.math.sc.edu/~mcnulty/alglatvar/lat0.pdf|0]], [[http://bigcheese.math.sc.edu/~mcnulty/alglatvar/lat1.pdf|1]] | ||