A proof-theoretic approach to abstract interpretation

技术摘要：抽象解释的证明论方法

问题陈述
抽象解释是形式化程序验证的基础理论，旨在生成程序语义的可靠近似，以解决不可判定或计算上难以处理的问题。传统上，该理论通过一对伴随映射将复杂的具体模型（例如程序执行集的幂集 $P(\Sigma)$）与有限抽象格 $A$ 联系起来：具体化映射 $\gamma$ 和抽象映射 $\alpha$。尽管抽象解释与逻辑之间的联系自该理论创立之初便已得到认可，但直到最近才得到系统化。先前的工作（例如 [5]、[3]）引入了抽象的“内部逻辑”概念，并确定了特定抽象背后的逻辑。然而，为任意抽象生成内部逻辑及其相应证明系统的通用、程序化方法仍然是一个未解决的挑战。

方法论
作者提出了一种通用过程，用于生成与有限抽象 $A = (A, \sqsubseteq, Op_A)$ 相对应的逻辑 $L_A$，其中包含具体化映射 $\gamma: A \to (P(\text{Struct}), \subseteq, Op_c)$。该方法构建逻辑，使其林登鲍姆 - 塔尔斯基代数同构于抽象代数 $A$。构建过程遵循以下步骤：

1. 连接词：$L_A$ 的逻辑连接词定义为那些被具体化映射 $\gamma$ 保持的操作。如果 $A$ 是有限分配格，则它是一个双 Heyting 代数，这使得蕴涵和共蕴涵成为可用的候选连接词。
2. 谓词：对于 $A$ 中的每个元素 $a$，向语言中添加一个一元谓词符号 $a(x)$。
3. 引入规则：对于每个被 $\gamma$ 保持的连接词，向证明系统中添加适当的引入规则。
4. 公理规则：
   • 对于二元连接词 $\star$，若 $a \star b = c$，则添加规则 $a(x) \star b(x) \dashv\vdash c(x)$。
   • 对于一元连接词 $\star$，若 $\star a = b$，则添加规则 $\star a(x) \dashv\vdash b(x)$。
   • 对于序关系，若 $a \leq b$，则添加规则 $a(x) \vdash b(x)$。

作者承认，由于公理中可能存在冗余，该过程是“朴素的”且计算效率低下，但强调其适用于任何有限格和具体化映射。

主要结果与理论发现
本文确立了关于所构建逻辑 $L_A$ 的三个主要引理：

• 可靠性（引理 1）：逻辑 $L_A$ 相对于具体化 $\gamma$ 是可靠的。这是通过对证明深度进行归纳来证明的，依赖于 $\gamma$ 保持连接词以及公理反映具体代数中关系的事实。
• 同构性（引理 2）：$L_A$ 的林登鲍姆 - 塔尔斯基代数 $L$ 同构于抽象代数 $A$。映射 $e: A \to L$ 定义为 $e(a) = [a(x)]$（谓词的等价类），被证明是满射、单射的序嵌入且为同态。
• 完备性（引理 3）：如果 $\gamma$ 是序嵌入，则 $L_A$ 相对于具体化是完备的。这一结果通过放宽条件（从 $\gamma$ 是单射右伴随减弱为仅仅是序嵌入），加强了先前的发现（特别是 [5, 命题 5]）。

案例研究与扩展
本文将该框架应用于特定场景：

• 笛卡尔积：该方法推广到 $n$ 个变量。当谓词由单变量谓词的合取构成（$\phi_i(x) = \bigwedge \psi^i_k(x_k)$）时，生成的格是单变量格的笛卡尔积。具体化映射对应于将集合分配给 $n$ 维矩形。
• 八边形逻辑：作者分析了形式为 $\pm x \pm y \geq c$ 的谓词。他们观察到，虽然 $\gamma$ 保持否定，但不保持合取或析取（因为此类谓词的交集通常导致无法由格中单个谓词表示的几何形状）。因此，仅依赖经典否定的逻辑是薄弱的。为了解决这个问题，作者建议使用合取和析取作为元连接词来处理序列，同时指出八边形的格结构由交不可约和并不可约元素组成（排除顶和底），从而允许存在对合否定。

意义与主张
本文将自己定位为正在进行的工作所产生的一系列初步结果和观察。其主要意义在于：

1. 推广：扩展 [3] 的结果，提供生成任何有限抽象内部逻辑的通用过程。
2. 系统化构建：提供一个具体（尽管朴素）的算法来生成证明系统，保证该逻辑的代数结构同构于抽象域。
3. 理论细化：加强具体化映射的序论性质与相关逻辑完备性之间的理论联系。

作者明确指出，当前过程效率低下且忽略了计算限制，将这项工作定位为表征非笛卡尔抽象的哪些属性“渗透”到笛卡尔情况的基础步骤，而非呈现一个即用的验证工具。