Wide and length-dependent counting gaps

WPP allows a GapP function to take either zero or a nonzero polynomial-time computable integer target; LWPP restricts that target to depend on input length. We follow Hemaspaandra et al., Definitions 2.4–2.5, crediting the original Fenner–Fortnow–Kurtz definitions. Targets use binary integers encIntBin; the length argument of LWPP uses unary encUnary, so an exponentially large numeric target is permitted. These are verifier-based counting classes, without a proved nondeterministic-machine characterization.

In addition to the basic containments (SPP ⊆ LWPP ⊆ WPP, UP ⊆ FewP ⊆ LWPP ⊆ WPP, and WPP ⊆ C=P ∩ coC=P) and Boolean closures (complement, intersection, union, difference, and symmetric difference), we prove two robustness properties from Hemaspaandra et al., Section 3:

• Finite multiple-target robustness (mem_WPP_of_finset_targets, mem_LWPP_of_finset_targets): if a GapP function takes 0 on nonmembers and one of a fixed finite family of nonzero polynomial-time targets on members, then interpolating the product ∏ i ∈ s, f i - ∏ i ∈ s, (f i - g) collapses the accepting targets to the single nonzero product ∏ i ∈ s, f i.
• Polynomial-time unary-indexed target normalization and reduction closure (mem_LWPP_of_polyTime_index, PolyTimeReducible.mem_LWPP): if the target is f (k a) for a unary-computable index k : α → ℕ (such as the encoded output length of a polynomial-time many-one reduction), multiplying the gap by the product of f i over all i ≤ p(|a|) with i ≠ k a normalizes the target to ∏_{i ≤ p(|a|)} f i, which depends only on the input length.

Full polynomial-family multiple-target robustness (Poly-LWPP = LWPP and Poly-WPP = WPP), with no computability assumption on the accepting index, is proved in WPP.Robustness. Oracle lowness of SPP, LWPP, and WPP (including fixed-target LWPPWithFixedTarget and WPPWithFixedTarget lowness with unrelativized FP targets) is proved in WPP.Lowness.

Main definitions

• WPP: an input-dependent nonzero FP target.
• LWPP: a nonzero FP target depending only on encoded input length.

Main results

• mem_WPP, mem_LWPP: membership through a polynomial-time target.
• SPP_subset_LWPP, LWPP_subset_WPP, UP_subset_LWPP, UP_subset_WPP, coUP_subset_LWPP, coUP_subset_WPP, FewP_subset_LWPP, FewP_subset_WPP, WPP_subset_CeqP, WPP_subset_coCeqP.
• compl_mem_WPP, inter_mem_WPP, union_mem_WPP, diff_mem_WPP, symmDiff_mem_WPP: Boolean closure of WPP.
• compl_mem_LWPP, inter_mem_LWPP, union_mem_LWPP, diff_mem_LWPP, symmDiff_mem_LWPP: length-dependent Boolean closure of LWPP.
• mem_WPP_of_finset_targets, mem_LWPP_of_finset_targets: finite multiple-target robustness.
• mem_LWPP_of_polyTime_index: normalization of a polynomial-time unary-indexed target to a length-dependent target.
• PolyTimeReducible.mem_WPP, PolyTimeReducible.mem_LWPP: polynomial-time many-one reduction closure.

References

• S. Fenner, L. Fortnow, S. Kurtz, Gap-definable counting classes
• E. Hemaspaandra et al., The Robustness of LWPP and WPP, with an Application to Graph Reconstruction

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

Wide gaps: zero on nonmembers and a nonzero binary FP target on members Fenner, Fortnow and Kurtz.

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

Wide gaps with a target computed in polynomial time from unary input length Fenner, Fortnow and Kurtz.

