面向非不相交等式理论并集的分层统一过程及其可终止组合

《Journal of Logical and Algebraic Methods in Programming》：Hierarchical Unification Procedures and Their Combinations

　　

等式统一（equational unification）问题——其底层等式理论可能由一个分量等式理论的并集给出——在实践中经常出现在自动推理（automated reasoning）、逻辑程序设计（logic programming）、声明式程序设计（declarative programming）和安全协议形式分析（formal analysis of security protocols）等诸多领域。研究人员通过分层统一（hierarchical unification）方法研究非不相交等式理论并集（non-disjoint union of equational theories）中的统一问题。在此背景下，针对子理论已知的统一算法通过附加推理规则（inference rules）进行扩展，以计入理论的其余部分。研究人员提出一种分层统一过程（hierarchical unification procedure）形式，它特别适合语法理论（syntactic theories），其中可通过突变规则（mutation rules）处理理论公理来获得统一过程。多种语法理论类对分层统一过程进行了示例说明。例如，研究人员考虑最优重写系统（optimal rewrite systems），其中任一最内层可归约表达式（innermost redex）可在单步中规范化。研究此情形使研究人员获得可用于协议分析的理论的终止分层统一过程。此外，研究人员考察已使用分层方法的理论的模块化方法（modularity methods）。研究人员给出获得终止（组合）分层统一过程的充分条件。

该论文作者为Serdar Erbatur、Andrew Marshall、Christophe Ringeissen。研究背景方面，等式统一（equational unification）是在项生成结构中求解方程约束的问题，在基于归结原理的逻辑系统、声明式程序设计计算和自动推理中具有核心作用；语法统一（syntactic unification）因可判定且幺正（unitary）而在逻辑程序设计中尤为重要。更一般地，等式统一在等式理论模下定义，一般不可判定，但针对特定理论类已有专门技术；结合性-交换性（Associativity-Commutativity, AC）等理论常用于表示算术算子，等式重写和等式统一也已集成到基于规则的编程语言中。安全协议形式分析是另一重要应用：协议通常表示为带等式的一阶逻辑子句，等式理论用于按Dolev-Yao符号模型刻画入侵者能力；推理需要等式统一过程及演绎问题、静态等价问题等知识问题判定过程。具有有限变体性质（Finite Variant Property, FVP）的理论可将等式统一归约为语法统一，Maude-NPA和Tamarin等协议分析器显式依赖变体统一（variant-based unification），其常用窄化（narrowing）实现；折叠变体窄化（folding variant narrowing）对FVP类完备且终止。FVP理论是语法理论（syntactic theories）的例子；语法理论可用突变（mutation）完成根变换以扩展经典分解规则，但语法性不足以保证突变型统一过程终止。AC是语法理论，但非不相交并集（non-disjoint union）的组合比不相交组合更困难，已有工作多集中于不相交组合或受限非不相交情形，终止组合过程尤其困难。因此，该研究开展分层统一与组合方法研究，以复用分量理论的E-统一算法并处理共享符号的理论并集。

研究开展与意义方面，研究人员提出分层统一过程框架H_E(U)，其中U为E-扩展简化器（E-extension simplifier），由固定组合规则、E-统一算法和U组成；进而研究最优E-构造TRS、E-保守理论（E-conservative theory）、E-语法理论（E-syntactic theory）、最优E-保守表示以及正则且无坍缩E-保守理论的组合，给出可靠完备及终止条件。其意义在于为协议分析中有用理论及非不相交理论并集提供模块化统一算法构造方法。

关键方法（不超过250字）：研究人员采用分层统一框架H_E(U)，以Coalesce、Split、Flatten、VA、U、Solve等规则构成组合循环；用突变型推理系统BSM_R、DMS、BSM_F处理非Σ₀方程；引入E-构造TRS（E-constructed TRS）、最优重写（IR¹）、E-保守标准化映射、E-消解表示（E-resolvent presentation）、E-capped理论和CSV复杂度证明终止；以分配指数、加密/解密、群密钥等示例说明。该研究为形式化理论研究，未涉及实验样本队列。

研究结果如下。2 预备知识：建立等式统一、E-统一问题、完全E-统一集CSU_E(G)、求解形式、E-收敛与Church-Rosser模E、构造子、E-构造TRS、最优IR¹及C-重命名稳定重写序等定义，为后续构造提供形式基础。3 分层统一：定义H_E(U)推理系统及分离有向无环图求解形式，证明任何分层统一过程均为可靠完备的F∪E-统一过程，终止者称为分层统一算法。4 具有构造子的理论：定义构造子集合与Σ₀-基，证明若Σ₀为F∪E的构造子集合，则E-统一对F∪E-统一的Σ₀片段完备；E-构造TRS满足该性质。5 最优E-构造TRS：使用BSM_R，证明对最优E-构造TRS，H_E(BSM_R)为可靠完备且终止的R∪E-统一算法；两个仅共享E的最优E-构造TRS之并也具有相应算法。6 E-保守理论：以C-重命名稳定重写序和E-构造标准化映射定义E-保守理论，证明其与E-构造标准化映射等价；该类对仅共享E的并集封闭；在6.1给出E-构造TRS和内构造子理论例子，在6.2证明E-统一对Σ₀片段完备。7 E-语法理论：定义E-消解表示与E-语法性，利用DMS突变规则构造E-扩展简化器；在E-保守且所有Σ\Σ₀-根项模F∪E为子项无坍缩时，H_E(DMS)可靠完备；7.2证明对E-保守F，F∪E语法当且仅当F∪E为E-语法且E语法。8 最优E-保守表示：定义最优E-保守表示，证明该类对仅共享E的并集封闭；BSM_F使F∪E为E-语法并给出终止可靠完备的H_E(BSM_F)算法；群密钥/成员密钥与删除示例说明该框架。9 正则且无坍缩E-保守理论：用i-抽象证明F_i∪E-统一对Σ_i片段完备；在简单组合条件下H_E(U₁∪U₂)可靠完备；E-capped保证简单组合；在递减复杂度下给出组合终止定理，CSV复杂度用于分配指数等例；并证明同一理论副本在仅共享E时可组合终止。

讨论与结论部分总结：该研究提出若干可应用分层组合统一方法的等式理论类，这些理论均为背景理论E的保守扩展并与语法性相关，有助于构造与E-统一算法组合的突变型推理系统；给出模块化结果，以模块化方式构造仅共享E的理论并集的统一过程；并识别出分层统一过程实际终止的若干情形，从而得到统一算法。讨论指出，判定一个理论是否属于所引入理论类并非易事，例如E-保守性或E-capped性不能以纯语法方式检查，需寻找额外充分条件；任意E-保守理论并集的组合仍是开放问题，但常量作为非内层共享构造子等特殊情形可能有组合结果。未来工作包括将分层方法用于析取统一（disunification）问题，以及安全协议符号分析中的演绎和静态等价等知识问题。研究结论翻译：研究人员提出了若干等式理论类，分层组合统一方法可适用于这些理论类，从而提供统一过程；在这些类中，等式理论被定义为某背景理论E的保守扩展，并可与语法性概念相关联，这有助于开发基于突变的推理系统并与E-统一算法组合；研究人员展示了若干模块化结果，通过模块化构造组合理论的统一过程来求解仅共享E的理论并集中的统一问题；并识别出若干分层统一过程实际终止的情形，产生统一算法，例如最优E-保守理论以及某些正则且无坍缩E-保守理论的特定并集。