widening operator & narrowing operator

咸咸的海风吹起来初江一般的情愫，唤醒了新治本能的勇气。

考虑在 concrete domain 中的 while 的语义：

$$\mathbb{S}[while\;c\;do\;s]R=\mathbb{C}[\neg c](lfp\;F)\\ where\;F(X)=R\cup\mathbb{S}[s](\mathbb{C}[c]X)$$

其实就是在求状态集合上的算子$F$ 的最小不动点（lfp=least fixed point）。然后根据 tarski 不动点定理，对于递增链：

$$R\subseteq F(R)\subseteq F^2(R)\subseteq...$$

有$lfp\;F$ 就是 F 的不动点，即$F(lfp\;F)=lfp\;F$。一般求$lfp\;F$ 就是不断迭代 F，迭代次数就是循环执行的次数。

---

然后我们想在 abstract domain 中，不用迭代那么多步，就给出$lfp\;F$ 的一个 sound abstraction。这怎么办呢？我们其实可以定义一个新的二元算子类型$\triangledown$，它要求：

• $x\sqsubseteq^\# x\triangledown y,y\sqsubseteq^\# x\triangledown y$。
• 对于任意一个序列$\{x_n\},\exists N,y_N=y_{N+1}$。其中$y_n=x_0\triangledown x_1\triangledown ...\triangledown x_n$。

这就是 widening operator 的定义。

然后在 abstract domain 中，会对 while 的 abstract 语义进行定义：

$$\mathbb{S}^\#[while\;c\;do\;s]R^\#=\mathbb{C}^\#[\neg c](lim\;T^\#)\\ where\;T^\#(X^\#)=X^\#\triangledown F^\#(X^\#);\\ F^\#(X^\#)=_{def}R^\#\cup^\#\mathbb{S}^\#[s_2](\mathbb{C}^\#[c]X^\#)$$

注意到几个问题，首先是$lfp\;F$ 对应成了$lim\;F^\#$。其次原本求$X\mapsto F(X)$ 的最小不动点，现在对应成了$X^\#\mapsto X^\#\triangledown F^\#(X^\#)$ 迭代的极限。我们其实可以说明，$lim\;T^\#$就是$lfp\;F$ 的一个 sound abstraction，而且它一定存在（由 widening operator 的定义要求）。考虑如下序列：

$$X_1^\#=R^\#\\ X_2^\#=X_1^\#\triangledown F^\#(X_1^\#)\\ X_3^\#=X_2^\#\triangledown F^\#(X_2^\#)\\ X_4^\#=X_3^\#\triangledown F^\#(X_3^\#)\\ .....$$

发现根据 widening operator 的定义，有$X_1^\#\sqsubseteq^\# X_2^\#\sqsubseteq...$，即这是个递增链。再根据定义，它一定存在个极限：

$$X_{lim}^\#=X_{lim}^\#\triangledown F^\#(X_{lim}^\#)$$

所以再根据定义，有$F^\#(X_{lim}^\#)\sqsubseteq^\# X_{lim}^\#$。再根据 Tarskian fixpoint approximation：

(Tarskian fixpoint approximation) 给定完全格$(C,\leq,\vee,\wedge,\perp,\top)$ 上的一个单调函数$f:C\rightarrow C$，和它在偏序集$(A,\sqsubseteq)$ 上的一个 sound abstraction (不一定单调)$g:A\rightarrow A$，那么就会有对于所有满足$g(a)\sqsubseteq a$ 的$a$，它都是$lfp\;f$ 的一个 sound abstraction。即$lfp\;f\leq \gamma(a)$。

因为$F^\#$是$F$ 的一个 sound abstraction（每一个符号都是 sound 的），所以有$X_{lim}^\#$就是$lfp\;F$ 的一个 sound abstraction。

在实际选择中，我们可以任意选择满足要求的 widening operator，以 interval domain 举例，甚至可以$[a,b]\triangledown[c,d]=[-\infin,+\infin]$。这样只需要迭代一次就找到了$X_{lim}^\#=[-\infin,+\infin]$，它显然是$lfp\;F$ 的 sound abstraction（它是任何$\mathcal{P}(\mathbb{I})$ 中元素的 sound abstraction）。但是显然这没什么意义，所以我们一般选择：

$$[a,b]\triangledown[c,d]=[\begin{cases}a&if\;a\leq c\\-\infin&otherwise\end{cases},\begin{cases}b&if\;b\leq d\\+\infin&otherwise\end{cases}]$$

这样只需要$O(|\mathbb{V}|)$ 次迭代我们就能找到$X_{lim}^\#$。

---

但是这是不够的。因为即使我们精心选择了 widening operator，可以得到$lfp\;F$ 的一个 sound abstraction，但它往往不够 precise。其实我们可以有一个提纯的过程（refine），即保持是 sound abstraction 的情况下，找到尽量小的那个。于是我们可以定义 narrowing operator：$\triangle$，要求它：

• $X^\#\sqcap^\# Y^\#\sqsubseteq^\# X^\#\triangle Y^\#\sqsubseteq^\# X^\#$。
• 对于任意一个序列$\{X_n^\#\},\exists N,Y_N^\#=Y_{N+1}^\#$。其中$Y_n^\#=X_0^\#\triangle...\triangle X_n^\#$。

它有什么作用呢？我们考虑一个迭代：$X^\#\mapsto X^\#\triangle F^\#(X^\#)$。

• 首先，它是保持 sound abstraction 的。假如$X^\#$是$lfp\;F$ 的一个 sound abstraction，那么有$lfp\;F\subseteq \gamma(X^\#)$。根据 F 的单调性，有$F(lfp\;F)\subseteq F(\gamma(X^\#))$。再根据$F^\#$是 F 的一个 sound abstraction，就有：

  $$lfp\;F=F(lfp\;F)\subseteq F(\gamma(X^\#))\subseteq\gamma(F^\#(X^\#))$$

  于是$F^\#(X^\#)$ 就是$lfp\;F$ 的一个 sound abstraction。然后我们可以证明：若$X^\#$，$F^\#(X^\#)$ 都是$lfp\;F$ 的 sound abstraction，那么$X^\#\triangle F^\#(X^\#)$ 也一定是$lfp\;F$ 的一个 sound abstraction。因为：

  $$\because lfp\;F\subseteq\gamma(X^\#),lfp\;F\subseteq\gamma(F^\#(X^\#))\\ \therefore lfp\;F\subseteq \gamma(X^\#)\cap\gamma(F^\#(X^\#))\subseteq \gamma(X^\#\sqcap^\#F^\#(X^\#))\subseteq \gamma(X^\#\triangle F^\#(X^\#))$$

• 其次，它是单调减的，因为有$X^\#\triangle F^\#(X^\#)\sqsubseteq^\# X^\#$。

因此，我们可以不断迭代，直到不再变化。这样迭代的过程就是 refine 的过程（譬如不断缩小 interval），而且最后得到的 abstraction 一定仍然是 sound 的。

我们譬如可以选择：

$$[a,b]\triangle[c,d]=[\begin{cases}c&if\;a=-\infin\\a&otherwise\end{cases},\begin{cases}d&if\;b=+\infin\\b&otherwise\end{cases}]$$

就满足了上述要求。

---

所以总之，迭代 widening operator 是为了尽快找到$lfp\;F$ 的一个 sound abstraction；而找到后可以接着迭代 narrowing operator 对我们找到的 sound abstraction 进行提纯，使得最后得到的 abstraction 尽量 precise。