A machine that clears a work tape

clearWork Symbol erases the word on its work tape and returns the head to the start. It never moves the input head and never outputs. It is the sequential composition of two one-tape machines:

• forwardWork Symbol moves the head right over the word until it reads the first blank, the frontier just past the word, and halts there (see Plumbing.ForwardWork).
• rewindWork Symbol (some none) rewinds the head to the start, erasing every symbol it walks over.

On a word of length l the forward pass takes l + 1 steps and the erasing rewind l + 2 steps. The head stays within the cells -1, …, l, so the machine runs in time 3 * (l + 1) and space l + 2; placed on tape i of k tapes, the remaining tapes contribute one cell each.

Main results

• Turing.MultiTapeTM.clearWork: the one-tape machine that clears its tape.
• Turing.MultiTapeTM.transformsTapes_clearWork: clearWork replaces the word on its tape by the empty word.
• Turing.MultiTapeTM.transformsTapes_clearWork_tapeEmb: placed on tape i of a k-tape machine it does so on that tape and leaves every other tape unchanged.

noncomputable def Turing.MultiTapeTM.clearWork (Symbol : Type u_2) : MultiTapeTM 1 Symbol (Unit ⊕ RewindWorkState)

The one-tape machine that clears its tape: it moves to the end of the word and erases it on the way back.

theorem Turing.MultiTapeTM.transformsTapes_clearWork {Symbol : Type u_1} (w : List Symbol) : (clearWork Symbol).TransformsTapes (fun (x : List Symbol) (ws : Fin 1 → List Symbol) => ws 0 = w) (fun (x : List Symbol) (x_1 ws' : Fin 1 → List Symbol) (emitted : List Symbol) => (ws' = fun (x : Fin 1) => []) ∧ emitted = []) (3 * (w.length + 1)) (w.length + 2)

The machine that clears its work tape replaces the word on it by the empty word, in at most 3 * (w.length + 1) steps and w.length + 2 cells.

Clearing one of several work tapes

theorem Turing.MultiTapeTM.transformsTapes_clearWork_tapeEmb {k : ℕ} {Symbol : Type u_1} (i : Fin k) (w : List Symbol) : ((clearWork Symbol).extendTapes (tapeEmb i)).TransformsTapes (fun (x : List Symbol) (ws : Fin k → List Symbol) => ws i = w) (fun (x : List Symbol) (ws ws' : Fin k → List Symbol) (emitted : List Symbol) => ws' = Function.update ws i [] ∧ emitted = []) (3 * (w.length + 1)) (w.length + 1 + k)

The machine that clears a work tape, placed on tape i of a k-tape machine, replaces the word on that tape by the empty word and leaves every other tape unchanged, in at most 3 * (w.length + 1) steps and w.length + 1 + k cells.