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

技術要約：$\Psi$-TM：ポインタチェイシングにおける正確なラウンド数対クエリ数のトレードオフ

問題定義
本論文は、決定論的なクエリアルゴリズムにおける適応性の根本的な問い、すなわち、適応的なラウンド数（adaptive rounds）を制限した場合に、どれほどの計算コスト（入力セルの読み取り数）が発生するかという問題に取り組んでいる。研究対象となっているのは、$k$ステップ・ポインタチェイシングである。

入力は、$m$個のエントリ $\{0, \dots, m-1\}$ を自身へと写像する$k$個のテーブル $T_0, \dots, T_{k-1}$ で構成される。アルゴリズムは $a_0 = 0$ から開始し、連鎖 $a_{j+1} = T_j(a_j)$ を生成する。目標は、最終的な値 $T_{k-1}(a_{k-1})$ が非ゼロであるかどうかを判定することである。

標準的な適応的設定では、アルゴリズムは1ラウンドにつき1ステップずつ連鎖を辿ることができ、これには$k$ラウンドと$k$回の読み取りを要する。しかし、ラウンド数が $d < k$ に制限されている場合、アルゴリズムは、前のクエリの結果を知る前に、一度のラウンドで複数のセルをまとめて読み込む（「バッチ」として扱う）必要がある。中心となる問いは、最大$d$ラウンドでこの問題を解決するために必要な最小の読み取り数（コスト）はいくらであるか、ということである。

手法とモデル
著者は、形式化のために設計された、自己完結的な形式モデルである $\Psi$-TM (Psi-Turing Machine) を導入している。

• インターフェース: マシンは、入力 $x: C \to V$ に対して、インターフェース $\iota(c) = x(c)$ を通じてのみアクセスする。マシンは入力を直接見ることは決してない。
• 戦略 (Strategies): 計算は、戦略の木としてモデル化される。戦略は、判定 (out) またはクエリバッチ (ask(Q, f)) のいずれかである。ask コンストラクタにおいて、マシンは1つのラウンドでセル集合 $Q$ を提出し、その制限 $x|_Q$ を受け取る。継続関数 $f$ は、これらの制限から後続の戦略への関数である。
• 指標:
  • 深さ ($d$): 使用されるラウンド（バッチ）の数。
  • コスト ($B$): 読み取られたセルの総数。セルを2回読み取った場合は2回としてカウントされる。
• 形式化: モデル、問題、および主要な定理は、外部ライブラリを使用せず、コアライブラリのみを用いて Lean 4 (バージョン 4.22.0) で形式化されている。証明は propext と Quot.sound の公理のみに依存しており、sorry によるプレースホルダーは含まれていない。

主要な結果
本論文は、$k$ステップ・ポインタチェイシングを最大$d$ラウンドで決定するための最小コスト $\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{if } d = 0 \\ (k - d)m + d & \text{if } 1 \le d \le k \\ k & \text{if } d \ge k \end{cases}$$

解釈:

• $d=0$: ラウンドなしでは、この問題を決定できるアルゴリズムは存在しない。
• $1 \le d \le k$: コストは正確に $(k-d)m + d$ である。
  • アルゴリズムは、最初の $d$ ステップを個別に辿る（コストは $d$ 回の読み取り）ことができる。
  • 残りの $k-d$ ステップについては、連鎖がどのテーブルに入るか（どこへ進入するか）がまだ不明であるため、テーブル全体を読み込む必要がある（各テーブルにつき $m$ 回の読み取り）。
  • 限界コスト (Marginal Cost): ラウンドを1つ減らす（$d$ を 1 減らす）と、コストは正確に $m-1$ 回増加する。
• $d \ge k$: コストは $k$ （非適応的な決定木の深さ）で飽和する。

証明手法

1. 上界 (Proposition 5.1): 著者は、最初の $d-1$ ラウンドでは連鎖を辿るために1ラウンドにつき1セルを読み込み、最終ラウンド（$d$）では次の連鎖のセルと、残りの $k-d$ 個のテーブルの全セルを読み込む戦略 $U_d$ を構築する。これにより、コスト $(k-d)m + d$ が達成される。
2. 下界 (Proposition 6.1): 著者は、新しい 恒等アドバーサリ (identity adversary) を用いる。
   • 標準的なアドバーサリ（オフチェーンのクエリに対して「0」と回答するもの）は、正確な下界を強制できない。
   • このアドバーサリは、「フロンティア」（連鎖の最初の未読セル）を除いて、入力が恒等関数 ($x(j, a) = a$) であるような入力を維持する。
   • アルゴリズムがフロンティアのセルを読み取ると、アドバーサリは入力を更新し、現在のテーブルの次にある、まだ未読のセルを含む最初のテーブルへと連鎖を誘導する。
   • これにより、アルゴリズムは、連鎖の経路を見逃さないためにテーブル全体を読み込むか、あるいはラベルを特定できなくなるかのいずれかを強いられる。証明によれば、任意の $d$ ラウンドの戦略は、このアドバーサリに対して少なくとも $(k-d)m + d$ 個の異なるセルを読み取らなければならない。

機械検証と計算による確認

• Lean による形式化: 戦略、アドバーサリ、不変量、および主要な定理の定義を含む論理構造全体が、Lean 4 によって機械的に検証されている。形式化はすべての $d$ についてのコスト境界をカバーしているが、単一の入力に対する「異なるセル」に関する具体的な証明は紙面上で行われており、形式版は総読み取り数を抑えるものであり、定理を証明するには十分である。
• 全探索: 独立した Python スクリプトが、小さなパラメータ（$k, m \le 6$）に対して、可能なすべての戦略に対するミニマックス探索を実行する。この計算によるチェックは、すべてのテストケースにおいて式 $(k-d)m + d$ が成立することを確認し、恒等アドバーサリが正しく下界を強制することを検証している。

意義と範囲
本論文は、以下の3つの特定の領域において重要であると主張している：

1. 正確性: Canonne や Gur らの先行研究は、多項式因子での適応性の階層や、確率的アルゴリズムにおけるラウンドの分離を確立したが、本論文は決定論的アルゴリズムにおけるあらゆる深さでの正確なトレードオフの値を提供している。
2. 簡潔性と形式化可能性: 証明は極めて初等的であり、外部ライブラリを使用せずに証明助手から第一原理のみを用いて完全に形式化できるほど単純である。これは、複雑なクエリ計算量の下界が機械検証可能になり得ることを示している。
3. アドバーサリの設計: 本論文は、ポインタチェイシングにおける標準的な「ゼロ・アドバーサリ」の限界を克服し、漸近的な下界ではなく正確な下界を導出することを可能にする、特定の「恒等アドバーサリ」を導入している。

著者は、この結果はクエリ計算量のみに関する記述であることを明記している。実行時間は分析されておらず、入力は定義されたインターフェースを通じて厳密にアクセスされる。本研究は新しい応用を提案するものではなく、決定木における適応性の理論的理解を洗練させるものである。