Composing tidy computations

tm₂.comp tm₁ mark runs tm₁ with its output written to a work tape, then runs tm₂ reading its input from that tape, and finally clears the tape. If both machines compute tidily, so does the composition. Its time is the sum of the two times plus a term linear in the length of the intermediate word; so is its space, since the intermediate word is kept on a work tape.

Main definitions

• Turing.MultiTapeTM.comp: the composed machine.

Main results

• Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.comp: tidy computations compose.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.comp: tidily computable functions compose.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.comp_linear: the same, with the overhead a constant multiple of the length of the intermediate word plus one.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.comp': the same, with the length of the intermediate word bounded by the time of the inner function.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpaceOfLength.comp: the same for bounds of the input length, given a bound l on the length of the intermediate word.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.computableInTimeAndSpace_comp: hence f ∘ g is computable in the sense of Turing.MultiTapeTM.ComputableInTimeAndSpace.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpaceOfLength.computableInTimeAndSpaceOfLength_comp: the same for bounds of the input length.

noncomputable def Turing.MultiTapeTM.comp {k₁ k₂ : ℕ} {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} (tm₂ : MultiTapeTM k₂ Symbol S₂) (tm₁ : MultiTapeTM k₁ Symbol S₁) (mark : Symbol) : MultiTapeTM (max k₁ k₂ + 2) Symbol ((S₁ ⊕ RewindWorkState) ⊕ (MarkWorkState ⊕ S₂ ⊕ MarkWorkState) ⊕ Unit ⊕ RewindWorkState)

tm₂ after tm₁, both with their work tapes padded to max k₁ k₂: run tm₁ with its output written to the work tape Fin.natAdd (max k₁ k₂) 0, run tm₂ reading its input from that tape (using mark on the last work tape to flag the left end of the input), then clear that tape.

theorem Turing.MultiTapeTM.transformsTapes_clearWork_only {Symbol : Type u_1} {k : ℕ} (i : Fin k) (w : List Symbol) : ((clearWork Symbol).extendTapes (tapeEmb i)).TransformsTapes (fun (x : List Symbol) (ws : Fin k → List Symbol) => ws = Function.update (fun (x : Fin k) => []) i w) (fun (x : List Symbol) (x_1 ws' : Fin k → List Symbol) (e : List Symbol) => (ws' = fun (x : Fin k) => []) ∧ e = []) (3 * (w.length + 1)) (w.length + 1 + k)

Clearing the only non-blank work tape leaves all work tapes blank.

theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.comp {k₁ k₂ : ℕ} {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} {tm₁ : MultiTapeTM k₁ Symbol S₁} {tm₂ : MultiTapeTM k₂ Symbol S₂} {x w y : List Symbol} {t₁ s₁ t₂ s₂ : ℕ} (h₁ : tm₁.ComputesTidilyInTimeAndSpace x w t₁ s₁) (h₂ : tm₂.ComputesTidilyInTimeAndSpace w y t₂ s₂) (mark : Symbol) : (tm₂.comp tm₁ mark).ComputesTidilyInTimeAndSpace x y (t₁ + t₂ + 4 * w.length + 9) (s₁ + s₂ + 5 * w.length + (6 * max k₁ k₂ + 20))

If tm₁ computes w from x tidily and tm₂ computes y from w tidily, then tm₂.comp tm₁ mark computes y from x tidily.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.comp {α : Type u_4} {β : Type u_5} {γ : Type u_6} {g : α → β} {f : β → γ} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {t₁ s₁ : α → ℕ} {t₂ s₂ : β → ℕ} (hf : ComputableTidilyInTimeAndSpace f encMid encOut t₂ s₂) (hg : ComputableTidilyInTimeAndSpace g encIn encMid t₁ s₁) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace (f ∘ g) encIn encOut (fun (a : α) => t₁ a + t₂ (g a) + 4 * (encMid (g a)).length + 9) fun (a : α) => s₁ a + s₂ (g a) + 5 * (encMid (g a)).length + c

