论文技术总结：基于希尔伯特第十问题的构造性证明里士定理与停机问题

1. 研究背景与问题定义

核心问题：
里士定理（Rice's Theorem）指出，任何非平凡的程序语义属性（Semantic Property）都是不可判定的。传统的证明方法通常依赖于停机问题（Halting Problem），并通过**对角化（Diagonalization）和排中律（Law of Excluded Middle, LEM）**来构建矛盾。

现有方法的局限性：

1. 非构造性：经典证明通常使用排中律（例如：假设程序要么停机要么不停机，或者假设某个属性 $P(\bot)$ 要么为真要么为假），这使得证明在直觉主义逻辑（Intuitionistic Logic）中无效。
2. 自引用与对角化：传统证明依赖于递归定理或自引用构造（如构造一个程序，其行为取决于判定器对其自身的判定），这在某些构造性框架（如程序提取系统 Coq/Agda）中难以直接执行或提取为验证程序。
3. 依赖层级：通常先证明停机问题不可判定，再推导里士定理。

本文目标：
提供里士定理和停机问题的构造性证明，满足以下条件：

• 在直觉主义逻辑中有效，不使用排中律（LEM）。
• 避免对角化和自引用。
• 仅依赖希尔伯特第十问题（Hilbert's Tenth Problem, H10）的不可判定性作为公理。
• 通过 Rocq（Coq）证明助手进行形式化验证。

2. 方法论：双见证构造（Two-Witness Construction）

本文的核心创新在于提出了一种双见证构造，直接利用希尔伯特第十问题（MRDP 定理）的不可判定性，而非通过停机问题。

2.1 核心思想

给定一个非平凡语义属性 $P$，存在两个显式给出的程序 $e_0$（不满足 $P$）和 $e_1$（满足 $P$）。对于任意丢番图多项式 $D$，构造两个程序 $S^0_D$ 和 $S^1_D$：

• 若 $D$ 有解：$S^0_D$ 的行为等价于 $e_0$，$S^1_D$ 的行为等价于 $e_1$。
• 若 $D$ 无解：$S^0_D$ 和 $S^1_D$ 均表现为完全发散（即等价于 $\bot$，对所有输入无限循环）。

2.2 构造细节

程序 $S^b_D$（其中 $b \in \{0, 1\}$）在输入 $y$ 上的行为如下：

1. 枚举：按规范顺序枚举所有可能的整数元组 $\vec{x}$。
2. 计算：计算 $D(\vec{x})$。
3. 分支：
   • 如果在第 $n$ 步发现 $D(\vec{x}) = 0$（即找到解），则对于所有燃料（fuel）$\ge n$ 的调用，直接返回 $e_b(y, \text{fuel})$ 的结果。
   • 如果枚举无限进行且从未找到解，则程序发散。

2.3 逻辑推导

假设存在一个判定器 $\text{Decide}_P$ 能判定属性 $P$。定义差值函数：
$$\delta_D = \text{Decide}_P(S^1_D) - \text{Decide}_P(S^0_D)$$

• 情况 A（$D$ 有解）：
  • $S^1_D \simeq e_1$（满足 $P$），故 $\text{Decide}_P(S^1_D) = 1$。
  • $S^0_D \simeq e_0$（不满足 $P$），故 $\text{Decide}_P(S^0_D) = 0$。
  • 结果：$\delta_D = 1$。
• 情况 B（$D$ 无解）：
  • $S^1_D \simeq \bot$ 且 $S^0_D \simeq \bot$。
  • 由于 $S^1_D$ 和 $S^0_D$ 在观测上等价（Observational Equivalence），根据语义属性的扩展性（Extensionality），$\text{Decide}_P(S^1_D) = \text{Decide}_P(S^0_D)$。
  • 结果：$\delta_D = 0$。
  • 关键点：此推导不需要知道 $P(\bot)$ 的具体真值，因为两个程序行为完全一致，判定器必然返回相同结果。

