How to play the Accordion: Uniformity and the (non-)conservativity of the linear approximation of the λ-calculus (extended version)

技术摘要：“如何演奏手风琴：$\lambda$-演算线性近似的均匀性与（非）保守性”

问题陈述
本文研究了 $\lambda$-演算在线性近似框架下的保守性（conservativity），特别是在 Ehrhard 和 Regnier 的微分 $\lambda$-演算与资源演算框架内。虽然泰勒展开 $T(M)$ 对 $\lambda$-项 $M$ 的模拟 $\beta$-归约（即若 $M \to_\beta N$，则 $T(M) \twoheadrightarrow_r T(N)$）已是公认的事实，但反向问题仍然存在：在资源演算中的每一次归约，是否都由源 $\lambda$-演算中的实际归约所诱导？

形式化地讲，给定资源演算中的一个归约 $T(M) \twoheadrightarrow_r T(N)$（作用于资源项的无限线性组合），是否存在一个 $\beta$-归约序列 $M \to_\beta N$？作者区分了两种设定：

1. 有限 $\lambda$-演算： 项是有限的，归约是有限序列。
2. 无穷 $\lambda$-演算 ($\lambda^{001}$)： 项可以是无限的（共归纳的），归约可以是无限序列 ($\to^{001}_\beta$)，前提是红克斯（redexes）在递增的深度处被触发。

核心问题在于，在线性近似是否为这些设定下的源演算的一个保守扩展（conservative extension）。

方法论
作者结合了重写理论、共归纳定义以及“混合”（mashup）技术（将源项与其资源近似值联系起来）。

1. 有限情况分析： 对于有限项，作者采用了 Kerinec 和 Vaux Auclair 使用的“混合”证明技术。他们定义了一个将 $\lambda$-项与资源近似值联系起来的关系 $\vdash$。通过证明如果 $T(M) \twoheadrightarrow_r T(N)$，则 $M \vdash T(N)$，并且随后证明 $M \vdash T(N)$ 蕴含 $M \to^*_\beta N$，从而确立了有限情况下的保守性。
2. 无穷情况的反例（手风琴）： 为了处理无穷情况，作者构造了一个特定的反例——手风琴 ($A$)。该项旨在模拟一个“拉伸”并“压缩”其结构的无限归约序列。
   • 项 $A$ 归约为一系列近似无限项 $\bar{A} = (\langle T \rangle)(\langle F \rangle)\omega$ 的项 $A_n$。
   • 至关重要的是，虽然 $T(A) \twoheadrightarrow_r T(\bar{A})$ 成立，但作者证明不存在有效的无穷 $\beta$-归约 $A \to^{001}_\beta \bar{A}$。$A$ 的归约路径要求在有界深度处进行“全局”步骤，这违反了无穷 $\beta$-归约所需的分层条件（引理 2.5）。
3. 均匀性与相干性： 为了在无穷设定下恢复保守性，作者引入了均匀性（uniformity），这一属性最初由 Ehrhard 和 Regnier 提出。他们定义了资源项上的相干关系 ($\bowtie$)，并将归约关系限制在均匀和（uniform sums，即所有元素两两相干的求和）上。
   • 他们定义了均匀资源归约 ($\to^{\curvearrowright}_r$) 及其无穷闭包 ($\to^{\curvearrowright \infty}_r$)。
   • 这种限制确保了资源演算中的归约严格对应于源演算中的归约，消除了那些无法映射到实际 $\beta$-归约的“非均匀”路径。
4. 向 $\beta_\perp$ 扩展： 作者将这些结果扩展到 $\beta_\perp$-归约（即将不可解项坍缩为 $\bot$），证明了均匀性在涉及 $\bot$-归约时仍能保持保守性。

核心贡献

1. 有限项的保守性： 本文提供了线性近似对于有限 $\lambda$-演算是保守的严谨证明（定理 3.1）。
2. 无穷项的非保守性： 作者证明了标准的逐点资源归约 ($\twoheadrightarrow_r$) 对于无穷 $\lambda$-演算是非保守的。他们构造了手风琴反例（定理 4.4），证明 $T(A) \twoheadrightarrow_r T(\bar{A})$ 并不意味着 $A \to^{001}_\beta \bar{A}$。
3. 通过均匀性恢复： 本文指出均匀性是恢复保守性所需的缺失要素。通过将资源演算限制为均匀归约 ($\to^{\curvearrowright \infty}_r$)，作者证明了线性近似成为了无穷 $\lambda$-演算的一个保守扩展（定理 5.10）。
4. $\beta_\perp$ 扩展： 结果被推广到 $\beta_\perp$-归约，表明均匀方法在涉及未定义项 $\bot$ 的归约时同样保持保守性（定理 5.18 和 5.19）。

结果

• 有限设定： 资源归约对有限 $\beta$-归约的模拟是保守的。
• 无穷设定（标准）： 标准逐点资源归约对无穷 $\beta$-归约的模拟是非保守的。手风琴项 $A$ 在资源演算中归约为 $\bar{A}$，但在 $\lambda$-演算中并非如此。
• 无穷设定（均匀）： 均匀资源归约对无穷 $\beta$-归约的模拟是保守的。
• $\beta_\perp$ 设定： 标准归约的非保守性延伸到了 $\beta_\perp$-归约，而均匀归约在 $\beta_\perp$ 下依然保持保守。

意义
本文阐明了线性近似作为 $\lambda$-演算动力学之忠实模型的精确条件。它解决了第一作者博士论文中的一个猜想，即关于定量线性近似在无穷设定下的非保守性问题。

其主要意义在于，作者不仅将均匀性视为泰勒展开的一种语义属性，更将其视为一种必要的、针对归约关系的句法约束，以确保保守性。如果没有这一限制，资源演算会允许产生没有源演算对应项的“幽灵”归约，尤其是在存在无限项的情况下。这项工作通过区分“模拟”（simulation）与“保守性”（conservativity），完善了对“交换定理”（即归约与近似是否交换）的理解，表明虽然模拟普遍成立，但保守性需要更严格的均匀框架。

作者明确指出，其工作通过为反例和均匀性结果提供完整证明，并将其分析扩展到 $\beta_\perp$-归约（这对于将项与其 Böhm 树联系起来至关重要），从而改进了之前的会议版本。