Reading from the input at the input head

An InputReader is a finite-state device that reads the input from the input head on: in state q on the symbol a it emits at most one symbol and continues in a new state, or stops after a. It also stops at the end of the input. appendRead r i appends what r emits to the word on work tape i and leaves the input head after what r read. Reading one token of a self-delimiting encoding is an instance.

Main definitions

• Turing.MultiTapeTM.InputReader: finite-state input readers.
• Turing.MultiTapeTM.InputReader.read: the word a reader emits and the number of symbols it reads.
• Turing.MultiTapeTM.appendRead: the machine that runs a reader, appending to a work tape.

Main results

• Turing.MultiTapeTM.transformsTapesAt_appendRead: its specification.

structure Turing.MultiTapeTM.InputReader (Symbol : Type u_3) (Q : Type u_4) : Type (max u_3 u_4)

A finite-state input reader: in state q on the symbol a it emits (step q a).2 and continues in (step q a).1, or stops after a if that is none.

• q₀ : Q

  The initial state.

• step : Q → Symbol → Option Q × Option Symbol

  The next state, or none to stop, and the emitted symbol, if any.

def Turing.MultiTapeTM.InputReader.read {Symbol : Type u_1} {Q : Type u_2} (r : InputReader Symbol Q) : Q → List Symbol → List Symbol × ℕ

The word r emits on w from state q, and the number of symbols it reads: it stops after a symbol leading to none, or at the end of w.

theorem Turing.MultiTapeTM.InputReader.read_cons_of_none {Symbol : Type u_1} {Q : Type u_2} (r : InputReader Symbol Q) {q : Q} {a : Symbol} (w : List Symbol) (h : (r.step q a).1 = none) : r.read q (a :: w) = ((r.step q a).2.toList, 1)

theorem Turing.MultiTapeTM.InputReader.read_cons_of_some {Symbol : Type u_1} {Q : Type u_2} (r : InputReader Symbol Q) {q q' : Q} {a : Symbol} (w : List Symbol) (h : (r.step q a).1 = some q') : r.read q (a :: w) = ((r.step q a).2.toList ++ (r.read q' w).1, (r.read q' w).2 + 1)

theorem Turing.MultiTapeTM.InputReader.read_snd_le {Symbol : Type u_1} {Q : Type u_2} (r : InputReader Symbol Q) (q : Q) (w : List Symbol) : (r.read q w).2 ≤ w.length

theorem Turing.MultiTapeTM.InputReader.length_read_fst_le {Symbol : Type u_1} {Q : Type u_2} (r : InputReader Symbol Q) (q : Q) (w : List Symbol) : (r.read q w).1.length ≤ (r.read q w).2

noncomputable def Turing.MultiTapeTM.InputReader.appendOne {Symbol : Type u_1} {Q : Type u_2} (r : InputReader Symbol Q) : MultiTapeTM 1 Symbol (Unit ⊕ Q ⊕ RewindWorkState)

r run on one work tape: move the head to the end of the word, append what r emits while reading the input, and move the head back to the start.

noncomputable def Turing.MultiTapeTM.appendRead {k : ℕ} {Symbol : Type u_1} {Q : Type u_2} (r : InputReader Symbol Q) (i : Fin k) : MultiTapeTM k Symbol (Unit ⊕ Q ⊕ RewindWorkState)

r run on work tape i, appending what it emits to the word there.

theorem Turing.MultiTapeTM.transformsTapesAt_appendRead {k : ℕ} {Symbol : Type u_1} {Q : Type u_2} (r : InputReader Symbol Q) (i : Fin k) (x : List Symbol) (p₀ : Fin (x.length + 2)) (hp₀ : ↑p₀ ≠ 0) (v : List Symbol) : have rd := r.read r.q₀ (List.drop (↑p₀ - 1) x); (appendRead r i).TransformsTapesAt (fun (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) => input = x ∧ ↑p = ↑p₀ ∧ ws i = v) (fun (x_1 : List Symbol) (x_2 : Fin (x_1.length + 2)) (ws : Fin k → List Symbol) (p' : Fin (x_1.length + 2)) (ws' : Fin k → List Symbol) (e : List Symbol) => ↑p' = ↑p₀ + rd.2 ∧ ws' = Function.update ws i (v ++ rd.1) ∧ e = []) (v.length + 1 + (rd.2 + 1 + ((v ++ rd.1).length + 2))) ((v ++ rd.1).length + 2 + (k - 1))

appendRead r i, started with the input head at p on the input x and v on work tape i, appends what r emits reading x from p on to v, moves the input head over what r read, and changes nothing else.