SA03 narrowing & widening

一句话：Widening 和 Narrowing 分别提供了对格上数据流分析的加速trick和精度trick。

Widening

某些格无限高，迭代算法不一定停机（即便最小不动点存在）。

数学意义上（超穷构造）的存在并不意味着可以通过停机的算法构造，一个经典的例子是收敛数列的极限。

修改格抽象

朴实的想法是对于太高的格 \(S_h\)，作一个新的更实际的格抽象 \(S_l\)，通过一个简单函数翻译 \(w\colon S_h\to S_l\)

修改转移函数

另一个想法是让迭代的转移函数跑得快些，这样可以得到一个收敛但不太精确的解。对于原本的转移函数 \(t\)，构造一个修正函数 \(w\)，使得 \(w\circ f\) 的不动点更好算，并且 \(w\circ f\) 的不动点是 \(f\) 不动点的一个安全估计。

聪明的读者可以发现第二种方法中的 \(w\) 类型会是 \(S\to S\)，也是一个翻译函数

Requirements

回忆我们的目的：

1. 构造一个修正函数 \(w\)
2. \(w\circ t\) 单调，可以迭代求不动点
3. \(w\circ t\) 的不动点应当停机（或更快停机）
4. \(w\circ t\) 的不动点应当是 \(t\) 不动点的安全估计

这要求

1. \(w\colon S\to S\)
2. \(\forall x, y\in S, x\le y\Rightarrow w(x)\le w(y)\)
3. \(w(S)=\Set{w(s)\mid s\in S}\) 尽可能小
4. \(\forall x\in S, x\le w(x)\)，这样才有 \(\forall x\in S, t(x)\le w(t(x))\)

不妨记 \(f_t, f_w\) 分别为 \(t, w\circ t\) 的最小不动点

一个简单粗暴的实现是——截断。就像模拟信号到数字信号的采样一样，多余的部分直接提升到 \(\top\)，非常直观

于是就获得了一个 \(w\circ t\) 这样好算简单的新函数，对它迭代就得到了一个原函数不动点的安全估计

Narrowing

指的是得到 \(f_w\) 后，继续计算 \(t(f_w)\) 的过程

注意到 \(f_t=t(f_t)\le t(f_w)\le w(t(f_w))=f_w\)

这说明 \(t(f_w)\) 仍然是 \(f_t\) 的安全估计，但不会比 \(f_w\) 更大。

实际上这样的迭代是是单调不增的，即从 \(f_w\) 出发求一个尽可能小的不动点，但并不一定收敛（此处迭代的是 \(t\)）。

这个过程精度不断提升，属于 more pay more gain

怎么样，是不是非常简单呢？