Languages in P are those with a polynomial-time verdict function

mem_P_of_decisionFn_bool puts a language in P given a one-bit verdict function in FP. The converse, exists_decisionFn_of_mem_P, runs a polynomial-time decider inside Cobham's algebra (Complexitylib.Classes.Containments.Internal.PVerdict). Together they characterize P.

Main results

• mem_P_iff_exists_decisionFn — L ∈ P iff a one-bit verdict function in FP decides L

theorem Complexity.mem_P_iff_exists_decisionFn {L : Language} : L ∈ P ↔ ∃ (g : List Bool → Bool), (fun (x : List Bool) => [g x]) ∈ FP ∧ ∀ (x : List Bool), x ∈ L ↔ g x = true

P is characterized by one-bit verdict functions. A language is in P exactly when some Boolean function g, with x ↦ [g x] computable in polynomial time, satisfies x ∈ L ↔ g x = true for every x. The forward direction is exists_decisionFn_of_mem_P; the reverse is mem_P_of_decisionFn_bool.