If g and f are tidily computable, so is f ∘ g, in the sum of their times and spaces plus a term linear in the length of the intermediate word encMid (g a).

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.comp_linear {α : Type u_4} {β : Type u_5} {γ : Type u_6} {g : α → β} {f : β → γ} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {t₁ s₁ : α → ℕ} {t₂ s₂ : β → ℕ} (hf : ComputableTidilyInTimeAndSpace f encMid encOut t₂ s₂) (hg : ComputableTidilyInTimeAndSpace g encIn encMid t₁ s₁) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace (f ∘ g) encIn encOut (fun (a : α) => t₁ a + t₂ (g a) + c * ((encMid (g a)).length + 1)) fun (a : α) => s₁ a + s₂ (g a) + c * ((encMid (g a)).length + 1)

If g and f are tidily computable, so is f ∘ g, in the sum of their times and spaces plus a constant multiple of the length of the intermediate word encMid (g a) plus one.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.comp' {α : Type u_4} {β : Type u_5} {γ : Type u_6} {g : α → β} {f : β → γ} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {t₁ s₁ : α → ℕ} {t₂ s₂ : β → ℕ} (hf : ComputableTidilyInTimeAndSpace f encMid encOut t₂ s₂) (hg : ComputableTidilyInTimeAndSpace g encIn encMid t₁ s₁) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace (f ∘ g) encIn encOut (fun (a : α) => 5 * t₁ a + t₂ (g a) + 9) fun (a : α) => s₁ a + s₂ (g a) + 5 * t₁ a + c

If g and f are tidily computable, so is f ∘ g: the intermediate word is no longer than the time of g.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpaceOfLength.comp {α : Type u_4} {β : Type u_5} {γ : Type u_6} {g : α → β} {f : β → γ} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {l t₁ s₁ t₂ s₂ : ℕ → ℕ} (ht : Monotone t₂) (hs : Monotone s₂) (hl : ∀ (a : α), (encMid (g a)).length ≤ l (encIn a).length) (hf : ComputableTidilyInTimeAndSpaceOfLength f encMid encOut t₂ s₂) (hg : ComputableTidilyInTimeAndSpaceOfLength g encIn encMid t₁ s₁) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpaceOfLength (f ∘ g) encIn encOut (fun (n : ℕ) => t₁ n + t₂ (l n) + 4 * l n + 9) fun (n : ℕ) => s₁ n + s₂ (l n) + 5 * l n + c

If g and f are tidily computable in time t₁, t₂ and space s₁, s₂ of the length of their input, for monotone t₂ and s₂, and the output of g on inputs of length n has length at most l n, then f ∘ g is tidily computable with bounds depending on t₂ (l n), s₂ (l n) and l n.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.computableInTimeAndSpace_comp {α : Type u_4} {β : Type u_5} {γ : Type u_6} {g : α → β} {f : β → γ} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {t₁ s₁ : α → ℕ} {t₂ s₂ : β → ℕ} (hf : ComputableTidilyInTimeAndSpace f encMid encOut t₂ s₂) (hg : ComputableTidilyInTimeAndSpace g encIn encMid t₁ s₁) : ∃ (c : ℕ), ComputableInTimeAndSpace (f ∘ g) encIn encOut (fun (a : α) => 5 * t₁ a + t₂ (g a) + 9) fun (a : α) => s₁ a + s₂ (g a) + 5 * t₁ a + c

If g and f are tidily computable, then f ∘ g is computable.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpaceOfLength.computableInTimeAndSpaceOfLength_comp {α : Type u_4} {β : Type u_5} {γ : Type u_6} {g : α → β} {f : β → γ} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {l t₁ s₁ t₂ s₂ : ℕ → ℕ} (ht : Monotone t₂) (hs : Monotone s₂) (hl : ∀ (a : α), (encMid (g a)).length ≤ l (encIn a).length) (hf : ComputableTidilyInTimeAndSpaceOfLength f encMid encOut t₂ s₂) (hg : ComputableTidilyInTimeAndSpaceOfLength g encIn encMid t₁ s₁) : ∃ (c : ℕ), ComputableInTimeAndSpaceOfLength (f ∘ g) encIn encOut (fun (n : ℕ) => t₁ n + t₂ (l n) + 4 * l n + 9) fun (n : ℕ) => s₁ n + s₂ (l n) + 5 * l n + c

If g and f are tidily computable in time t₁, t₂ and space s₁, s₂ of the length of their input, for monotone t₂ and s₂, and the output of g on inputs of length n has length at most l n, then f ∘ g is computable.