Case distinction

If c, f and g are tidily computable from a common input, so is fun x => if c x then f x else g x, within the bounds of c plus those of the branch taken.

iteTM tmc tm₁ tm₂ runs tmc with its output written to a new work tape, runs tm₁ if that word is non-empty and tm₂ otherwise (Turing.MultiTapeTM.branch), and clears the tape. The condition c may be computed with any encoding of Bool: a finite-state transducer turns its output into a word that is empty exactly for false.

Main definitions

• Turing.MultiTapeTM.iteTM: the machine for a case distinction.

Main results

• Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.ite: the machine-level case distinction.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.ite: case distinctions are tidily computable; each branch need only be computable on the inputs where it is taken.

noncomputable def Turing.MultiTapeTM.iteTM {k₀ k₁ k₂ : ℕ} {Symbol : Type u_1} {S₀ : Type u_2} {S₁ : Type u_3} {S₂ : Type u_4} (tmc : MultiTapeTM k₀ Symbol S₀) (tm₁ : MultiTapeTM k₁ Symbol S₁) (tm₂ : MultiTapeTM k₂ Symbol S₂) : MultiTapeTM (max k₀ (max k₁ k₂) + 1) Symbol ((S₀ ⊕ RewindWorkState) ⊕ Option (S₁ ⊕ S₂) ⊕ Unit ⊕ RewindWorkState)

Run tmc with its output on a new last work tape, then tm₁ if that word is non-empty and tm₂ otherwise, and clear the tape. All three machines are padded to max k₀ (max k₁ k₂) work tapes.

theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.ite {k₀ k₁ k₂ : ℕ} {Symbol : Type u_1} {S₀ : Type u_2} {S₁ : Type u_3} {S₂ : Type u_4} {tmc : MultiTapeTM k₀ Symbol S₀} {tm₁ : MultiTapeTM k₁ Symbol S₁} {tm₂ : MultiTapeTM k₂ Symbol S₂} {x w y : List Symbol} {tc sc t₁ s₁ t₂ s₂ : ℕ} (hc : tmc.ComputesTidilyInTimeAndSpace x w tc sc) (h₁ : w ≠ [] → tm₁.ComputesTidilyInTimeAndSpace x y t₁ s₁) (h₂ : w = [] → tm₂.ComputesTidilyInTimeAndSpace x y t₂ s₂) : (tmc.iteTM tm₁ tm₂).ComputesTidilyInTimeAndSpace x y ((tc + if w = [] then t₂ else t₁) + 4 * w.length + 6) ((sc + if w = [] then s₂ else s₁) + 3 * w.length + 5 * max k₀ (max k₁ k₂) + 10)

If tmc computes w from x tidily, tm₁ computes y from x tidily when w is non-empty and tm₂ does when w is empty, then iteTM tmc tm₁ tm₂ computes y from x tidily, within the bounds of tmc plus those of the machine that runs.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.restrict {α : Type u_5} {β : Type u_6} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} {t s : α → ℕ} (h : ComputableTidilyInTimeAndSpace f encIn encOut t s) (p : α → Prop) : ComputableTidilyInTimeAndSpace (f ∘ Subtype.val) ((Function.Embedding.subtype p).trans encIn) encOut (t ∘ Subtype.val) (s ∘ Subtype.val)

A function tidily computable on all inputs is tidily computable on the inputs satisfying p, by the same machine.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.ite {γ : Type u_5} {β : Type u_6} {encIn : γ ↪ List Bool} {encC : Bool ↪ List Bool} {encOut : β ↪ List Bool} {c : γ → Bool} {f g : γ → β} {tc sc tf sf tg sg : γ → ℕ} (hc : ComputableTidilyInTimeAndSpace c encIn encC tc sc) (hf : ComputableTidilyInTimeAndSpace (f ∘ Subtype.val) ((Function.Embedding.subtype fun (x : γ) => c x = true).trans encIn) encOut (tf ∘ Subtype.val) (sf ∘ Subtype.val)) (hg : ComputableTidilyInTimeAndSpace (g ∘ Subtype.val) ((Function.Embedding.subtype fun (x : γ) => c x = false).trans encIn) encOut (tg ∘ Subtype.val) (sg ∘ Subtype.val)) : ∃ (k : ℕ), ComputableTidilyInTimeAndSpace (fun (x : γ) => if c x = true then f x else g x) encIn encOut (fun (x : γ) => (tc x + if c x = true then tf x else tg x) + k) fun (x : γ) => (sc x + if c x = true then sf x else sg x) + k

Case distinctions are tidily computable: if c is tidily computable, f on the inputs where c holds and g on the others, then fun x => if c x then f x else g x is tidily computable, within the bounds of c plus those of the branch taken, up to a constant. The condition may be computed with any encoding of Bool.