Differences

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

--- sav08:interval_analysis_and_widening [2008/05/20 19:53]
vkuncak
+++ sav08:interval_analysis_and_widening [2009/01/21 14:53]
vkuncak
@@ Line 40: / Line 40: @@
 \]
-Another approach: iterate a few times with $H_i$ only (without using $w$), if not a fixpoint at this program point, then widen.
+Approaches:
-  * This is not monotonic: if you start at fixpoint, it converges, if start below, can jump over fixpoint
+  * always apply widening (we will assume this)
+  * iterate a few times with $H_i$ only (without using $w$), if not a fixpoint at this program point, then widen.
+       * this is not monotonic: if you start at fixpoint, it converges, if start below, can jump over fixpoint
 Standard iteration: $\bot, \ldots, (F^{\#})^n(\bot), \ldots$
 Widening: $\bot, \ldots, ((W \circ F)^{\#})^n(\bot), \ldots$
-Narrowing: apply fixpoint iteration after widening to improve precision.
-Why will narrowing improve the result?
+Here, $x \sqsubseteq W(x)$ for all $x$ by definition of $W$
+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 $x_* \sqsubseteq y_*$ and
+\[
+    x_* = F^{\#}(x_*) \sqsubseteq F^{\#}(y_*) \sqsubseteq (W \circ F^{\#})(y_*) \sqsubseteq y_*
+\]