LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav07_lecture_22 [2007/06/14 22:50]
simon.blanchoud
sav07_lecture_22 [2008/05/21 01:17]
vkuncak
Line 43: Line 43:
  
 ===== Notion of set constraints ===== ===== Notion of set constraints =====
 +
  
 ==== Syntax ==== ==== Syntax ====
Line 52: Line 53:
 where $c$ is a constant, $v$ is a terminal (it can be a variable or function symbol), $f$ is an application function and $f^{-i}$ is the projection of th $i^{th}$ parameter of $f$. where $c$ is a constant, $v$ is a terminal (it can be a variable or function symbol), $f$ is an application function and $f^{-i}$ is the projection of th $i^{th}$ parameter of $f$.
  
-When using the set contraints as it is here we might encounter problems with the  substraction term ($\setminus$) as it is not monotonic. The problem ​is that monotonicity is needed in order to converge to a fixed point (and that is what we are looking for). +Note: set difference ​($\setminus$) as it is not monotonic, so its use is restricted if we want to ensure existence ​of solutions.
-  * Proof :  +
-    - In our lattice, we are trying ​to find a sequence ​of the type \[ \perp \sqsubseteq F(\perp) \sqsubseteq F(F(\perp)) \sqsubseteq ... \sqsubseteq F(x^*) = x^*  \] +
-    - We always have that $\perp \sqsubseteq F(\perp)$ as $\perp$ is by definition the lowest element of the lattice +
-    - But inferring from there $F(\perp) \sqsubseteq F(F(\perp))$ can be done only if $F$ is monotonic.+