Canonical cleanup for the multi-tape to TM2 compiler

Cleanup discards the input and work stacks, reverses the accumulated output onto the output stack, and resets finite control. Existing output is retained as a suffix.

Main definitions

• StateTransition.EvalsToInTime.cons, .mono: prepend one transition or enlarge the clock of a bounded partial execution.
• Turing.MultiTapeTM.ToTM2.auxiliaryLength: storage discarded by cleanup.
• Turing.MultiTapeTM.ToTM2.totalStackLength: storage on all stacks, including input and output.

Main results

• Turing.MultiTapeTM.ToTM2.cleanupEvals: canonical halting with an explicit linear clock.
• Turing.MultiTapeTM.ToTM2.cleanup_stack_bound: cleanup never increases total stack storage.

References

• C. Papadimitriou, Computational Complexity, Chapter 2

def StateTransition.EvalsToInTime.cons {α : Type} {f : α → Option α} {a b c : α} {n : ℕ} (hs : f a = some b) (h : EvalsToInTime f b (some c) n) : EvalsToInTime f a (some c) (n + 1)

Prepend one transition to a bounded execution.

def StateTransition.EvalsToInTime.mono {α : Type} {f : α → Option α} {a c : α} {m n : ℕ} (h : EvalsToInTime f a (some c) m) (hmn : m ≤ n) : EvalsToInTime f a (some c) n

Increase the clock of a bounded execution.

@[simp]

theorem Turing.MultiTapeTM.ToTM2.mem_auxiliaries {k : ℕ} (s : Stack k) : s ∈ auxiliaries k ↔ s ≠ Stack.output ∧ s ≠ Stack.reversed

Exactly the stacks other than the two output stacks are discarded.

theorem Turing.MultiTapeTM.ToTM2.auxiliaries_nodup (k : ℕ) : (auxiliaries k).Nodup

Each auxiliary is popped exactly once in a cleanup round.

def Turing.MultiTapeTM.ToTM2.auxiliaryLength {k : ℕ} (store : (s : Stack k) → List (Alphabet s)) : ℕ

Total auxiliary storage before a cleanup round.

def Turing.MultiTapeTM.ToTM2.totalStackLength {k : ℕ} {State : Type} (cfg : TM2.Cfg Alphabet Label (Control k State)) : ℕ

Total stack storage, counting both output stacks and all auxiliary stacks.

theorem Turing.MultiTapeTM.ToTM2.totalStackLength_eq {k : ℕ} {State : Type} (cfg : TM2.Cfg Alphabet Label (Control k State)) : totalStackLength cfg = auxiliaryLength cfg.stk + (cfg.stk Stack.reversed).length + (cfg.stk Stack.output).length

Every stack contributes exactly once to the storage accounting.

theorem Turing.MultiTapeTM.ToTM2.auxiliaryLength_eq_zero_iff {k : ℕ} (store : (s : Stack k) → List (Alphabet s)) : auxiliaryLength store = 0 ↔ ∀ s ∈ auxiliaries k, store s = []

Zero auxiliary storage is equivalent to emptiness of every auxiliary stack.

noncomputable def Turing.MultiTapeTM.ToTM2.cleanupEvals {k : ℕ} {State : Type} [Fintype State] (q₀ : State) (transition : State → Option Bool → (Fin k → Option Bool) → Action k Bool State) (cfg : (machine q₀ transition).Cfg) (hl : cfg.l = some Label.clean) : StateTransition.EvalsToInTime (machine q₀ transition).step cfg (some (haltList (machine q₀ transition) ((cfg.stk Stack.reversed).reverse.append (cfg.stk Stack.output)))) (auxiliaryLength cfg.stk + (cfg.stk Stack.reversed).length + 2)

Configuration form of cleanEvals, allowing arbitrary finite control and stack contents.

theorem Turing.MultiTapeTM.ToTM2.cleanup_stack_bound {k : ℕ} {State : Type} [Fintype State] (q₀ : State) (transition : State → Option Bool → (Fin k → Option Bool) → Action k Bool State) (cfg : (machine q₀ transition).Cfg) (hl : cfg.l = some Label.clean) (i : ℕ) : totalStackLength ((TM2.stepTotal (machine q₀ transition).m)^[i] cfg) ≤ totalStackLength cfg

Every cleanup and reversal step, even after halting, uses at most the initial total storage.