Evaluating a game tree with an explicit stack

A game tree alternates a sum over the messages and a maximum over the replies. The value of a node with n + 1 rounds to go is its leaf value plus, for every message, the largest value over the replies of the child reached by the message and the reply; a node with no rounds to go has its leaf value (Cslib.Complexity.GameTree.value). The messages and the replies are the first N iterates next^[i] first of an enumeration, whose last one last recognizes, and a node is identified by the messages and replies leading to it, the most recent first. Every value is capped at cap, so that all numbers stay at most cap; the cap does not change values that are at most cap.

The evaluator (Cslib.Complexity.GameTree.step) is the depth-first traversal with an explicit stack. A frame stores the current message and reply of a node, the capped sum over the earlier messages, which starts at the leaf value, and the maximum over the earlier replies to the current message. A node with n rounds to go returns its value to the same stack after Cslib.Complexity.GameTree.time N n steps (Cslib.Complexity.GameTree.iterate_step_node), at most (N + 1) ^ (2 * n + 1) (Cslib.Complexity.GameTree.time_le); the evaluation from the empty stack then stays put (Cslib.Complexity.GameTree.iterate_step_eval). Along the way the stack holds at most D frames, the depth of the root, each storing two iterates and two numbers at most cap (Cslib.Complexity.GameTree.Good, Cslib.Complexity.GameTree.good_iterate_step). Thus the retained state has size polynomial in D, the size of the iterates and the size of cap. Overall time and space bounds also require resource bounds for the leaf, successor and final-element callbacks; the step count alone does not bound their cost. The certified specialization in IP/PSPACE supplies these bounds for evaluating the optimal prover in the proof of IP ⊆ PSPACE Arora and Barak, Chapter 8.

Main definitions

• Cslib.Complexity.GameTree.value: the value of a node.
• Cslib.Complexity.GameTree.step: one step of the evaluator.
• Cslib.Complexity.GameTree.time: the number of steps of an evaluation.
• Cslib.Complexity.GameTree.Good: the invariant bounding the states.

Main results

• Cslib.Complexity.GameTree.iterate_step_node: a node returns its value.
• Cslib.Complexity.GameTree.iterate_step_eval: the evaluation from the empty stack.
• Cslib.Complexity.GameTree.time_le: the number of steps.
• Cslib.Complexity.GameTree.good_iterate_step: the states stay small.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

@[reducible, inline]

abbrev Cslib.Complexity.GameTree.Frame (X : Type) : Type

A frame: the current message and reply, the capped sum over the earlier messages, and the maximum over the earlier replies to the current message.

def Cslib.Complexity.GameTree.history {X : Type} (st : List (Frame X)) : List (X × X)

The messages and replies leading to the node of a stack, the most recent first.

@[simp]

theorem Cslib.Complexity.GameTree.history_nil {X : Type} : history [] = []

@[simp]

theorem Cslib.Complexity.GameTree.history_cons {X : Type} (f : Frame X) (st : List (Frame X)) : history (f :: st) = (f.1, f.2.1) :: history st

@[simp]

theorem Cslib.Complexity.GameTree.length_history {X : Type} (st : List (Frame X)) : (history st).length = st.length

def Cslib.Complexity.GameTree.value {X : Type} (N cap : ℕ) (first : X) (next : X → X) (leaf : List (X × X) → ℕ) : ℕ → List (X × X) → ℕ

The value of a node with n rounds to go: the leaf value plus, for every message, the largest value over the replies of the child, capped at cap.

def Cslib.Complexity.GameTree.step {X : Type} (D cap : ℕ) (first : X) (next : X → X) (last : X → Bool) (leaf : List (X × X) → ℕ) : List (Frame X) × Option ℕ → List (Frame X) × Option ℕ

One step of the evaluator. Without a value to return, a node at depth D returns its leaf value, and any other node pushes a frame for its first message and reply. A value returned into a frame updates the maximum, and moves on to the next reply; after the last reply, it adds the maximum to the sum and moves on to the next message; after the last message, it pops the frame and returns the sum. A value returned into the empty stack is a fixed point.

def Cslib.Complexity.GameTree.time (N : ℕ) : ℕ → ℕ

The number of steps to evaluate a node with n rounds to go.

Correctness

theorem Cslib.Complexity.GameTree.iterate_step_node {X : Type} {D N cap : ℕ} {first : X} {next : X → X} {last : X → Bool} {leaf : List (X × X) → ℕ} (hN : 0 < N) (hlast : ∀ i < N, last (next^[i] first) = decide (i + 1 = N)) (n : ℕ) (st : List (Frame X)) (hst : st.length + n = D) : (step D cap first next last leaf)^[time N n] (st, none) = (st, some (value N cap first next leaf n (history st)))

A node returns its value after time N n steps, to the same stack.

theorem Cslib.Complexity.GameTree.iterate_step_eval {X : Type} {D N cap : ℕ} {first : X} {next : X → X} {last : X → Bool} {leaf : List (X × X) → ℕ} (hN : 0 < N) (hlast : ∀ i < N, last (next^[i] first) = decide (i + 1 = N)) {K : ℕ} (hK : time N D ≤ K) : (step D cap first next last leaf)^[K] ([], none) = ([], some (value N cap first next leaf D []))

The evaluation from the empty stack returns the value of the root within time N D steps and stays put afterwards.

theorem Cslib.Complexity.GameTree.time_le {N : ℕ} (n : ℕ) : time N n ≤ (N + 1) ^ (2 * n + 1)

The evaluation of a node with n rounds to go takes at most (N + 1) ^ (2 * n + 1) steps.

Bounds on the states

structure Cslib.Complexity.GameTree.Good {X : Type} (D cap : ℕ) (P : X → Prop) (state : List (Frame X) × Option ℕ) : Prop

The invariant of the evaluation: at most D frames, whose messages and replies satisfy P, and all numbers at most cap.

• length : state.1.length ≤ D

  At most D frames.

• frames (f : Frame X) : f ∈ state.1 → P f.1 ∧ P f.2.1 ∧ f.2.2.1 ≤ cap ∧ f.2.2.2 ≤ cap

  The frames store messages and replies satisfying P, and numbers at most cap.

• value (v : ℕ) : v ∈ state.2 → v ≤ cap

  The returned value is at most cap.

theorem Cslib.Complexity.GameTree.good_iterate_step {X : Type} {D cap : ℕ} {first : X} {next : X → X} {last : X → Bool} {leaf : List (X × X) → ℕ} {P : X → Prop} (hfirst : P first) (hnext : ∀ (x : X), P x → P (next x)) (k : ℕ) : Good D cap P ((step D cap first next last leaf)^[k] ([], none))

The states stay small: every state of the evaluation from the empty stack satisfies the invariant.