The step of the Tree Evaluation read machine within its space budget

The halting test, the address and the step of Cslib.TreeEval.Reader.machine, on tuples, are tidily computable within the space budget Cslib.TreeEval.Reader.stepBudget: the length of the encoded tuple, the value length, the height, and the registers with every entry as long as the prime and the round of the top frame together. On the states the machine reaches, the budget is O((h + ℓ) log ℓ).

Main definitions

• Cslib.TreeEval.Reader.stepBudget: the space budget of a step.

Main results

• Cslib.TreeEval.Reader.stepT_inSpace: the step within the budget.

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.regLen (x : Tuple) : ℕ

The total length of the registers and of the sums of a tuple.

@[reducible, inline]

abbrev Cslib.TreeEval.Reader.encStepInT : Tuple × Bool ↪ List Bool

The encoding of the inputs of a step.

def Cslib.TreeEval.Reader.stepBudget (y : Tuple × Bool) : ℕ

The space budget of a step, on the tuple and the bit read.

theorem Cslib.TreeEval.Reader.len_le_stepBudget : Turing.MultiTapeTM.BigOLe (fun (y : Tuple × Bool) => (encStepInT y).length) stepBudget

theorem Cslib.TreeEval.Reader.ell_le_stepBudget : Turing.MultiTapeTM.BigOLe (fun (y : Tuple × Bool) => y.1.ell) stepBudget

theorem Cslib.TreeEval.Reader.height_le_stepBudget : Turing.MultiTapeTM.BigOLe (fun (y : Tuple × Bool) => y.1.height) stepBudget

Projections

theorem Cslib.TreeEval.Reader.hEll : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (y : Tuple × Bool) => y.1.ell) encStepInT Turing.MultiTapeTM.encNat stepBudget

theorem Cslib.TreeEval.Reader.hHeight : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (y : Tuple × Bool) => y.1.height) encStepInT Turing.MultiTapeTM.encNat stepBudget

theorem Cslib.TreeEval.Reader.hStack : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (y : Tuple × Bool) => y.1.stack) encStepInT (Turing.MultiTapeTM.encList encFrame) stepBudget

theorem Cslib.TreeEval.Reader.hTag : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (y : Tuple × Bool) => y.1.tag) encStepInT (Turing.MultiTapeTM.encFinEnum (Fin 7)) stepBudget

theorem Cslib.TreeEval.Reader.hN₁ : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (y : Tuple × Bool) => y.1.n₁) encStepInT Turing.MultiTapeTM.encNat stepBudget

theorem Cslib.TreeEval.Reader.hRest : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (y : Tuple × Bool) => y.1.stack.tail) encStepInT (Turing.MultiTapeTM.encList encFrame) stepBudget

The rest of the stack.

Constructing frames, stacks and tuples

The branches of the step

@[reducible, inline]

abbrev Cslib.TreeEval.Reader.encStepOut : Tuple × List Bool ↪ List Bool

The encoding of the results of a step.

theorem Cslib.TreeEval.Reader.hSucc {n : Tuple × Bool → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInSpace n encStepInT Turing.MultiTapeTM.encNat stepBudget) : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (y : Tuple × Bool) => n y + 1) encStepInT Turing.MultiTapeTM.encNat stepBudget

theorem Cslib.TreeEval.Reader.stepT_inSpace : Turing.MultiTapeTM.ComputableTidilyInSpace stepT encStepInT encStepOut stepBudget

The step within its space budget.