The class parity-P

⊕P is the parity operator applied to P (Cslib.Complexity.ParityP) Papadimitriou and Zachos, Arora and Barak, Section 17.4: L ∈ ⊕P when, for a polynomial p and a function V : α × List Bool → Bool computable in polynomial time on inputs encPair enc encBits (a, w) = frame (enc a) ++ w, a ∈ L exactly when an odd number of the strings w of length p (enc a).length have V (a, w) = true (Cslib.Complexity.mem_ParityP). Equivalently, L consists of the instances where some function in #P is odd (Cslib.Complexity.mem_ParityP_iff_exists_SharpP).

⊕P is closed under complement (Cslib.Complexity.compl_mem_ParityP): the verifier Cslib.Complexity.succVerifier V accepts the string of falses and the strings true :: w with V (a, w) = true, so it accepts exactly one string more than V, one bit longer (Cslib.Complexity.acceptCount_succVerifier), by counting words by their first bit (Cslib.BitString.card_filter_ofFn_succ).

Main definitions

• Cslib.Complexity.ParityP: the class ⊕P.
• Cslib.Complexity.succTest, Cslib.Complexity.succVerifier: a word test and a verifier accepting one more string.

Main results

• Cslib.Complexity.acceptCount_succVerifier, Cslib.Complexity.acceptCount_succTest: one more accepted string.
• Cslib.Complexity.mem_ParityP, Cslib.Complexity.mem_ParityP_iff_exists_SharpP: ⊕P through verifiers and through #P.
• Cslib.Complexity.P_subset_ParityP, Cslib.Complexity.compl_mem_ParityP.

References

• C. H. Papadimitriou, S. Zachos, Two remarks on the power of counting
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

Counting accepted strings

def Cslib.Complexity.succTest (g : List Bool → Bool) (w : List Bool) : Bool

The word test accepting one word more than g, one bit longer: the word of falses, and true :: w for every word w accepted by g.

def Cslib.Complexity.succVerifier {α : Type} (V : α × List Bool → Bool) (x : α × List Bool) : Bool

The verifier accepting one string more than V, one bit longer: the string of falses, and true :: w for every w with V (a, w) = true.

theorem Cslib.Complexity.acceptCount_succVerifier {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : acceptCount (succVerifier V) a (n + 1) = acceptCount V a n + 1

One more accepted string: succVerifier V accepts exactly one string of length n + 1 more than V accepts strings of length n.

theorem Cslib.Complexity.acceptCount_succTest {α : Type} (g : List Bool → Bool) (a : α) (n : ℕ) : acceptCount (fun (x : α × List Bool) => succTest g x.2) a (n + 1) = acceptCount (fun (x : α × List Bool) => g x.2) a n + 1

One more accepted word: succTest g accepts exactly one word of length n + 1 more than g accepts words of length n.

theorem Cslib.Complexity.odd_acceptCount_succVerifier_iff {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : Odd (acceptCount (succVerifier V) a (n + 1)) ↔ ¬Odd (acceptCount V a n)

The parity of one more accepted string is the opposite parity.

theorem Cslib.Complexity.computableInPolyTime_succTest {γ : Type} {input : γ ↪ List Bool} {g : γ → List Bool → Bool} {w : γ → List Bool} (hg : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : γ × List Bool) => g p.1 p.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hw : Turing.MultiTapeTM.ComputableInPolyTime w input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => succTest (g x) (w x)) input Turing.MultiTapeTM.encBool

succTest is polynomial-time, with a test that may use the input.

theorem Cslib.Complexity.computableInPolyTime_succVerifier {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (succVerifier V) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

succVerifier V is polynomial-time when V is.

The class

def Cslib.Complexity.ParityP {α : Type} (enc : α ↪ List Bool) : Set (Set α)

The class ⊕P: the parity operator applied to P. A problem L is in ⊕P when, for a polynomial p and a polynomial-time V, a ∈ L exactly when an odd number of the strings w of length p (enc a).length have V (a, w) = true (mem_ParityP) Papadimitriou and Zachos, Arora and Barak, Section 17.4.

theorem Cslib.Complexity.mem_ParityP {α : Type} {enc : α ↪ List Bool} {L : Set α} : L ∈ ParityP enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ ∀ (a : α), a ∈ L ↔ Odd (acceptCount V a (Polynomial.eval (enc a).length p))

⊕P through verifiers.

theorem Cslib.Complexity.mem_ParityP_iff_exists_SharpP {α : Type} {enc : α ↪ List Bool} {L : Set α} : L ∈ ParityP enc ↔ ∃ f ∈ SharpP enc, ∀ (a : α), a ∈ L ↔ Odd (f a)

⊕P through #P: a problem is in ⊕P exactly when it is the set of instances where some function in #P is odd.

theorem Cslib.Complexity.compl_mem_ParityP {α : Type} {enc : α ↪ List Bool} {L : Set α} (hL : L ∈ ParityP enc) : Lᶜ ∈ ParityP enc

⊕P is closed under complement: succVerifier accepts one more string.

theorem Cslib.Complexity.P_subset_ParityP {α : Type} {enc : α ↪ List Bool} : P enc ⊆ ParityP enc

P ⊆ ⊕P: a decider accepts the empty string or nothing.