theorem Cslib.Complexity.mem_WPP {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ WPP enc ↔ ∃ g ∈ GapP enc, ∃ (f : α → ℤ), Turing.MultiTapeTM.ComputableInPolyTime f enc Turing.MultiTapeTM.encIntBin ∧ (∀ (a : α), f a ≠ 0) ∧ (∀ (a : α), g a = 0 ∨ g a = f a) ∧ ∀ (a : α), a ∈ A ↔ g a = f a

theorem Cslib.Complexity.mem_LWPP {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ LWPP enc ↔ ∃ g ∈ GapP enc, ∃ (f : ℕ → ℤ), Turing.MultiTapeTM.ComputableInPolyTime f Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encIntBin ∧ (∀ (n : ℕ), f n ≠ 0) ∧ (∀ (a : α), g a = 0 ∨ g a = f (enc a).length) ∧ ∀ (a : α), a ∈ A ↔ g a = f (enc a).length

theorem Cslib.Complexity.SPP_subset_LWPP {α : Type} {enc : α ↪ List Bool} : SPP enc ⊆ LWPP enc

The constant target one witnesses the SPP containment.

theorem Cslib.Complexity.LWPP_subset_WPP {α : Type} {enc : α ↪ List Bool} : LWPP enc ⊆ WPP enc

Computing the encoded input length turns an LWPP target into a WPP target.

theorem Cslib.Complexity.UP_subset_LWPP {α : Type} {enc : α ↪ List Bool} : UP enc ⊆ LWPP enc

Unambiguous polynomial time is contained in LWPP via SPP.

theorem Cslib.Complexity.UP_subset_WPP {α : Type} {enc : α ↪ List Bool} : UP enc ⊆ WPP enc

Unambiguous polynomial time is contained in WPP.

theorem Cslib.Complexity.coUP_subset_LWPP {α : Type} {enc : α ↪ List Bool} : coUP enc ⊆ LWPP enc

coUP is contained in LWPP via SPP.

theorem Cslib.Complexity.coUP_subset_WPP {α : Type} {enc : α ↪ List Bool} : coUP enc ⊆ WPP enc

coUP is contained in WPP.

theorem Cslib.Complexity.FewP_subset_LWPP {α : Type} {enc : α ↪ List Bool} : FewP enc ⊆ LWPP enc

Polynomially bounded ambiguity FewP is contained in LWPP via FewP ⊆ SPP.

theorem Cslib.Complexity.FewP_subset_WPP {α : Type} {enc : α ↪ List Bool} : FewP enc ⊆ WPP enc

Polynomially bounded ambiguity FewP is contained in WPP.

theorem Cslib.Complexity.WPP_subset_CeqP {α : Type} {enc : α ↪ List Bool} : WPP enc ⊆ CeqP enc

Subtraction of the target gives a zero test for WPP membership.

theorem Cslib.Complexity.WPP_subset_coCeqP {α : Type} {enc : α ↪ List Bool} : WPP enc ⊆ coCeqP enc

A WPP gap is nonzero exactly on members.

theorem Cslib.Complexity.compl_mem_WPP {α : Type} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ WPP enc) : Aᶜ ∈ WPP enc

Complement exchanges the zero and target values.

theorem Cslib.Complexity.inter_mem_WPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ WPP enc) (hB : B ∈ WPP enc) : A ∩ B ∈ WPP enc

Products preserve the zero-or-target condition and the target is still nonzero.

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

WPP as a Boolean subalgebra of Set α.

@[simp]

theorem Cslib.Complexity.WPP.coe_booleanSubalgebra {α : Type} {enc : α ↪ List Bool} : ↑(booleanSubalgebra enc) = WPP enc

@[simp]

theorem Cslib.Complexity.WPP.mem_booleanSubalgebra {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ booleanSubalgebra enc ↔ A ∈ WPP enc

theorem Cslib.Complexity.union_mem_WPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ WPP enc) (hB : B ∈ WPP enc) : A ∪ B ∈ WPP enc

Union follows by De Morgan's law.

theorem Cslib.Complexity.diff_mem_WPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ WPP enc) (hB : B ∈ WPP enc) : A \ B ∈ WPP enc

WPP is closed under set difference.

theorem Cslib.Complexity.symmDiff_mem_WPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ WPP enc) (hB : B ∈ WPP enc) : symmDiff A B ∈ WPP enc

WPP is closed under symmetric difference.

theorem Cslib.Complexity.PolyTimeReducible.mem_WPP {α β : Type} {enc : α ↪ List Bool} {A : Set α} {encB : β ↪ List Bool} {B : Set β} (h : PolyTimeReducible enc encB A B) (hB : B ∈ WPP encB) : A ∈ WPP enc

Polynomial-time precomposition preserves the target and the exact gap.

theorem Cslib.Complexity.compl_mem_LWPP {α : Type} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ LWPP enc) : Aᶜ ∈ LWPP enc

The complementary gap uses the same length-dependent target.

theorem Cslib.Complexity.inter_mem_LWPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ LWPP enc) (hB : B ∈ LWPP enc) : A ∩ B ∈ LWPP enc

Multiplying length-dependent targets preserves length dependence.

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

LWPP as a Boolean subalgebra of Set α.

@[simp]

theorem Cslib.Complexity.LWPP.coe_booleanSubalgebra {α : Type} {enc : α ↪ List Bool} : ↑(booleanSubalgebra enc) = LWPP enc

@[simp]

