Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
tarski_fixed_point_theorem [2007/04/15 15:16] vkuncak |
tarski_fixed_point_theorem [2007/05/11 17:45] 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}$. | ||
| Line 25: | Line 25: | ||
| * $a$ is a lower bound on $\mbox{Post}$ so it is also a lower bound on a smaller set $\mbox{Fix}$ | * $a$ is a lower bound on $\mbox{Post}$ so it is also a lower bound on a smaller set $\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}$. | + | 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 | + | Tarski's Fixed Point theorem shows that in a complete lattice with a monotonic function $G$ on this lattice, there is at least one fixed point of $G$, namely the least fixed point $\sqcap \mbox{Post}$.\\ |
| - | [[http://bigcheese.math.sc.edu/~mcnulty/alglatvar/lat0.pdf|0]], | + | To find this fixed point, we can start from $\bot$. Then the sequence $\bot \sqsubseteq G(\bot) \sqsubseteq G^2(\bot) \sqsubseteq \cdots$ will converge to the least fixed point if $G$ is $\omega$-continuous, i.e. if $G(\sqcup_{n \geq 0}x_n)=\sqcup_{n \geq 0}G(x_n)$.\\ |
| - | [[http://bigcheese.math.sc.edu/~mcnulty/alglatvar/lat1.pdf|1]] | + | In order to converge faster, we can use techniques such as widening.\\ |
| + | |||
| + | More information: | ||
| + | * [[http://www.di.ens.fr/~cousot/COUSOTpapers/Tarski-79.shtml|Constructive proof using ordinals, by Cousot & Cousot]] | ||
| + | * [[http://129.3.20.41/eps/ge/papers/0305/0305001.pdf|A shorter constructive proof using ordinals]] | ||
| + | * 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]] | ||