One-call counting reductions, and the one-call closure of a counting class

A parsimonious reduction preserves the number of solutions, hence also whether there is one: no problem with an easy decision version is parsimoniously #P-hard unless P = NP (DescriptiveComplexity.NP_subset_PTIME_of_sharpP_parsimoniousHard). The classical #P-complete problems of that kind – counting the models of a DNF formula, the independent sets of a graph – are complete under a weaker notion, defined here.

A one-call reduction C ≤ᶜ[≤] D is a relativized ordered first-order interpretation I together with a post-processing term post (DescriptiveComplexity.PostTerm), such that

C A = post.eval A (D (I.MapRel A))

on every finite ordered structure: one question is asked of the oracle for D, at an instance defined first-order, and the count is recovered from the answer by arithmetic on it and on first-order definable cardinalities of the instance.

Relation to the literature

• A parsimonious reduction is the case post = oracle (DescriptiveComplexity.RelOrderedParsimoniousReduction.toOneCall).
• A one-call reduction is what the literature calls a metric reduction, f(x) = ψ(x, g(φ(x))) with φ and ψ computable in polynomial time, a notion due to Krentel 1988 (here as stated in Faliszewski and Hemaspaandra 2009, Definition 1.2), or equivalently a polynomial-time 1-Turing reduction: one oracle call, and polynomial-time computation before and after it. It is a restricted one, φ being a first-order interpretation and ψ a fixed arithmetic term. A one-call hard problem is therefore #P-hard under metric reductions, hence under Turing reductions, the sense the literature most often means. There is no single agreed notion of completeness for classes of functions: beside the metric and the parsimonious reductions, the many-one reductions for functions ask that ψ not read the input, f(x) = ψ(g(φ(x))); a one-call reduction is one of those when its term mentions no cardinality of the instance. Durand, Haak, Kontinen, Vollmer 2016 use exactly the reduction of #SAT to #DNF by 2 ^ n - oracle, under the name of an AC⁰-Turing reduction (their Lemma 19; the preprint of the paper calls it a metric reduction), and a division of the oracle's answer for another, a TC⁰-Turing reduction (their Lemma 20), as the digit extractions of this library do.
• That notion is coarse. Toda and Watanabe 1992 show that a problem #P-hard under polynomial-time 1-Turing reductions is hard for the higher counting classes #·Πₖᵖ as well, which is strong evidence that #P is not closed under such reductions. Membership in a counting class is therefore closed under parsimonious reductions only, never under these, and one-call hardness does not tell #P apart from the classes above it.
• The subtractive reductions of Durand, Hermann, Kolaitis 2005 were introduced to repair this: a strong subtractive reduction asks the oracle two questions, at instances f(x) and g(x) with the solutions of the first among those of the second, and returns the difference of the answers; #P is closed under them (their Theorem 3.3). The reduction of #SAT to #DNF is one (their Proposition 3.4), g(x) being a tautology: here it is the one-call reduction with term 2 ^ n - oracle, the answer at the tautology being known. Subtractive reductions are formalized in DescriptiveComplexity.Counting.Subtractive, with the closure of #P. The reductions that read a digit by a quotient and a remainder are not subtractive, and nothing is claimed here about whether their targets are complete under subtractive reductions.

The one-call closure of a class

#P is not expected to be closed under one-call reductions, so the plain words hard and complete are not used for them: as on the decision side, those words belong to reductions the class is closed under, here the subtractive ones (DescriptiveComplexity.Counting.Subtractive). What one-call reductions are the reductions of is the one-call closure of a class, DescriptiveComplexity.CountingClass.OneCallMem: the problems that reduce with one call to a problem of the class. It contains the class, is closed under one-call reductions (DescriptiveComplexity.CountingClass.OneCallMem.of_oneCall), and DescriptiveComplexity.CountingClass.OneCallHard is hardness for it (DescriptiveComplexity.CountingClass.oneCallHard_iff); DescriptiveComplexity.CountingClass.OneCallComplete conjoins the two. Parsimonious hardness implies one-call hardness (DescriptiveComplexity.oneCallHard_sharpP_of_parsimoniousHard).

The one-call closure of #P is a logical counterpart of the class FP^#P of the functions computable in polynomial time with a #P oracle. It is not given that name: that it is the same class would need one oracle call to suffice, and a polynomial-time computation after the call to be replaceable by a post-processing term, and neither is proved here.

