P is CSLib polynomial time #
Combining both directions of the multi-tape bridge: a language is in P
exactly when a CSLib multi-tape machine decides it within polynomial time and
space in the input length.
Main results #
theorem
Complexity.mem_P_iff_decidableInTimeAndSpace
{L : Language}
:
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 is exactly CSLib polynomial time. A language is in P if and only
if some CSLib multi-tape machine decides it within polynomial time and space
in the input length.