Information Propagation and Contraction in Functional Interpretations

技术摘要：函数解释中的信息传播与收缩

问题陈述
函数解释（起源于哥德尔的 Dialectica 解释）是提取证明中计算内容的核心技术，尤其是在证明挖掘（proof mining）领域。现有的变体（例如 Diller–Nahm、单调、有界、Herbrand 化解释）通常同时结合了多种证明论机制：见证（witness）与挑战（challenge）信息的传播、重复假设的处理（收缩/contraction），以及外延性（extensionality）的处理。这种混杂使得难以分离出负责不同方面的特定代数结构。本文旨在识别一种将仿射信息传播（其中假设不被复制）与收缩（其中复制的假设必须进行合并）机制分离开来的方法。

方法论
作者提出了一个模块化框架，通过两个主要的代数组件来解耦这些机制：

1. 信息核（Information Nuclei）： 一个旨在捕捉函数解释之仿射核心的代数接口。一个定义在目标系统 $S$ 上的信息核由以下部分组成：

   • 一个从有限类型 $\sigma$ 到信息类型 $\sigma^\sharp$ 的映射。
   • 一个精确对象 $x$ 与信息对象 $a$ 之间的相容关系 $x \triangleleft_\sigma a$。
   • 一个单位操作 $\eta_\sigma: \sigma \to \sigma^\sharp$，将精确对象嵌入到信息中。
   • 一个 Kleisli 扩展 $\kappa_{\sigma,\tau}: (\sigma \to \tau^\sharp) \to \sigma^\sharp \to \tau^\sharp$，用于通过函数传播信息。
     这些组件必须满足公理，以确保精确对象与其嵌入保持相容，并且信息能够通过函数应用正确传播。

2. 收缩结构（Contraction Structures）： 将仿射解释扩展到完全直觉主义系统所需的额外层。这涉及一个以公式为索引的操作 $ctr_A$，它接收由重复假设产生的两个挑战界限，并将它们还原为单个界限。该操作的正确性由一个性质定义，该性质确保：针对合并后的界限的有效性蕴含了针对原始分离界限的有效性。

该框架在有限类型算术系统中运行，特别区分了：

• $N\text{-}HA^\omega_{aff}$：不带收缩的仿射系统。
• $N\text{-}HA^\omega$：带有完整收缩的完整系统。
• $HA^\omega_{obs}$：具有观测相等性（可判定基类型）的系统，用于恢复标准的 Dialectica 解释。

主要贡献与结果

• 关注点分离（Separation of Concerns）： 本文确立了函数解释的复杂性是可以分解的。“仿射核心”完全由信息核表征，而收缩则由独立的结构处理。这使得能够独立于假设如何重用，来系统地指定提取实值（realizers）所携带的信息。
• 可靠性定理（Soundness Theorems）：
  • 仿射可靠性（定理 17）： 任何信息核都会诱导一个对于仿射有限类型算术（$N\text{-}HA^\omega_{aff}$）可靠的函数解释。提取的实值和挑战界限满足源公式在目标系统中的翻译。
  • 完全可靠性（定理 22）： 如果一个信息核配备了合适的收缩结构，该解释可以扩展到完整的有限类型算术（$N\text{-}HA^\omega$）和具有观测相等性的系统（$HA^\omega_{obs}$）。
• 恢复已知解释： 该框架将现有的解释统一为信息核和收缩结构的特定实例：
  • 精确信息核（Exact Information Nucleus）： 其中 $\sigma^\sharp \equiv \sigma$ 且相容性为相等。结合“选择型”收缩结构（基于可判定性在两个挑战中选择其一），这恢复了 $HA^\omega_{obs}$ 上的标准 Dialectica 解释。
  • 有限候选信息核（Finite Candidate Nucleus）： 其中 $\sigma^\sharp$ 代表候选集合，相容性为成员关系。结合“合并型”收缩结构（集合的并集），这产生了 Herbrand 型解释。
• 丰富实值： 一个重要的技术结果是能够系统地用辅助数据丰富提取的实值。通过选择一个信息对象携带额外结构的信息核，提取过程可以自然地传播这些数据。
  • 连续性示例： 本文通过一个“连续性核”展示了这一点，其中信息对象由一个值和一个连续模组成。由此产生的解释不仅提取见证，还提取携带逐点连续性数据的实值，这些数据是通过证明的组合方式而非通过后处理得到的。

意义与主张
本文声称提供了一种“指定提取实值所携带信息的统一方法”。不同于以往试图通过单一复杂参数化来恢复所有解释的统一框架，本方法隔离了一个用于仿射部分的最小代数接口，并识别了处理收缩所需的精确额外结构。

作者强调，这种模块化视角将信息的指定与处理重复假设的结构性处理分离开来。这种分离允许通过简单地改变信息核来系统地用辅助数据（如连续性信息）丰富函数解释，而不必改变提取的底层逻辑机制。论文明确指出，目前将外延性处理留作未来工作，指出当前的框架恢复了观测相等性下的标准 Dialectica 解释，但尚未处理弱外延性或全外延性规则。

这项工作被定位为对“统一”和“参数化”计划（如 Oliva 及其合作者）的改进，提供了一种更细粒度的代数分离，有助于通过证明传播额外的计算数据。