Branching on a work tape

branch i tm₁ tm₂ reads the cell under the head of work tape i and then runs tm₁ if that cell is not blank and tm₂ if it is. On a Turing.wordsCfg configuration the head of tape i is on the first cell of its word, so the machine runs tm₂ exactly when the word on tape i is empty.

Main definitions

• Turing.MultiTapeTM.branch: the branching machine.

Main results

• Turing.MultiTapeTM.transformsTapes_branch: a specification of branch i tm₁ tm₂ from specifications of tm₁ for a non-empty word on tape i and of tm₂ for an empty one.

noncomputable def Turing.MultiTapeTM.branch {k : ℕ} {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} (i : Fin k) (tm₁ : MultiTapeTM k Symbol S₁) (tm₂ : MultiTapeTM k Symbol S₂) : MultiTapeTM k Symbol (Option (S₁ ⊕ S₂))

Reads the cell under the head of work tape i, moving no head and writing nothing, then runs tm₁ if the cell is not blank and tm₂ if it is.

theorem Turing.MultiTapeTM.transformsTapes_branch {k : ℕ} {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} (i : Fin k) {tm₁ : MultiTapeTM k Symbol S₁} {tm₂ : MultiTapeTM k Symbol S₂} {P : List Symbol → (Fin k → List Symbol) → Prop} {Q : List Symbol → (Fin k → List Symbol) → (Fin k → List Symbol) → List Symbol → Prop} {t₁ s₁ t₂ s₂ : ℕ} (h₁ : tm₁.TransformsTapes (fun (inp : List Symbol) (ws : Fin k → List Symbol) => P inp ws ∧ ws i ≠ []) Q t₁ s₁) (h₂ : tm₂.TransformsTapes (fun (inp : List Symbol) (ws : Fin k → List Symbol) => P inp ws ∧ ws i = []) Q t₂ s₂) : (branch i tm₁ tm₂).TransformsTapes P Q (max t₁ t₂ + 1) (max s₁ s₂ + k)

If tm₁ performs the transformation Q within t₁ steps and s₁ cells whenever the word on tape i is non-empty, and tm₂ within t₂ steps and s₂ cells whenever it is empty, then branch i tm₁ tm₂ performs Q with one more step and at most k more cells.