Complexitylib time classes on CSLib multi-tape machines

CSLib measures the complexity of a language through its multi-tape machines (Turing.MultiTapeTM): MultiTapeTM.DecidableInTimeAndSpace L enc t s says that some machine over the binary alphabet with finitely many states decides L within time t x and space s x on every input x, emitting the single bit true on inputs in L and false otherwise. Space counts the work cells its heads visit. Our languages are sets of binary strings, so they are passed to CSLib with the identity encoding.

This file shows that our deterministic time classes run on those machines with a constant-factor overhead. The simulator TM.toMultiTape (Complexitylib.Interop.Cslib.MultiTape.Defs) executes a machine tm : TM n step for step on 2n + 3 CSLib work tapes and then reads off the verdict.

Main results

• Complexity.TM.DecidesInTime.decidableInTimeAndSpace — a decider within time f yields a CSLib decider within time and space (2n + 3) (2 f + 5)
• Complexity.decidableInTimeAndSpace_of_mem_DTIME — DTIME(T) languages are CSLib-decidable within time and space O(T)
• Complexity.decidableInTimeAndSpace_of_mem_P — P languages are CSLib-decidable within polynomial time and space
• Complexity.TM.DecidesInTimeSpace.decidableInTimeAndSpace — a decider within time T and space S yields a CSLib decider within time 2 T + 4 and space (2n + 3) (S + 2)
• Complexity.decidableInTimeAndSpace_of_mem_DTISP — DTISP(T, S) languages are CSLib-decidable within time O(T) and space O(S + 1)
• Complexity.TM.ComputesInTime.computableInTimeAndSpace — a machine computing f within time T yields a CSLib machine computing f within time 3 T + 4 and space (2n + 3) (3 T + 5)
• Complexity.computableInTimeAndSpace_of_mem_FP — FP functions are CSLib-computable within polynomial time and space

The converse is Complexitylib.Interop.Cslib.FromMultiTape, and together the two directions give mem_P_iff_decidableInTimeAndSpace.

theorem Complexity.TM.DecidesInTime.decidableInTimeAndSpace {n : ℕ} {tm : TM n} {L : Language} {f : ℕ → ℕ} (h : tm.DecidesInTime L f) : Turing.MultiTapeTM.DecidableInTimeAndSpace L (Function.Embedding.refl (List Bool)) (fun (x : List Bool) => (2 * n + 3) * (2 * f x.length + 5)) fun (x : List Bool) => (2 * n + 3) * (2 * f x.length + 5)

A Complexitylib decider runs on CSLib. If tm decides L within time f, a CSLib multi-tape machine decides L within time and space (2n + 3) (2 f + 5).

theorem Complexity.decidableInTimeAndSpace_of_mem_DTIME {L : Language} {T : ℕ → ℕ} (hL : L ∈ DTIME T) : ∃ (t : ℕ → ℕ), BigO t T ∧ Turing.MultiTapeTM.DecidableInTimeAndSpace L (Function.Embedding.refl (List Bool)) (fun (x : List Bool) => t x.length) fun (x : List Bool) => t x.length

DTIME transfers to CSLib. Every language in DTIME(T) is decided by a CSLib multi-tape machine within time and space O(T) in the input length.

theorem Complexity.decidableInTimeAndSpace_of_mem_P {L : Language} (hL : L ∈ P) : ∃ (p : Polynomial ℕ), Turing.MultiTapeTM.DecidableInTimeAndSpace L (Function.Embedding.refl (List Bool)) (fun (x : List Bool) => Polynomial.eval x.length p) fun (x : List Bool) => Polynomial.eval x.length p

P transfers to CSLib. Every language in P is decided by a CSLib multi-tape machine within polynomial time and space in the input length.

theorem Complexity.TM.DecidesInTimeSpace.decidableInTimeAndSpace {n : ℕ} {tm : TM n} {L : Language} {T S : ℕ → ℕ} (h : tm.DecidesInTimeSpace L T S) : Turing.MultiTapeTM.DecidableInTimeAndSpace L (Function.Embedding.refl (List Bool)) (fun (x : List Bool) => 2 * T x.length + 4) fun (x : List Bool) => (2 * n + 3) * (S x.length + 2)

A space-bounded Complexitylib decider runs on CSLib in the same space. If tm decides L within time T and space S (TM.DecidesInTimeSpace), a CSLib multi-tape machine decides L within time 2 T + 4 and space (2n + 3) (S + 2).

theorem Complexity.decidableInTimeAndSpace_of_mem_DTISP {L : Language} {T S : ℕ → ℕ} (hL : L ∈ DTISP T S) : ∃ (t : ℕ → ℕ) (s : ℕ → ℕ), BigO t T ∧ (BigO s fun (m : ℕ) => S m + 1) ∧ Turing.MultiTapeTM.DecidableInTimeAndSpace L (Function.Embedding.refl (List Bool)) (fun (x : List Bool) => t x.length) fun (x : List Bool) => s x.length

DTISP transfers to CSLib. Every language in DTISP(T, S) is decided by a CSLib multi-tape machine within time O(T) and space O(S + 1) in the input length.

theorem Complexity.TM.ComputesInTime.computableInTimeAndSpace {n : ℕ} {tm : TM n} {f : List Bool → List Bool} {T : ℕ → ℕ} (h : tm.ComputesInTime f T) : Turing.MultiTapeTM.ComputableInTimeAndSpace f (Function.Embedding.refl (List Bool)) (Function.Embedding.refl (List Bool)) (fun (x : List Bool) => 3 * T x.length + 4) fun (x : List Bool) => (2 * n + 3) * (3 * T x.length + 5)

A Complexitylib function computation runs on CSLib. If tm computes f within time T, a CSLib multi-tape machine computes f (with identity encodings) within time 3 T + 4 and space (2n + 3) (3 T + 5).

theorem Complexity.computableInTimeAndSpace_of_mem_FP {f : List Bool → List Bool} (hf : f ∈ FP) : ∃ (p : Polynomial ℕ), Turing.MultiTapeTM.ComputableInTimeAndSpace f (Function.Embedding.refl (List Bool)) (Function.Embedding.refl (List Bool)) (fun (x : List Bool) => Polynomial.eval x.length p) fun (x : List Bool) => Polynomial.eval x.length p

FP transfers to CSLib. Every function in FP is computed by a CSLib multi-tape machine within polynomial time and space in the input length.