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.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {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_1} {β : Type u_2} {γ : Type u_3} {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_1} {β : Type u_2} {γ : Type u_3} {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_1} {β : Type u_2} {γ : Type u_3} {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_1} {β : Type u_2} {γ : Type u_3} {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_1} {β : Type u_2} {γ : Type u_3} {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.