Repeating a machine while the input head reads a symbol

whileInput tm reads the symbol under the input head and halts if it is blank; otherwise it runs tm and repeats. A body that consumes the input from left to right, leaving the input head after what it read (Turing.MultiTapeTM.TransformsTapesAt), is thus run until the input is used up.

Main definitions

• Turing.MultiTapeTM.inputSymbolAt: the symbol at a position of the input.
• Turing.MultiTapeTM.whileInput: the loop.

Main results

• Turing.MultiTapeTM.transformsTapesAt_whileInput: a loop invariant preserved by every round gives a specification of whileInput tm, with the times of the rounds adding up.

def Turing.MultiTapeTM.inputSymbolAt {Symbol : Type u_1} (input : List Symbol) (p : Fin (input.length + 2)) : Option Symbol

The symbol at position p of the input tape holding input: blank at both ends.

theorem Turing.MultiTapeTM.inputSymbol_eq_inputSymbolAt {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (c : Cfg k Symbol State input) : c.inputSymbol = inputSymbolAt input c.inputPos

noncomputable def Turing.MultiTapeTM.whileInput {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) : MultiTapeTM k Symbol (RepeatUntilBlankState State)

From check, the machine halts if the input head reads a blank and otherwise starts tm, moving no head. Each round of tm returns to check.

@[simp]

theorem Turing.MultiTapeTM.val_moveInputPos_neg {n : ℕ} (p : Fin (n + 2)) : ↑(moveInputPos p (-1)) = ↑p - 1

A move to the left stops at the blank before the input.

@[simp]

theorem Turing.MultiTapeTM.val_moveInputPos_pos {n : ℕ} (p : Fin (n + 2)) : ↑(moveInputPos p 1) = min (↑p + 1) (n + 1)

A move to the right stops at the blank after the input.

theorem Turing.MultiTapeTM.transformsTapesAt_whileInput {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {P : ℕ → (input : List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → List Symbol → Prop} {R : (input : List Symbol) → Fin (input.length + 2) → (Fin k → List Symbol) → List Symbol → Prop} {rounds : ℕ} {t : ℕ → ℕ} {s : ℕ} (hround : ∀ n < rounds, ∀ (emitted : List Symbol), tm.TransformsTapesAt (fun (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) => P n input p ws emitted) (fun (input : List Symbol) (x : Fin (input.length + 2)) (x_1 : Fin k → List Symbol) (p' : Fin (input.length + 2)) (ws' : Fin k → List Symbol) (e : List Symbol) => P (n + 1) input p' ws' (emitted ++ e)) (t n) s) (hmore : ∀ n < rounds, ∀ (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) (emitted : List Symbol), P n input p ws emitted → inputSymbolAt input p ≠ none) (hend : ∀ (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) (emitted : List Symbol), P rounds input p ws emitted → inputSymbolAt input p = none ∧ R input p ws emitted) : tm.whileInput.TransformsTapesAt (fun (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) => P 0 input p ws []) (fun (input : List Symbol) (x : Fin (input.length + 2)) (x_1 : Fin k → List Symbol) (p' : Fin (input.length + 2)) (ws' : Fin k → List Symbol) (emitted : List Symbol) => R input p' ws' emitted) (∑ n ∈ Finset.range rounds, (t n + 1) + 1) (2 * k * s + k)

Let P n be a loop invariant after n rounds, on the input position, the words on the tapes and the word emitted so far. If each round n < rounds starts on a symbol of the input and takes P n to P (n + 1) within t n steps and s cells, and P rounds implies that the input head is on a blank and that R holds, then whileInput tm takes P 0 to R.