Tree Evaluation in small space

Cook and Mertz: Tree Evaluation of value length ℓ and height H is computable on multi-tape Turing machines in space O((ℓ + H + 1) · log (ℓ + 2) + log (n + 2)), where n is the length of the encoded instance. On nontrivial instances (1 ≤ ℓ and 1 ≤ H), both 2 ^ ℓ and 2 ^ H are at most n, so ℓ, H < |n| and |ℓ| ≤ ||n|| (writing |m| for the binary length of m), which yields the headline input-size space bound O(|n| · ||n||) = O(log n · log log n).

The step machine simulating the read machine Cslib.TreeEval.Reader.machine has a resource certificate. Its run on an instance halts with the value of the tree. The states along the run follow those of the read machine together with the head position and stay within the space bound.

Main definitions

• Cslib.TreeEval.NontrivialInstance: Tree Evaluation instances with 1 ≤ ℓ and 1 ≤ H.
• Cslib.TreeEval.encNontrivialInstance: the encoding of nontrivial instances.

Main results

• Cslib.TreeEval.computableInSpace_eval: Tree Evaluation in space O(spaceBound ℓ H + log (n + 2)), with the value not charged to the space bound (Turing.MultiTapeTM.ComputableInBigO).
• Cslib.TreeEval.spaceBound_add_length_le_log_mul_log_log: on nontrivial instances, spaceBound ℓ H + |n + 1| ≤ 6 · |n| · ||n||.
• Cslib.TreeEval.computableInSpace_eval_log_mul_log_log: Tree Evaluation on nontrivial instances in space O(|n| · ||n||) = O(log n · log log n).

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

@[reducible, inline]

abbrev Cslib.TreeEval.NontrivialInstance : Type

A nontrivial Tree Evaluation instance: both the value length ℓ and the height H are positive.

def Cslib.TreeEval.encNontrivialInstance : NontrivialInstance ↪ List Bool

The encoding of nontrivial Tree Evaluation instances.

@[simp]

theorem Cslib.TreeEval.encNontrivialInstance_apply (I : NontrivialInstance) : encNontrivialInstance I = encInstance ↑I

theorem Cslib.TreeEval.computableInSpace_eval : ∃ (t : Instance → ℕ), Turing.MultiTapeTM.ComputableInBigO (fun (I : Instance) => List.ofFn I.tree.eval) encInstance Turing.MultiTapeTM.encBits t fun (I : Instance) => Reader.spaceBound I.ell I.height + (Turing.MultiTapeTM.encNat ((encInstance I).length + 1)).length

Tree Evaluation in small space (Cook–Mertz): the value of the tree of an instance of value length ℓ and height H is computable from its encoding in space O((ℓ + H + 1) · log (ℓ + 2) + log (n + 2)); the value is not charged to the space bound.

theorem Cslib.TreeEval.spaceBound_add_length_le_log_mul_log_log {I : Instance} (hℓ : 1 ≤ I.ell) (hH : 1 ≤ I.height) : Reader.spaceBound I.ell I.height + (Turing.MultiTapeTM.encNat ((encInstance I).length + 1)).length ≤ 6 * ((Turing.MultiTapeTM.encNat (encInstance I).length).length * (Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encNat (encInstance I).length).length).length)

On a nontrivial instance (1 ≤ ℓ and 1 ≤ H), the parameter space bound plus the head-counter length is at most 6 · |n| · ||n||, where n = (encInstance I).length and |m| = (encNat m).length.

theorem Cslib.TreeEval.computableInSpace_eval_log_mul_log_log : ∃ (t : NontrivialInstance → ℕ), Turing.MultiTapeTM.ComputableInBigO (fun (I : NontrivialInstance) => List.ofFn (↑I).tree.eval) encNontrivialInstance Turing.MultiTapeTM.encBits t fun (I : NontrivialInstance) => (Turing.MultiTapeTM.encNat (encNontrivialInstance I).length).length * (Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encNat (encNontrivialInstance I).length).length).length

Tree Evaluation in space O(log n · log log n) (Cook–Mertz): on nontrivial instances (1 ≤ ℓ and 1 ≤ H), the value of the tree is computable from its encoding in space O(|n| · ||n||), where n is the length of the encoded instance and |m| = (encNat m).length; the value is not charged to the space bound.