第 3 章：可判定性、量词消去与表达能力

直觉

一个逻辑理论可判定，是说存在一个总会停机的算法，能够对该理论中任意句子回答“真”或“假”。这是一项关于算法存在性与终止性的保证，不是关于日常运行成本的保证。公式变长、量词交替增加、系数或模数变大时，中间公式可能急剧膨胀；所以“Presburger 算术可判定”绝不等于“每个编译器查询都廉价”。可判定性的历史依据可追溯到 Presburger 的原始工作英文译注。

量词消去试图把含量词的公式改写为不含相应量词、但对剩余自由变量等价的公式。对集合而言，消去一个存在量词就是投影掉一个坐标：保留下来的点，正是至少存在一个被删除坐标使原约束成立的点。

整数与实数的消元有一个关键差异：整数点带有整除和余数条件。Cooper 的方法通过规范化被消去变量的系数，并显式处理界与固定模数，给出整数线性算术的量词消去路线；本章依据其1972 年原文解释思想。

形式定义

令 $Th(\mathbb{Z},+,\le)$ 表示整数加法与序的一阶理论，即所有在结构 $(\mathbb{Z},0,1,+,\le)$ 中为真的句子集合。称它可判定，若存在算法 Decide，对任意该语言中的句子 $\psi$ 都在有限时间内终止，并满足

$$ Decide(\psi)=\texttt{true} \quad\Longleftrightarrow\quad \mathbb{Z}\models\psi. $$

令 m,n 为非负整数。若公式 $\varphi(x,y)$ 的自由变量包含坐标向量 $x\in\mathbb{Z}^m$ 和 $y\in\mathbb{Z}^n$，则消去 $y$ 是寻找只含 $x$ 的公式 $\widehat\varphi(x)$，使

$$ \mathbb{Z}\models \widehat\varphi(x)\leftrightarrow\exists y\,\varphi(x,y). $$

对由 $\varphi$ 定义的集合

$$ X=\{(x,y)\in\mathbb{Z}^{m+n}\mid\varphi(x,y)\}, $$

令 $I_x$ 表示 $X$ 中属于向量 $x$ 的坐标索引集合。按照全文契约，保留坐标集合 $I$ 的投影统一记为 proj_I(X)；因此这里保留 $x$ 坐标的投影写作 $\operatorname{proj}_{I_x}(X)$，并满足

$$ \operatorname{proj}_{I_x}(X) =\{x\in\mathbb{Z}^m\mid\exists y\in\mathbb{Z}^n:\varphi(x,y)\}. $$

在只含 $0,1,+,\le$ 的基础语言里，消元结果未必能方便地写成单个合取。Cooper 风格消元通常在加入固定模数整除原子的扩展语言中得到量词自由的布尔组合；这些整除原子本身又可用存在量词线性定义。这里的“量词消去”应按这种常用扩展语法理解，而不是声称每个结果都是单个凸多面体。

手算示例

一个 Cooper 风格的教学性小推导

考虑自由参数 $a,b\in\mathbb{Z}$ 和公式

$$ \Phi(a,b):\quad \exists x\in\mathbb{Z}: a\le2x\le b\land x\equiv1\pmod3. $$

第一步是把被消去变量前的非单位系数规范化。令新变量 z=2x。条件 $x\equiv1\pmod3$ 等价于存在 $q\in\mathbb{Z}$ 使 x=3q+1，从而

$$ z=2x=6q+2 \quad\Longleftrightarrow\quad z\equiv2\pmod6. $$

反向也成立：若 z=6q+2，则 z=2(3q+1)，可取 x=3q+1。因此

$$ \Phi(a,b)\quad\Longleftrightarrow\quad \exists z\in\mathbb{Z}:a\le z\le b\land z\equiv2\pmod6. $$

现在只需判断闭区间 [a,b] 是否含有一个模 6 余 2 的整数。按 $a$ 的余数分六种情况。令 $\delta_r$ 表示当 $a\equiv r\pmod6$ 时，从 $a$ 向上到最近目标余数 2 的距离，则

$$ (\delta_0,\delta_1,\delta_2,\delta_3,\delta_4,\delta_5) =(2,1,0,5,4,3). $$

最小候选是 $z=a+\delta_r$；区间中存在目标点当且仅当该候选不超过 $b$。于是量词自由结果为

$$ \bigvee_{r=0}^{5} \left(a\equiv r\pmod6\land a+\delta_r\le b\right). $$

例如 a=7,b=9 时，$a\equiv1\pmod6$，最近候选是 8，故公式为真，对应 x=4；a=9,b=12 时，$a\equiv3\pmod6$，最近候选是 14>b，故为假。

这个推导展示了三件事：通过公倍数/换元整理系数、从下界产生有限候选、用模条件枚举有限余数类。它是教学性小例子，不冒充完整 Cooper 算法。完整算法还必须系统处理否定范式、多个上下界、无界情形、多个整除条件、系数的最小公倍数以及消元后的公式化简；其正确性不能由本例替代。

三角域的投影

令 $N\in\mathbb{Z}$，并定义整数点集

$$ X_{\mathrm{tri}}(N)= \{(i,j)\in\mathbb{Z}^2\mid0\le j\le i\land0\le i<N\}. $$

