Polynomial-time functions and tests in counting classes

Binary-encoded natural outputs of polynomial-time functions are in #P; binary-encoded integer outputs are in GapP Fortnow, Theorem 3.5. The verifier guesses a fixed-width binary word and accepts just those representing values below the computed output. The witness width bounds the binary output length, not its potentially exponential numeric value.

Polynomial-time Boolean control also permits selection between two counting functions. The control certificate is separate from the branches' counting-class membership.

Main results

• mem_SharpP_of_polyTime: polynomial-time binary natural functions are in #P.
• mem_GapP_of_polyTime: polynomial-time binary integer functions are in GapP.
• SharpP.ite_mem, GapP.ite_mem: selection by a polynomial-time Boolean test.

References

• L. Fortnow, Counting Complexity, Theorem 3.5.

theorem Cslib.Complexity.mem_SharpP_of_polyTime {α : Type} {enc : α ↪ List Bool} {f : α → ℕ} (hf : Turing.MultiTapeTM.ComputableInPolyTime f enc Turing.MultiTapeTM.encNat) : f ∈ SharpP enc

A polynomial-time function with binary natural output is a #P function.

theorem Cslib.Complexity.mem_GapP_of_polyTime {α : Type} {enc : α ↪ List Bool} {f : α → ℤ} (hf : Turing.MultiTapeTM.ComputableInPolyTime f enc Turing.MultiTapeTM.encIntBin) : f ∈ GapP enc

A polynomial-time function with binary integer output is a GapP function.

theorem Cslib.Complexity.SharpP.ite_mem {α : Type} {enc : α ↪ List Bool} {c : α → Bool} {f g : α → ℕ} (hc : Turing.MultiTapeTM.ComputableInPolyTime c enc Turing.MultiTapeTM.encBool) (hf : f ∈ SharpP enc) (hg : g ∈ SharpP enc) : (fun (a : α) => if c a = true then f a else g a) ∈ SharpP enc

A polynomial-time Boolean test may select between two #P functions on the same input. Its two Boolean masks are polynomial-time functions; multiplication and addition select the corresponding count exactly.

theorem Cslib.Complexity.GapP.ite_mem {α : Type} {enc : α ↪ List Bool} {c : α → Bool} {f g : α → ℤ} (hc : Turing.MultiTapeTM.ComputableInPolyTime c enc Turing.MultiTapeTM.encBool) (hf : f ∈ GapP enc) (hg : g ∈ GapP enc) : (fun (a : α) => if c a = true then f a else g a) ∈ GapP enc

A polynomial-time Boolean test may select between two GapP functions on the same input. Apply #P selection to the positive and negative counting functions of each branch.