Differences
This shows you the differences between two versions of the page.
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. | + | |