[2025年4月2日提交 (v1)，最后修订于2026年7月30日（本版本，v5）]

查看 PDF

摘要：方程集 E 在基于重写的系统 R 中具有重要的计算作用。E 诱导的等价关系 =E 将项划分成 E 等价类，在这些等价类上执行重写计算，记作 ->R/E，称为模 E 的重写。本文研究了基于条件重写的系统的 ->R/E 的汇合性，通常称为 E-汇合性，其中重写步骤由条件规则确定。我们采用 Jouannaud 和 Kirchner 的框架来研究抽象集合 A 上抽象关系 R 模抽象等价关系 E 的汇合性。我们展示了如何将此框架具体化以用于条件系统。然后，我们展示了如何定义适当的有限条件对集合来证明和否定 E-汇合性。我们引入了 (i) 基于逻辑的条件临界对，它不需要使用（通常无限多的）E-合一子来提供抽象框架中考虑的局部峰值的有限表示。我们还引入了 (ii) 参数化条件变量对，这对于在 E-汇合性分析中处理条件规则至关重要。最后，我们引入了 (iii) 向下条件对，这通常是否定 E-汇合性所必需的。我们的结果适用于众所周知的基于重写的系统类别，改进了先前的结果。对于无条件系统，我们的结果适用于等式项重写系统，首先由 Huet 研究，随后由 Jouannaud、Jouannaud 和 Kirchner 等人研究。对于条件系统，我们的结果也适用于条件重写理论和 Maude。

提交历史

来自：Salvador Lucas [查看电子邮件]
[v1] 2025年4月2日 15:55:06 UTC (184 KB)
[v2] 2025年4月3日 14:25:55 UTC (79 KB)
[v3] 2026年1月31日 19:58:23 UTC (123 KB)
[v4] 2026年7月29日 15:52:35 UTC (128 KB)
[v5] 2026年7月30日 06:03:35 UTC (128 KB)