Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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