The existing single-machine tidy normalization construction

Machine declarations are moved from their original module without changing programs or resource formulas. Higher computability-calculus theorems remain in the original facade.

Clearing a work tape and its shadow

def Turing.MultiTapeTM.pairEmb {k : ℕ} (i : Fin k) : Fin 2 ↪ Fin (k + k)

The embedding of work tape i and its shadow k + i.

@[simp]

theorem Turing.MultiTapeTM.pairEmb_zero {k : ℕ} (i : Fin k) : (pairEmb i) 0 = Fin.castAdd k i

@[simp]

theorem Turing.MultiTapeTM.pairEmb_one {k : ℕ} (i : Fin k) : (pairEmb i) 1 = i.addNat k

The shadow of work tape i is tape k + i, written i.addNat k in simp normal form.

theorem Turing.MultiTapeTM.pairIdx_eq_iff {k : ℕ} {j : Fin (k + k)} {i : Fin k} : pairIdx j = i ↔ j = Fin.castAdd k i ∨ j = i.addNat k

The tapes of the pair i are work tape i and its shadow.

theorem Turing.MultiTapeTM.partialInv_pairEmb {k : ℕ} (i : Fin k) (j : Fin (k + k)) : partialInv (pairEmb i) j = if j = Fin.castAdd k i then some 0 else if j = i.addNat k then some 1 else none

Tape j is a tape of the pair i exactly when it is work tape i or its shadow.

structure Turing.MultiTapeTM.PairReady {k : ℕ} {Symbol : Type u_1} {input : List Symbol} {σ : Type u_2} (m₀ m₁ : Symbol) (C : Cfg (k + k) Symbol σ input) (i : Fin k) (a b c : ℕ) (V : Finset ℤ) : Prop

Work tape i of C and its shadow k + i are ready to be cleared: the heads of both are on cell c - a, the shadow marks cells V that together with c - a form the interval [-a, b], and the work tape is blank outside it.

• pos_castAdd : C.workTapePos (Fin.castAdd k i) = ↑c - ↑a

  The head of the work tape is on cell c - a.

• pos_natAdd : C.workTapePos (Fin.natAdd k i) = ↑c - ↑a

  The head of the shadow is on cell c - a.

• insert_eq : insert (↑c - ↑a) V = Finset.Icc (-↑a) ↑b

  The marked cells and the cell under the heads form the interval [-a, b].

• shadow_eq : C.workTapes (Fin.natAdd k i) = shadowTape m₀ m₁ V

  The shadow marks the cells V.

• blank (y : ℤ) : y ∉ Finset.Icc (-↑a) ↑b → C.workTapes (Fin.castAdd k i) y = none

  The work tape is blank outside [-a, b].

