Tidiness is free at zero space

A machine that runs in zero space has no work tapes (Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_no_work_tapes), so the only part of its final configuration that can differ from the start is the input head. Following it with Turing.MultiTapeTM.rewindInput moves that head back, which makes the computation tidy in the sense of Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.

Main definitions

• Turing.MultiTapeTM.tidyCopy: the identity, as a tidy machine without work tapes.

Main results

• Turing.MultiTapeTM.ComputableInTimeAndSpace.computableTidilyInTimeAndSpace: a function computable in time t and zero space is computable tidily in time 2 * t + 2 and zero space.
• Turing.MultiTapeTM.computableTidilyInTimeAndSpace_id: the identity is tidily computable in linear time and zero space.

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

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.computableTidilyInTimeAndSpace {α : Type u_2} {β : Type u_3} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} {t : α → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t fun (x : α) => 0) : ComputableTidilyInTimeAndSpace f encIn encOut (fun (a : α) => 2 * t a + 2) fun (x : α) => 0

A function computable in time t and zero space is computable tidily in time 2 * t + 2 and zero space: the machine has no work tapes, so it suffices to rewind the input head.

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.

theorem Turing.MultiTapeTM.computableTidilyInTimeAndSpace_id {α : Type u_2} {enc : α ↪ List Bool} : ComputableTidilyInTimeAndSpace id enc enc (fun (a : α) => 2 * (enc a).length + 4) fun (x : α) => 0

The identity is tidily computable in time linear in the length of the input and zero space.