The space of the Tree Evaluation read machine

On the encoding of an instance of value length ℓ and height H, the space budget of every state that Cslib.TreeEval.Reader.machine reaches is O((ℓ + H + 1) · log (ℓ + 2)): residues below the prime p ≤ 4ℓ + 2 have O(log (ℓ + 2)) bits. The registers and the sums hold ℓ of them, the stack holds at most H frames with a residue each, and the counters have O(ℓ + log (H + 2)) bits.

Main definitions

• Cslib.TreeEval.Reader.spaceBound: the bound (ℓ + H + 1) · (|ℓ| + 1), with |ℓ| the length of ℓ in binary.

Main results

• Cslib.TreeEval.Reader.stateBudget_le: the budget of every state reached is O(spaceBound ℓ H).

References

• J. Cook and I. Mertz, Tree Evaluation is in Space O(log n · log log n)
• O. Goldreich, On the Cook–Mertz Tree Evaluation procedure, Algorithm 1, which the machine runs.

def Cslib.TreeEval.Reader.spaceBound (ℓ H : ℕ) : ℕ

The space bound (ℓ + H + 1) · (|ℓ| + 1).

structure Cslib.TreeEval.Reader.Bounds (ℓ H : ℕ) (s : State) : Prop

The bounds on the components of a state that satisfies the invariant.

• ell : s.ell ≤ ℓ
• height : s.height ≤ H
• p : (Turing.MultiTapeTM.encNat s.p).length ≤ (Turing.MultiTapeTM.encNat ℓ).length + 3
• regs (r : Fin 3) : (s.regs.get r).length ≤ ℓ ∧ ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (s.regs.get r)).length ≤ ℓ * (2 * ((Turing.MultiTapeTM.encNat ℓ).length + 3) + 1)
• stack : s.stack.length ≤ H
• rounds (fr : Iter.Frame) : fr ∈ s.stack → (Turing.MultiTapeTM.encNat fr.round).length ≤ (Turing.MultiTapeTM.encNat ℓ).length + 3
• n₁ : (Turing.MultiTapeTM.encNat s.ctl.toTuple.2.1).length ≤ (Turing.MultiTapeTM.encNat ℓ).length + H + 3 * ℓ + 4
• n₂ : (Turing.MultiTapeTM.encNat s.ctl.toTuple.2.2.1).length ≤ (Turing.MultiTapeTM.encNat ℓ).length + 3
• acc : s.ctl.toTuple.2.2.2.length ≤ ℓ ∧ ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) s.ctl.toTuple.2.2.2).length ≤ ℓ * (2 * ((Turing.MultiTapeTM.encNat ℓ).length + 3) + 1)

theorem Cslib.TreeEval.Reader.bounds_of_inv {ℓ H : ℕ} {s : State} (hs : Inv ℓ H s) : Bounds ℓ H s

theorem Cslib.TreeEval.Reader.stateBudget_le {ℓ H : ℕ} {s : State} (hb : Bounds ℓ H s) : stateBudget s ≤ 2 ^ 12 * spaceBound ℓ H

The budget of a state within the space bound.