def Turing.MultiTapeTM.clearedCfg {k : ℕ} {Symbol : Type u_1} {input : List Symbol} {σ : Type u_2} {σ' : Type u_3} (l : List (Fin k)) (C : Cfg (k + k) Symbol σ input) : Cfg (k + k) Symbol σ' input

C, halted, with the work tapes in l and their shadows blank and their heads on the start cell.

@[simp]

theorem Turing.MultiTapeTM.clearedCfg_nil {k : ℕ} {Symbol : Type u_1} {input : List Symbol} {σ : Type u_2} {σ' : Type u_3} (C : Cfg (k + k) Symbol σ input) : clearedCfg [] C = C.withState none

theorem Turing.MultiTapeTM.clearedCfg_cons {k : ℕ} {Symbol : Type u_1} {input : List Symbol} {σ : Type u_2} {σ' : Type u_3} {σ₁ : Type u_4} (i : Fin k) (l : List (Fin k)) (C : Cfg (k + k) Symbol σ input) : clearedCfg (i :: l) C = clearedCfg l (clearedCfg [i] C)

@[simp]

theorem Turing.MultiTapeTM.Sequential.rightCfg_clearedCfg {k : ℕ} {Symbol : Type u_1} {input : List Symbol} {σ : Type u_2} {State₀ : Type u_4} {State₁ : Type u_5} (l : List (Fin k)) (C : Cfg (k + k) Symbol σ input) : rightCfg (clearedCfg l C) = clearedCfg l C

theorem Turing.MultiTapeTM.PairReady.clearedCfg {k : ℕ} {Symbol : Type u_1} {input : List Symbol} {m₀ m₁ : Symbol} {σ : Type u_2} {σ' : Type u_3} {C : Cfg (k + k) Symbol σ input} {i : Fin k} {a b c : ℕ} {V : Finset ℤ} {l : List (Fin k)} (h : PairReady m₀ m₁ C i a b c V) (hil : i ∉ l) : PairReady m₀ m₁ (MultiTapeTM.clearedCfg l C) i a b c V

Clearing tapes l preserves PairReady on any tape i ∉ l.

theorem Turing.MultiTapeTM.runFrom_clearShadowed_pairEmb {k : ℕ} {Symbol : Type u_1} [DecidableEq Symbol] {input : List Symbol} {m₀ m₁ : Symbol} {σ : Type u_2} (hm : m₀ ≠ m₁) {C : Cfg (k + k) Symbol σ input} {i : Fin k} {a b c : ℕ} {V : Finset ℤ} (h : PairReady m₀ m₁ C i a b c V) : runFrom (C.withState (some ClearShadowedState.start)) (a + 2 * b + c + 5) = clearedCfg [i] C

Clearing one work tape and its shadow inside a machine with k + k work tapes.

def Turing.MultiTapeTM.ClearListState : ℕ → Type

The control states of clearList for a list of length n.

instance Turing.MultiTapeTM.instFiniteClearListState (n : ℕ) : Finite (ClearListState n)

noncomputable def Turing.MultiTapeTM.clearList {k : ℕ} {Symbol : Type u_1} [DecidableEq Symbol] (m₀ m₁ : Symbol) (l : List (Fin k)) : MultiTapeTM (k + k) Symbol (ClearListState l.length)

Clear the work tapes in l along their shadows, one after the other.

theorem Turing.MultiTapeTM.exists_runPath_clearList {k : ℕ} {Symbol : Type u_1} [DecidableEq Symbol] {input : List Symbol} {m₀ m₁ : Symbol} {σ : Type u_2} (hm : m₀ ≠ m₁) (l : List (Fin k)) (hl : l.Nodup) (a b c : Fin k → ℕ) (V : Fin k → Finset ℤ) (C : Cfg (k + k) Symbol σ input) (hC : ∀ i ∈ l, PairReady m₀ m₁ C i (a i) (b i) (c i) (V i)) : ∃ (p : (clearList m₀ m₁ l).RunPath input), RelSeries.head p = C.withState (some (clearList m₀ m₁ l).q₀) ∧ RelSeries.last p = clearedCfg l C ∧ p.time ≤ (List.map (fun (i : Fin k) => a i + 2 * b i + c i + 5) l).sum + 1

Clearing a list of work tapes with their shadows, each ready to be cleared: a run path of clearList m₀ m₁ l to the configuration with these tapes cleared.

The tidy normal form

noncomputable def Turing.MultiTapeTM.tidy {k : ℕ} {Symbol : Type u_1} [DecidableEq Symbol] (m₀ m₁ : Symbol) {State : Type u_4} (tm : MultiTapeTM k Symbol State) : MultiTapeTM (k + k) Symbol ((Option State ⊕ ClearListState (List.finRange k).length) ⊕ RewindState)

The tidy normal form of tm: run tm with shadowed work tapes, clear every work tape along its shadow, and rewind the input head. The symbols m₀ and m₁ mark the shadows.

theorem Turing.MultiTapeTM.exists_runPath_tidy {k : ℕ} {Symbol : Type u_1} [DecidableEq Symbol] {input : List Symbol} {m₀ m₁ : Symbol} {State : Type u_4} {tm : MultiTapeTM k Symbol State} (hm : m₀ ≠ m₁) {u : ℕ} (hlt : ∀ m < u, ¬(runFrom (tm.initCfg input) m).Halted) (hu : (runFrom (tm.initCfg input) u).Halted) : ∃ (p : (tidy m₀ m₁ tm).RunPath input), RelSeries.head p = (tidy m₀ m₁ tm).initCfg input ∧ RelSeries.last p = wordsCfg input none (fun (x : Fin (k + k)) => []) (runFrom (tm.initCfg input) u).output ∧ p.time ≤ 2 * u + 3 * (MultiTapeNTM.RunPath.ofDeterministic tm (tm.initCfg input) u).space + 2 * k + 4 ∧ p.space ≤ 2 * (MultiTapeNTM.RunPath.ofDeterministic tm (tm.initCfg input) u).space + 2 * k * (3 * (MultiTapeNTM.RunPath.ofDeterministic tm (tm.initCfg input) u).space + 2 * k + 3)

The run of the tidy normal form. If tm first halts at step u, having used S cells, then tidy m₀ m₁ tm has a run path to the halted configuration with blank work tapes, every head on its start cell and the output of tm, taking at most 2 u + 3 S + 2 k + 4 steps and visiting at most 2 S + 2 k (3 S + 2 k + 3) cells.

theorem Turing.MultiTapeTM.ComputesInTimeAndSpace.computesTidily_tidy {k : ℕ} {Symbol : Type u_1} [DecidableEq Symbol] {input : List Symbol} {m₀ m₁ : Symbol} {State : Type u_4} {tm : MultiTapeTM k Symbol State} (hm : m₀ ≠ m₁) {output : List Symbol} {t s : ℕ} (h : tm.ComputesInTimeAndSpace input output t s) : (tidy m₀ m₁ tm).ComputesTidilyInTimeAndSpace input output (2 * t + 3 * s + 2 * k + 4) (2 * s + 2 * k * (3 * s + 2 * k + 3))

The tidy normal form. What tm computes within t steps and s cells, tidy m₀ m₁ tm computes tidily within 2 t + 3 s + 2 k + 4 steps and 2 s + 2 k (3 s + 2 k + 3) cells, for any two distinct marks m₀ and m₁.