🔢 mathematics

Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-Čubrić Interpolation

本文基于双向类型化原则，为Čubrić在简单类型λ演算中提出的证明相关插值定理提供了新证明，并在Rocq中完成了形式化验证。

原作者： Meven Lennon Bertrand, Alexis Saurin

发布于 2026-03-04

📖 1 分钟阅读🧠 深度阅读

原作者： Meven Lennon Bertrand, Alexis Saurin

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文讲述了一个关于**“如何在两个不同的逻辑世界之间架起桥梁”的故事。为了让你轻松理解，我们可以把这篇论文的核心内容想象成“翻译官”与“乐高积木”**的游戏。

1. 核心故事：寻找“中间人” (插值定理)

想象你有两个朋友，A 和 B。

A 说的是“只有苹果和香蕉”的语言。
B 说的是“只有香蕉和橙子”的语言。
现在，A 证明了一个结论，这个结论能推导出 B 的某个观点（即 $A \vdash B$ ）。

克雷格插值定理 (Craig Interpolation) 告诉我们：在 A 和 B 之间，一定存在一个**“中间人” (插值项 I)**。

这个中间人只说**“香蕉”**（也就是 A 和 B 共有的概念）。
A 能说服中间人，中间人也能说服 B。
这就好比：A 不需要直接跟 B 吵架，而是通过一个大家都听得懂的“香蕉”概念来传递信息。

2. 这篇论文做了什么？(从“只给答案”到“展示过程”)

以前的研究（比如 Čubrić 的工作）虽然找到了这个“中间人”，但他们的证明过程有点**“黑箱操作”**：

他们像是一个魔术师，直接变出了中间人，但没告诉你具体是怎么变出来的。
他们的证明方法很繁琐，像是在数积木的块数，然后一块块地替换，容易出错，而且很难让人看懂其中的逻辑。

这篇论文的突破在于：
作者 Meven Lennon-Bertrand 和 Alexis Saurin 不仅找到了中间人，还重新设计了搭建桥梁的方法，让整个过程变得清晰、优雅，并且完全可验证。

他们做了一件很酷的事：把“证明”本身也变成了可以计算的“程序”。

以前：A 证明 $\to$ 中间人 $\to$ B。
现在：A 的证明过程 + 中间人的证明过程 + B 的证明过程 = 原始的完整证明。
这就像你不仅得到了一个翻译好的句子，还拿到了翻译的逐字逐句的对照表，你可以看到每一个词是怎么转换的。

3. 关键工具：双向 typing (像“双向车道”的导航)

为了理清这个复杂的证明，作者引入了一种叫**“双向类型检查” (Bidirectional Typing)** 的技术。

打个比方：
想象你在玩一个乐高积木游戏。

传统方法：你手里拿着一堆积木，试图拼出一个形状，但不知道下一步该拿哪块，只能盲目尝试（这就像传统的“推断”模式）。
双向方法：
1. 输入模式 (检查)：有人告诉你：“这里必须放一个红色的三角形”。你只需要检查手里的积木是不是红色的三角形。
2. 输出模式 (推断)：你手里拿着一块积木，系统自动告诉你：“这块积木是红色的三角形”。

这篇论文发现，“双向车道”的导航逻辑，恰好完美对应了数学中**“子公式性质”**（即证明过程中用到的所有概念都必须来自开头或结尾，不能凭空捏造）。

作者发现，那些最完美的、没有冗余步骤的证明（称为“正规形式”），天然就符合这种“双向导航”的规则。
利用这个规则，他们把原本像“迷宫”一样的证明过程，变成了一条清晰的、有路标的**“高速公路”**。

4. 为什么要这么做？(不仅仅是为了好看)

作者把这篇论文的内容写进了一个叫 Rocq 的计算机证明助手（以前叫 Coq）里。

之前的困境：以前的证明太复杂，计算机很难自动验证，人类读起来也头大。
现在的成果：
1. 更清晰：用“双向导航”的逻辑重新梳理了证明，像把乱麻理成了顺绳。
2. 可验证：所有的步骤都在计算机里跑通了，证明是 100% 正确的，没有漏洞。
3. 新发现：他们发现，以前大家以为“双向导航”在处理“加法/求和”类型的逻辑时会失效，但这次证明其实并没有失效，只是大家之前没找对打开方式。

