Shadowing the work tapes of a machine

shadow m₀ m₁ tm runs tm on its first k work tapes, while work tape k + i shadows work tape i: its head moves with the head of tape i and marks every cell it reads, the start cell with m₀ and the other cells with m₁ (shadowTape). When tm halts, the marks record the cells the head of tape i visited before the halting step; only the cell under the head after the halting step may be unmarked. A machine cannot tell these cells from the tape of tm alone, since tm may leave blanks among the cells it wrote, but a machine that cleans up after tm can sweep the marked cells (Turing.MultiTapeTM.clearShadowed).

The first step of shadow m₀ m₁ tm marks the start cells; after it, the machine mirrors tm step by step (Shadow.runFrom_cfg), and if tm first halts at step u it has halted at step u + 1 (runFrom_shadow).

Main definitions

• Turing.MultiTapeTM.shadowTape: the marks of a set of cells.
• Turing.MultiTapeTM.shadow: the shadowing machine.

Main results

• Turing.MultiTapeTM.runFrom_shadow: the configuration of shadow m₀ m₁ tm when tm has halted.
• Turing.MultiTapeTM.space_shadow: shadow m₀ m₁ tm uses twice the space of tm.

def Turing.MultiTapeTM.pairIdx {k : ℕ} (j : Fin (k + k)) : Fin k

The work tape a tape of k + k belongs to: tape i and its shadow k + i belong to i.

@[simp]

theorem Turing.MultiTapeTM.pairIdx_castAdd {k : ℕ} (i : Fin k) : pairIdx (Fin.castAdd k i) = i

theorem Turing.MultiTapeTM.pairIdx_natAdd {k : ℕ} (i : Fin k) : pairIdx (Fin.natAdd k i) = i

@[simp]

theorem Turing.MultiTapeTM.pairIdx_addNat {k : ℕ} (i : Fin k) : pairIdx (i.addNat k) = i

pairIdx_natAdd in simp normal form, since Fin.natAdd k i simplifies to i.addNat k.

The shadowing machine

def Turing.MultiTapeTM.shadowTape {Symbol : Type u_1} (m₀ m₁ : Symbol) (V : Finset ℤ) : ℤ → Option Symbol

The shadow tape marking the cells V: m₀ on the start cell, m₁ on the other cells of V, blank elsewhere.

theorem Turing.MultiTapeTM.shadowTape_eq_none_iff {Symbol : Type u_1} {m₀ m₁ : Symbol} {V : Finset ℤ} {x : ℤ} : shadowTape m₀ m₁ V x = none ↔ x ≠ 0 ∧ x ∉ V

A shadow tape is blank exactly away from the start cell and the marked cells.

theorem Turing.MultiTapeTM.shadowTape_insert {Symbol : Type u_1} {m₀ m₁ : Symbol} (V : Finset ℤ) (x : ℤ) : shadowTape m₀ m₁ (insert x V) = if (shadowTape m₀ m₁ V x).isNone = true then Function.update (shadowTape m₀ m₁ V) x (some m₁) else shadowTape m₀ m₁ V

Recording one more cell marks it, unless it is marked already.

