Basic properties of tidy computations #
A tidy computation is a computation, it emits at most one symbol per step, and it stays tidy when the machine is given more work tapes.
Main results #
Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.computableInTimeAndSpace: a tidily computable function is computable, within the same bounds.Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.length_output_le: a tidy computation emits at most one symbol per step.Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.length_le: the output of a tidily computable function is no longer than its time bound.Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.extendTapes: a tidy computation stays tidy with more work tapes.
theorem Turing.MultiTapeTM.ComputesFunTidilyInTimeAndSpace.computesFunInTimeAndSpace {α : Type u_1} {β : Type u_2} {k : ℕ} {Symbol : Type u_3} {State : Type u_4} {tm : MultiTapeTM k Symbol State} {encIn : α ↪ List Symbol} {encOut : β ↪ List Symbol} {f : α → β} {t s : α → ℕ} (h : tm.ComputesFunTidilyInTimeAndSpace encIn encOut f t s) :
tm.ComputesFunInTimeAndSpace encIn encOut f t s
A tidy computation of a function is a computation of it.
theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.length_le {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t s : α → ℕ} (h : ComputableTidilyInTimeAndSpace f encIn encOut t s) (a : α) :
The output of a tidily computable function is no longer than its time bound.
theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.computableInTimeAndSpace {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t s : α → ℕ} (h : ComputableTidilyInTimeAndSpace f encIn encOut t s) :
ComputableInTimeAndSpace f encIn encOut t s
A tidily computable function is computable.