From a polynomial-time decision function to membership in P

A language whose verdict is computed by a polynomial-time function is in P. This is the bridge that lets a development establish membership in P by exhibiting a function — in particular by building one in Cobham's algebra, where Complexitylib.Classes.P.Cobham supplies CobhamFP_eq_FP — instead of constructing a decider machine by hand.

The proof reads the verdict off the output through the polynomial-time language Language.containsOne: a verdict string is accepted exactly when it contains a 1, and P is closed under polynomial-time preimages.

Main results

• mem_P_of_decisionFn — a verdict function in FP puts its language in P
• mem_P_of_decisionFn_bool — the same with a Bool-valued verdict

theorem Complexity.mem_P_of_decisionFn {f : List Bool → List Bool} {L : Language} (hf : f ∈ FP) (hL : ∀ (x : List Bool), x ∈ L ↔ ∃ b ∈ f x, b = true) : L ∈ P

A polynomial-time verdict function decides a polynomial-time language. If f ∈ FP and x ∈ L exactly when f x contains a 1-bit, then L ∈ P.

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

The Bool-valued form: a polynomial-time function that emits the verdict as a one-bit string decides its language.