Bounds up to constants on plain machines

Turing.MultiTapeTM.ComputableInO, computability within time O(T a) and space O(S a) by any machine, agrees with its tidy counterpart Turing.MultiTapeTM.ComputableTidilyInO, with the same bounds. A tidy machine is a machine, with the same bounds. Conversely, the tidy normal form makes a machine within time t and space s tidy within time 2 t + 3 s + c and space c (s + 1) (Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_computableTidilyInTimeAndSpace). A machine within time t visits at most k t + k work-tape cells, where k is its number of work tapes, so the space in the time bound may be replaced by the time: the overhead is a constant factor in each bound separately (Turing.MultiTapeTM.ComputableInTimeAndSpace.computableTidilyInO), which the notion absorbs.

Proofs switch between the notions with Turing.MultiTapeTM.ComputableInO.tidy and Turing.MultiTapeTM.ComputableInO.of_tidy.

Main results

• Turing.MultiTapeTM.ComputableInTimeAndSpace.computableTidilyInO: a machine within time t and space s whose values fit in space s gives tidy computability within time O(t) and space O(s).
• Turing.MultiTapeTM.computableInO_iff_computableTidilyInO: the plain and tidy notions agree, with the shortcuts Turing.MultiTapeTM.ComputableInO.tidy, Turing.MultiTapeTM.ComputableInO.of_tidy and Turing.MultiTapeTM.ComputableTidilyInO.computableInO.

Plain bounds are tidy bounds up to constants

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.computableTidilyInO {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t s : α → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t s) (hl : ∀ (a : α), (encOut (f a)).length ≤ s a) : ComputableTidilyInO f encIn encOut t s

Plain bounds are tidy bounds up to constant factors. A function computable within time t and space s, whose encoded values fit in space s, is tidily computable within time O(t) and space O(s).

Plain and tidy bounds up to constants

theorem Turing.MultiTapeTM.computableInO_iff_computableTidilyInO {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {T S : α → ℕ} : ComputableInO f encIn encOut T S ↔ ComputableTidilyInO f encIn encOut T S

Plain and tidy computability within bounds up to constants agree.