抽象解释中的 Galois 连接

伴随条件 ​

设 $(C,{\le }_C)$ 是具体性质格，$(A,{\le }_A)$ 是抽象域公理库抽象域Abstract domain · Domain of abstract properties用带精度次序和合流运算的抽象元素表示具体状态集合，为可靠静态近似提供语义空间。。两个单调映射公理库偏序集上的单调映射Monotone map on posets · Order-preserving map · Isotone map在偏序之间保持次序的映射，以及它作为单调算子参与不动点迭代时的基本结构。

$$\alpha :C\to A,\gamma :A\to C$$

构成 Galois connection，若对所有 $c\in C,a\in A$ 有

$$\alpha (c){\le }_{A}a⟺c{\le }_C\gamma (a).$$

$\alpha$ 是左伴随，选择能够覆盖具体性质 $c$ 的最精确抽象值；$\gamma$ 是右伴随，解释抽象值代表哪些具体行为。静态分析常取 $C=\mathcal{P}(\mathrm{\Sigma })$、${\le }_C=\subseteq$。

这个双条件比“$\alpha ,\gamma$ 大致互逆”精确得多。抽象会遗忘信息，一般不可能有 $\gamma \alpha (c)=c$；真正需要的是有方向的可靠外包络。

两条 unit/counit 不等式 ​

令 $a=\alpha (c)$ 代入伴随条件，可得

$$c{\le }_C\gamma (\alpha (c)).$$

具体性质先抽象再具体化不会漏掉原元素。令 $c=\gamma (a)$ 则得

$$\alpha (\gamma (a)){\le }_{A}a.$$

抽象值先解释再取最佳抽象，不会比原值更粗。两条不等式配合单调性推出 $\gamma \alpha$ 是具体格上的 closure operator：单调、extensive 且 idempotent。

若还满足 $\alpha \gamma =i{d}_A$，称为 Galois insertion；这表示抽象域没有两个不同元素拥有同一个 concrete meaning。它是更强性质，不是一般连接的定义。

符号域的最佳抽象 ​

具体域取整数幂集。抽象域含

$$\mathrm{\perp },\mathsf{neg},\mathsf{zero},\mathsf{pos},\mathsf{nonpos},\mathsf{nonneg},\mathrm{\top },$$

并按 concretization 的集合包含排序。$\gamma (\mathsf{nonneg})=\{n:n\ge 0\}$，其他元素类似。

对 $X=\{-3,-1\}$，覆盖它的最精确元素是 $\mathsf{neg}$；对 $X=\{-1,0\}$ 是 $\mathsf{nonpos}$；对 $X=\{-1,1\}$，若域没有 nonzero 元素，只能取 $\mathrm{\top }$。

于是 $\alpha (X)$ 不是给样本贴一个任意标签，而是在所有满足 $X\subseteq \gamma (a)$ 的 $a$ 中取最小者。若某个域对某些 $X$ 没有最小覆盖值，就不能由这份 concretization 自动得到左伴随。

最佳抽象变换 ​

给定具体单调变换 $f:C\to C$，其最佳抽象变换是

$$f^{\star }=\alpha \circ f\circ \gamma .$$

对抽象输入 $a$，先解释所有可能具体状态，执行精确变换，再取域内最精确覆盖。任何可靠抽象变换 $f^{\mathrm{\#}}:A\to A$ 都应满足

$$f^{\star }(a){\le }_A{f}^{\mathrm{\#}}(a).$$

“最佳”只相对于选定抽象域。若域不能表达变量关系，最佳区间或符号变换仍可能产生假警报；换更强域才会改变表达上限。

直接计算 $\alpha f\gamma$ 也可能与原具体语义一样昂贵。工程分析器常实现一个较粗但可计算的 $f^{\mathrm{\#}}$，然后单独证明它位于最佳抽象之上。

join 保存与边界 ​

左伴随 $\alpha$ 保存所有存在的 join，右伴随 $\gamma$ 保存所有 meet。这使分支合流可先在具体域取并再抽象，等于对各分支抽象后取 join。

反方向的运算一般不保存。若擅自假设 $\gamma (a\bigsqcup b)=\gamma (a)\cup \gamma (b)$，可能忽略抽象 join 为获得可表示性而加入的额外状态。

这里的 Galois connection 是序理论伴随，与域扩张、群作用和多项式可解性的 Galois 理论无关。名称共享历史来源，数学对象和证明责任完全不同。

参考资料

• Patrick Cousot and Radhia Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis,” POPL, 1977, pp. 238–252。
• Patrick Cousot and Radhia Cousot, “Systematic Design of Program Analysis Frameworks,” POPL, 1979, pp. 269–282。
• Flemming Nielson, Hanne Riis Nielson, and Chris Hankin, Principles of Program Analysis, Springer, 1999, Chs. 4–5。