技术摘要：具有全局追踪条件的无穷演算 Lambda 演算

问题陈述

本文解决了定义一个稳健的、支持全函数（total functions）和有意义的无限归约的无穷 Lambda 演算（infinitary lambda calculus）所面临的挑战。虽然由 Kennaway 等人建立的无穷 Lambda 演算 ($\Lambda^\infty$) 允许无限项和无限归约，但它允许“无意义”的项（例如 $0\ 0$ 或 $\text{succ}(\lambda x.x)$）以及“活跃”（active）项（即无限次地归约到红/赤项，却无法产生有意义的输出）。此外，标准的无穷项类型系统通常无法确保类型的唯一性，也无法保证类型为 $\text{Nat}$ 的闭项能归约为数（numerals）。作者旨在构建一个扩展了 $\Lambda^\infty$ 且包含算术常量（$0$, $\text{succ}$, $\text{cond}$）的系统，并采用类似于哥德尔 System T 的类型系统，同时强制执行确保强收敛性和全性的条件。

方法论

1. 项集的构建

作者通过一系列连续的限制来定义该演算，以确保句法和语义的健全性：

• 行项 (Row-Terms, $\text{Row-}\Lambda^\infty_T$)： 由变量、$\lambda$-抽象、应用和算术常量（$0$, $\text{succ}$, $\text{cond}$）生成的可能为无限项的基集。这些项是有限项度量完备化（metric completion）中的元素。
• 有限变量项 (Finite Variable Terms, $\text{FinVar-}\Lambda^\infty_T$)： $\text{Row-}\Lambda^\infty_T$ 的一个子集，仅包含有限个自由变量。这一限制对于在不产生歧义的情况下通过余归纳（corecursively）定义 $\alpha$-等价和替换至关重要。
• 良型项 (Well-Typed Terms, $\text{WTyped}$)： 在特定类型系统中具有类型推导的 $\text{FinVar-}\Lambda^\infty_T$ 中的项。
• GTC-项 (GTC-Terms, $\text{GTC-}\Lambda^\infty_T$)： 满足全局追踪条件 (Global Trace Condition, GTC) 的最终良型项子集。

2. 类型系统与追踪关系

作者引入了一个与标准简单类型 Lambda 演算具有不同特征的类型系统（图 1）：

• 上下文作为序列： 上下文是变量类型的有限序列而非集合，因此需要显式的弱化（weakening）和交换（exchange）规则（$wk$）。
• 分裂应用规则： 应用规则被分为 $apv$（当参数为变量时）和$ap\neg v$（否则），反映了结构收缩。
• 追踪关系 (Trace Relations)： 系统包含了“追踪关系”（在推导中体现为蓝色和红色箭头），将上下文中的变量与参数位置的类型联系起来。
  • 静态 (Stationary, 蓝色)： 代表非递减的引用。
  • 进展 (Progressing, 红色)： 特别是将 $\text{cond}$ 项结论中的第一个参数与其前提中对应的参数联系起来，代表数值的减少。

3. 全局追踪条件 (GTC)

借鉴 Brotherston 和 Simpson 的循环证明（Cyclic Proofs）以及 Das 的循环 System T 的概念，GTC 被定义在推导树上：

• 追踪 (Trace) 是沿推导分支的一条由追踪关系组成的链。
• 进展点 (Progress Point) 是在条件项归约过程中出现的红色（进展）追踪关系。
• GTC 要求： 若一条推导满足 GTC，则每一条无限分支都必须包含一条无限次发生进展的追踪。
• 该条件有效地排除了“活跃”项（即没有输出的无限循环）以及不表示全泛函（total functionals）的项。

4. 归约与收敛

论文定义了 $\beta$-归约和 $\text{cond}$-归约规则。为了处理无限归约，作者引入了 $\text{cond}$-收敛 (cond-convergence)：

• 如果对于任何极限序数，被收缩红项（特别是那些位于 $\text{cond}$ 右分支的红项）的深度都趋于无穷大，则称该归约为 $\text{cond}$-收敛。
• 这是一个比标准强收敛更强的条件，确保通过 $\text{cond}$ 进行的递归调用不会在“else”分支上陷入无限循环。

核心贡献与结果

1. 强收敛与规范化

核心定理（定理 3.2）确立了对于任何项 $t \in \text{GTC-}\Lambda^\infty_T$：

• 所有归约都是 $\text{cond}$-收敛的（从而也是强收敛的）。
• 规范化 (Normalization)： 任何始终归约最小 $\text{cond}$-深度的红项的策略，都会在最多 $\omega$ 步内终止于规范型（normal form）。
• 全性 (Totality)： 若 $t$ 是类型为 $\text{Nat}$ 的闭项，则此类归约会在有限步内终止于形式为 $\text{succ}^n(0)$ 的数。

2. 类型唯一性与主体规约

定理 2.3 证明了对于 $\text{GTC-}\Lambda^\infty_T$ 中的项：

• 唯一性： 对于任何上下文 $\Gamma$，存在唯一的类型 $A$ 使得 $\Gamma \vdash t : A$ 是可证明的。
• 主体规约 (Subject Reduction)： 如果 $\Gamma \vdash t : A$ 可证且 $t \to t'$，那么 $\Gamma \vdash t' : A$ 同样可证。
• 作者指出，虽然证明本身不是唯一的，但可以通过将上下文限制为自由变量并折叠冗余的弱化规则，将其转化为唯一的规范形式。

3. 表达能力与等价性

• 论文认为，当限制在正则项（regular terms）时，该演算精确地定义了 Das 的循环 System T（一种不含 $\lambda$ 的 System T 的无穷版本）中所定义的全函数。
• 因此，该系统捕捉到了与哥德尔 System T 相同的表达能力。
• 作者声称该演算满足 极限意义下的 Church-Rosser 性，从而确保了 $\text{Nat}$ 类型闭项所得结果的唯一性。

意义与主张

本文声称为具有算术的无穷 Lambda 演算提供了一个健全的基础，通过类型论条件（GTC）保证了全性和强收敛性。通过将循环证明技术应用于 Lambda 演算，作者成功地过滤掉了无意义的无限项和活跃循环，确保了良型项表现为全泛函。

其意义在于弥合了无穷重写系统与类型论之间的鸿沟，证明了全局追踪条件即使在存在无限项和无限归约的情况下，也能强制实现强规范化属性。作者谦虚地推测其系统的表达能力等价于哥德尔 System T，将 $\text{GTC-}\Lambda^\infty_T$ 定位为 Das 循环 System T 的 Lambda 演算扩展。