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.ComputesTidilyInTimeAndSpace.computesInTimeAndSpace {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {t s : ℕ} {input output : List Symbol} (h : tm.ComputesTidilyInTimeAndSpace input output t s) :
tm.ComputesInTimeAndSpace input output t s
A tidy computation is a computation in the sense of
Turing.MultiTapeTM.ComputesInTimeAndSpace.
theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.length_output_le {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {t s : ℕ} {input output : List Symbol} (h : tm.ComputesTidilyInTimeAndSpace input output t s) :
A tidy computation within t steps emits at most t symbols.
theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.extendTapes {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {t s : ℕ} {input output : List Symbol} {k' : ℕ} (h : tm.ComputesTidilyInTimeAndSpace input output t s) (e : Fin k ↪ Fin k') :
(tm.extendTapes e).ComputesTidilyInTimeAndSpace input output t (s + (k' - k))
A tidy computation stays tidy with more work tapes, at one cell per added tape.
theorem Turing.MultiTapeTM.ComputesFunTidilyInTimeAndSpace.computesFunInTimeAndSpace {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {α : Type u_3} {β : Type u_4} {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_3} {β : Type u_4} {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_3} {β : Type u_4} {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.