Moving words between the ends of tapes

Small native machines that move a word along its tape or between two tapes, specified by runs between Turing.tapesCfg configurations (Turing.MultiTapeTM.RunsBetween), so that the words may sit anywhere on their tapes. They implement a stack kept on a tape that grows to the left.

Main definitions

• Turing.MultiTapeTM.seekEnd: move the head from the first cell of a word to the cell after it.
• Turing.MultiTapeTM.copyBack: move a word, read from its end, to the front of the word on a second tape.
• Turing.MultiTapeTM.eraseFrame: erase a framed word (Turing.MultiTapeTM.frame) at the front of a tape.
• Turing.MultiTapeTM.popFrame: move a framed word at the front of a tape to a blank second tape, prefixed by [true, true], or write [false] there if the first tape is blank.

Main results

• Turing.MultiTapeTM.runsBetween_seekEnd, Turing.MultiTapeTM.runsBetween_copyBack, Turing.MultiTapeTM.runsBetween_eraseFrame, Turing.MultiTapeTM.runsBetween_popFrame_nil, Turing.MultiTapeTM.runsBetween_popFrame_frame: their runs, in time linear in the words moved.

Shifted words

theorem Turing.tapeOfList_eq_ite {Symbol : Type u_1} (w : List Symbol) (z : ℤ) : tapeOfList w z = if 0 ≤ z then w[z.toNat]? else none

theorem Turing.tapeOfList_cons_of_ne {Symbol : Type u_1} (x : Symbol) (l : List Symbol) {z : ℤ} (hz : z ≠ 0) : tapeOfList (x :: l) z = tapeOfList l (z - 1)

theorem Turing.update_shifted_append {Symbol : Type u_1} (w : List Symbol) (x : Symbol) (o : ℤ) : Function.update (fun (z : ℤ) => tapeOfList w (z - o)) (o + ↑w.length) (some x) = fun (z : ℤ) => tapeOfList (w ++ [x]) (z - o)

Writing after the end of a shifted word appends to it.

theorem Turing.update_shifted_cons_none {Symbol : Type u_1} (x : Symbol) (l : List Symbol) (o : ℤ) : Function.update (fun (z : ℤ) => tapeOfList (x :: l) (z - o)) o none = fun (z : ℤ) => tapeOfList l (z - (o + 1))

Erasing the first cell of a shifted word drops its first letter.

theorem Turing.update_shifted_append_none {Symbol : Type u_1} (l : List Symbol) (x : Symbol) (o : ℤ) : Function.update (fun (z : ℤ) => tapeOfList (l ++ [x]) (z - o)) (o + ↑l.length) none = fun (z : ℤ) => tapeOfList l (z - o)

Erasing the last cell of a shifted word drops its last letter.

theorem Turing.update_shifted_pred {Symbol : Type u_1} (v : List Symbol) (x : Symbol) (o : ℤ) : Function.update (fun (z : ℤ) => tapeOfList v (z - o)) (o - 1) (some x) = fun (z : ℤ) => tapeOfList (x :: v) (z - (o - 1))

Writing before the first cell of a shifted word prepends to it.

theorem Turing.tapeOfList_cons_sub_self {Symbol : Type u_1} (x : Symbol) (l : List Symbol) (o : ℤ) : tapeOfList (x :: l) (o - o) = some x

The first letter of a shifted word, read at its first cell.

theorem Turing.tapeOfList_add_length_sub {Symbol : Type u_1} (w : List Symbol) (o : ℤ) : tapeOfList w (o + ↑w.length - o) = none

The cell after a shifted word is blank.

theorem Turing.tapeOfList_sub_one_sub {Symbol : Type u_1} (w : List Symbol) (o : ℤ) : tapeOfList w (o - 1 - o) = none

The cell before a shifted word is blank.

Moving the head to the end of a word

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

Moves the head of its only tape right until it reads a blank.

