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.

def Turing.MultiTapeTM.RepeatUntilBlank.blankTest {k : ℕ} {Symbol : Type u_1} (i : Fin k) : MultiTapeTM k Symbol Unit

The test of tape i: it halts if the cell under the head of tape i is blank and otherwise stays in its only state, moving no head.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

tm combined with the test of tape i: halting of tm goes to the test, which halts the loop if the cell under the head of tape i is blank and otherwise restarts tm.

Equations

• One or more equations did not get rendered due to their size.

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.