Tree Evaluation in small space

Cook and Mertz: Tree Evaluation of value length ℓ and height H is tidily 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 is tidy, its run on an instance halts with the value of the tree, and its states along the run, which follow the states of the read machine together with the position of the head, 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.computableTidilyInSpace_eval: Tree Evaluation in space O(spaceBound ℓ H + log (n + 2)).
• Cslib.TreeEval.spaceBound_add_length_le_log_mul_log_log: on nontrivial instances, spaceBound ℓ H + |n + 1| ≤ 6 · |n| · ||n||.
• Cslib.TreeEval.computableTidilyInSpace_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.computableTidilyInSpace_eval : ∃ (t : Instance → ℕ), Turing.MultiTapeTM.ComputableTidilyInBigO (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 tidily computable from its encoding in space O((ℓ + H + 1) · log (ℓ + 2) + log (n + 2)).

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.computableTidilyInSpace_eval_log_mul_log_log : ∃ (t : NontrivialInstance → ℕ), Turing.MultiTapeTM.ComputableTidilyInBigO (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 tidily computable from its encoding in space O(|n| · ||n||), where n is the length of the encoded instance and |m| = (encNat m).length.