theorem Turing.MultiTapeTM.runFrom_seekEnd {Symbol : Type u_1} {input : List Symbol} (w suf pre : List Symbol) (hw : w = pre ++ suf) (o : ℤ) (out : List Symbol) : runFrom ((tapesCfg input (fun (x : Fin 1) => w) (fun (x : Fin 1) => o) (fun (x : Fin 1) => o + ↑pre.length) out).withState (some ())) (suf.length + 1) = (tapesCfg input (fun (x : Fin 1) => w) (fun (x : Fin 1) => o) (fun (x : Fin 1) => o + ↑w.length) out).withState none

theorem Turing.MultiTapeTM.runsBetween_seekEnd {Symbol : Type u_1} {input : List Symbol} (w : List Symbol) (o : ℤ) (out : List Symbol) : (seekEnd Symbol).RunsBetween (tapesCfg input (fun (x : Fin 1) => w) (fun (x : Fin 1) => o) (fun (x : Fin 1) => o) out) (tapesCfg input (fun (x : Fin 1) => w) (fun (x : Fin 1) => o) (fun (x : Fin 1) => o + ↑w.length) out) (w.length + 1) (w.length + 1 + 1)

Moving a word to the front of another

inductive Turing.MultiTapeTM.CopyBackState : Type

The states of Turing.MultiTapeTM.copyBack.

• first : CopyBackState

  Step both heads left.

• loop : CopyBackState

  Move one letter.

@[instance_reducible]

instance Turing.MultiTapeTM.instDecidableEqCopyBackState : DecidableEq CopyBackState

@[instance_reducible]

instance Turing.MultiTapeTM.instFintypeCopyBackState : Fintype CopyBackState

noncomputable def Turing.MultiTapeTM.copyBack (Symbol : Type u_2) : MultiTapeTM 2 Symbol CopyBackState

Started with the head of tape 0 on the cell after a word and the head of tape 1 on the first cell of another, moves the first word letter by letter, from its end, to the front of the second, erasing it, and halts with both heads on the first cells of their words.

theorem Turing.MultiTapeTM.runFrom_copyBack_loop {Symbol : Type u_1} {input : List Symbol} (w v u : List Symbol) (oA oB oB' : ℤ) (hu : u = w ++ v) (hB : oB' = oB - ↑w.length) (out : List Symbol) : runFrom ((tapesCfg input ![w, v] ![oA, oB] ![oA + ↑w.length - 1, oB - 1] out).withState (some CopyBackState.loop)) (w.length + 1) = (tapesCfg input ![[], u] ![oA, oB'] ![oA, oB'] out).withState none

theorem Turing.MultiTapeTM.runsBetween_copyBack {Symbol : Type u_1} {input : List Symbol} (w v : List Symbol) (oA oB : ℤ) (out : List Symbol) : (copyBack Symbol).RunsBetween (tapesCfg input ![w, v] ![oA, oB] ![oA + ↑w.length, oB] out) (tapesCfg input ![[], w ++ v] ![oA, oB - ↑w.length] ![oA, oB - ↑w.length] out) (w.length + 2) (2 * (w.length + 2 + 1))

Erasing a framed word

inductive Turing.MultiTapeTM.EraseFrameState : Type

The states of Turing.MultiTapeTM.eraseFrame.

• loop : EraseFrameState

  At the start of a pair, or at the final false.

• bit : EraseFrameState

  At the second cell of a pair.

@[instance_reducible]

instance Turing.MultiTapeTM.instDecidableEqEraseFrameState : DecidableEq EraseFrameState

@[instance_reducible]

instance Turing.MultiTapeTM.instFintypeEraseFrameState : Fintype EraseFrameState

noncomputable def Turing.MultiTapeTM.eraseFrame : MultiTapeTM 1 Bool EraseFrameState

Erases the framed word at the head of its only tape, moving right, and halts on the cell after it.

