Clock, output and workspace facts for plain machines #
These facts are moved unchanged from the former polynomial-time bridge module. They use only machine semantics and carry no higher computability-calculus dependency.
theorem Turing.MultiTapeTM.ComputesInTimeAndSpace.space_linear {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input output : List Symbol} {t s : ℕ} (h : tm.ComputesInTimeAndSpace input output t s) :
tm.ComputesInTimeAndSpace input output t (k * t + k)
A computation within t steps needs no separate space bound: it visits at most k t + k
work-tape cells.
theorem Turing.MultiTapeTM.ComputesInTimeAndSpace.length_output_le {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input output : List Symbol} {t s : ℕ} (h : tm.ComputesInTimeAndSpace input output t s) :
A computation within t steps emits at most t symbols.
theorem Turing.MultiTapeTM.Computes.exists_computesInTimeAndSpace {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input output : List Symbol} (h : tm.Computes input output) :
∃ (t : ℕ) (s : ℕ), tm.ComputesInTimeAndSpace input output t s
An output computed without bounds is computed within bounds: the time at which the machine halts, and the space it has used by then.
theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_space_linear {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t s : α → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t s) :
∃ (c : ℕ), ComputableInTimeAndSpace f encIn encOut t fun (a : α) => c * t a + c
A function computable within time t is computable within time t and space c t + c, for
a constant c: the number of work tapes of the machine.
theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.length_le {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t s : α → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t s) (a : α) :
The encoded values of a function computable within time t have length at most t.