The tidy normal form

Every computation can be made tidy (Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace) at a linear cost in time and space: tidy m₀ m₁ tm runs tm with every work tape shadowed (Turing.MultiTapeTM.shadow), then clears each work tape along its shadow (Turing.MultiTapeTM.clearShadowed), and finally rewinds the input head (Turing.MultiTapeTM.rewindInput); the symbols m₀ ≠ m₁ mark the shadows. A computation of tm within t steps and s cells becomes a tidy computation of tidy m₀ m₁ tm within 2 t + 3 s + 2 k + 4 steps (ComputesInTimeAndSpace.computesTidily_tidy). So tidiness, which makes machines composable, is no restriction on what is computable within given resources up to constant factors (ComputableInTimeAndSpace.exists_computableTidilyInTimeAndSpace).

The shadow tapes are needed because a work tape may hold blanks among the cells tm has written: sweeping until the first blank would not find them all.

Main definitions

• Turing.MultiTapeTM.clearList: clear a list of work tapes along their shadows.
• Turing.MultiTapeTM.tidy: the tidy normal form of a machine.

Main results

• Turing.MultiTapeTM.exists_runPath_tidy: the run path of tidy m₀ m₁ tm when tm halts.
• Turing.MultiTapeTM.ComputesInTimeAndSpace.computesTidily_tidy: tidy m₀ m₁ tm computes tidily what tm computes.
• Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_computableTidilyInTimeAndSpace: computable functions are tidily computable.

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_computableTidilyInTimeAndSpace {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t s : α → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t s) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace f encIn encOut (fun (a : α) => 2 * t a + 3 * s a + c) fun (a : α) => c * (s a + 1)

Computable functions are tidily computable, at a linear cost: a function computable within time t and space s is computable tidily within time 2 t + 3 s + c and space c (s + 1), for a constant c that depends on the number of work tapes of the machine.