The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (Full Version)

技术摘要：用于 $\beta\eta$-范式高阶重写的可计算路径序

问题陈述
高阶重写涵盖了多种形式化方法，特别是“普通”高阶重写（使用句法匹配并将 $\beta$-归约视为重写规则）和“范式”高阶重写（使用模 $\beta\eta$ 匹配并考虑 $\beta\eta$-范式项）。虽然对于普通重写存在强大的终止判定方法，例如可计算路径序（CPO），但将这些方法适配到范式高阶重写（特别是类似于 Nipkow 的高阶重写系统，HRS）时面临着重大挑战。

现有的 HRS 方法（如 NHORPO）通常依赖于一种称为“中性化”（neutralization）的转换技术，以处理核心序失效的情况。然而，中性化增加了自动化的难度。此外，标准的路径序难以处理范式重写，因为与 $\beta\eta$ 相容的良基序在传统意义上通常不是单调的（对上下文封闭）或稳定的（对替换封闭）。例如，如果一个序与 $\beta\eta$ 相容且对上下文封闭，它可能会导致诸如 $c > c$ 之类的矛盾，从而违反良基性。

方法论
作者提出将最初为普通高阶重写定义的计算路径序（CPO）提升到 $\beta\eta$-范式高阶重写的设定中。由此产生的序被称为 $\beta\eta$-范式可计算路径序（NCPO）。

该方法论依赖于以下核心组件：

1. 归约序对： 遵循 Jouannaud 和 Rubio 的方法，作者定义了一个归约序对 $(>, \sqsupset)$，其中 $>$ 是主要序（NCPO），而 $\sqsupset$ 是其“普通”变体（CPO）。该对满足 $\beta\eta$-范式稳定性：如果 $s > t$，则对于所有替换 $\sigma$，$s\sigma\downarrow \sqsupset^+ t\sigma\downarrow$ 成立（其中 $\downarrow$ 表示 $\beta\eta$-范式化）。这使得证明终止性可以依赖于普通 CPO 组件的良基性和单调性。
2. 非多变项（Nonversatile Terms）： 一个关键的技术创新是将该序的应用限制在非多变项上。如果一个项在进行替换并随后进行 $\beta\eta$-范式化后，仅影响其真子项，则称该项为非多变的。作者提供了一个比之前工作更改进的非多变性充分条件（引理 1），这对于证明该序的稳定性至关重要。
3. 从 CPO 扩展： NCPO 包含了来自原始 CPO 的两个关键扩展：
   • 可达子项（Accessible Subterms）： 这些允许递归比较绕过由类型位置（正/负基类型位置）决定的特定情况下的严格类型下降。
   • 小符号（Small Symbols）： 该特性允许某些函数符号被视为“小的”，从而实现对标准递归路径序失效的系统（例如列表处理函数）的终止性证明。
4. 规则集： 该序通过一组规则（图 1）归纳定义，处理函数符号（大/小）、应用和抽象。值得注意的是，处理 $\beta$ 和 $\eta$ 归约定向的规则被移除了，因为该序直接作用于范式。引入了一个新的规则 $\langle \lambda\triangleright\eta \rangle$，用于处理涉及可达子项背景下 $\eta$-扩张的特定情况。

核心贡献

• NCPO 的定义： 本文正式定义了 NCPO，这是第一个专门为 $\beta\eta$-范式高阶重写设计的、集成了可达子项和小符号的计算路径序。
• 正确性证明： 作者证明了序对 $(>_\tau, \sqsupset_\tau)$ 构成了一个有效的 $\beta\eta$-范式高阶归约序（定理 2），从而保证了任何与其相容的 HRS 的终止性。
• 改进的非多变性条件： 本文提供了一个更精炼的非多变性充分条件，该条件比 NHORPO 基础工作中提供的条件更强。
• 通过 SAT/SMT 实现自动化： 作者认为 NCPO 比使用中性化的 NHORPO 更易于自动化。由于中性化需要依赖于符号参数的复杂句法分析（使得 SMT 编码困难），而 NCPO 的参数（优先级、类型序、状态）可以更直接地进行编码。

结果
作者使用 Haskell 实现了一个 NCPO 原型，利用 Hasmtlib 包将终止问题编码为 SML-LIB 2 格式，并使用 Z3 求解器进行求解。实验结果（表 1）将 NCPO 与 NHORPO（包括带中性化和不带中性化的情况）以及 WANDA 和 CSI$^{ho}$ 中的 HORPO 实现进行了对比。

• 优于 NHORPO： NCPO 成功证明了若干 NHORPO（即使使用中性化）无法证明终止的系统。具体而言：
  • 示例 8（列表递增）： NCло 使用小符号证明了终止，而这是 NHORPO 所缺失的特性。
  • 示例 7（否定范式）： NCPO 使用可达子项证明了终止，而使用中性化的 NHORPO 由于无法处理比较中的多变项而无法定向规则。
• 不可比的效力： 研究识别了一些案例（例如 neutr.p），在这些案例中，使用中性化的 NHORPO 成功而 NCPO 失败，表明两者具有不可比的效力。
• 效率： 研究表明，寻找 NCPO 参数在计算上是高效的，其耗时通常与 NHORPO 搜索相当，而搜索中性化参数的复杂度可能会发生爆炸。

意义与主张
本文声称 NCPO 为 NHORPO 与中性化的组合提供了一个强大且轻量级的替代方案。作者强调，虽然带中性化的 NHORPO 是一个强有力的竞争者，但由于自动化中性化技术的复杂性，NCPO 是范式高阶重写中自动终止证明更实用的选择。

作者谦虚地指出，NCPO 的传递性仍是一个开放性问题，因为底层普通序中 $\beta$-归约的包含使得 CPO 和 NHORPO 具有非传递性，而 NCPO 的具体属性仍需进一步研究。此外，他们建议将 NCPO 集成到范式高阶重写的依赖对技术中是逻辑上的下一步。文章最后强调了对高阶终止方法进行形式化验证的必要性，以避免先前文献中出现的错误，例如关于 NHORPO 能解决某些示例的错误主张。