5. 总结：这篇论文意味着什么？

如果把逻辑学比作建筑学：

旧方法：建筑师告诉你“这栋楼很稳固”，但他只给你看一张模糊的蓝图，而且有些结构是偷偷加固的，别人看不懂。
这篇论文：建筑师不仅告诉你楼很稳固，还把每一块砖的摆放逻辑、每一根梁的受力分析都画了出来，并且用计算机模拟了无数次，证明它绝对结实。

这对我们有什么意义？
虽然这听起来很学术，但这种“证明过程可计算、可追踪”的思想，是未来人工智能、软件安全、密码学的基础。

如果未来的 AI 能像这篇论文描述的那样，不仅给出答案，还能给出完美、可验证的推导过程，那么我们在开发自动驾驶、医疗诊断或金融系统时，就能更放心地信任 AI 的决策，因为我们可以像检查乐高说明书一样，检查它的每一个逻辑步骤。

一句话总结：
这篇论文用一种更聪明、更清晰的方法（双向导航），重新证明了逻辑世界中“中间人”的存在，并且把整个过程变成了计算机可以严格检查的代码，让逻辑推理变得更加透明和可靠。

这篇论文《Lambda 演算的双向插值：重访与形式化 Craig-Čubrić 插值》由 Meven Lennon-Bertrand 和 Alexis Saurin 撰写，主要研究了在带有和类型（sums）的简单类型 Lambda 演算（STLC+）中，如何构建并形式化证明相关（proof-relevant）的 Craig 插值定理。

以下是对该论文的详细技术总结：

1. 研究背景与问题 (Problem)

Craig 插值定理：逻辑学中的经典定理，指出如果 $A \vdash B$ ，则存在一个插值公式 $I$ ，它仅包含 $A$ 和 $B$ 中共同的谓词符号，且满足 $A \vdash I$ 和 $I \vdash B$ 。
证明相关插值 (Proof-relevant Interpolation)：传统的插值定理仅关注公式的存在性。证明相关版本（由 Čubrić 在 STLC+ 中提出）进一步要求：如果有一个证明项 $t$ 证明 $A \vdash B$ ，那么存在一个中间类型 $C$ （插值类型）和两个项 $u: A \to C$ 和 $v: C \to B$ ，使得它们的组合 $(\lambda y.v) u$ 在归约后等于原始项 $t$ 。这不仅是逻辑公式的分解，更是证明项（Proof terms）的分解。
现有挑战：
- Čubrić 的原始证明基于对项大小的归纳，通过逐步用变量替换子项来实现。这种方法结构不清晰，且在某些情况下（如处理和类型时）存在逻辑漏洞或表述不清。
- 在带有和类型（ $+$ ）和空类型（ $\bot$ ）的 STLC+ 中，普通的 $\beta$ -正规形式（ $\beta$ -normal forms）不具备良好的子公式性质（subformula property），这使得插值证明变得困难。
- 需要一种更结构化的方法来处理正规形式，以便进行归纳证明。

2. 方法论 (Methodology)

作者提出了一种基于**双向类型检查（Bidirectional Typing）**的新证明方法，并利用 Rocq（Coq 的继任者）进行了完全的形式化。

双向类型系统与正规形式：
- 作者将正规形式（Normal Forms）和中性项（Neutral Forms）通过双向类型系统（推断 $\triangleright$ 和检查 $\triangleleft$ ）进行归纳刻画。
- 核心洞察：双向类型系统天然地捕捉了“子公式性质”。在推断模式下，类型是输出；在检查模式下，类型是输入。这种信息流限制了项中出现的类型必须源自上下文或子项，从而保证了子公式性质。
- 针对和类型和空类型，作者引入了交换转换（Commuting Conversions）。普通的 $\beta$ -归约不足以处理正类型（Positive Types）的正规形式，必须通过交换转换将消除符（eliminations）推入正类型内部，以获得具有良好子公式性质的正规形式。
逻辑关系与正规化：
- 为了证明所有良类型项都能归约到这种双向定义的正规形式，作者使用了**逻辑关系（Logical Relations）**方法。
- 定义了“覆盖（Covering）”概念，用于处理正类型上的消除符（如 raise 和 if），确保即使项不是中性的，也能被逻辑关系所覆盖。
- 证明了语义类型化（Semantic Typing）蕴含正规化（Normalization）。
插值证明策略：
- 利用双向类型系统的归纳结构，对正规形式和中性项进行互归纳（Mutual Induction）。
- 引入了**上下文划分（Context Partition）**的概念，将上下文 $\Gamma$ 划分为源部分（ $\Gamma_s$ ）和目标部分（ $\Gamma_t$ ），以追踪词汇（Vocabulary）的来源。
- 对于中性项，根据其主要变量来自源上下文还是目标上下文，分情况讨论插值类型的构造。