noncomputable def Turing.MultiTapeTM.shadow {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (m₀ m₁ : Symbol) (tm : MultiTapeTM k Symbol State) : MultiTapeTM (k + k) Symbol (Option State)

tm on the first k of k + k work tapes, with tape k + i shadowing tape i. The state none marks the start cells of the shadow tapes with m₀; in state some q the machine runs tm in state q and marks the cells under the shadow heads that are not yet marked with m₁.

noncomputable def Turing.MultiTapeTM.Shadow.visited {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (c : Cfg k Symbol State input) (n : ℕ) (i : Fin k) : Finset ℤ

The cells visited by the head of work tape i in the first n steps from c, not counting the cell it is on after them.

theorem Turing.MultiTapeTM.Shadow.visited_succ {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (c : Cfg k Symbol State input) (n : ℕ) (i : Fin k) : visited tm c (n + 1) i = insert ((runFrom c n).workTapePos i) (visited tm c n i)

One more step visits the cell the head was on.

theorem Turing.MultiTapeTM.Shadow.visitedByTapeHead_eq_insert {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (c : Cfg k Symbol State input) (n : ℕ) (i : Fin k) : visitedByTapeHead c n i = insert ((runFrom c n).workTapePos i) (visited tm c n i)

The cells visited up to step n are the cells visited before step n and the cell the head is on at step n.

def Turing.MultiTapeTM.Shadow.cfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (m₀ m₁ : Symbol) (c : Cfg k Symbol State input) (V : Fin k → Finset ℤ) : Cfg (k + k) Symbol (Option State) input

The configuration of shadow m₀ m₁ tm mirroring the configuration c of tm, with shadow tape i marking the cells V i.

@[simp]

theorem Turing.MultiTapeTM.Shadow.inputSymbol_cfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {m₀ m₁ : Symbol} (c : Cfg k Symbol State input) (V : Fin k → Finset ℤ) : (cfg m₀ m₁ c V).inputSymbol = c.inputSymbol

theorem Turing.MultiTapeTM.Shadow.step_initCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {m₀ m₁ : Symbol} {tm : MultiTapeTM k Symbol State} : step ((shadow m₀ m₁ tm).initCfg input) = cfg m₀ m₁ (tm.initCfg input) fun (x : Fin k) => ∅

The first step marks the start cells.

theorem Turing.MultiTapeTM.Shadow.step_cfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {m₀ m₁ : Symbol} {tm : MultiTapeTM k Symbol State} {c : Cfg k Symbol State input} {q : State} (hq : c.state = some q) (V : Fin k → Finset ℤ) : step (cfg m₀ m₁ c V) = cfg m₀ m₁ (step c) fun (i : Fin k) => insert (c.workTapePos i) (V i)

A live step of tm is mirrored by one step of shadow m₀ m₁ tm, which marks the cells under the heads.

theorem Turing.MultiTapeTM.Shadow.runFrom_cfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {m₀ m₁ : Symbol} {tm : MultiTapeTM k Symbol State} (c : Cfg k Symbol State input) (V : Fin k → Finset ℤ) (n : ℕ) (h : ∀ m < n, (runFrom c m).state ≠ none) : runFrom (cfg m₀ m₁ c V) n = cfg m₀ m₁ (runFrom c n) fun (i : Fin k) => V i ∪ visited tm c n i

While tm runs, shadow m₀ m₁ tm mirrors it, marking the visited cells.

theorem Turing.MultiTapeTM.Shadow.runFrom_succ_initCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {m₀ m₁ : Symbol} {tm : MultiTapeTM k Symbol State} {u : ℕ} (h : ∀ m < u, ¬(runFrom (tm.initCfg input) m).Halted) {m : ℕ} (hm : m ≤ u) : runFrom ((shadow m₀ m₁ tm).initCfg input) (m + 1) = cfg m₀ m₁ (runFrom (tm.initCfg input) m) (visited tm (tm.initCfg input) m)

After its first step, shadow m₀ m₁ tm mirrors the run of tm until tm halts.

theorem Turing.MultiTapeTM.runFrom_shadow {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {m₀ m₁ : Symbol} {tm : MultiTapeTM k Symbol State} {u : ℕ} (h : ∀ m < u, ¬(runFrom (tm.initCfg input) m).Halted) : runFrom ((shadow m₀ m₁ tm).initCfg input) (u + 1) = Shadow.cfg m₀ m₁ (runFrom (tm.initCfg input) u) (Shadow.visited tm (tm.initCfg input) u)

If tm has not halted before step u, then after u + 1 steps shadow m₀ m₁ tm holds the configuration of tm after u steps, and shadow tape i marks the cells visited by the head of tape i before step u. In particular, if tm halts at step u, so has shadow m₀ m₁ tm at step u + 1.

theorem Turing.MultiTapeTM.space_shadow {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {m₀ m₁ : Symbol} {tm : MultiTapeTM k Symbol State} {u : ℕ} (h : ∀ m < u, ¬(runFrom (tm.initCfg input) m).Halted) : space ((shadow m₀ m₁ tm).initCfg input) (u + 1) = 2 * space (tm.initCfg input) u

Until tm halts, shadow m₀ m₁ tm uses twice the space of tm.