Towards Weak Stratification for Logics of Definitions

技术摘要：迈向定义逻辑的弱分层化

问题陈述
定义逻辑（Logic of Definitions）是一类用于编码和推理由推理规则指定的判断（judgments）的逻辑，其中原子谓词与可能依赖于该谓词自身的逻辑公式相关联。为了解决此类定义中固有的表观循环问题，标准方法引入了“分层条件”（stratification condition），确保谓词不会在自身定义的体（body）中负向出现（即出现在蕴含式的左侧）。这一条件实际上是将定义视为单调不动点算子。

然而，许多有用的规范（特别是涉及证明编程语言属性的逻辑关系/logical relations）需要允许谓词负向出现的定义。在 Abella 证明助手所基于的逻辑 $\mathcal{G}$ 中，此类定义是不被允许的。虽然 Tiu [19] 此前引入了一种名为 $\mathcal{LD}$ 的逻辑，该逻辑将分层条件放宽为“弱分层”（允许负向出现，只要负向出现的层级严格小于头部谓词的层级），但 $\mathcal{LD}$ 仅限于一个核心片段。它缺乏对 $\nabla$ 量词（$\nabla$ quantifier，对于通过名常量处理名称及其新鲜度至关重要）以及超越自然数归纳的一般性归纳定义（general inductive definitions）的支持。本研究旨在解决的任务是：在包含 $\nabla$ 量词和一般归纳定义的情况下，将定义逻辑扩展到弱分层化，同时保持一致性。

方法论
本文定义了一种新的逻辑 $\mathcal{LD}\mu\nabla$，它通过引入 $\nabla$ 量词和一般归纳定义来扩展 Tiu 的 $\mathcal{LD}$。其方法论分为三个主要阶段：

1. $\mathcal{LD}\mu\nabla$ 的语法与语义：
   该逻辑被构建为一阶序贯演算（first-order sequent calculus）的扩展，包含一组定义 $\mathcal{D}$ 和一组归纳定义 $\mathcal{I}$。

   • 弱分层（Weak Stratification）： 若对于每一个子句 $H \triangleq_X B$ 及实例化替换 $\rho$，满足 $\text{lvl}(H\rho) \ge \text{lvl}(B\rho)$，则称定义集 $\mathcal{D}$ 是弱分层的。至关重要的是，这允许负向出现的定义谓词，前提是该负向出现的层级严格小于头部的层级。
   • 归纳的严格分层（Strict Stratification for Induction）： 本文对归纳定义 $\mathcal{I}$ 施加了更严格的条件：它们必须是“严格分层”的（即基础原子谓词的层级必须独立于其参数）。这种限制对于防止结合归纳与弱分层时出现不一致性是必要的。
   • $\nabla$ 量词： 该逻辑引入了 $\nabla$ 量词以处理名常量（nominal constants）和新鲜度，区分了名称的泛化实例（generic instances）与特定实例（specific instances）。

2. 基底逻辑与解释：
   为了证明一致性，作者构造了一个基底版本的逻辑 $\mathcal{LD}\mu\nabla_\infty$，其中所有公式均为基底公式（无特征变量/eigenvariables）。

   • 基底引理（Grounding Lemma）： 一个关键的技术步骤是证明 $\mathcal{LD}\mu\nabla$ 中的任何推导都可以通过基底替换（grounding substitution）解释为 $\mathcal{LD}\mu\nabla_\infty$ 中的推导。这把全逻辑的一致性问题简化为了基底逻辑的一致性问题。
   • 无穷规则（Infinitary Rules）： 在 $\mathcal{LD}\mu\nabla_\infty$ 中，标准的 $\forall R$ 和 $\exists L$ 规则被替换为对所有基底项进行量化的无穷规则，且用于归纳的 $\mu L$ 规则也同样扩展到了涵盖所有基底实例。

3. 切消除（Cut Elimination）：
   一致性证明的核心是消除基底逻辑 $\mathcal{LD}\mu\nabla_\infty$ 中的切规则（具体为多切规则/multicut rule）。

   • 归约关系（Reduction Relation）： 定义了一个针对推导的归约关系，规定了如何将切向上推或消除。
   • 可归约性（Reducibility）： 遵循由 McDowell 和 Miller 改编的 Tait-Martin-Löf 技术，作者定义了推导的“可归约性”（reducibility）及“可归约化”（normalizability）的概念。他们证明了 $\mathcal{LD}\mu\nabla_\infty$ 中的每个推导都是可归约的。
   • 归纳情况处理： 处理弱分层与归纳之间相互作用的一个关键方面是：作者表明，虽然弱分层对于一般定义是足够的，但归纳定义必须保持严格分层。作者通过一个反例（第 3.3 节）展示了允许归纳定义进行弱分层会导致逻辑不一致。

主要贡献

• 定义 $\mathcal{LD}\mu\nabla$： 本文正式定义了一种结合了弱分层、$\nabla$ 量词和一般归纳定义的逻辑。
• 一致性证明： 主要贡献在于证明了 $\mathcal{LD}\mu\nabla$ 的一致性。这是通过证明基底逻辑 $\mathcal{LD}\mu\nabla_\infty$ 的切消除，并建立基底解释来实现的。
• 分层约束： 本工作阐明了许可定义与不许可定义之间的界限。研究表明，虽然弱分层足以支持一般定义（从而实现逻辑关系），但归纳定义需要严格分层以维持一致性。
• 反例： 文中提供了一个具体的反例，显示放松归纳定义的分层条件会导致逻辑不一致，从而证明了对 $\mathcal{I}$ 所施加限制的正当性。

结果

• 一致性： $\mathcal{LD}\mu\nabla$ 被证明是一致的。因此，$\mathcal{LD}\mu\nabla_\infty$ 对于所有可证明的序列都允许无切推导。
• 反转性质（Inversion Properties）： 本文确立了 $\mathcal{LD}\mu\nabla_\infty$ 的元理论性质，包括各种引入规则（如 $\wedge R, \vee L, \nabla R$）的可反转性，以及在上下文为空时 $\vee R, \exists R$ 和定义规则（$\Delta R$）的部分可反转性。这些性质对于证明搜索过程至关重要。
• 局限性： 切消除定理仅针对基底逻辑 $\mathcal{LD}\mu\nabla_\infty$ 成立。文中指出，将此结果扩展到包含特征变量的全逻辑 $\mathcal{LD}\mu\nabla$ 仍是一个开放性挑战。

意义
这项工作的意义在于其扩展 Abella 证明助手能力的潜力。Abella 基于逻辑 $\mathcal{G}$，而目前的 $\mathcal{G}$ 限制定义必须是严格分层的。通过证明引入弱分层定义的合理性，本研究为 Abella 原生支持“逻辑关系”铺平了道路，而逻辑关系是证明编程语言语义属性（如类型安全性和编译器正确性）的一种基本技术。

本文将此工作定位为向更广泛的 $\mathcal{G}$ 扩展迈出的基础性一步。虽然目前的结果处理了带有 $\nabla$ 和归纳的弱分层，但作者指出，要实现对 Abella 的完全正当化，还需要进一步的扩展，以包含共归纳（co-induction）和名抽象（nominal abstraction）。这项工作也强调了保持归纳定义严格分层性的必要性，这一约束防止了将弱分层与归纳混合使用时可能产生的不一致性。