当它表示第 1 章的循环域时，采用尺寸参数上下文 $C(N):N\ge0$。在有序坐标 (i,j) 中，令索引集合 $I=\{1\}$ 表示只保留第一维 $i$；依照契约，所求投影记为 $\operatorname{proj}_{I}(X_{\mathrm{tri}}(N))$。对应的存在量词公式是

$$ \exists j\in\mathbb{Z}: 0\le j\le i\land0\le i<N. $$

它表示从三角域中投影掉 $j$，只保留 $i$。分两向证明：

• 若存在 $j$ 满足 $0\le j\le i$，则由传递性得到 $0\le i$；原式又直接给出 i<N。
• 若 $0\le i<N$，取见证 j=0，便有 $0\le j\le i$。

所以精确的消元结果是

$$ \exists j: 0\le j\le i\land0\le i<N \quad\Longleftrightarrow\quad 0\le i<N. $$

等价地，

$$ \operatorname{proj}_{I}(X_{\mathrm{tri}}(N)) =\{i\in\mathbb{Z}\mid0\le i<N\}. $$

这个等价式对每个整数 $N\in\mathbb{Z}$ 都成立：若 N<0，左右两侧同为空集；$C(N):N\ge0$ 只是把 $N$ 解释为合法循环尺寸时采用的参数语义，并不是上述逻辑等价成立的前提。几何上，投影把三角域的所有整数点沿 $j$ 轴压到 $i$ 轴；逻辑上的存在量词与集合上的投影是同一件事的两种表述。

编译器用途

投影和可满足性查询贯穿 polyhedral 编译：

• 从含辅助计数器 $k$ 的步长域中消去 $k$，得到关于循环变量的区间与同余条件；
• 从实例—内存位置关系中消去内存坐标或实例坐标，计算像、逆像和候选冲突；
• 从多维约束中逐层消去内层坐标，推导外层循环边界或运行时 guard；
• 判断某个依赖关系是否为空，或变换后的非法次序是否存在。

这里必须区分两种结论。判定过程回答的是“某个整数公式是否有解/是否恒真”；优化器还要考虑公式表示规模、消元顺序和最坏情况爆炸。工程工具通常会选择受限片段、启发式顺序、缓存和近似，以控制成本。Pugh 的 Omega Test 是整数仿射约束在编译器依赖分析中的经典判定路线，但不能因此泛称为任意 Presburger 输入都同样廉价。

常见误区

1. 把可判定理解成高效。 “总会停机并给出正确真值”没有给出小的时间或空间上界；量词消去可能产生大量析取与同余条件。
2. 把整数投影当成实数区间投影。 实数消元可能漏掉整数整除条件。例如 $\exists x:z=2x$ 在实数上对每个 $z$ 都有解，在整数上只定义偶数 $z$。
3. 认为消元结果必是一个凸多面体。 模条件和析取会产生周期或非凸集合；一般 Presburger 集合比单个凸多面体更广。
4. 把教学推导当成 Cooper 全算法。 本章只演示系数规范化、界和余数类的核心思想，没有覆盖算法的全部分支与复杂度控制。
5. 用量词消去越过语言边界。 A[i*i] 含非线性地址，A[B[i]] 含运行时决定的间接地址，while (A[i] > 0) 含数据相关控制。Cooper 消元只处理整数线性公式，不会把这些表达式自动变成精确 Presburger 约束。运行时检查、保守近似或扩展模型必须被明确标成另外的路线。
6. 把存在性与实际执行顺序混为一谈。 投影能回答“是否存在匹配坐标”，但精确依赖还需要原始顺序、访问方向以及最后写等语义，不能仅凭同址存在性完成。

练习

练习 EX03-D01｜偶数区间的量词消去（推导）

消去 $\exists x:c\le x\le d\land x\equiv0\pmod2$ 中的 $x$。按 $c$ 的奇偶性写出量词自由公式。

答案索引： ANS-EX03-D01

练习 EX03-D02｜带正下界的三角投影（推导）

对 $\exists j:1\le j\le i\land0\le i<N$ 求关于 $i$ 的投影，并指出它与本章三角域投影的边界差异。

答案索引： ANS-EX03-D02

练习 EX03-B01｜仿射像与同余类（基础）

判断 $\exists x:z=4x+1$ 定义哪一个同余类；解释为什么只写 $z\ge1$ 不等价。

答案索引： ANS-EX03-B01

练习 EX03-C01｜析取投影构造（综合）

给出一个含析取的二维整数集合，使其投影仍是两个分离区间；写出集合、逐分支存在见证，并手算投影。

答案索引： ANS-EX03-C01

练习 EX03-B02｜查询种类辨析（基础）

分别说明下列三项查询的种类：（1）固定 $N=N_0$，判断 $\exists i:\varphi(i,N_0)$ 是否成立；（2）判断带参数上下文的全称蕴含 $\forall i(\varphi\Rightarrow\psi)$ 是否有效；（3）求 $\exists j:\varphi(i,j)$ 的等价无 $j$ 公式。再说明若第（1）项不固定 $N$，它与投影的关系。

答案索引： ANS-EX03-B02

本章小结

Presburger 算术的可判定性保证句子真值可由终止算法决定，却不保证查询廉价。量词消去把存在量词转成对剩余变量的等价约束；在整数域中，界之外还必须保留整除和同余信息。三角域说明投影就是存在量词消去，Cooper 风格小例子则说明整数消元为何需要有限余数分类。该能力为后续集合、关系、依赖与代码生成提供逻辑基础，但不覆盖非线性下标、间接访问或数据相关控制。