E-统一中积极变量消除的完备性

# E-统一中积极变量消除的完备性 ## 1. 引言 E-统一旨在为给定等式理论 E 中的给定方程找到一组解。这一问题在计算机科学的诸多领域，如形式验证、定理证明和逻辑编程中频繁出现。一般而言，E-统一问题，即在非空等式理论 E 中为给定方程寻找解的集合，是不可判定的，这与句法统一问题（即在空等式理论中为方程寻找解）不同。不过，E-统一问题是半可判定的，并且存在完备的算法来解决它。 目标导向的 E-统一算法基于将目标方程转化为可轻松定义解的形式这一理念。有一种推理系统，其中的变量消除规则，若应用于目标中形如 x ≈ v 的方程，会从目标的所有其他方程中消除 x，从而求解该方程。这里强制积极应用变量消除规则，因为没有其他规则来处理 x 不在 v 中作为变量的 x ≈ v 形式的方程。 此前，尚无证据表明该推理系统对于 E-统一是完备的。当允许其他规则应用于方程 x ≈ v 时，系统是完备的，但此时变量消除规则无法积极应用。这一问题最初由 Gallier 和 Snyder 发现，并被称为积极变量消除问题。 积极变量消除在句法统一（空等式理论）的背景下是合理的，因为它在保留一组解的同时减少了目标中未求解变量的数量，且其他规则不会增加未求解变量的数量，所以可以确定推理会终止。 在 E-统一的背景下，还需使用另一个名为“Mutate”的规则。需要注意的是，Mutate 和变量消除规则对目标的应用结果存在冲突：变量消除减少了目标中未求解变量的数量，但 Mutate 增加了这个数量；Mutate 减少了目标实例的基础证明的长度，而变量消除可能会增加该长度。 本文证明了在不破坏 E-统一过程完备性的情况下，可以积极应用变量消除规则。积极应用变量消除规则可减少一般 E-统一算法中固有的非确定性，减少推理的冗余，并限制给定方程解的搜索空间。 证明推理规则完备性的主要思路是考虑目标的基础等式证明。本文大部分内容围绕等式基础证明理论的描述以及反映积极变量消除效果的新等式证明的构建展开。之后引入等式证明中路径的概念，这使得我们能够定义目标的度量，并通过对该度量进行归纳来证明结果。 ## 2. 预备知识 我们使用标准定义。考虑形如 s ≈ t 的方程，其中 s 和 t 是项。需注意，本文中这些方程被视为有方向的，即 s ≈ t 与 t ≈ s 是不同的方程。设 E 是一组方程，u ≈ v 是一个方程，若 u ≈ v 在包含 E 的任何模型中都为真，则记为 E |= u ≈ v（或 u =E v），称 E 为等式理论，并假设 E 在对称运算下封闭。目标（E-统一问题）通常用 G 表示，它是一组方程，E |= G 意味着 E 满足 G 中的所有方程。 我们将基础项视为可能具有或不具有相同句法形式的基础对象，更关注项的出现而非其值。项可通过其在证明序列中的地址以及在证明中作为子项的位置来识别。因此，基础项之间的等号处理方式特殊：若 u、v 是基础项，u = v 表示 u 与 v 是相同的对象；当仅需句法相等时，用 u == v 表示；句法不等用 u ̸== v 表示。同一性和句法同一性的区别在于，前者涉及对象，后者涉及名称。 变量 x 指向其在项 u 中的出现，在某个基础替换 γ 下，这些出现中的每一个都与 uγ 在位置 α 处的某个子项相同（xγ = uγ|α）。同一变量的不同出现是不同的对象，尽管它们具有相同的句法形式。为区分同一变量的不同出现，我们使用上标数字，通常按其在等式证明中出现的顺序从左到右编号，例如 xγ1 和 xγ2 是 x 在证明中的不同出现。 有时我们想表明某个子项具有 xγ 的形式（或值），但与 xγ 不相同（即不由变量 x 指向），这将用引号表示。例如，w[“xγ”]α 与 w[xγ]α 不同，因为在第二个项中 xγ 实际出现在位置 α 处，而在第一个项中只有一个具有 xγ 值的子项。 若 γ 是基础替换，γx 表示该替换对变量 x 的限制。例如，若 γ = [x → a, y → b, z → c]，则 γx = [x → a]。 ## 3. 等式证明 给定等式理论 E，我们将等式证明定义为一对 (Π, γ)，其中 Π 是一系列基础项，γ 是基础替换。 ### 3.1 等式证明的定义 设 E 是一组方程。方程 u ≈ v 的等式证明是一对 (Π, γ)，其中 Π = (w1, w2, ..., wn) 是来自 TΣE 的基础项系列，称为证明序列，满足： 1. uγ = w1，vγ = wn； 2. 对于 1 ≤ i ≤ (n - 1) 的每一对 (wi, wi+1)，存在一个方程 s ≈ t ∈ E 和一个匹配器 ρ，使得 wi 有一个子项 wi|α，wi+1 有一个子项 wi+1|α，且 wi|α = sρ，wi+1|α = tρ。 我们可以将等式证明写为： uγ = w1 ≈[α1,s1≈t1,ρ1] w2 ≈[α2,s2≈t2,ρ2] ... ≈[αn−1,sn−1≈tn−1,ρn−1] wn = vγ 其中 [αi, si ≈ ti, ρi] 表示匹配子项的位置 αi、使用的 E 中的方程 (si ≈ ti) 以及该方程中变量的替换方式 (ρ)。上述序列中的每个 wi 称为证明中的项，与 wi 的任何真子项不同，真子项不被视为证明中的项。我们有时会借用数组的表示法，Π[i] 表示 Π 中的第 i 项。 由于每个步骤的匹配器都使用 E 中方程的重命名版本，匹配器的域与 γ 的域以及证明中所有其他步骤的匹配器的域不相交，我们将 γ 扩展为 γ′，使得：γ′ = γ ∪ ρ1 ∪ ... ∪ ρn。从现在起，我们假设 γ 是其扩展版本。 为了能够识别可能应用变量分解规则引入的新变量，我们需要进一步扩展 γ。如果 γx = [x → v]，γ 的一般扩展会为项 v 的每个子项添加变量，我们称这些新变量为子项变量。 ### 3.2 变量替换的一般扩展 设 γ 是基础替换。γ 的一般扩展 ex(γ) 递归定义如下： 1. 若 γx = [x → v] 且 |v| = 1（v 是常量），则 ex(γx) = γx； 2. 若 γx = [x → f(v1, ..., vn)] 且 n ≥ 1，则令 γyi = [yi → vi]，对于 1 ≤ i ≤ n，且 ex(γx) = γx ∪ ex(γy1) ∪ ··· ∪ ex(γyn)； 3. ex(γ) = ∑x∈Dom(γ) ex(γx) 从现在起，我们将 (Π, γ) 中的 γ 视为其一般扩展。 Dom(γ) 中有三种类型的变量： - 目标变量，即 u ≈ v 中的变量； - 系统变量，若在 (Π, γ) 中有步骤 Π[i] ≈[αi,si≈ti,γ] Π[i + 1]，则 si ≈ ti 中的变量称为系统变量； - 证明中每个 Π[i] 的子项变量，即由 γ 的一般扩展引入的变量。 每个变量出现都会在等式证明中开始或结束某个子证明。为了定义这个子证明，我们定义变量出现的方向如下： ### 3.3 变量出现的方向 设 (Π, γ) 是等式证明，x ∈ Dom(γ)。 1. 若 xγ 是 Π[i] ≈[αi,si≈ti,γ] Π[i + 1] 中的系统变量出现，且 xγ = Π[i]|α 对于某个位置 α，则 xγ 具有左方向；若 xγ = Π[i + 1]|α，则 xγ 具有右方向。 2. 若 xγ 是 Π[1] 中的目标变量出现（xγ = Π[1]|α），则 xγ 具有右