Direct linear-time and workspace certificates

Machine normalization and composition preserve a common linear bound. No output-space condition is added: intermediate output is bounded by the actual clock of the first machine.

Main results

• ComputableInLinearTimeAndSpace.comp: direct machine composition.
• ComputableInLinearTimeAndSpace.const, .of_eq: constant and word-preserving functions.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.of_transducer {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {Q : Type} [Finite Q] (τ : Transducer Bool Q) {f : α → β} (h : ∀ (a : α), encMid (f a) = τ.run τ.q₀ (encIn a)) : ComputableInLinearTimeAndSpace f encIn encMid

A finite transducer gives a common linear bound from its actual clock and zero workspace.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.of_frame {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = frame (encIn a)) : ComputableInLinearTimeAndSpace f encIn encMid

Frame the encoded input using the shared streaming machine.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.of_unframe {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = unframe (encIn a)) : ComputableInLinearTimeAndSpace f encIn encMid

Read the first framed word, including the prescribed behavior on incomplete frames.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.of_dropFrame {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = dropFrame (encIn a)) : ComputableInLinearTimeAndSpace f encIn encMid

Drop the first framed word using the same shared parser.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.of_eq {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = encIn a) : ComputableInLinearTimeAndSpace f encIn encMid

Reuse the copy machine when the encoded output is the encoded input.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.const {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (b : β) : ComputableInLinearTimeAndSpace (fun (x : α) => b) encIn encMid

A fixed encoded output takes constant time and no workspace.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.of_finite {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} [Finite α] (f : α → β) : ComputableInLinearTimeAndSpace f encIn encMid

A fixed function on a finite domain is realized by its finite lookup machine.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : β → γ} {g : α → β} (hf : ComputableInLinearTimeAndSpace f encMid encOut) (hg : ComputableInLinearTimeAndSpace g encIn encMid) : ComputableInLinearTimeAndSpace (fun (a : α) => f (g a)) encIn encOut

Compose linear certificates; the clock bounds the stored intermediate word.