一句话: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
回忆我们的目的:
- 构造一个修正函数 \(w\)
- \(w\circ t\) 单调,可以迭代求不动点
- \(w\circ t\) 的不动点应当停机(或更快停机)
- \(w\circ t\) 的不动点应当是 \(t\) 不动点的安全估计
这要求
- \(w\colon S\to S\)
- \(\forall x, y\in S, x\le y\Rightarrow w(x)\le w(y)\)
- \(w(S)=\Set{w(s)\mid s\in S}\) 尽可能小
- \(\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
怎么样,是不是非常简单呢?