Moving words between tapes

Three machines, built from the tidy identity Turing.MultiTapeTM.tidyCopy, that move a word between the input, the work tapes and the output, leaving everything else as it is:

• Turing.MultiTapeTM.loadWord Symbol i writes the input to the blank work tape i;
• Turing.MultiTapeTM.copyWord e mark copies the word on tape e 1 to the blank tape e 0;
• Turing.MultiTapeTM.emitWord e mark outputs the word on tape e 0.

The last two use a further blank tape to flag the left end of the word with mark.

Main results

• Turing.MultiTapeTM.transformsTapes_loadWord, Turing.MultiTapeTM.transformsTapes_copyWord, Turing.MultiTapeTM.transformsTapes_emitWord: their specifications.

noncomputable def Turing.MultiTapeTM.loadWord {k : ℕ} (Symbol : Type u_2) (i : Fin k) : MultiTapeTM k Symbol ((Unit ⊕ RewindState) ⊕ RewindWorkState)

Writes the input to the work tape i.

noncomputable def Turing.MultiTapeTM.copyWord {k : ℕ} {Symbol : Type u_1} (e : Fin (0 + 1 + 2) ↪ Fin k) (mark : Symbol) : MultiTapeTM k Symbol (MarkWorkState ⊕ ((Unit ⊕ RewindState) ⊕ RewindWorkState) ⊕ MarkWorkState)

Copies the word on tape e 1 to tape e 0, using tape e 2 to flag the left end of the word with mark.

noncomputable def Turing.MultiTapeTM.emitWord {k : ℕ} {Symbol : Type u_1} (e : Fin (0 + 2) ↪ Fin k) (mark : Symbol) : MultiTapeTM k Symbol (MarkWorkState ⊕ (Unit ⊕ RewindState) ⊕ MarkWorkState)

Outputs the word on tape e 0, using tape e 1 to flag the left end of the word with mark.

theorem Turing.MultiTapeTM.transformsTapes_loadWord {k : ℕ} {Symbol : Type u_1} (i : Fin k) (v : List Symbol) : (loadWord Symbol i).TransformsTapes (fun (inp : List Symbol) (ws : Fin k → List Symbol) => inp = v ∧ ws i = []) (fun (x : List Symbol) (ws ws' : Fin k → List Symbol) (e : List Symbol) => ws' = Function.update ws i v ∧ e = []) (3 * v.length + 6) (2 * v.length + k + 3)

loadWord Symbol i writes the input v to the blank tape i and changes nothing else.

theorem Turing.MultiTapeTM.transformsTapes_copyWord {k : ℕ} {Symbol : Type u_1} (e : Fin (0 + 1 + 2) ↪ Fin k) (mark : Symbol) (v : List Symbol) : (copyWord e mark).TransformsTapes (fun (x : List Symbol) (ws : Fin k → List Symbol) => ws (e 1) = v ∧ ws (e 0) = [] ∧ ws (e 2) = []) (fun (x : List Symbol) (ws ws' : Fin k → List Symbol) (em : List Symbol) => ws' = Function.update ws (e 0) v ∧ em = []) (3 * v.length + 10) (4 * v.length + k + 15)

copyWord e mark writes the word v on tape e 1 to the blank tape e 0, given a blank tape e 2, and changes nothing else.

theorem Turing.MultiTapeTM.transformsTapes_emitWord {k : ℕ} {Symbol : Type u_1} (e : Fin (0 + 2) ↪ Fin k) (mark : Symbol) (v : List Symbol) : (emitWord e mark).TransformsTapes (fun (x : List Symbol) (ws : Fin k → List Symbol) => ws (e 0) = v ∧ ws (e 1) = []) (fun (x : List Symbol) (ws ws' : Fin k → List Symbol) (em : List Symbol) => ws' = ws ∧ em = v) (2 * v.length + 8) (2 * v.length + k + 10)

emitWord e mark outputs the word v on tape e 0, given a blank tape e 1, and changes no tape.