$\Psi$-TM: An Exact Rounds-versus-Queries Trade-off for Pointer Chasing, Machine-Checked in Lean 4

技术摘要：$\Psi$-TM：针对指针追踪（Pointer Chasing）的精确轮数与查询次数权衡

问题定义
本文探讨了确定性查询算法中关于适应性（adaptivity）的一个基本问题：当限制自适应轮数时，会产生多少计算代价（以读取输入单元的数量衡量）？所研究的具体问题是 $k$ 步指针追踪（$k$-step pointer chasing）。

输入由 $k$ 个表 $T_0, \dots, T_{k-1}$ 组成，每个表将 $m$ 个条目组成的集合 $\{0, \dots, m-1\}$ 映射到其自身。算法从 $a_0 = 0$ 开始，生成一条链 $a_{j+1} = T_j(a_j)$。目标是判定最终值 $T_{k-1}(a_{k-1})$ 是否为非零。
在标准的自适应设置中，算法可以每轮追踪链的一步，需要 $k$ 轮和 $k$ 次读取。然而，如果轮数被限制在 $d < k$ 以内，算法必须在不知道之前查询结果的情况下，在单轮内读取多个单元（即“批次”）。核心问题是：在最多 $d$ 轮内解决该问题所需的最小读取次数（代价）是多少？

方法论与模型
作者引入了一个名为 $\Psi$-TM（Psi-Turing Machine）的自包含形式化模型，专门用于形式化描述。

• 接口（The Interface）： 机器仅通过接口 $\iota(c) = x(c)$ 访问输入 $x: C \to V$。它永远不会直接看到输入。
• 策略（Strategies）： 计算被建模为策略树。一个策略要么是一个判定（out），要么是一个查询批次（ask(Q, f)）。在 ask 构造函数中，机器在一个轮次内提交一组单元 $Q$，并接收其限制（restriction）$x|_Q$。后续策略的延续 $f$ 是一个从这些限制到后续策略的函数。
• 度量指标（Metrics）：
  • 深度 ($d$)： 使用的轮数（批次）数量。
  • 代价 ($B$)： 读取的总单元数。读取两次的单元计为两次。
• 形式化（Formalization）： 该模型、问题以及主定理均使用 Lean 4（版本 4.22.0）进行形式化，且仅使用了其核心库（未引入 Mathlib）。证明过程完全依赖于公理 propext 和 Quot.sound，且不包含任何 sorry 占位符。

关键结果
论文确立了在最多 $d$ 轮内决定 $k$ 步指针追踪的最小代价的精确权衡公式，记作 $\text{cost}_d(L_k)$。

定理 4.1（精确权衡）：
对于整数 $k \ge 1, m \ge 2, d \ge 0$：
$$\text{cost}_d(L_k) = \begin{cases} \infty & \text{若 } d = 0 \\ (k - d)m + d & \text{若 } 1 \le d \le k \\ k & \text{若 } d \ge k \end{cases}$$

解读：

• $d=0$： 在没有任何轮数的情况下，没有任何算法能判定该问题。
• $1 \le d \le k$： 代价恰好为 $(k-d)m + d$。
  • 算法可以承担单独追踪前 $d$ 步的代价（消耗 $d$ 次读取）。
  • 剩余的 $k-d$ 步必须通过读取整个表来覆盖（每个表消耗 $m$ 次读取），因为算法此时尚不知道链是如何进入这些表的。
  • 边际代价（Marginal Cost）： 每减少一轮（将 $d$ 减少 1），代价会增加恰好 $m-1$ 次读取。
• $d \ge k$： 代价饱和于 $k$（即决策树的非自适应深度）。

证明技术

1. 上界（命题 5.1）： 作者构造了一个策略 $U_d$，在前 $d-1$ 轮中每轮读取一个单元以追踪链，并在最后一轮（第 $d$ 轮）读取下一个链单元以及剩余 $k-d$ 个表的所有单元。这实现了代价 $(k-d)m + d$。
2. 下界（命题 6.1）： 作者采用了一种新颖的 恒等对手（identity adversary）。
   • 不同于传统的通过对链外查询回答“0”来强制边界的对手（这无法强制得出精确界限），该对手维持一个输入，该输入在除“前沿”（chain frontier，即第一个未被读取的链单元）以外的所有地方都是恒等函数（$x(j, a) = a$）。
   • 当算法读取前沿单元时，对手会更新输入，以引导链向第一个仍有未读单元的表移动。
   • 这迫使算法要么读取整个表（以确保不会错过链的路径），要么无法确定标签。证明表明，任何具有 $d$ 轮的策略在面对该对手时，必须至少读取 $(k-d)m + d$ 个不同的单元。

机器检查验证与计算确认

• Lean 形式化： 整个逻辑结构，包括策略、对手、不变式和主定理的定义，均已在 Lean 4 中完成机器检查。形式化涵盖了所有 $d$ 的代价边界，尽管关于单个输入上“不同单元”的具体证明是在纸面上完成的（形式化版本界定了总读取次数，这足以证明定理）。
• 穷举搜索： 一个独立的 Python 脚本针对较小的参数（$k, m \le 6$）执行了穷举极小极大搜索（minimax search）。计算检查确认了对于所有测试情况，公式 $(k-d)m + d$ 均成立，并验证了恒等对手确实能够强制实现下界。

意义与范围
作者声称该研究在以下三个特定领域具有重要意义：

1. 精确性： 虽然以往的工作（如 Canonne 和 Gur）建立了适应性层级和轮数分离，但其结果通常仅限于多项式因子或针对随机算法，而本文为确定性算法提供了每一深度的精确权衡值。
2. 简洁性与可形式化性： 证明足够基础，以至于可以完全从第一原理开始在证明助手中进行形式化，无需外部库。这证明了复杂的查询复杂度下界可以实现机器可验证。
3. 对手设计： 论文引入了一种特定的“恒等对手”，克服了指针追踪中标准“零对手”（zero-adversaries）的局限性，从而能够推导出精确的下界，而非仅仅是渐近下界。

作者明确指出，该结果是关于查询复杂度的陈述；文中未分析运行时间，且输入严格通过定义的接口进行访问。这项工作并非提出新的应用，而是完善了对决策树适应性的理论理解。