The existing zero-workspace rewind and copy machines

Machine declarations are moved from their original module without changing programs or resource formulas. Higher computability-calculus theorems remain in the original facade.

Machines without work tapes

theorem Turing.MultiTapeTM.computesTidily_seq_rewindInput_of_runPath {Symbol : Type u_1} {input : List Symbol} {State : Type u_2} {tm : MultiTapeTM 0 Symbol State} {q : tm.RunPath input} (hh : RelSeries.head q = wordsCfg input (some tm.q₀) (fun (x : Fin 0) => []) []) (hl : (RelSeries.last q).Halted) : (tm.seq (rewindInput Symbol)).ComputesTidilyInTimeAndSpace input (RelSeries.last q).output (q.time + (↑(RelSeries.last q).inputPos - 1 + 2)) 0

If a machine without work tapes has a run path from its start to a halted configuration, then following it with Turing.MultiTapeTM.rewindInput computes the output of that configuration tidily: the rewind returns the input head from its position p in p - 1 + 2 further steps.

theorem Turing.MultiTapeTM.ComputesInTimeAndSpace.computesTidily_seq_rewindInput {Symbol : Type u_1} {input : List Symbol} {State : Type u_2} {tm : MultiTapeTM 0 Symbol State} {output : List Symbol} {t s : ℕ} (h : tm.ComputesInTimeAndSpace input output t s) : (tm.seq (rewindInput Symbol)).ComputesTidilyInTimeAndSpace input output (2 * t + 2) 0

A machine without work tapes that computes output in time t, followed by Turing.MultiTapeTM.rewindInput, computes output tidily in time 2 * t + 2: in t steps the input head moves at most t cells, so the rewind takes at most t + 2 steps.

Zero space

The identity

noncomputable def Turing.MultiTapeTM.tidyCopy (Symbol : Type u_2) : MultiTapeTM 0 Symbol (Unit ⊕ RewindState)

The identity as a tidy machine without work tapes: copy the input to the output, then move the input head back to the start.

theorem Turing.MultiTapeTM.computesTidily_tidyCopy {Symbol : Type u_1} (w : List Symbol) : (tidyCopy Symbol).ComputesTidilyInTimeAndSpace w w (2 * w.length + 4) 0

tidyCopy computes the identity tidily, in time linear in the length of the word.