theorem Turing.MultiTapeTM.runFrom_eraseFrame (w rest u : List Bool) (o o' : ℤ) {input : List Bool} (hu : u = frame w ++ rest) (ho : o' = o + ↑(2 * w.length + 1)) (out : List Bool) : runFrom ((tapesCfg input (fun (x : Fin 1) => u) (fun (x : Fin 1) => o) (fun (x : Fin 1) => o) out).withState (some EraseFrameState.loop)) (2 * w.length + 1) = (tapesCfg input (fun (x : Fin 1) => rest) (fun (x : Fin 1) => o') (fun (x : Fin 1) => o') out).withState none

theorem Turing.MultiTapeTM.runsBetween_eraseFrame (w rest : List Bool) (o : ℤ) {input : List Bool} (out : List Bool) : eraseFrame.RunsBetween (tapesCfg input (fun (x : Fin 1) => frame w ++ rest) (fun (x : Fin 1) => o) (fun (x : Fin 1) => o) out) (tapesCfg input (fun (x : Fin 1) => rest) (fun (x : Fin 1) => o + ↑(frame w).length) (fun (x : Fin 1) => o + ↑(frame w).length) out) (2 * w.length + 1) (2 * w.length + 1 + 1)

Popping a framed word

inductive Turing.MultiTapeTM.PopFrameState : Type

The states of Turing.MultiTapeTM.popFrame.

• start : PopFrameState

  Reading the first cell of tape 0.

• pre : PopFrameState

  Writing the second true of the prefix.

• loop : PopFrameState

  At the start of a pair, or at the final false.

• bit : PopFrameState

  At the second cell of a pair.

@[instance_reducible]

instance Turing.MultiTapeTM.instDecidableEqPopFrameState : DecidableEq PopFrameState

@[instance_reducible]

instance Turing.MultiTapeTM.instFintypePopFrameState : Fintype PopFrameState

noncomputable def Turing.MultiTapeTM.popFrame : MultiTapeTM 2 Bool PopFrameState

If tape 0 is blank under its head, writes false at the head of tape 1. Otherwise writes [true, true] and then moves the framed word at the head of tape 0 there, erasing it. Both heads move right as they go. The specifications below start with a blank tape 1; the loop Turing.MultiTapeTM.runFrom_popFrame_loop appends to any word ending before the head.

theorem Turing.MultiTapeTM.runFrom_popFrame_loop (w rest u acc acc' : List Bool) (oS oS' oR hR' : ℤ) {input : List Bool} (hu : u = frame w ++ rest) (hacc : acc' = acc ++ frame w) (hS : oS' = oS + ↑(2 * w.length + 1)) (hR : hR' = oR + ↑acc'.length) (out : List Bool) : runFrom ((tapesCfg input ![u, acc] ![oS, oR] ![oS, oR + ↑acc.length] out).withState (some PopFrameState.loop)) (2 * w.length + 1) = (tapesCfg input ![rest, acc'] ![oS', oR] ![oS', hR'] out).withState none

theorem Turing.MultiTapeTM.runsBetween_popFrame_nil (oS oR : ℤ) {input : List Bool} (out : List Bool) : popFrame.RunsBetween (tapesCfg input ![[], []] ![oS, oR] ![oS, oR] out) (tapesCfg input ![[], [false]] ![oS, oR] ![oS, oR + 1] out) 1 (2 * (1 + 1))

On a blank tape 0, popFrame writes [false].

theorem Turing.MultiTapeTM.runsBetween_popFrame_frame (w rest : List Bool) (oS oR : ℤ) {input : List Bool} (out : List Bool) : popFrame.RunsBetween (tapesCfg input ![frame w ++ rest, []] ![oS, oR] ![oS, oR] out) (tapesCfg input ![rest, frame (true :: w)] ![oS + ↑(frame w).length, oR] ![oS + ↑(frame w).length, oR + ↑(frame (true :: w)).length] out) (2 * w.length + 3) (2 * (2 * w.length + 3 + 1))

On a framed word frame w at the head of tape 0, popFrame moves it to tape 1 as frame (true :: w).