The Tree Evaluation read machine within its space budget

The halting test, the address and the step of Cslib.TreeEval.Reader.machine are computable within the space budget Cslib.TreeEval.Reader.stateBudget of its states, and the step machine simulating it has a plain resource certificate.

Main definitions

• Cslib.TreeEval.Reader.stateBudget: the space budget of a state.

Main results

• Cslib.TreeEval.Reader.machine_resourceCertificate: the simulating step machine has a resource certificate.

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.

theorem Cslib.TreeEval.Reader.pairFalse_inSpace : Turing.MultiTapeTM.ComputableInSpace (fun (x : Tuple) => (x, false)) encTuple encStepInT fun (x : Tuple) => stepBudget (x, false)

The tuple with the bit false, as an input of a step.

On states

def Cslib.TreeEval.Reader.stateBudget (s : State) : ℕ

The space budget of a state.

theorem Cslib.TreeEval.Reader.machine_resourceCertificate : ∃ (T : State → ℕ), machine.toStepMachine.ResourceCertificate (Turing.MultiTapeTM.encPair encState Turing.MultiTapeTM.encNat) (Turing.ReadMachine.stateT encState T stateBudget) (Turing.ReadMachine.stateS encState stateBudget)

The simulating step machine has a resource certificate, within the space of its states together with the position of its head.