Space bounds for the CSLib multi-tape simulation

The simulator TM.toMultiTape keeps each CSLib work head at the position of the head it simulates: data and marker tapes follow our work and output heads, and the overshoot counter sits h - (|x| + 1) cells right of position 0 when our input head is at h. The rewind phase only walks the output copy back to cell 0 and then to cell 1. So when every reachable configuration of tm obeys Cfg.WithinDecisionSpace with bound S, every CSLib head stays in the interval [0, S + 1], and the simulator uses at most (2n + 3) (S + 2) cells (TM.toMultiTape_computesFun_space).

def Complexity.MultiTape.PosBound {k : ℕ} {S : Type u_1} {Q : Type u_2} {input : List S} (B : ℕ) (d : Turing.Cfg k S Q input) : Prop

All work heads of d lie in the interval [0, B].

Equations

• Complexity.MultiTape.PosBound B d = ∀ (i : Fin k), 0 ≤ d.workTapePos i ∧ d.workTapePos i ≤ ↑B

theorem Complexity.MultiTape.spaceUsed_le_of_posBound {k : ℕ} {S : Type u_1} {Q : Type u_2} {input : List S} (M : Turing.MultiTapeTM k S Q) (d : Turing.Cfg k S Q input) (t B : ℕ) (h : ∀ m ≤ t, PosBound B (Turing.MultiTapeTM.runFrom d m)) : Turing.MultiTapeTM.spaceUsed d t ≤ k * (B + 1)

If every work head stays in [0, B] for the first t steps, the run uses at most k (B + 1) cells.

theorem Complexity.TM.simIdx_cases {n : ℕ} (i : Fin (simTapes n)) : (∃ (j : Fin (n + 1)), i = dataIdx j) ∨ (∃ (j : Fin (n + 1)), i = markIdx j) ∨ i = overIdx

Every CSLib work tape of the simulator is a data tape, a marker tape, or the overshoot counter.

theorem Complexity.TM.simTape_head_le {n : ℕ} {tm : TM n} {c : Cfg n tm.Q} {N s : ℕ} (hc : c.WithinDecisionSpace N s) (j : Fin (n + 1)) : (simTape c j).head ≤ s + 1

Within the decision-space bound s, every simulated read-write head is at most at s + 1.

theorem Complexity.TM.MultiTapeSim.posBound {n : ℕ} {tm : TM n} {x : List Bool} {c : Cfg n tm.Q} {z : InputZone} {d : tm.SimCfg x} (h : tm.MultiTapeSim x c z d) {s : ℕ} (hc : c.WithinDecisionSpace x.length s) : MultiTape.PosBound (s + 1) d

A simulated configuration within the decision-space bound s keeps every CSLib head in [0, s + 1].

theorem Complexity.TM.MultiTapeSim.reachesIn_prefix {n : ℕ} {tm : TM n} {x : List Bool} {t : ℕ} {c c' : Cfg n tm.Q} (hreach : tm.reachesIn t c c') {z : InputZone} {d : tm.SimCfg x} (h : tm.MultiTapeSim x c z d) (j : ℕ) : j ≤ t → ∃ (cj : Cfg n tm.Q) (z' : InputZone), tm.reachesIn j c cj ∧ tm.MultiTapeSim x cj z' (Turing.MultiTapeTM.runFrom d j)

Every prefix of a run of our machine is simulated by the same prefix of the simulator's run.

theorem Complexity.TM.MultiTapeSim.halt_workTapePos {n : ℕ} {tm : TM n} {x : List Bool} {c : Cfg n tm.Q} {z : InputZone} {d : tm.SimCfg x} (h : tm.MultiTapeSim x c z d) (hc : c.state = tm.qhalt) : (Turing.MultiTapeTM.step d).workTapePos = d.workTapePos

The step leaving the simulation phase moves no head.

theorem Complexity.TM.AtVerdict.workTapePos_step {n : ℕ} {tm : TM n} {x : List Bool} {t : Tape} {d : tm.SimCfg x} (h : tm.AtVerdict x t d) : (Turing.MultiTapeTM.step d).workTapePos = d.workTapePos

The verdict step moves no head.

theorem Complexity.TM.Rewinding.posBound_step {n : ℕ} {tm : TM n} {x : List Bool} {t : Tape} {d : tm.SimCfg x} {B : ℕ} (h : tm.Rewinding x t d) (hb : MultiTape.PosBound B d) (hB : 1 ≤ B) : MultiTape.PosBound B (Turing.MultiTapeTM.step d)

A rewind step keeps every CSLib head in [0, B] when 1 ≤ B.

theorem Complexity.TM.Rewinding.posBound_run {n : ℕ} {tm : TM n} {x : List Bool} {B : ℕ} (hB : 1 ≤ B) (m : ℕ) {t : Tape} {d : tm.SimCfg x} : tm.Rewinding x t d → t.head = m → MultiTape.PosBound B d → ∀ s ≤ m + 2, MultiTape.PosBound B (Turing.MultiTapeTM.runFrom d s)

The whole rewind phase from output-head position m keeps every CSLib head in [0, B] when 1 ≤ B.

theorem Complexity.TM.toMultiTape_computesFun_space {n : ℕ} (tm : TM n) {L : Language} {T S : ℕ → ℕ} (hdec : tm.DecidesInTimeSpace L T S) : tm.toMultiTape.ComputesFunInTimeAndSpace (Function.Embedding.refl (List Bool)) verdictEmb (Turing.MultiTapeTM.indicator L) (fun (x : List Bool) => 2 * T x.length + 4) fun (x : List Bool) => simTapes n * (S x.length + 2)

The simulator decides what tm decides, space-faithfully. If tm decides L within time T and space S, the simulator decides L within time 2 T + 4 and space (2n + 3) (S + 2).