递归数据结构与整数约束的决策程序

### 递归数据结构与整数约束的决策程序 #### 1. 引言 递归定义的数据结构是编程语言中的重要组成部分。直观地说，如果一个数据结构部分由相同结构的更小或更简单的实例组成，那么它就是递归定义的，像列表、栈、计数器、树、记录和队列等。在验证包含递归定义数据结构的程序时，我们需要对这些数据结构进行推理。虽然已经存在一些针对单一数据结构的决策程序，但在程序验证中，单一理论的决策程序往往不适用，因为编程语言通常涉及多个数据域，从而产生跨越多个理论的验证条件。常见的“混合”约束示例是数据结构与这些结构大小的整数约束的组合。 这里考虑将Presburger算术与递归数据结构进行集成。递归数据结构满足项代数的特定属性：数据域是仅通过应用构造函数生成的数据对象集合，且每个数据对象是唯一生成的。例如，列表、栈、计数器、树和记录属于此类，而队列不属于，因为它不是唯一生成的，可在两端增长。 集成理论的语言有两种类型：整数类型 $Z$ 和数据（项）类型 $\lambda$。该语言直观上是递归数据结构语言和Presburger算术语言的集合论并集，再加上额外的长度函数 $|.| : \lambda \to Z$。公式由数据文字和整数文字使用逻辑连接词和量化形成。 将针对该理论的不同变体提出四种决策程序，具体取决于语言是否有无限多个原子以及理论是否为无量词的。无量词理论的决策程序基于Oppen针对具有无限原子域的无环递归数据结构的算法。当输入中没有整数约束时，这些决策程序可视为Oppen原始算法对循环结构和具有有限原子域结构的扩展。 #### 2. 预备知识 - **签名与项**：签名 $\Sigma$ 是一组参数（函数符号和谓词符号），每个参数都有一个关联的元数。函数符号元数为0时也称为常量。$\Sigma$-项 $T (\Sigma, X)$ 递归定义：常量 $c \in \Sigma$ 或变量 $x \in X$ 是项；若 $f \in \Sigma$ 是 $n$ 元函数符号，$t_1, \ldots, t_n$ 是项，则 $f(t_1, \ldots, t_n)$ 是项。 - **公式类型**：原子公式是 $P(t_1, \ldots, t_n)$ 形式的公式，其中 $P$ 是 $n$ 元谓词符号，$t_1, \ldots, t_n$ 是项（等式视为二元谓词符号）。文字是原子公式或其否定。无变量的公式是基公式。变量在公式中无量化作用域时为自由出现。无自由变量的公式是句子。无量词的公式可化为析取范式，即文字合取的析取。 - **结构与解释**：$\Sigma$-结构 $A$ 是元组 $\langle A, I \rangle$，其中 $A$ 是非空域，$I$ 将每个 $n$ 元函数符号 $f$（或谓词符号 $P$）与 $A$ 上的 $n$ 元函数 $f^A$（或关系 $P^A$）关联。变量赋值 $\nu$ 是将每个变量赋值为 $A$ 中元素的函数。公式的真值由解释和变量赋值确定。 - **可满足性与有效性**：公式 $\phi$ 在某些变量赋值下为真时是可满足的，否则不可满足。公式 $\phi$ 在所有变量赋值下为真时是有效的，$\phi$ 有效当且仅当 $\neg \phi$ 不可满足。若集合 $T$ 中的每个句子在结构 $A$ 中为真，则 $A$ 是 $T$ 的模型。若 $\phi$ 在 $T$ 的每个模型中为真，则称 $\phi$ 由 $T$ 逻辑蕴含（或 $T$-有效），记为 $T \models \phi$。类似地，若 $\phi$ 在 $T$ 的某个模型中为真，则称 $\phi$ 是 $T$-可满足的，否则 $T$-不可满足。理论 $T$ 是在逻辑蕴含下封闭的句子集合。 - **项代数与Presburger算术**：$\Sigma$ 以 $X$ 为基的项代数 $TA$ 是域为 $T (\Sigma, X)$ 的结构。Presburger算术（PA）是整数加法的一阶理论，对应结构记为 $A_Z = \langle Z; 0, +, < \rangle$。所有无量词理论的决策程序基于反驳，确定公式 $\phi$ 的有效性只需确定 $\neg \phi$ 的不可满足性，进一步归结为确定 $\neg \phi$ 析取范式中每个析取项的不可满足性。因此，在讨论无量词理论时，输入公式通常指文字的合取。 #### 3. 递归数据结构与Oppen算法 ##### 3.1 递归数据结构的定义 递归数据结构 $A_{\lambda} : \langle \lambda; A, C, S, T \rangle$ 包含以下部分： 1. $\lambda$：数据域，由常量通过应用构造函数构建的所有项组成，其中的元素称为 $\lambda$-项（或数据项）。 2. $A$：一组原子（常量），如 $a, b, c, \ldots$。 3. $C$：有限的构造函数集合，如 $\alpha, \beta, \gamma, \ldots$，$\alpha$ 的元数记为 $ar(\alpha)$。若对象的最外层构造函数是 $\alpha$，则称其为 $\alpha$-类型（或 $\alpha$-项）。 4. $S$：有限的选择器集合。对于每个元数 $k > 0$ 的构造函数 $\alpha$，$S$ 中有 $k$ 个选择器 $s_{\alpha}^1, \ldots, s_{\alpha}^k$，称 $s_{\alpha}^i (1 \leq i \leq k)$ 为第 $i$ 个 $\alpha$-选择器。对于项 $x$，若 $x$ 是 $\alpha$-项，$s_{\alpha}^i (x)$ 返回 $x$ 的第 $i$ 个分量，否则返回 $x$ 本身。 5. $T$：有限的测试器集合。对于每个构造函数 $\alpha$，有对应的测试器 $Is_{\alpha}$。对于项 $x$，$Is_{\alpha}(x)$ 为真当且仅当 $x$ 是 $\alpha$-项。还有一个特殊测试器 $Is_A$，$Is_A(x)$ 为真当且仅当 $x$ 是原子。 递归数据结构的理论本质上是项代数的理论（变量基为空），可公理化如下： | 公理模式 | 描述 | | ---- | ---- | | A. $t(x) \neq x$，若 $t$ 仅由构造函数构建且 $t$ 适当地包含 $x$ | 防止项与自身的非平凡构造形式相等 | | B. $a \neq b$，$a \neq \alpha(x_1 \ldots, x_{ar(\alpha)})$，$\alpha(x_1 \ldots, x_{ar(\alpha)}) \neq \beta(y_1, \ldots, y_{ar(\beta)})$，若 $a$ 和 $b$ 是不同原子，$\alpha$ 和 $\beta$ 是不同构造函数 | 保证原子和不同构造函数生成的项不相等 | | C. $\alpha(x_1, \ldots, x_{ar(\alpha)}) = \alpha(y_1, \ldots, y_{ar(\alpha)}) \to \bigwedge_{1\leq i\leq ar(\alpha)} x_i = y_i$ | 相同构造函数生成的项相等时，其对应分量相等 | | D. $Is_{\alpha}(x) \leftrightarrow \exists \overline{z}_{\alpha} \alpha(\overline{z}_{\alpha}) = x$，$Is_A(x) \leftrightarrow \bigwedge_{\alpha \in C} \neg Is_{\alpha}(x)$ | 定义测试器的逻辑关系 | | E. $s_{\alpha}^i (x) = y \leftrightarrow \exists \overline{z}_{\alpha} (\alpha(\overline{z}_{\alpha}) = x \wedge y = z_i) \vee (\forall \overline{z}_{\alpha}(\alpha(\overline{z}_{\alpha}) \neq x) \wedge x = y)$ | 定义选择器的逻辑关系 | 例如，对于LISP列表结构 $A_{List} = \langle List; cons, car, cdr \rangle$，上述公理模式可简化为： 1. $Is_A(x) \leftrightarrow \neg Is_{cons}(x)$ 2. $car(cons(x, y)) = x$ 3. $cdr(co