3. 主要贡献 (Key Contributions)

新的插值证明：
- 提出了一种基于双向类型系统的新证明，替代了 Čubrić 基于项大小归纳的旧证明。
- 新证明更加直接、结构清晰，且易于形式化。它明确利用了正规形式的归纳刻画，避免了旧证明中模糊的“类似情况”处理。
- 证明了对于任何 $x: A \vdash t: B$ ，存在类型 $C$ 和项 $u, v$ ，使得 $u \circ v \twoheadrightarrow^* t$ 。
STLC+ 的元理论形式化：
- 在 Rocq 中形式化了带有和类型及交换转换的简单类型 Lambda 演算的元理论。
- 首次形式化了带有交换转换的 STLC+ 的正规化定理（Normalisation）。这是该领域的一个重要里程碑，因为之前的形式化工作通常避免处理交换转换的复杂性。
- 形式化代码量约 4000 行（包括自动生成代码），相比其他插值形式化工作（如 Férée 等人的工作）更加紧凑高效。
双向类型与子公式性质的关联：
- 明确建立了双向类型系统与子公式性质之间的联系。作者指出，虽然双向类型系统通常被认为在和类型上会失效（因为无法保证唯一性），但在处理插值所需的“弱”正规形式（具有子公式性质但不一定是 $\eta$ -长形式）时，双向类型系统是完美的工具。
词汇与常量的处理：
- 将插值定理推广到包含任意常量和等式理论的语言，并精确控制了插值类型中使用的词汇（包括常量类型）。

4. 结果 (Results)

定理 22 & 25 (插值定理)：成功证明了在 STLC+ 中，对于任何良类型的项 $t$ ，都可以分解为两个项的复合，且中间类型仅包含源和目标共享的词汇。
定理 18 & 19 (正规化)：证明了所有良类型项都可以通过归约（包含 $\beta$ 和交换转换）到达一个由双向类型系统定义的正规形式。
形式化验证：所有主要定理（包括正规化、插值、合流性的部分证明）均在 Rocq 中得到验证。
性能：形式化编译时间极短（约 30 秒），证明了该方法的自动化程度高且易于维护。

5. 意义与影响 (Significance)

理论深度：该工作不仅重访了经典的 Čubrić 定理，还通过引入双向类型视角，揭示了证明相关插值与类型系统结构之间的深层联系。它澄清了双向类型系统在处理正类型正规形式时的适用性。
形式化基准：提供了第一个带有交换转换的 STLC+ 正规化定理的完整形式化证明，为后续在 Rocq 中研究更复杂的类型系统（如依赖类型）奠定了基础。
自动化实践：论文详细讨论了在 Rocq 中使用自动化求解器（如 asimpl, setoid rewriting）的经验教训，特别是处理替换演算（Substitution Calculus）和合流性证明时的挑战，为未来的形式化工作提供了宝贵的工程指导。
未来方向：
- 非正规项的插值：目前结果仅适用于正规形式。未来工作旨在通过引入类型注解（Annotations）来扩展至包含红式（Redexes）的项，实现“带割（with cuts）”的插值。
- 均匀插值（Uniform Interpolation）：探索是否存在不依赖于具体证明项 $t$ 的均匀插值。
- 依赖类型：尝试将结果扩展到依赖类型理论，尽管这面临交换转换在依赖类型中可能不保持良类型的挑战（如“车队模式”问题）。

总结：
这篇论文通过结合双向类型系统的结构优势，成功重访并简化了 Craig-Čubrić 插值定理的证明，并首次在 Rocq 中完成了包含交换转换的 STLC+ 的正规化与插值的形式化。这项工作不仅解决了旧证明中的技术缺陷，还展示了现代交互式定理证明器在处理复杂类型理论元理论问题时的强大能力。