Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
tarski_fixed_point_theorem [2007/05/11 17:32]
ghid.maatouk
tarski_fixed_point_theorem [2007/05/11 17:45] (current)
ghid.maatouk
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}$.\\ 
 + 
 +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}$.\\ 
 +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)$.\\ 
 +In order to converge faster, we can use techniques such as widening.\\
  
 More information:​ More information:​
 
tarski_fixed_point_theorem.txt · Last modified: 2007/05/11 17:45 by ghid.maatouk
 
© EPFL 2018 - Legal notice