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.

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.computableTidilyInTimeAndSpace {α : Type u_1} {β : Type u_2} {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.

theorem Turing.MultiTapeTM.computableTidilyInTimeAndSpace_id {α : Type u_1} {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.