Clearing a work tape along its shadow

clearShadowed m₀ m₁ is a machine with two work tapes, a work tape W and its shadow S in the sense of Turing.MultiTapeTM.shadow, whose heads are on the same cell. When the shadow marks an interval [L, R] of cells around the start cell, the start cell with m₀ and the others with m₁, except possibly the cell under the heads, and the work tape is blank outside [L, R], the machine blanks both tapes and parks both heads on the start cell (runFrom_clearShadowed):

• start: mark the cell under the heads (which the shadow may not have marked yet) and move left;
• left: move left to the blank cell L - 1 and step back onto L;
• sweep: move right to R + 1, blanking both tapes, except for a temporary mark m₁ on the work tape at the start cell;
• home: move left to the temporary mark, erase it and halt.

Main definitions

• Turing.MultiTapeTM.clearShadowed: the clearing machine.

Main results

• Turing.MultiTapeTM.runFrom_clearShadowed: its run, in a + 2 b + c + 5 steps for [L, R] = [-a, b] and the heads at c - a.

inductive Turing.MultiTapeTM.ClearShadowedState : Type

The control states of clearShadowed.

• start : ClearShadowedState
• left : ClearShadowedState
• sweep : ClearShadowedState
• home : ClearShadowedState

@[instance_reducible]

instance Turing.MultiTapeTM.instDecidableEqClearShadowedState : DecidableEq ClearShadowedState

@[instance_reducible]

instance Turing.MultiTapeTM.instFintypeClearShadowedState : Fintype ClearShadowedState

@[reducible, inline]

abbrev Turing.MultiTapeTM.ClearShadowed.action {Symbol : Type u_1} (w₀ w₁ : Option (Option Symbol)) (d : SignType) (q : Option ClearShadowedState) : Action 2 Symbol ClearShadowedState

An action of clearShadowed: write w₀ on the work tape and w₁ on the shadow, move both heads by d and enter q.

def Turing.MultiTapeTM.clearShadowed {Symbol : Type u_1} [DecidableEq Symbol] (m₀ m₁ : Symbol) : MultiTapeTM 2 Symbol ClearShadowedState

The machine clearing a work tape (tape 0) along its shadow (tape 1) marked with m₀ on the start cell and m₁ elsewhere.

@[reducible, inline]

abbrev Turing.MultiTapeTM.ClearShadowed.cfg {Symbol : Type u_1} {input : List Symbol} (q : Option ClearShadowedState) (ip : Fin (input.length + 2)) (W S : ℤ → Option Symbol) (x : ℤ) (out : List Symbol) : Cfg 2 Symbol ClearShadowedState input

The configuration with work tape W, shadow S, both heads on cell x, input head ip and output out.

theorem Turing.MultiTapeTM.runFrom_clearShadowed {Symbol : Type u_1} [DecidableEq Symbol] {input : List Symbol} {m₀ m₁ : Symbol} (hm : m₀ ≠ m₁) {ip : Fin (input.length + 2)} {out : List Symbol} {a b c : ℕ} {V : Finset ℤ} (hV : insert (↑c - ↑a) V = Finset.Icc (-↑a) ↑b) {W : ℤ → Option Symbol} (hW : ∀ y ∉ Finset.Icc (-↑a) ↑b, W y = none) : runFrom (ClearShadowed.cfg (some ClearShadowedState.start) ip W (shadowTape m₀ m₁ V) (↑c - ↑a) out) (a + 2 * b + c + 5) = ClearShadowed.cfg none ip (fun (x : ℤ) => none) (fun (x : ℤ) => none) 0 out

Clearing a shadowed tape. If the shadow marks the cells V, which together with the cell c - a under the heads form the interval [-a, b], and the work tape is blank outside it, then clearShadowed m₀ m₁ blanks both tapes and parks both heads on the start cell, in a + 2 b + c + 5 steps.