积极变量消除的E-合一完备性解析

### 积极变量消除的 E - 合一完备性解析 在等式证明和 E - 合一的研究领域中，积极变量消除是一个重要的概念。它对于简化证明过程、提高求解效率有着重要的作用。下面我们将深入探讨等式证明中的变量求解、路径概念以及 E - 合一的完备性等关键内容。 #### 等式证明中的变量求解 在等式证明中，变量的求解是一个核心问题。当我们选择一个形如 \(x \approx t\) 的等式进行积极变量消除时，会对等式证明产生一系列的影响。 假设我们有一个等式证明 \((\Pi, \gamma)\)，其证明序列为： \(\Pi = (w_1 \approx[\alpha_1,s_1\approx t_1,\gamma] w_2 \approx[\alpha_2,s_2\approx t_2,\gamma] \cdots \approx[\alpha_{n - 1},s_{n - 1}\approx t_{n - 1},\gamma] w_n)\) 其中 \(\gamma\) 是一个扩展的基替换。设 \(U = \{x_1, \cdots, x_n\}\) 是 \((\Pi, \gamma)\) 中被称为“未求解”的变量集合，\(G_{\Pi}\) 是仅针对未求解变量构建的图。 若 \(x \in U\) 且 \(x\gamma\) 是 \(G_{\Pi}\) 中的最大节点，设 \(ass(x\gamma) = v\)。当 \(x\) 不在 \(v\) 中出现时，我们可以创建一个新的证明 \((\Pi^*, \gamma^*)\)，具体步骤如下： 1. **扩展**： - 当 \(x\gamma = w_i|\alpha\) 即 \(w_i = w_i[x\gamma]\) 时： - 若 \(x\gamma\) 具有右方向，将 \(w_i\)（\((\Pi, \gamma)\) 中的第 \(i\) 步）替换为： \(w_i[v]_{\alpha} \approx(\Sigma'_{v\approx“x\gamma”}) \approx w_i[“x\gamma”]_{\alpha}\) 其中 \((\Sigma'_{v\approx“x\gamma”})\) 表示 \((\Sigma_{“x\gamma”\approx v}, \gamma)\) 的重命名并反向嵌入 \(w_i\) 在位置 \(\alpha\) 向左。 - 若 \(x\gamma\) 具有左方向，将 \(w_i\) 替换为： \(w_i[“x\gamma”]_{\alpha} \approx(\Sigma'_{“x\gamma”\approx v}) \approx w_i[v]_{\alpha}\) 其中 \((\Sigma'_{“x\gamma”\approx v})\) 表示 \((\Sigma_{“x\gamma”\approx v}, \gamma)\) 的重命名并嵌入 \(w_i\) 在位置 \(\alpha\) 向右。 2. **标准收缩**： 对于 \((\Pi, \gamma)\) 中每个未求解变量 \(y\) 的出现，如果 \((\Sigma_{y\gamma\approx s}, \gamma)\) 是该出现的一个适当关联子证明，并且在扩展后的证明序列 \(\Pi^*\) 中有子证明序列 \(\Sigma_{s\approx“y\gamma”}\Sigma_{“y\gamma”\approx s}\)，则将该子证明序列收缩为一个单元素序列 \(s\)。 替换 \(\gamma^*\) 定义如下： - \(\gamma^*_x = [x \to v]\) - 若 \(y\gamma|\alpha = x\gamma\) 且 \(y \notin U\)，则 \(\gamma^*_y = [y \to y\gamma[x\gamma^*]_{\alpha}]\) - 若 \(z \notin Dom(\gamma)\)，\(z\) 是 \(Dom(\gamma)\) 中某个变量 \(z'\) 的重命名且出现在 \((\Sigma'_{x\gamma\approx v}, \gamma')\) 中，则 \(\gamma^*_z = [z \to z'\gamma]\) - 对于其他变量，\(\gamma^* = \gamma\) 若 \(x\) 在 \(v\) 中出现，则 \((\Pi^*, \gamma^*) = (\Pi, \gamma)\)。同时，我们标记变量 \(x\) 在 \((\Pi^*, \gamma^*)\) 中已求解。若 \(x\) 不在 \(v\) 中出现，也标记 \(x\) 的所有子项变量为已求解，\(Dom(\gamma^*)\) 中未在 \(Dom(\gamma)\) 中出现的新变量标记为未求解。 下面通过一个例子来说明： 设等式证明为 \(f(a, g(b, b)) \approx[<1>,a\approx b,[]] f(b, g(b, b)) \approx[\epsilon,f(x,g(x,x))\approx c,[x\to b]] c\)，与 \(\leftarrow x\gamma_1\) 关联的子证明是 \(b \approx a\)。我们要通过 \(x \to a\) 求解 \(x\)，扩展后得到： \(f(a, g(b, b)) \approx[<1>,a\approx b,[]] f(b, g(b, b)) \approx[<1>,b\approx a,[]] f(a, g(b, b)) \approx[<2>,b\approx a,[]] f(a, g(a, b)) \approx[<3>,b\approx a,[]] f(a, g(a, a)) \approx[\epsilon,f(x,g(x,x))\approx c,[x\to a]] c\) 经过标准收缩后，证明缩短为： \(f(a, g(b, b)) \approx[<2>,b\approx a,[]] f(a, g(a, b)) \approx[<3>,b\approx a,[]] f(a, g(a, a)) \approx[\epsilon,f(x,g(x,x))\approx c,[x\to a]] c\) #### 等式证明中的路径 路径的概念是变量出现关联子证明的一种推广。在等式证明 \((\Pi, \gamma)\) 中，路径是从某个变量出现开始的子证明的组合，其定义是递归的。 设 \((\Pi, \gamma)\) 是等式证明，\(U\) 是 \(Dom(\gamma)\) 中未求解变量的集合，\(x \in U\) 且 \(x\gamma\) 是 \((\Pi, \gamma)\) 中给定的变量出现。从 \(x\gamma\) 开始的路径 \(\Sigma_1 \cdots \Sigma_n\) 定义如下： 1. 若 \(y\) 是已求解变量且 \(\Sigma_{v_1\approx“y\gamma'_i”}\Sigma_{“y\gamma'_k”\approx v_2}\) 是 \((\Pi, \gamma)\) 中的子证明，则 \(y\gamma'_k\) 是该子证明中涉及的已求解变量的出现。 2. 若 \(\Sigma_{x\gamma\approx v}\) 是 \(x\gamma\) 的关联子