矛盾：
函数 $D \mapsto \delta_D$ 构成了一个可计算的布尔分离器（将丢番图方程的可解性映射为 1 或 0），这与 MRDP 定理（希尔伯特第十问题不可判定）直接矛盾。

3. 关键贡献

1. 完全构造性证明：

   • 证明在直觉主义逻辑中有效，未使用排中律（LEM）。
   • 避免了经典证明中常见的对角化论证和自引用（Self-reference）。
   • 消除了对 $P(\bot)$ 真值的依赖（即不需要假设 $P(\bot) \lor \neg P(\bot)$）。

2. 新的归约路径：

   • 改变了传统的证明方向：经典证明是 $\text{Halting} \to \text{Rice}$，而本文证明是 $\text{MRDP} \to \text{Rice} \to \text{Halting}$。
   • 停机问题的不可判定性作为里士定理的一个直接推论（Corollary）出现，仅需一行代码实例化。

3. 形式化验证：

   • 使用 Rocq（Coq）证明助手完成了完整的形式化。
   • 基于**步进索引模型（Step-indexed model）**定义观测等价性，避免了传统部分递归函数模型中的复杂性。
   • 所有定理（包括 MRDP 的不可判定性）均通过形式化验证，零经典公理（Zero Classical Axioms），唯一的公理依赖是 Larchey-Wendling 和 Forster 在 coq-library-undecidability 中证明的希尔伯特第十问题不可判定性。

4. 无全总性要求（No Totality Condition）：

   • 通过让见证程序 $S^b_D$ 将完整的“燃料预算”传递给 $e_b$，解决了以往构造中需要见证程序全总性（Totality）的问题，使得定理适用于任意部分程序。

4. 主要结果

• 里士定理（构造性版本）：对于任何非平凡语义属性 $P$，不存在能判定 $P$ 的程序。
• 停机问题：作为里士定理的特例（属性为“在输入 0 上稳定终止”），其不可判定性被直接推导出来。
• 公理依赖分析：
  • 整个证明链中，唯一的非构造性假设来源是希尔伯特第十问题的不可判定性（MRDP）。
  • 该假设本身在 CIC（构造性演算）中已被证明，不依赖经典逻辑。
  • 里士定理和停机问题的证明在 Rocq 中显示为"Closed under the global context"（即不依赖任何额外的外部假设）。

5. 意义与影响

1. 计算内容（Computational Content）：

   • 构造性证明意味着该不可判定性论证可以被“提取”为验证程序。在程序提取系统（如 Coq/Agda）中，经典证明无法直接执行，而本文的证明可以内化到这些系统中，无需引入额外的经典公理。

2. 反向数学（Reverse Mathematics）：

   • 精确界定了证明里士定理所需的非构造性原则：仅需希尔伯特第十问题的不可判定性，无需排中律或对角化。这有助于理解计算理论中不同不可判定性结果之间的逻辑强度关系。

3. 结构新颖性：

   • 提出了“非分支归约”（Non-branching reduction）：信息编码在两个程序之间的关系差异（$\delta_D$）中，而不是基于单个程序行为的分支判断。这种结构特性可能具有独立的研究价值。

4. 实际应用与边界：

   • 文章讨论了有界程序（Bounded Programs）的可判定性边界，指出里士定理的不可判定性依赖于无界计算。
   • 提供了一个 C 语言示例程序 undecidable.c，展示了该构造在现实世界中的对应物，其终止性等价于一个未解决的数论猜想（关于整数立方和的猜想）。

总结

Jonathan Brossard 的这篇论文通过引入双见证构造，成功地在直觉主义逻辑框架下重新证明了里士定理和停机问题。该方法摒弃了经典证明中的对角化和排中律，直接利用希尔伯特第十问题的不可判定性作为基石。这一成果不仅在理论计算机科学中深化了对不可判定性本质的理解，也为在形式化验证工具中内化这些不可判定性论证提供了可行的构造性路径。