第 2 章：Presburger 算术的语法与语义
直觉
第 1 章把循环实例看成整数点，本章回答一个更基础的问题：可以用什么样的逻辑公式挑选这些点？Presburger 算术允许整数常量、加法、比较、布尔组合和量词。它足以表达仿射边界、析取、投影以及固定周期的步长，却刻意排除一般的变量乘变量。
“允许固定常数乘变量”与“不允许变量乘变量”是核心分界。例如 3y 只是 y+y+y 的缩写；yz 中乘数 $z$ 随赋值变化，不能展开成固定次数的加法。
Presburger 1929 年的原始工作建立了这一加法算术体系的完备性与可判定性；这里采用整数编译器建模所需的语法，并在涉及历史定理时回溯其稳定英文译注。
形式定义
语言和项
令 $\mathcal{L}_{PA}$ 表示本章使用的一阶语言，论域先取整数集合 $\mathbb{Z}$。变量记为 x,y,z,k；整数常量记为 $c\in\mathbb{Z}$。线性项 $t$ 可写为
$$ t ::= c\mid x\mid t+t\mid -t. $$
等价地，每个线性项都可整理为
$$ t=c+a_1x_1+\cdots+a_nx_n, $$
其中 $a_1,\ldots,a_n\in\mathbb{Z}$ 是固定系数。a_ix_i 表示常数乘法；它不是两个变量的乘积。
原子公式和公式
由线性项构造原子公式 t_1=t_2 和 $t_1\le t_2$。严格序 t_1<t_2 是 $t_1\le t_2\land t_1\ne t_2$ 的缩写；在整数上也可写成 $t_1+1\le t_2$。再用布尔联结词和量词构造公式：
$$ \varphi ::= t_1=t_2\mid t_1\le t_2 \mid\neg\varphi\mid(\varphi\land\varphi)\mid(\varphi\lor\varphi) \mid\exists x\,\varphi\mid\forall x\,\varphi. $$
蕴含 $\varphi\Rightarrow\psi$ 是 $\neg\varphi\lor\psi$ 的缩写。给定固定正整数 $m$，整除原子 $m\mid t$ 和同余原子
$$ t_1\equiv t_2\pmod m $$
常作为便于量词消去的扩展语法；其语义分别是“存在整数 $q$ 使 t=mq”和 $m\mid(t_1-t_2)$。因此它们不增加可定义集合，只让公式更紧凑。
赋值、自由变量与真值
变量赋值 $\sigma$ 把每个自由变量映到一个整数。记 $\llbracket t\rrbracket_\sigma$ 为线性项 $t$ 在赋值 $\sigma$ 下的整数值。满足关系 $\mathbb{Z},\sigma\models\varphi$ 递归定义如下：等式和序比较相应整数值；布尔联结词采用通常真值规则；并且
$$ \mathbb{Z},\sigma\models\exists x\,\varphi \quad\Longleftrightarrow\quad \text{存在 }a\in\mathbb{Z},\quad \mathbb{Z},\sigma[x\mapsto a]\models\varphi. $$
全称量词类似。$FV(\varphi)$ 表示公式 $\varphi$ 的自由变量集合，即未被量词绑定的变量。例如
$$ FV(\exists k:\ x=3k+1)=\{x\}. $$
没有自由变量的公式称为句子，它在整数结构中只有真或假，不再依赖外部赋值。
自然数版和整数版
若量词与赋值范围取非负整数集合 $\mathbb{N}=\{0,1,2,\ldots\}$，得到自然数版；本教程的循环坐标、差值和调度统一使用整数版 $\mathbb{Z}$。两者不能在推导中无提示地混用。例如整数版的 $\exists x:x+1=0$ 为真，自然数版为假。
需要搬运集合结论时，可把一个整数坐标 $z$ 编码成两个非负坐标之差 z=z^+-z^-，其中 $z^+,z^-\in\mathbb{N}$，并同步改写公式。Ginsburg–Spanier 对 modified Presburger formulas 与半线性集等价的直接论域是 $\mathbb{N}^n$；整数版必须先做这类显式编码，不能省略域的变化。参见其原始论文。
手算示例
逐式判断表达能力
| 谓词 | 是否可表达 | 理由或等价写法 |
|---|---|---|
x = 3y + 2 | 是 | 3、2 是固定常数，右侧是线性项。 |
x ≡ 1 (mod 3) | 是 | 可作扩展同余原子，或写成 $\exists k\in\mathbb{Z}:x=3k+1$。 |
x = yz | 一般否 | $y$、$z$ 都是变量，这是一般变量乘变量，不是固定次数的加法。若乘法图可定义，令 z=y 便会得到平方图。 |
x = y² | 一般否 | $y^2=y\cdot y$ 仍是变量乘变量。若平方图可定义，投影 $y$ 就能定义所有平方数；但一元 Presburger 集合最终呈固定周期，平方数间距却无界增长。 |
∃k: x = 3k + 1 | 是 | $k$ 被存在量词绑定，矩阵仍是线性等式；它恰好定义余数为 1 的整数。 |
(0 ≤ x ≤ N) ∨ (2N ≤ x ≤ 3N) | 是 | 两个仿射区间的析取；$N$ 是自由参数，所有乘数都是固定常数。 |
表中的“一般否”强调统一的无限整数关系。若把所有变量限制在某个固定有限集合，当然可以穷举成有限析取，但这不等于得到对任意参数规模都有效的 Presburger 乘法定义。
析取例子的自由变量集合是 {x,N}。若外层另给参数上下文 $C(N):N\ge0$，它定义两个可能分离的整数区间，说明一般 Presburger 集合不必是单个凸多面体。
非单位步长循环
考虑
for (int i = 1; i < N; i += 3) S(i);
引入整数迭代计数 $k\in\mathbb{Z}$。初始化对应 k=0、第 $k$ 次执行时 i=1+3k，且循环只沿正方向执行，因此域可写成
$$ D_S(N)=\{i\in\mathbb{Z}\mid \exists k\in\mathbb{Z}: i=1+3k\land0\le k\land i<N\}. $$
由 i=1+3k 和 $k\ge0$ 可得 $i\ge1$ 以及 $i\equiv1\pmod3$。反过来，若 $i\ge1$ 且 $i\equiv1\pmod3$，则存在整数 $k=(i-1)/3\ge0$。所以等价的同余写法是
$$ D_S(N)=\{i\in\mathbb{Z}\mid1\le i<N\land i\equiv1\pmod3\}. $$
取 N=11，从 k=0 开始手算：
$$ k=0,1,2,3\quad\Longrightarrow\quad i=1,4,7,10. $$
k=4 时 i=13，已不满足 i<11。因此全部实例恰为
$$ D_S(11)=\{1,4,7,10\}. $$
若只保留区间 $1\le i<N$，就会得到 {1,2,3,4,5,6,7,8,9,10}，其中 2,3,5,6,8,9 是原循环从不到达的虚假实例。区间描述丢掉了模 3 的周期信息。
编译器用途
Presburger 公式给编译器一种统一方式来表示：
- 仿射循环边界与参数上下文；
if条件形成的交、并、补；- 非单位步长形成的同余类；
- 引入辅助变量后的投影，即存在量词；
- 对所有候选实例成立的合法性条件，即全称量词。
自由变量决定一个公式描述什么坐标空间。对 $\varphi(i,j,N)$，若把 $N$ 视为参数，则固定 $N$ 后自由迭代坐标是 (i,j)；若消去 $j$，所得公式只描述 (i,N)。后续的集合与关系代数会把这种变量角色显式组织成输入、输出和参数空间。
同余不是装饰信息。若分析器把 i += 3 松弛为普通区间，后续依赖测试可能报告并不存在的实例和冲突；精确整数模型必须保留步长带来的周期结构。
常见误区
- 把固定常数乘法与一般乘法混为一谈。
7x合法，因为7固定；xy不合法，因为重复加法次数由变量决定。 - 认为存在量词让任意运算都可表达。 $\exists k:x=3k+1$ 仍只含线性项；增加量词不会把
x=yz变成线性公式。 - 混用 $\mathbb{N}$ 与 $\mathbb{Z}$。 负数见证可能改变句子真值。若从自然数结果搬到整数，必须给出编码。
- 认为同余是额外的非线性能力。 固定模数同余可展开为带存在量词的线性等式，它仍处于 Presburger 范围内。
- 认为析取仍一定是一个凸域。 两个分离区间的并可以由公式表达，却不能当成单个凸多面体。
- 把数据依赖控制或地址的表达式强行线性化。
A[i*i]、A[B[i]]和while (A[i] > 0)分别引入非线性下标、间接下标和数据相关控制；删掉这些信息得到的只是近似，不是原程序的精确 Presburger 语义。
练习
练习 EX02-B01｜同余的量词形式与自由变量（基础）
写出谓词 $x\equiv2\pmod5$ 的存在量词形式，并求其自由变量集合。
答案索引： ANS-EX02-B01
练习 EX02-D01｜Presburger 可定义性判定（推导）
判断 $x=4y-N$、$x=Ny$、$x=y+z$、$x=|y|$ 是否可定义。对最后一式尝试用析取展开绝对值。
答案索引： ANS-EX02-D01
练习 EX02-D02｜固定步长循环建模（推导）
把 for (i=2; i<=20; i+=4) 写成存在量词形式与同余形式，并枚举全部实例。
答案索引： ANS-EX02-D02
练习 EX02-B02｜整数版与自然数版真值（基础）
在整数版和自然数版中分别判断 $\exists x:2x+1=0$ 的真值，并说明这道命题对区分两个论域的诊断力为何有限。
答案索引： ANS-EX02-B02
练习 EX02-C01｜析取域的参数边界（综合）
对 $\varphi(i,N):(0\le i<N)\lor(2N\le i<3N)$，分别讨论 $N=0$、$N=2$ 时定义的集合。
答案索引： ANS-EX02-C01
本章小结
整数版 Presburger 算术以线性项、比较、布尔联结词和量词描述整数点集。固定常数乘变量、固定模数同余、析取和投影都可表达；一般变量乘变量、非线性或数据相关地址则不在经典边界内。非单位步长例子显示，整数集合不仅需要区间，也需要同余所携带的周期信息。