Concatenating the outputs of tidy computations #
A tidy machine leaves its tapes as it found them, so a second tidy machine can run after it on the
same input. appendTM tm₁ tm₂ runs tm₁ and then tm₂; the outputs concatenate.
Main definitions #
Turing.MultiTapeTM.appendTM: the machine that runs two machines one after the other.
Main results #
Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.append: the outputs of two tidy computations on the same input concatenate.Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.append: a function whose encoded value is the concatenation of the encoded values of two tidily computable functions is tidily computable.
noncomputable def Turing.MultiTapeTM.appendTM {k₁ k₂ : ℕ} {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} (tm₁ : MultiTapeTM k₁ Symbol S₁) (tm₂ : MultiTapeTM k₂ Symbol S₂) :
MultiTapeTM (max k₁ k₂) Symbol (S₁ ⊕ S₂)
Run tm₁ and then tm₂, both with their work tapes padded to max k₁ k₂.
Instances For
theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.append {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 y₁ y₂ : List Symbol} {t₁ s₁ t₂ s₂ : ℕ} (h₁ : tm₁.ComputesTidilyInTimeAndSpace x y₁ t₁ s₁) (h₂ : tm₂.ComputesTidilyInTimeAndSpace x y₂ t₂ s₂) :
If tm₁ computes y₁ from x tidily and tm₂ computes y₂ from x tidily, then
appendTM tm₁ tm₂ computes y₁ ++ y₂ from x tidily.
theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.append {γ : Type u_4} {α₁ : Type u_5} {α₂ : Type u_6} {β : Type u_7} {encIn : γ ↪ List Bool} {enc₁ : α₁ ↪ List Bool} {enc₂ : α₂ ↪ List Bool} {encOut : β ↪ List Bool} {f₁ : γ → α₁} {f₂ : γ → α₂} {g : γ → β} {t₁ s₁ t₂ s₂ : γ → ℕ} (h₁ : ComputableTidilyInTimeAndSpace f₁ encIn enc₁ t₁ s₁) (h₂ : ComputableTidilyInTimeAndSpace f₂ encIn enc₂ t₂ s₂) (hg : ∀ (x : γ), encOut (g x) = enc₁ (f₁ x) ++ enc₂ (f₂ x)) :
∃ (k : ℕ), ComputableTidilyInTimeAndSpace g encIn encOut (fun (x : γ) => t₁ x + t₂ x) fun (x : γ) => s₁ x + s₂ x + k
If f₁ and f₂ are tidily computable and the encoded value of g is the concatenation of
their encoded values, then g is tidily computable within the sum of their bounds, plus a constant
for the space.