Repeating a machine until a tape goes blank

repeatUntilBlank i tm runs tm repeatedly. After each round it reads the cell under the head of work tape i and halts if that cell is blank. Each round of a Turing.MultiTapeTM.TransformsTapes specification ends with every head on the first cell of its word, so the loop halts exactly when the word on tape i is empty. The body always runs at least once.

Main results

• Turing.MultiTapeTM.transformsTapes_repeatUntilBlank: a loop invariant preserved by every round gives a specification of repeatUntilBlank i tm, with time bound (rounds + 1) * (t + 1) and space bound 2 * k * s + k.

inductive Turing.MultiTapeTM.RepeatUntilBlankState (State : Type u_3) : Type u_3

The states of repeatUntilBlank i tm: those of tm, and a state check for reading tape i between rounds.

• run {State : Type u_3} (q : State) : RepeatUntilBlankState State

  The repeated machine is running, in its state q.

• check {State : Type u_3} : RepeatUntilBlankState State

  Tape i is being read, between two rounds.

instance Turing.MultiTapeTM.instFiniteRepeatUntilBlankState {State : Type u_2} [Finite State] : Finite (RepeatUntilBlankState State)

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

tm, with its halting transitions sent to the state check. From check, the machine halts if the cell under the head of tape i is blank and otherwise restarts tm, moving no head.

theorem Turing.MultiTapeTM.transformsTapes_repeatUntilBlank {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (i : Fin k) {tm : MultiTapeTM k Symbol State} {P : ℕ → List Symbol → (Fin k → List Symbol) → List Symbol → Prop} {R : List Symbol → (Fin k → List Symbol) → List Symbol → Prop} {rounds t s : ℕ} (hround : ∀ n < rounds, ∀ (emitted : List Symbol), tm.TransformsTapes (fun (input : List Symbol) (ws : Fin k → List Symbol) => P n input ws emitted) (fun (input : List Symbol) (x ws' : Fin k → List Symbol) (e : List Symbol) => P (n + 1) input ws' (emitted ++ e) ∧ ws' i ≠ []) t s) (hstop : ∀ (emitted : List Symbol), tm.TransformsTapes (fun (input : List Symbol) (ws : Fin k → List Symbol) => P rounds input ws emitted) (fun (input : List Symbol) (x ws' : Fin k → List Symbol) (e : List Symbol) => R input ws' (emitted ++ e) ∧ ws' i = []) t s) : (repeatUntilBlank i tm).TransformsTapes (fun (input : List Symbol) (ws : Fin k → List Symbol) => P 0 input ws []) (fun (input : List Symbol) (x ws' : Fin k → List Symbol) (emitted : List Symbol) => R input ws' emitted) ((rounds + 1) * (t + 1)) (2 * k * s + k)

Let P n be a loop invariant after n rounds, on the words on the tapes and the word emitted so far. If each round n < rounds takes P n to P (n + 1) and leaves tape i non-empty, and the round after that takes P rounds to R and empties tape i, then repeatUntilBlank i tm takes P 0 to R.

Each of the rounds + 1 rounds takes at most t + 1 steps. No head leaves [-s, s], since every round starts with all heads at cell 0 and uses at most s cells.