Repeating a machine while a condition holds

whileCond c tm reads the symbols under its heads and halts unless the condition c holds of them; otherwise it runs tm and repeats. Unlike Turing.MultiTapeTM.repeatUntilBlank, the rounds may leave the input head anywhere (Turing.MultiTapeTM.TransformsTapesAt), so the loop can drive a two-way input head.

Main definitions

• Turing.MultiTapeTM.whileCond: the loop.

Main results

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

noncomputable def Turing.MultiTapeTM.whileCond {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (c : Option Symbol → (Fin k → Option Symbol) → Bool) (tm : MultiTapeTM k Symbol State) : MultiTapeTM k Symbol (RepeatUntilBlankState State)

From check, the machine halts unless c holds of the symbols under the input head and the work-tape heads, and otherwise starts tm, moving no head. Each round of tm returns to check.

def Turing.MultiTapeTM.condAt {k : ℕ} {Symbol : Type u_1} (c : Option Symbol → (Fin k → Option Symbol) → Bool) (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) : Bool

The condition c on the configuration with the input head at p and the words ws on the work tapes, read at the start of each word.

theorem Turing.MultiTapeTM.transformsTapesAt_whileCond {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {c : Option Symbol → (Fin k → Option Symbol) → Bool} {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 → condAt c input p ws = true) (hend : ∀ (input : List Symbol) (p : Fin (input.length + 2)) (ws : Fin k → List Symbol) (emitted : List Symbol), P rounds input p ws emitted → condAt c input p ws = false ∧ R input p ws emitted) : (whileCond c tm).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 with the condition holding and takes P n to P (n + 1) within t n steps and s cells, and P rounds implies that the condition fails and that R holds, then whileCond c tm takes P 0 to R.