Polynomial-time normal forms

P and FP membership can be witnessed by deterministic machines whose running-time bounds are evaluations of polynomials with natural coefficients. Unlike the arbitrary asymptotic witnesses in the class definitions, these normalized bounds are valid on every input length and are monotone.

Main result

• mem_P_iff_decidesInTime_polynomial — polynomial-evaluation normal form for P
• mem_FP_iff_computesInTime_polynomial — polynomial-evaluation normal form for FP

theorem Complexity.mem_P_iff_decidesInTime_polynomial {L : Language} : L ∈ P ↔ ∃ (k : ℕ) (tm : TM k) (p : Polynomial ℕ), tm.DecidesInTime L fun (x : ℕ) => Polynomial.eval x p

A language belongs to P exactly when some deterministic machine decides it within the evaluation of a natural-coefficient polynomial.

theorem Complexity.mem_FP_iff_computesInTime_polynomial {f : List Bool → List Bool} : f ∈ FP ↔ ∃ (k : ℕ) (tm : TM k) (p : Polynomial ℕ), tm.ComputesInTime f fun (x : ℕ) => Polynomial.eval x p

A function belongs to FP exactly when some deterministic machine computes it within the evaluation of a natural-coefficient polynomial.