Decision classes defined by counting

The classes of decision problems whose answer is a property of the number of witnesses of an existential second-order sentence – classically, of the number of accepting runs of a nondeterministic polynomial-time machine:

• ⊕P (DescriptiveComplexity.ParityP, Papadimitriou, Zachos 1982, Goldschlager, Parberry 1986): the number is odd;
• Mod_k P (DescriptiveComplexity.ModP k, Cai, Hemachandra 1990): the number is not a multiple of k;
• PP (DescriptiveComplexity.PP, Gill 1977): one number exceeds another – classically, more runs accept than reject;
• C₌P (DescriptiveComplexity.CeqP, Wagner 1986): the two numbers are equal;
• UP (DescriptiveComplexity.UP, Valiant 1976): the number is at most one, and the answer is whether it is one.

Each is DescriptiveComplexity.countClass S R for a side condition S and a relation R on two numbers: a problem is in the class when, on nonempty finite ordered structures, S holds of the two witness counts and the answer is R of them (DescriptiveComplexity.CountDefinable). The witness counts are those of DescriptiveComplexity.SharpPDefinable, read over the ordered expansion; the two-number form is the characterization of these classes by GapP functions, differences of two #P functions (Fenner, Fortnow, Kurtz 1994), which needs no integer-valued problem.

Closure under first-order reductions is the pullback of the two kernels through the interpretation, as for #P (DescriptiveComplexity.CountDefinable.of_orderedReduction); hardness is cofinal, as for every class of the library. A problem of the class is given by two counting problems of #P (DescriptiveComplexity.mem_countClass_of_sharpP), which is how memberships are proved.

Inclusions: UP ⊆ NP, UP ⊆ ⊕P, NP ⊆ PP, coNP ⊆ PP; ⊕P and PP are closed under complement, by adding one witness to a kernel (DescriptiveComplexity.pairKernel with the kernel ⊤ over the block without variables). Whether C₌P is closed under complement is open. The complete problems are in DescriptiveComplexity.Problems.Sat.CountingDecision.

Problems defined by a relation between two witness counts

def DescriptiveComplexity.CountDefinable {L : FirstOrder.Language} [L.IsRelational] (S R : ℕ → ℕ → Prop) (P : DecisionProblem L) : Prop

A decision problem is defined by the relation R between two witness counts under the side condition S if, on nonempty finite ordered structures, the two counts satisfy S and the problem holds exactly when they satisfy R.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.CountDefinable.congr {L : FirstOrder.Language} [L.IsRelational] {S R : ℕ → ℕ → Prop} {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) (hP : CountDefinable S R P) : CountDefinable S R Q

theorem DescriptiveComplexity.CountDefinable.of_orderedReduction {L : FirstOrder.Language} [L.IsRelational] {S R : ℕ → ℕ → Prop} {L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : OrderedFOReduction P Q) (h : CountDefinable S R Q) : CountDefinable S R P

Closure under ordered first-order reductions: both kernels are pulled back through the interpretation, extended with the lexicographic order.

theorem DescriptiveComplexity.CountDefinable.of_foReduction {L : FirstOrder.Language} [L.IsRelational] {S R : ℕ → ℕ → Prop} {L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : FOReduction P Q) (h : CountDefinable S R Q) : CountDefinable S R P

Closure under first-order reductions.

The classes

noncomputable def DescriptiveComplexity.countClass (S R : ℕ → ℕ → Prop) : ComplexityClass

The class of the problems defined by the relation R between two witness counts under the side condition S, with cofinal hardness.

Equations

• DescriptiveComplexity.countClass S R = DescriptiveComplexity.ComplexityClass.ofMem (fun {L₀ : FirstOrder.Language} [L₀.IsRelational] => DescriptiveComplexity.CountDefinable S R) ⋯ ⋯ ⋯

noncomputable def DescriptiveComplexity.ParityP : ComplexityClass

⊕P: the number of witnesses is odd.

Equations

• DescriptiveComplexity.ParityP = DescriptiveComplexity.countClass (fun (x x_1 : ℕ) => True) fun (c x : ℕ) => Odd c

noncomputable def DescriptiveComplexity.ModP (k : ℕ) : ComplexityClass

Mod_k P: the number of witnesses is not a multiple of k.

Equations

• DescriptiveComplexity.ModP k = DescriptiveComplexity.countClass (fun (x x_1 : ℕ) => True) fun (c x : ℕ) => ¬k ∣ c

noncomputable def DescriptiveComplexity.PP : ComplexityClass

PP: the first number of witnesses exceeds the second – classically, more runs accept than reject.

Equations

• DescriptiveComplexity.PP = DescriptiveComplexity.countClass (fun (x x_1 : ℕ) => True) fun (c d : ℕ) => d < c

noncomputable def DescriptiveComplexity.CeqP : ComplexityClass

C₌P: the two numbers of witnesses are equal.

Equations

• DescriptiveComplexity.CeqP = DescriptiveComplexity.countClass (fun (x x_1 : ℕ) => True) fun (c d : ℕ) => c = d

noncomputable def DescriptiveComplexity.UP : ComplexityClass

UP: at most one witness, and the answer is whether there is one. No complete problem is known for it, and the question does not relativize (Hartmanis, Hemachandra 1988); the class is here for its inclusions.

Equations

• DescriptiveComplexity.UP = DescriptiveComplexity.countClass (fun (c x : ℕ) => c ≤ 1) fun (c x : ℕ) => c = 1

theorem DescriptiveComplexity.mem_countClass_of_sharpP {L : FirstOrder.Language} [L.IsRelational] {S R : ℕ → ℕ → Prop} {C D : CountingProblem L} (hC : SharpP.Mem C) (hD : SharpP.Mem D) {P : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A] [Nonempty A], S (C.Count A) (D.Count A) ∧ (P.Holds A ↔ R (C.Count A) (D.Count A))) : (countClass S R).Mem P

A problem of the class, from two counting problems of #P. Registered in the Lax archive as Lax175070.CountClassMembership.mem_countClass_of_sharpP.

Inclusions needing no arithmetic on the kernels

theorem DescriptiveComplexity.UP_subset_parityP : UP ⊆ ParityP

UP ⊆ ⊕P: at most one witness, and one is an odd number of them. Registered in the Lax archive as Lax175070.CountClassInclusions.UP_subset_parityP.

theorem DescriptiveComplexity.UP_subset_NP : UP ⊆ NP

UP ⊆ NP: a problem with at most one witness is a problem with a witness, and the order the kernel reads is re-quantified. Registered in the Lax archive as Lax175070.CountClassInclusions.UP_subset_NP.

theorem DescriptiveComplexity.NP_subset_PP : NP ⊆ PP

NP ⊆ PP: a problem with a witness has more witnesses than the kernel ⊥ has, namely none. Registered in the Lax archive as Lax175070.CountClassInclusions.NP_subset_PP.

theorem DescriptiveComplexity.compl_mem_parityP {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : ParityP.Mem P) : ParityP.Mem Pᶜ

⊕P is closed under complement: a number is even exactly when its successor is odd. Registered in the Lax archive as Lax175070.CountClassComplements.compl_mem_parityP.

theorem DescriptiveComplexity.compl_mem_PP {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : PP.Mem P) : PP.Mem Pᶜ

PP is closed under complement: ¬ (d < c) is c < d + 1, with the counts swapped. Registered in the Lax archive as Lax175070.CountClassComplements.compl_mem_PP.

theorem DescriptiveComplexity.coNP_subset_PP : coNP ⊆ PP

coNP ⊆ PP. Registered in the Lax archive as Lax175070.CountClassInclusions.coNP_subset_PP.