A machine that rewinds a work-tape head

A machine that moves the head of its work tape to the left end of its contents and halts. It optionally writes a certain symbol to or clears the cells it moves over while traveling to the left. The input tape is not modified. This machine can be run between two phases of a computation to re-normalise a work-tape head without disturbing anything else.

In its initial state start the machine takes one unconditional step left, into state scan. In state scan it walks left over symbols, writing write to every cell it leaves; on the first blank it moves the head right and halts. By default write is none and the machine writes nothing; with write := some none it erases the part of the word it walks over.

This is a one-tape machine; to rewind tape i of a k-tape machine, 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.rewindWork: the one-tape machine that rewinds its head to the start of its word.
• Turing.MultiTapeTM.runFrom_rewindWork: its run from the initial state, with the special cases Turing.MultiTapeTM.runFrom_rewindWork_none (nothing is written) and Turing.MultiTapeTM.runFrom_rewindWork_erase (the whole word is erased).
• Turing.MultiTapeTM.workTapePos_runFrom_rewindWork: the rewound head stays within [-1, p].

inductive Turing.MultiTapeTM.RewindWorkState : Type

The control states of the work-tape-rewinding machine: start takes one unconditional step left, scan walks left towards the start of the word.

• start : RewindWorkState
• scan : RewindWorkState

@[instance_reducible]

instance Turing.MultiTapeTM.instDecidableEqRewindWorkState : DecidableEq RewindWorkState

@[instance_reducible]

instance Turing.MultiTapeTM.instFintypeRewindWorkState : Fintype RewindWorkState

def Turing.MultiTapeTM.rewindWork (Symbol : Type u_2) (write : Option (Option Symbol) := none) : MultiTapeTM 1 Symbol RewindWorkState

The one-tape rewinding machine. In state start it moves its head left, unconditionally, and enters state scan. In state scan it writes write over a symbol and moves left, staying in scan; on the first blank it moves right and halts. The input head never moves and nothing is ever output.

theorem Turing.MultiTapeTM.runFrom_rewindWork {Symbol : Type u_1} {input : List Symbol} (write : Option (Option Symbol)) (ip : Fin (input.length + 2)) (t : ℤ → Option Symbol) (out : List Symbol) {w : List Symbol} (hw : t = tapeOfList w) {p : ℕ} (hp : p ≤ w.length) : runFrom { state := some (rewindWork Symbol write).q₀, inputPos := ip, workTapes := fun (x : Fin 1) => t, workTapePos := fun (x : Fin 1) => ↑p, output := out } (p + 2) = { state := none, inputPos := ip, workTapes := fun (x : Fin 1) (z : ℤ) => if 0 ≤ z ∧ z < ↑p then write.getD (t z) else t z, workTapePos := fun (x : Fin 1) => 0, output := out }

The run of the one-tape machine that rewinds its head. Started with the tape holding a word w and the head at a position p ≤ w.length — inside the word or at the frontier just past it — after p + 2 steps the machine has halted with the head back at position 0, write applied to the cells 0, …, p - 1 and nothing else changed.

theorem Turing.MultiTapeTM.runFrom_rewindWork_none {Symbol : Type u_1} {input : List Symbol} (ip : Fin (input.length + 2)) (t : ℤ → Option Symbol) (out : List Symbol) {w : List Symbol} (hw : t = tapeOfList w) {p : ℕ} (hp : p ≤ w.length) : runFrom { state := some (rewindWork Symbol).q₀, inputPos := ip, workTapes := fun (x : Fin 1) => t, workTapePos := fun (x : Fin 1) => ↑p, output := out } (p + 2) = { state := none, inputPos := ip, workTapes := fun (x : Fin 1) => t, workTapePos := fun (x : Fin 1) => 0, output := out }

Rewinding without writing changes nothing but the position of the head.

theorem Turing.MultiTapeTM.runFrom_rewindWork_erase {Symbol : Type u_1} {input : List Symbol} (ip : Fin (input.length + 2)) (t : ℤ → Option Symbol) (out : List Symbol) {w : List Symbol} (hw : t = tapeOfList w) : runFrom { state := some (rewindWork Symbol (some none)).q₀, inputPos := ip, workTapes := fun (x : Fin 1) => t, workTapePos := fun (x : Fin 1) => ↑w.length, output := out } (w.length + 2) = { state := none, inputPos := ip, workTapes := fun (x : Fin 1) (x_1 : ℤ) => none, workTapePos := fun (x : Fin 1) => 0, output := out }

Rewinding while erasing from the frontier of the word leaves the tape blank.

theorem Turing.MultiTapeTM.workTapePos_runFrom_rewindWork {Symbol : Type u_1} {input : List Symbol} (write : Option (Option Symbol)) (ip : Fin (input.length + 2)) (t : ℤ → Option Symbol) (out : List Symbol) {w : List Symbol} (hw : t = tapeOfList w) {p : ℕ} (hp : p ≤ w.length) (m : ℕ) : (runFrom { state := some (rewindWork Symbol write).q₀, inputPos := ip, workTapes := fun (x : Fin 1) => t, workTapePos := fun (x : Fin 1) => ↑p, output := out } m).workTapePos 0 ∈ Set.Icc (-1) ↑p

At every step, the head is within [-1, p]: it walks from its start p ≤ w.length down to -1 and back to 0, where it stays.