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.

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