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.
theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.append {γ : Type u_1} {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} {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.