theorem Cslib.Complexity.LWPP.mem_booleanSubalgebra {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ booleanSubalgebra enc ↔ A ∈ LWPP enc

theorem Cslib.Complexity.union_mem_LWPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ LWPP enc) (hB : B ∈ LWPP enc) : A ∪ B ∈ LWPP enc

Union preserves length-dependent targets.

theorem Cslib.Complexity.diff_mem_LWPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ LWPP enc) (hB : B ∈ LWPP enc) : A \ B ∈ LWPP enc

LWPP is closed under set difference.

theorem Cslib.Complexity.symmDiff_mem_LWPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ LWPP enc) (hB : B ∈ LWPP enc) : symmDiff A B ∈ LWPP enc

LWPP is closed under symmetric difference.

Finite multiple-target robustness

theorem Cslib.Complexity.mem_WPP_of_finset_targets {α : Type} {enc : α ↪ List Bool} {A : Set α} {ι : Type u_1} (s : Finset ι) {g : α → ℤ} {f : ι → α → ℤ} (hg : g ∈ GapP enc) (hf : ∀ i ∈ s, Turing.MultiTapeTM.ComputableInPolyTime (f i) enc Turing.MultiTapeTM.encIntBin) (hn : ∀ i ∈ s, ∀ (a : α), f i a ≠ 0) (hr : ∀ (a : α), g a = 0 ∨ ∃ i ∈ s, g a = f i a) (hA : ∀ (a : α), a ∈ A ↔ ∃ i ∈ s, g a = f i a) : A ∈ WPP enc

Finite multiple-target robustness for WPP: a GapP function that takes 0 outside A and one of a fixed finite family of nonzero polynomial-time targets on A witnesses A ∈ WPP (the fixed-Finset case of Hemaspaandra et al., Theorem 3.7, whose proof is the product interpolation of their Theorem 3.1).

theorem Cslib.Complexity.mem_LWPP_of_finset_targets {α : Type} {enc : α ↪ List Bool} {A : Set α} {ι : Type u_1} (s : Finset ι) {g : α → ℤ} {f : ι → ℕ → ℤ} (hg : g ∈ GapP enc) (hf : ∀ i ∈ s, Turing.MultiTapeTM.ComputableInPolyTime (f i) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encIntBin) (hn : ∀ i ∈ s, ∀ (n : ℕ), f i n ≠ 0) (hr : ∀ (a : α), g a = 0 ∨ ∃ i ∈ s, g a = f i (enc a).length) (hA : ∀ (a : α), a ∈ A ↔ ∃ i ∈ s, g a = f i (enc a).length) : A ∈ LWPP enc

Finite multiple-target robustness for LWPP: a GapP function that takes 0 outside A and one of a fixed finite family of nonzero length-dependent polynomial-time targets on A witnesses A ∈ LWPP (the fixed-Finset case of the product interpolation in Hemaspaandra et al., Theorem 3.1).

Unary-indexed target normalization and LWPP reduction closure

theorem Cslib.Complexity.mem_LWPP_of_polyTime_index {α : Type} {enc : α ↪ List Bool} {A : Set α} {g : α → ℤ} {f : ℕ → ℤ} {k : α → ℕ} (hg : g ∈ GapP enc) (hf : Turing.MultiTapeTM.ComputableInPolyTime f Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encIntBin) (hn : ∀ (n : ℕ), f n ≠ 0) (hk : Turing.MultiTapeTM.ComputableInPolyTime k enc Turing.MultiTapeTM.encUnary) (hr : ∀ (a : α), g a = 0 ∨ g a = f (k a)) (hA : ∀ (a : α), a ∈ A ↔ g a = f (k a)) : A ∈ LWPP enc

Unary-indexed target normalization for LWPP: if a GapP function takes 0 outside A and f (k a) on A, where f : ℕ → ℤ is a nonzero unary-input polynomial-time target and k : α → ℕ is computable in polynomial time in unary, then multiplying the gap by the FP-computable product of f i over i ≤ p(|a|) with i ≠ k a normalizes the target to depend only on (enc a).length Fenner–Fortnow–Kurtz; Hemaspaandra et al., Section 3.

theorem Cslib.Complexity.PolyTimeReducible.mem_LWPP {α β : Type} {enc : α ↪ List Bool} {A : Set α} {encB : β ↪ List Bool} {B : Set β} (h : PolyTimeReducible enc encB A B) (hB : B ∈ LWPP encB) : A ∈ LWPP enc

Polynomial-time many-one reductions preserve LWPP Fenner–Fortnow–Kurtz; Hemaspaandra et al., Section 3: the target f |r(a)| has unary-computable index k a = |r(a)|, which mem_LWPP_of_polyTime_index normalizes to a function of |a|.