Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic

技术摘要：单类型常数域模态 Lambda 演算 I：距离化 Beta 归约与组合逻辑

1. 问题与动机
本文旨在解决模态逻辑与类型化 lambda 演算在形式化整合方面的空白。尽管理查德·蒙太格（Richard Montague）和达纳·加林（Dana Gallin）曾开发过整合这两个领域的系统，但其工作依赖于丘奇的简单类型论（包括恒等性和量化），并且在处理状态变量方面存在局限。当代类型化 lambda 演算，特别是简单类型化 lambda 演算（STLC），是计算机科学和语言学的标准基础理论，但缺乏实现现代语义分析所需的特定模态特征（例如多个状态变量和内涵上下文）。

作者肖恩·沃尔什（Sean Walsh）识别了现有框架中的两个主要缺陷：

1. 过强性： 蒙太格的系统对于现代应用来说“过强”，因为它假设了丘奇简单类型论的全套资源，而现代系统通常使用更弱的基础理论，如 STLC。
2. 过弱性： 蒙太格的系统在模态表达能力方面“过弱”；它缺乏处理二维语义、现实算子以及在单个表达式中绑定多个不同状态变量的机制。

本文旨在通过开发一个名为 $\lambda\theta$ 的系统来弥补这一缺陷，该系统将模态逻辑与简单类型化 lambda 演算相结合。一个核心挑战在于 $\lambda\theta$ 的“有限变量”特性：该系统限制了每个状态类型可用的变量数量（由参数 $\theta$ 控制）。这种限制使得无法使用标准的开项模型（open term models）来证明完备性，因为当可用变量不足以进行不捕获变量的 $\alpha$-转换时，通常的 $\alpha$-转换技术就会失效。

2. 方法论与核心定义
本文引入了 $\lambda\theta$，这是一个由 $\theta$ 参数化的系统族，其中 $\theta$ 将每个状态类型映射到一个基数（从 $1$到$\omega$），代表可用变量的数量。

• 类型： 状态类型不能作为函数类型的陪域（即，如果 $A$ 是状态类型，则 $A \to B$ 不是一种类型）。这确保了状态类型的项严格为变量或常量（命题 2.6）。
• 距离化 Beta 归约（Distanced Beta Reduction）： 一个新颖的贡献是定义了“距离化” $\beta$-归约。与直接将参数应用于 lambda 抽象的标准 $\beta$-归约不同，距离化归约允许参数 $N$ 与抽象 $\lambda v:A.L$ 被一系列中间项 $\vec{M}$ 分隔开：
  $$(\lambda \vec{x}: \vec{B}. \lambda v:A. L) \vec{M} N \to_\beta (\lambda \vec{x}: \vec{B}. L[v := N]) \vec{M}$$
  这种机制对于在缺乏足够变量进行标准 $\alpha$-转换以避免变量捕获的情况下，在 lambda 抽象之下执行归约是必要的。
• 组合逻辑基础： 本文采用了以 BCDKW 组合子（B, C, D, K, W）为中心的组合逻辑基础，而非传统的 SKI 基础。其中 Dardinal ($D$) 组合子的加入是针对本系统的特殊设计，用于处理将常量代入函数的情况。

3. 主要贡献与结果

• 模型的组合特征化 (定理 1.5)：
  本文将 Andrews 对 STLC 的 Henkin 模型特征化推广到了模态设置。它证明了一个框架是 $\lambda\theta$ 的模型，当且仅当所有 BCDKW-组合项 的指派是良定义的。这种特征化绕过了对开项模型的需求，因为由于缺乏用于 $\alpha$-转换的变量，开项模型在非极大参数（例如 $\lambda_1$）下是不存在的（例 3.9）。

• 语义保守性与可表达性 (定理 1.1 & 1.2)：
  本文解决了 Zimmermann (1989) 提出的关于极大系统 $\lambda\omega$（其中对于所有状态类型 $\theta(A) = \omega$）与受限系统 $\lambda\theta$ 之间关系的问题。

  • 保守性： 每个 $\lambda\theta$ 的模型都是 $\lambda\omega$ 的模型。因此，语义有效性得以保持：$\lambda\theta \models M = N$ 当且仅当 $\lambda\omega \models M = N$。
  • 可表达性： $\lambda\omega$ 中任何自由变量和常量均取自 $\lambda\theta$ 的项，都可以由具有相同指派的 $\lambda\theta$ 项来表达。
    这些结果意味着，“有限变量”限制并不会削弱系统在标准语义下的表达能力；极大系统对于受限系统是保守的。

• 模态与非模态系统之间的演绎关系 (定理 1.3 & 1.4)：
  本文建立了模态系统 $\lambda\omega$ 与普通非模态 STLC ($\lambda$) 之间的关系。

  • 演绎保守性： 对于 $\lambda\omega$ 中的项，$\beta\eta$-等价在 $\lambda\omega$ 中成立，当且仅仅当它在 $\lambda$ 中成立。
  • 演绎可表达性： 类型和常量与 $\lambda\omega$ 兼容的 $\lambda$ 项可以在 $\lambda\omega$ 内部表达。
    这些证明依赖于 STLC 的标准工具（Church-Rosser、强规范化），并且相对较短。

• 通过 $\infty$-规则实现的完备性 (定理 1.6)：
  由于 $\lambda\theta$（对于非极大 $\theta$）缺乏开项模型，并且在标准 $\beta\eta$-归约下不满足 Church-Rosser 性质（例 2.26），本文引入了 $\infty$-规则。该规则允许如果 $M =_{\beta\eta} N$ 在极大系统 $\lambda\omega$ 中成立，则进行归约 $M \to_\infty N$。通过添加此规则，$\lambda\theta$ 在其语义下变得演绎完备。

• 弱演绎保守性 (定理 1.7)：
  本文研究了“弱” lambda 演算，在这种演算中，归约和等价关系在 lambda 抽象下不被保持（没有 $\xi$-规则）。通过使用基于 BCDKW 基础的纯内涵组合逻辑 (CL$\theta$)，作者证明了 $\lambda\omega$ 中的弱 $\beta$-等价性被保守地扩展到了 $\lambda\theta$ 中的 $\beta\eta$-等价性（前提是签名中不包含状态类型的常量）。这一结果依赖于使用 Takahashi 的完全展开方法为弱组合逻辑建立 Church-Rosser 性质。

4. 意义与主张
本文声称提供了第一个对“现代”简单类型化模态 lambda 演算进行深入开发的成果，该系统将当代 STLC 的资源与模态逻辑相整合。其意义在于：

1. 回答了 Zimmermann 的问题： 它在很大程度上肯定了极大模态系统的表达能力即使在受限的、有限变量的设置下（无论是语义上还是通过 $\infty$-规则在演绎上）也能得到捕捉。
2. 元理论工具： 它引入了“距离化 $\beta$-归约”和基于 BCDKW 的组合逻辑，作为处理变量可用性受限系统的必要工具，克服了标准开项模型失效的问题。
3. 内涵语义： 它支持了即便在内涵上下文中，类型为 $A \to B$ 的项也可以被解释为过程的观点，方法是证明了受限系统 $\lambda\theta$ 在语义上等价于极大系统 $\lambda\omega$。

本文明确指出了局限性：它并未提供仅使用标准 $\beta\eta$-规则的 $\lambda\theta$ 完备性定理（问题 4.17），并且承认该系统并未将其解释（如可达关系）直接显露出来，而是需要特定的类型约定来对其进行建模。配套论文将这些结果扩展到了丘奇的简单类型论。