P and FP agree with 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.
Likewise a string function belongs to FP exactly when a CSLib multi-tape
machine computes it within polynomial time and space, using identity encodings.
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.
theorem
Complexity.mem_FP_iff_computableInTimeAndSpace
{f : List Bool → List Bool}
:
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
Canonical FP is exactly CSLib polynomial-time computation of complete binary strings.