成员等式逻辑规范的声明式调试

# 成员等式逻辑规范的声明式调试 ## 1. 错误等式与成员公理的定义 在成员等式逻辑规范中，成员公理是能够从有效信息中推导出无效结论的规范片段。下面给出错误等式实例和错误成员公理实例的定义。 ### 定义 1 设 \(R \equiv(af \Leftarrow u_1 = u_1' \land \cdots \land u_n = u_n' \land v_1 : s_1 \land \cdots \land v_m : s_m)\)，其中 \(af\) 表示一个原子公式，即在规范 \(S\) 中，它要么是一个有向等式，要么是一个成员公理。那么： - 对于预期解释 \(I\)，\(\theta(R)\) 是一个错误等式实例（或错误成员公理实例），当满足以下条件： - 存在 \(t_1, \cdots, t_n\)，使得对于 \(i = 1 \cdots n\)，有 \(I \models \theta(u_i) \to t_i\) 且 \(I \models \theta(u_i') \to t_i\)。 - 对于 \(j = 1 \cdots m\)，有 \(I \models \theta(v_j) : s_j\)。 - \(\theta(af)\) 在 \(I\) 中不成立。 - 如果 \(R\) 存在某个错误实例，那么 \(R\) 是一个错误等式（或错误成员公理）。 ## 2. 证明树与错误节点 为了方便表示演算中的推导过程，我们将其表示为证明树，其中每个推理步骤的前提是结论的子节点。例如，图 2 所示的证明树对应于第 2.3 节末尾描述的排序列表示范中的归约结果。 在声明式调试中，我们特别关注错误节点，即所有子节点都有效的无效节点。下面的命题描述了我们设定中的错误节点。 ### 命题 2 设 \(N\) 是图 1 演算中某个证明树相对于预期解释 \(I\) 的错误节点。那么： 1. \(N\) 是成员推理步骤或替换推理步骤的结果。 2. 与 \(N\) 关联的等式是错误等式或错误成员公理。 ## 3. 缩写证明树 我们的目标是在以用户检测到的初始错误症状为根的任何证明树 \(T\) 中找到一个错误节点。可以通过以下自顶向下的策略向用户询问树中节点的有效性来实现： - **输入**：根节点无效的树 \(T\)。 - **输出**：\(T\) 中的一个错误节点。 - **描述**：考虑 \(T\) 的根节点 \(N\)，有两种情况： - 如果 \(N\) 的所有子节点都有效，则将 \(N\) 识别为错误节点并结束。 - 否则，选择以任何无效子节点为根的子树，并递归使用相同的策略来查找错误节点。 通过对 \(T\) 的高度进行归纳，可以很容易地证明该策略是完备的。因此，有以下结果： ### 命题 3 设 \(T\) 是根节点无效的证明树。那么存在一个错误节点 \(N \in T\)，使得 \(N\) 的所有祖先节点都是无效的。 然而，我们不使用证明树 \(T\) 作为调试树，而是使用一个合适的缩写，记为 \(APT(T)\)（缩写证明树）。选择 \(APT\) 而不是原始证明树的原因是，它在保持技术的正确性和完备性的同时，减少并简化了向用户询问的问题。特别是，\(APT\) 只包含与规范中声明的替换和成员推理相关的节点，正如命题 2 所示，这些是唯一可能的错误节点。 下面是 \(APT(T)\) 的定义规则： ```plaintext (APT1) APT [ T1 ...Tn af (R) ] = APT′ [ T1 ...Tn af (R) ] af (with (R) any inference rule) (APT2) APT′ [ e →e (Rf) ] = ∅ (APT3) APT′ [ T1 ...Tn e1 →e′ (Rep) T ′ e1 →e2 (Tr) ] = { APT′(T1)...APT′(Tn) APT′(T ′) e1 →e2 (Rep) } (APT4) APT′ [ T1 T2 e1 →e2 (Tr) ] = {APT′(T1), APT′(T2)} (APT5) APT′ [ T1 ...Tn e1 →e2 (Cong) ] = {APT′(T1),...,APT ′(Tn)} (APT6) APT′ [ T1 T2 e : s (SRed) ] = {APT′(T1), APT′(T2)} (APT7) APT′ [ T1 ...Tn e : s (Mb) ] = { APT′(T1)...APT′(Tn) e : s (Mb) } (APT8) APT′ [ T1 ...Tn e1 →e2 (Rep) ] = { APT′(T1)...APT′(Tn) e1 →e2 (Rep) } ``` 在证明调试技术的正确性和完备性之前，我们需要一些辅助结果： - **引理 1**：设 \(T\) 是一个证明树，其根节点相对于预期解释 \(I\) 无效。那么存在某个 \(T' \in APT'(T)\)，使得 \(T'\) 的根节点相对于 \(I\) 无效。 - **引理 2**：设 \(T\) 是一个证明树，\(APT(T)\) 是其缩写证明树。那么 \(APT(T)\) 的根节点不可能是错误节点。 ### 定理 1 设 \(S\) 是一个规范，\(I\) 是其预期解释，\(T\) 是一个根节点无效的有限证明树。那么： - \(APT(T)\) 至少包含一个错误节点（完备性）。 - \(APT(T)\) 中的任何错误节点都与 \(S\) 中的一个错误等式相关联。 这个定理表明，我们可以安全地使用缩写证明树作为 Maude 功能模块声明式调试的基础：该技术将从用户检测到的任何初始症状开始找到一个错误节点。当然，这些结果假设用户正确回答了调试器关于 \(APT\) 节点有效性的所有问题。 ## 4. 使用调试器 ### 4.1 假设 由于我们正在调试 Maude 功能模块，它们需要满足适当的可执行性要求，即规范必须是终止的、合流的和排序递减的。 我们的工具允许用户通过对可疑声明应用标签来信任某些声明。这意味着未标记的声明被假定为正确的。在实现中，受信任的声明的处理方式与 \(APT\) 转换中处理自反性、传递性和同余规则的方式相同；更具体地说，与受信任声明对应的成员或替换推理规则的实例在缩写证明树中会被合并。 为了获得非空的缩写证明树，用户必须标记一些声明（所有标签都不同）；否则，一切都被假定为正确。特别是，为了找到错误声明，必须对其进行标记。当并非所有声明都被标记时，第 3 节中显示的正确性和完备性结果取决于用户负责的标记的正确性。 尽管用户可以引入导入其他模块的模块，但调试过程在扁平化模块中进行。然而，调试器允许用户信任整个导入模块。 如引言中所述，调试树的导航是通过向外部神谕（在我们的情况下，是用户或用户引入的另一个模块）提问来进行的。在这两种情况下，答案都被假定为正确的。如果模块实际上不正确或