Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:interval_analysis_and_widening [2008/05/20 20:33] vkuncak |
sav08:interval_analysis_and_widening [2009/01/21 14:53] vkuncak |
||
---|---|---|---|
Line 54: | Line 54: | ||
Narrowing: after finding fixpoint of $(W \circ F)^{\#}$, apply $F^{\#}$ to improve precision. | Narrowing: after finding fixpoint of $(W \circ F)^{\#}$, apply $F^{\#}$ to improve precision. | ||
- | Observation: if $F^{\#}$ and $W$ are $\omega$-continuous functions and $x \sqsubseteq W(x)$ for all $x$, then narrowing will improve the result, that is, if $x_* = lfp (F^{\#})$ and $y_* = lfp (W \circ F^{\#})$, then | + | Observation: if $F^{\#}$ and $W$ are $\omega$-continuous functions and $x \sqsubseteq W(x)$ for all $x$, then narrowing will improve the result, that is, if $x_* = lfp (F^{\#})$ and $y_* = lfp (W \circ F^{\#})$, then $x_* \sqsubseteq y_*$ and |
\[ | \[ | ||
- | x_* = F(x_*) \sqsubseteq F^{\#}(y_*) \sqsubseteq (W \circ F^{\#})(y_*) \sqsubseteq y_* | + | x_* = F^{\#}(x_*) \sqsubseteq F^{\#}(y_*) \sqsubseteq (W \circ F^{\#})(y_*) \sqsubseteq y_* |
\] | \] | ||