Computing functions on CSLib multi-tape machines

A decider only constrains output cell 1, so the decision simulator TM.toMultiTape emits that single cell. To compute a function, the simulator TM.toMultiTapeFun shares its marking, simulation, and rewind phases, but its final phase copies output cells 1, 2, … to CSLib's output until the first blank cell. Since both machines agree away from that final state, every lemma about the shared phases transfers (TM.runFrom_toMultiTapeFun).

Main results

• Complexity.TM.toMultiTapeFun_computesFun — if tm computes f within time T, the simulator computes f within time 3 T + 4 and space (2n + 3) (3 T + 5)

theorem Complexity.TM.toMultiTapeFun_step_eq {n : ℕ} {tm : TM n} {x : List Bool} {d : tm.SimCfg x} (h : d.state ≠ some MultiTapeState.verdict) : Turing.MultiTapeTM.step d = Turing.MultiTapeTM.step d

Away from the final state, the two simulators take the same step.

theorem Complexity.TM.runFrom_toMultiTapeFun {n : ℕ} {tm : TM n} {x : List Bool} (d : tm.SimCfg x) (m : ℕ) (h : ∀ j < m, (Turing.MultiTapeTM.runFrom d j).state ≠ some MultiTapeState.verdict) : Turing.MultiTapeTM.runFrom d m = Turing.MultiTapeTM.runFrom d m

Runs that avoid the final state agree on the two simulators.

theorem Complexity.TM.Rewinding.toVerdict {n : ℕ} {tm : TM n} {x : List Bool} (m : ℕ) {t : Tape} {d : tm.SimCfg x} : tm.Rewinding x t d → t.head = m → (∀ s ≤ m, (Turing.MultiTapeTM.runFrom d s).state = some MultiTapeState.rewind) ∧ ∃ (t' : Tape), t'.cells = t.cells ∧ tm.AtVerdict x t' (Turing.MultiTapeTM.runFrom d (m + 1))

The rewind phase from output-head position m stays in the rewind state for m + 1 configurations and then reaches the final state.

structure Complexity.TM.Dumping {n : ℕ} (tm : TM n) (x : List Bool) (t : Tape) (pre : List Bool) (d : tm.SimCfg x) : Prop

The function simulator is copying its simulated output tape t to CSLib's output, having emitted pre so far.

• state : d.state = some MultiTapeState.verdict
• out : TapeSim t (d.workTapePos (dataIdx (Fin.last n))) (d.workTapePos (markIdx (Fin.last n))) (d.workTapes (dataIdx (Fin.last n))) (d.workTapes (markIdx (Fin.last n)))
• head : 1 ≤ t.head
• output : d.output = pre

theorem Complexity.TM.Dumping.ofCell {n : ℕ} {tm : TM n} {x : List Bool} {t : Tape} {pre : List Bool} {d : tm.SimCfg x} (h : tm.Dumping x t pre d) : Γ.ofCell (Turing.Cfg.workTapeSymbols d (dataIdx (Fin.last n))) = t.cells t.head

The data cell under the simulated output head holds the output cell there.

theorem Complexity.TM.Dumping.step_some {n : ℕ} {tm : TM n} {x : List Bool} {t : Tape} {pre : List Bool} {d : tm.SimCfg x} (h : tm.Dumping x t pre d) {b : Bool} (hb : t.cells t.head = Γ.ofBool b) : tm.Dumping x (t.move Dir3.right) (pre ++ [b]) (Turing.MultiTapeTM.step d)

Copying a non-blank output cell.

theorem Complexity.TM.Dumping.step_none {n : ℕ} {tm : TM n} {x : List Bool} {t : Tape} {pre : List Bool} {d : tm.SimCfg x} (h : tm.Dumping x t pre d) (hb : t.cells t.head = Γ.blank) : (Turing.MultiTapeTM.step d).state = none ∧ (Turing.MultiTapeTM.step d).output = pre

Halting at the first blank output cell.

theorem Complexity.TM.Dumping.run {n : ℕ} {tm : TM n} {x : List Bool} (y : List Bool) {t : Tape} {pre : List Bool} {d : tm.SimCfg x} : tm.Dumping x t pre d → (∀ (i : ℕ) (hi : i < y.length), t.cells (t.head + i) = Γ.ofBool y[i]) → t.cells (t.head + y.length) = Γ.blank → (Turing.MultiTapeTM.runFrom d (y.length + 1)).state = none ∧ (Turing.MultiTapeTM.runFrom d (y.length + 1)).output = pre ++ y

The copy phase emits the output string y found from the head onward and halts after |y| + 1 steps.

theorem Complexity.TM.toMultiTapeFun_computesFun {n : ℕ} (tm : TM n) {f : List Bool → List Bool} {T : ℕ → ℕ} (hf : tm.ComputesInTime f T) : tm.toMultiTapeFun.ComputesFunInTimeAndSpace (Function.Embedding.refl (List Bool)) (Function.Embedding.refl (List Bool)) f (fun (x : List Bool) => 3 * T x.length + 4) fun (x : List Bool) => simTapes n * (3 * T x.length + 5)

The function simulator computes what tm computes, within time 3 T + 4 and space (2n + 3) (3 T + 5) when tm computes within time T.