structure DescriptiveComplexity.OneCallReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] (C : CountingProblem L) (D : CountingProblem L') : Type 1

A one-call counting reduction: a relativized ordered interpretation and a post-processing term recovering the count of the source from the count of the interpreted instance.

• Tag : Type

  The tags used by the underlying interpretation.

• tagFinite : Finite self.Tag

  Tags are finite, so that finite structures map to finite structures.

• dim : ℕ

  The dimension of the underlying interpretation.

• toRelInterpretation : RelFOInterpretation (L.sum FirstOrder.Language.order) L' self.Tag self.dim

  The underlying relativized interpretation, over the ordered expansion.

• dom_nonempty (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : ∃ (t : self.Tag) (w : Fin self.dim → A), (self.toRelInterpretation.domFormula t).Realize w

  The definable domain is inhabited.

• post : PostTerm L

  The arithmetic applied to the answer of the oracle.

• correct (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : C.Count A = PostTerm.eval A (D.Count (self.toRelInterpretation.MapRel A)) self.post

  The count of the source is the post-processed count of the interpreted instance, whatever the linear order.

def DescriptiveComplexity.«term_≤ᶜ[≤]_» : Lean.TrailingParserDescr

A one-call counting reduction: a relativized ordered interpretation and a post-processing term recovering the count of the source from the count of the interpreted instance.

Equations

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

theorem DescriptiveComplexity.OneCallReduction.mapRel_nonempty {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : OneCallReduction C D) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : Nonempty (f.toRelInterpretation.MapRel A)

The relativized universe of the output of a reduction is nonempty on nonempty finite ordered inputs.

def DescriptiveComplexity.RelOrderedParsimoniousReduction.toOneCall {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : RelOrderedParsimoniousReduction C D) : OneCallReduction C D

A relativized parsimonious reduction is a one-call reduction that returns the answer of the oracle unchanged.

Equations

• f.toOneCall = { Tag := f.Tag, tagFinite := ⋯, dim := f.dim, toRelInterpretation := f.toRelInterpretation, dom_nonempty := ⋯, post := DescriptiveComplexity.PostTerm.oracle, correct := ⋯ }

def DescriptiveComplexity.OrderedParsimoniousReduction.toOneCall {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : OrderedParsimoniousReduction C D) : OneCallReduction C D

An ordered parsimonious reduction is a one-call reduction.

Equations

• f.toOneCall = f.toRel.toOneCall

noncomputable def DescriptiveComplexity.ParsimoniousReduction.toOneCall {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : ParsimoniousReduction C D) : OneCallReduction C D

A parsimonious reduction is a one-call reduction.

Equations

• f.toOneCall = f.toOrdered.toOneCall

def DescriptiveComplexity.OneCallReduction.congrSource {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} {C' : CountingProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], C.Count A = C'.Count A) (g : OneCallReduction C D) : OneCallReduction C' D

Replacing the source of a one-call reduction by a counting problem with the same values on finite structures.

Equations

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

def DescriptiveComplexity.OneCallReduction.congrTarget {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D D' : CountingProblem L'} (h : ∀ (A : Type) [inst : L'.Structure A] [Finite A], D.Count A = D'.Count A) (g : OneCallReduction C D) : OneCallReduction C D'

Replacing the target of a one-call reduction by a counting problem with the same values on finite structures.

Equations

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

def DescriptiveComplexity.OneCallReduction.ofPost {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} {C' : CountingProblem L} (g : OneCallReduction C' D) (post : PostTerm L) (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], C.Count A = PostTerm.eval A (C'.Count A) post) : OneCallReduction C D

Post-processing a reduction. If the count of C is recovered from the count of C' by a post-processing term, a one-call reduction from C' gives one from C.

Equations

• g.ofPost post h = { Tag := g.Tag, tagFinite := ⋯, dim := g.dim, toRelInterpretation := g.toRelInterpretation, dom_nonempty := ⋯, post := post.subst g.post, correct := ⋯ }

def DescriptiveComplexity.CountingProblem.pullback {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {Tag : Type} {dim : ℕ} (D : CountingProblem L') (I : FOInterpretation L L' Tag dim) : CountingProblem L

A counting problem read through an interpretation: the count of the interpreted structure.

Equations

• D.pullback I = { Count := fun (A : Type) (x : L.Structure A) => D.Count (I.Map A), iso_invariant := ⋯ }

def DescriptiveComplexity.CountingProblem.pullbackReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {Tag : Type} [Finite Tag] [Nonempty Tag] {dim : ℕ} (D : CountingProblem L') (I : FOInterpretation L L' Tag dim) : ParsimoniousReduction (D.pullback I) D

A counting problem read through an interpretation reduces parsimoniously to the problem itself, by that interpretation.

Equations

• D.pullbackReduction I = { Tag := Tag, tagFinite := inst✝¹, tagNonempty := inst✝, dim := dim, toInterpretation := I, correct := ⋯ }

noncomputable def DescriptiveComplexity.OneCallReduction.trans {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] {C : CountingProblem L₁} {D : CountingProblem L₂} {E : CountingProblem L₃} (g : OneCallReduction C D) (f : OneCallReduction D E) : OneCallReduction C E

Transitivity of one-call reductions. The interpretations compose as for relativized reductions; the post-processing of the second reduction is pulled back to the instance and substituted for the oracle's answer in the post-processing of the first. There is still one call.

Equations

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

The one-call closure of a class: membership, hardness, completeness

def DescriptiveComplexity.CountingClass.OneCallMem (K : CountingClass) {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) : Prop

A counting problem is in the one-call closure of a class when it reduces with one call to a problem of the class.

Equations

• K.OneCallMem C = ∃ (L'' : FirstOrder.Language) (x : L''.IsRelational) (D : DescriptiveComplexity.CountingProblem L''), K.Mem D ∧ Nonempty (DescriptiveComplexity.OneCallReduction C D)

def DescriptiveComplexity.CountingClass.OneCallHard (K : CountingClass) {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) : Prop

A counting problem is one-call hard for a class when every problem of the class reduces to it with one call.

Equations

• K.OneCallHard C = ∀ {L'' : FirstOrder.Language} [inst : L''.IsRelational] (D : DescriptiveComplexity.CountingProblem L''), K.Mem D → Nonempty (DescriptiveComplexity.OneCallReduction D C)

def DescriptiveComplexity.CountingClass.OneCallComplete (K : CountingClass) {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) : Prop

A counting problem is one-call complete for a class when it is in the one-call closure of the class and one-call hard for it.

Equations

• K.OneCallComplete C = (K.OneCallMem C ∧ K.OneCallHard C)

theorem DescriptiveComplexity.CountingClass.OneCallComplete.oneCallMem {K : CountingClass} {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (h : K.OneCallComplete C) : K.OneCallMem C

theorem DescriptiveComplexity.CountingClass.OneCallComplete.oneCallHard {K : CountingClass} {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (h : K.OneCallComplete C) : K.OneCallHard C

theorem DescriptiveComplexity.CountingClass.OneCallMem.of_mem {K : CountingClass} {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (h : K.Mem C) : K.OneCallMem C

A problem of the class is in its one-call closure.

theorem DescriptiveComplexity.CountingClass.OneCallMem.of_oneCall {K : CountingClass} {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : OneCallReduction C D) (hD : K.OneCallMem D) : K.OneCallMem C

The one-call closure is closed under one-call reductions.

theorem DescriptiveComplexity.CountingClass.OneCallHard.of_oneCall {K : CountingClass} {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : OneCallReduction C D) (hC : K.OneCallHard C) : K.OneCallHard D

One-call hardness travels forward along one-call reductions.

theorem DescriptiveComplexity.CountingClass.oneCallHard_iff {K : CountingClass} {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} : K.OneCallHard C ↔ ∀ {L'' : FirstOrder.Language} [inst : L''.IsRelational] (D : CountingProblem L''), K.OneCallMem D → Nonempty (OneCallReduction D C)

One-call hardness is hardness for the one-call closure: every problem of the closure, and not only of the class, reduces to a one-call hard problem. Registered in the Lax archive as Lax859101.OneCallClosure.oneCallHard_iff.

theorem DescriptiveComplexity.CountingClass.OneCallHard.of_relOrderedParsimonious {K : CountingClass} {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : RelOrderedParsimoniousReduction C D) (hC : K.OneCallHard C) : K.OneCallHard D

One-call hardness travels forward along relativized parsimonious reductions.

theorem DescriptiveComplexity.CountingClass.OneCallHard.of_orderedParsimonious {K : CountingClass} {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : OrderedParsimoniousReduction C D) (hC : K.OneCallHard C) : K.OneCallHard D

One-call hardness travels forward along ordered parsimonious reductions.

theorem DescriptiveComplexity.CountingClass.OneCallHard.of_parsimonious {K : CountingClass} {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : ParsimoniousReduction C D) (hC : K.OneCallHard C) : K.OneCallHard D

One-call hardness travels forward along parsimonious reductions.

theorem DescriptiveComplexity.CountingClass.oneCallHard_congr_finite {K : CountingClass} {L : FirstOrder.Language} [L.IsRelational] {C D : CountingProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], C.Count A = D.Count A) : K.OneCallHard C ↔ K.OneCallHard D

One-call hardness only depends on the values of a counting problem on finite structures.

theorem DescriptiveComplexity.CountingClass.OneCallComplete.of_mem {K : CountingClass} {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (hC : K.Mem C) (h : K.OneCallHard C) : K.OneCallComplete C

A problem of the class that is one-call hard for it is one-call complete.

theorem DescriptiveComplexity.oneCallHard_sharpP_of_parsimoniousHard {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (h : SharpP.ParsimoniousHard C) : SharpP.OneCallHard C

Parsimonious #P-hardness implies one-call #P-hardness: a parsimonious reduction is a one-call reduction.

theorem DescriptiveComplexity.oneCallComplete_sharpP_of_parsimoniousComplete {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (h : SharpP.ParsimoniousComplete C) : SharpP.OneCallComplete C

A parsimoniously #P-complete problem is one-call #P-complete. Registered in the Lax archive as Lax859101.OneCallClosure.oneCallComplete_sharpP_of_parsimoniousComplete.