Resource bounds for the reverse TM2 compiler

Input storage is counted, whereas the native work-space convention excludes read-only input and write-only output. Raw work-stack lengths are bounded by the cells visited by the source heads. The space estimates therefore apply independently of the source runtime.

Main results

• Turing.MultiTapeTM.ToTM2.outputsInTime: output correspondence with a linear simulation clock.
• Turing.MultiTapeTM.ToTM2.reachable_stack_bound: a bound on every target configuration.

theorem Turing.MultiTapeTM.ToTM2.reachable_stack_bound {k : ℕ} {State : Type} [Fintype State] (tm : MultiTapeTM k Bool State) {input output : List Bool} {s : ℕ} (hc : tm.Computes input output) (hs : tm.RunsInSpace input s) (i : ℕ) : totalStackLength ((TM2.stepTotal (machine tm.q₀ tm.tr).m)^[i] (initList (machine tm.q₀ tm.tr) input)) ≤ input.length + s + output.length

Every target configuration counts the stored input and output as well as native work space. The estimate holds for arbitrary padded target time, independently of the source runtime.

noncomputable def Turing.MultiTapeTM.ToTM2.outputsInTime {k : ℕ} {State : Type} [Fintype State] (tm : MultiTapeTM k Bool State) {input output : List Bool} {t : ℕ} (hc : tm.Computes input output) (ht : tm.RunsInTime input t) : TM2OutputsInTime (machine tm.q₀ tm.tr) input (some output) (input.length + (k + 1) * (t + 1) + output.length + 3)

A native computation is simulated with a linear clock, including clearing every auxiliary stack, reversing its output and restoring Mathlib's canonical halting control.

noncomputable def Turing.MultiTapeTM.ToTM2.outputs {k : ℕ} {State : Type} [Fintype State] (tm : MultiTapeTM k Bool State) {input output : List Bool} (hc : tm.Computes input output) : TM2Outputs (machine tm.q₀ tm.tr) input (some output)

Terminating native computation yields terminating canonical TM2 computation.