Tapes holding words and configurations of such tapes

The normal form in which "tape transformer" machines (cf. TransformsTapes.lean) start and finish: every work tape holds a word in the cells 0, 1, … and is blank everywhere else, with every head at the start.

Main definitions

• Turing.tapeOfList: the tape holding exactly a given word.
• Turing.wordsCfg: the configuration whose tapes hold given words.

def Turing.tapeOfList {Symbol : Type u_2} (xs : List Symbol) : ℤ → Option Symbol

A tape containing exactly the symbols of xs at positions 0, ..., xs.length - 1.

@[simp]

theorem Turing.tapeOfList_ofNat {Symbol : Type u_2} (xs : List Symbol) (n : ℕ) : tapeOfList xs ↑n = xs[n]?

@[simp]

theorem Turing.tapeOfList_negSucc {Symbol : Type u_2} (xs : List Symbol) (n : ℕ) : tapeOfList xs (Int.negSucc n) = none

theorem Turing.tapeOfList_append_single {Symbol : Type u_2} (xs : List Symbol) (x : Symbol) : tapeOfList (xs ++ [x]) = Function.update (tapeOfList xs) (↑xs.length) (some x)

Appending one symbol writes precisely the cell after the existing word.

theorem Turing.tapeOfList_eq_none_iff {Symbol : Type u_2} (xs : List Symbol) (z : ℤ) : tapeOfList xs z = none ↔ z < 0 ∨ ↑xs.length ≤ z

A cell of tapeOfList xs is blank exactly outside the positions 0, …, xs.length - 1.

@[simp]

theorem Turing.tapeOfList_nil {Symbol : Type u_2} : tapeOfList [] = fun (x : ℤ) => none

The blank tape holds the empty word.

theorem Turing.tapeOfList_zero {Symbol : Type u_2} (xs : List Symbol) : tapeOfList xs 0 = xs.head?

The cell at position 0 holds the first symbol of the word.

def Turing.wordsCfg {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : Cfg k Symbol State input

The configuration whose work tape i holds exactly the word ws i with its head at the start, whose input head is at the start of the input, in state q with output out.

@[simp]

theorem Turing.wordsCfg_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : (wordsCfg input q ws out).state = q

@[simp]

theorem Turing.wordsCfg_workTapes {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) (i : Fin k) (a✝ : ℤ) : (wordsCfg input q ws out).workTapes i a✝ = tapeOfList (ws i) a✝

@[simp]

theorem Turing.wordsCfg_workTapePos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) (x✝ : Fin k) : (wordsCfg input q ws out).workTapePos x✝ = 0

@[simp]

theorem Turing.wordsCfg_output {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : (wordsCfg input q ws out).output = out

@[simp]

theorem Turing.wordsCfg_inputPos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : (wordsCfg input q ws out).inputPos = 1

@[simp]

theorem Turing.mapState_wordsCfg {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {State' : Type u_3} (φ : Option State → Option State') (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : Cfg.mapState φ (wordsCfg input q ws out) = wordsCfg input (φ q) ws out

Remapping the state of a wordsCfg remaps its state and leaves the words alone.

@[simp]

theorem Turing.withState_wordsCfg {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {State' : Type u_3} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) (q' : Option State') : (wordsCfg input q ws out).withState q' = wordsCfg input q' ws out

Changing the state of a wordsCfg leaves the words alone.

@[simp]

theorem Turing.prependOutput_wordsCfg {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out pre : List Symbol) : (wordsCfg input q ws out).prependOutput pre = wordsCfg input q ws (pre ++ out)

Prepending a word to the output of a wordsCfg prepends it to the output word.

theorem Turing.Cfg.init_eq_wordsCfg {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (q₀ : State) (input : List Symbol) : init q₀ input = wordsCfg input (some q₀) (fun (x : Fin k) => []) []

The initial configuration is the word configuration with blank tapes and no output.