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

Technical Summary: $\Psi$-TM: An Exact Rounds-versus-Queries Trade-off for Pointer Chasing

Problem Definition
The paper addresses the fundamental question of adaptivity in deterministic query algorithms: how much computational cost (in terms of the number of input cells read) is incurred when the number of adaptive rounds is restricted? The specific problem studied is $k$-step pointer chasing.

The input consists of $k$ tables, $T_0, \dots, T_{k-1}$, each mapping a set of $m$ entries $\{0, \dots, m-1\}$ to itself. An algorithm starts at $a_0 = 0$ and generates a chain $a_{j+1} = T_j(a_j)$. The goal is to decide whether the final value $T_{k-1}(a_{k-1})$ is non-zero.
In a standard adaptive setting, an algorithm can follow the chain one step per round, requiring $k$ rounds and $k$ reads. However, if the number of rounds is limited to $d < k$, the algorithm must read multiple cells in a single round (a "batch") before knowing the results of previous queries. The central question is: what is the exact minimum number of reads (cost) required to solve the problem with at most $d$ rounds?

Methodology and Model
The author introduces a self-contained formal model called $\Psi$-TM (Psi-Turing Machine), designed specifically for formalization.

• The Interface: The machine accesses the input $x: C \to V$ only through an interface $\iota(c) = x(c)$. It never sees the input directly.
• Strategies: Computation is modeled as a tree of strategies. A strategy is either a verdict (out) or a query batch (ask(Q, f)). In the ask constructor, the machine submits a list of cells $Q$ in one round and receives the restriction $x|_Q$. The continuation $f$ is a function from these restrictions to subsequent strategies.
• Metrics:
  • Depth ($d$): The number of rounds (batches) used.
  • Cost ($B$): The total number of cells read. A cell read twice counts twice.
• Formalization: The model, the problem, and the main theorem are formalized in Lean 4 (version 4.22.0) using only the core library (no Mathlib). The proofs rely solely on the axioms propext and Quot.sound and contain no sorry placeholders.

Key Results
The paper establishes an exact trade-off formula for the minimum cost of deciding $k$-step pointer chasing with at most $d$ rounds, denoted as $\text{cost}_d(L_k)$.

Theorem 4.1 (Exact Trade-off):
For integers $k \ge 1$, $m \ge 2$, and $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}$$

Interpretation:

• $d=0$: No algorithm can decide the problem without any rounds.
• $1 \le d \le k$: The cost is exactly $(k-d)m + d$.
  • An algorithm can afford to follow $d$ steps of the chain individually (costing $d$ reads).
  • The remaining $k-d$ steps must be covered by reading entire tables (costing $m$ reads per table), because the algorithm does not yet know where the chain enters those tables.
  • Marginal Cost: Removing one round (reducing $d$ by 1) increases the cost by exactly $m-1$ reads.
• $d \ge k$: The cost saturates at $k$ (the non-adaptive depth of the decision tree).

Proof Techniques

1. Upper Bound (Proposition 5.1): The author constructs a strategy $U_d$ that reads one cell per round for the first $d-1$ rounds to follow the chain, and in the final round ($d$), reads the next chain cell plus all cells of the remaining $k-d$ tables. This achieves the cost $(k-d)m + d$.
2. Lower Bound (Proposition 6.1): The author employs a novel identity adversary.
   • Unlike standard adversaries that answer "0" to off-chain queries (which fails to force the exact bound), this adversary maintains an input that is the identity function ($x(j, a) = a$) everywhere except at the "frontier" (the first unread cell of the chain).
   • When the algorithm reads the frontier cell, the adversary updates the input to steer the chain to the first table after the current one that still contains unread cells.
   • This forces the algorithm to either read the entire table (to ensure it doesn't miss the chain's path) or fail to determine the label. The proof shows that any strategy with $d$ rounds must read at least $(k-d)m + d$ distinct cells against this adversary.

Machine-Checked Verification and Computational Confirmation

• Lean Formalization: The entire logical structure, including the definition of strategies, the adversary, the invariants, and the main theorem, is machine-checked in Lean 4. The formalization covers the cost bounds for all $d$, though the specific proof regarding "distinct cells" on a single input remains on paper (the formal version bounds total reads, which suffices for the theorem).
• Exhaustive Search: An independent Python script performs an exhaustive minimax search over all possible strategies for small parameters ($k, m \le 6$). This computational check confirms the formula $(k-d)m + d$ for all tested cases and verifies that the identity adversary correctly forces the lower bound.

Significance and Scope
The paper claims significance in three specific areas:

1. Exactness: While previous work (e.g., Canonne and Gur) established adaptivity hierarchies and round separations up to polynomial factors or for randomized algorithms, this paper provides the exact value of the trade-off at every depth for deterministic algorithms.
2. Simplicity and Formalizability: The proof is elementary enough to be fully formalized from first principles in a proof assistant without external libraries, demonstrating that complex query complexity lower bounds can be made machine-verifiable.
3. Adversary Design: The paper introduces a specific "identity adversary" that overcomes the limitations of standard "zero-adversaries" in pointer chasing, allowing for the derivation of the exact lower bound rather than just an asymptotic one.

The author explicitly states that the result is a statement about query complexity only; running time is not analyzed, and the input is accessed strictly through the defined interface. The work does not propose new applications but rather refines the theoretical understanding of adaptivity in decision trees.