A machine that moves to the end of a word

forwardWork Symbol moves the head of its work tape to the right over the word it holds and halts on the frontier, the first blank cell just past the word. It never modifies a tape, never moves the input head and never outputs.

On a word of length l, started with the head at cell p ≤ l, the machine takes l - p + 1 steps and the head stays within the cells p, …, l.

This is a one-tape machine; to move the head of tape i of a k-tape machine to the end of its word, place it there with Turing.MultiTapeTM.tapeEmb and transport its run with Turing.MultiTapeTM.runFrom_tapeEmb. The input head, the output and every other tape are then untouched by construction.

Main results

• Turing.MultiTapeTM.forwardWork: the one-tape machine that moves its head to the frontier of its word.
• Turing.MultiTapeTM.runFrom_forwardWork: its run from the initial state.
• Turing.MultiTapeTM.workTapePos_runFrom_forwardWork: its head stays within [p, w.length].

def Turing.MultiTapeTM.forwardWork (Symbol : Type u_2) : MultiTapeTM 1 Symbol Unit

The one-tape machine that moves its head to the end of its word. Over a symbol it moves right; on the first blank it halts without moving.

theorem Turing.MultiTapeTM.runFrom_forwardWork {Symbol : Type u_1} {input : List Symbol} (inpos : Fin (input.length + 2)) (w out : List Symbol) {p n : ℕ} (hpn : p + n = w.length) : runFrom { state := some (forwardWork Symbol).q₀, inputPos := inpos, workTapes := fun (x : Fin 1) => tapeOfList w, workTapePos := fun (x : Fin 1) => ↑p, output := out } (n + 1) = { state := none, inputPos := inpos, workTapes := fun (x : Fin 1) => tapeOfList w, workTapePos := fun (x : Fin 1) => ↑w.length, output := out }

The run of the machine that moves to the end of the word. Started with the tape holding a word w and the head at a cell p with p + n = w.length, after n + 1 steps the machine has halted with the head on the frontier w.length and nothing else changed.

theorem Turing.MultiTapeTM.workTapePos_runFrom_forwardWork {Symbol : Type u_1} {input : List Symbol} (inpos : Fin (input.length + 2)) (w out : List Symbol) {p : ℕ} (hp : p ≤ w.length) (m : ℕ) : (runFrom { state := some (forwardWork Symbol).q₀, inputPos := inpos, workTapes := fun (x : Fin 1) => tapeOfList w, workTapePos := fun (x : Fin 1) => ↑p, output := out } m).workTapePos 0 ∈ Set.Icc ↑p ↑w.length

At every step, the head is within [p, w.length].