The Tree Evaluation read machine within its space budget

The halting test, the address and the step of Cslib.TreeEval.Reader.machine are tidily computable within the space budget Cslib.TreeEval.Reader.stateBudget of its states, and the step machine simulating it is tidy.

Main definitions

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

Main results

• Cslib.TreeEval.Reader.tidy_machine: the step machine simulating the read machine is tidy.

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.ComputableTidilyInSpace (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.tidy_machine : ∃ (T : State → ℕ), machine.toStepMachine.Tidy (Turing.MultiTapeTM.encPair encState Turing.MultiTapeTM.encNat) (Turing.ReadMachine.stateT encState T stateBudget) (Turing.ReadMachine.stateS encState stateBudget)

The step machine simulating the read machine is tidy, within the space of its states together with the position of its head.