Subtractive reductions #
The reductions of Durand, Hermann, Kolaitis 2005,
which sit between the parsimonious reductions and the one-call reductions of
DescriptiveComplexity.Counting.Reduction, and under which #P is closed.
A strong subtractive reduction from C to D
(DescriptiveComplexity.StrongSubtractiveReduction) draws two instances of
D, the subtrahend and the minuend, such that the solutions of the first
are among those of the second and
C A = D (minuend A) - D (subtrahend A).
The condition on solutions is what keeps the difference inside #P, and it is
about solutions, not counts. So D comes with a presentation: a second-order
block and a first-order kernel whose witnesses it counts
(DescriptiveComplexity.StrongSubtractiveReduction.present), which plays the
part of the relation B in the paper's #·B. The two interpretations share
their tags and their dimension, so the two instances have the same universe,
ordered the same way, and a witness of one can be compared with a witness of
the other (DescriptiveComplexity.FOInterpretation.WitAt).
Strong subtractive reductions do not compose, and a subtractive reduction
C ≤ˢ D (DescriptiveComplexity.SubtractiveReducible) is a finite chain of
steps, as in the paper. Two departures from it, both forced:
- a step is a strong subtractive reduction or a parsimonious reduction, in its most general form, relativized and ordered. The paper obtains the second as the special case of the first whose subtrahend has no solution, which needs the target to have such an instance, definably; admitting the step directly asks for nothing;
- the target of a strong step is presented by a first-order kernel, hence is
itself in
#P. The paper's relations are arbitrary, which is what lets it speak of the classes above#P; the library has no such classes yet.
#P is closed under subtractive reductions
(DescriptiveComplexity.SharpPDefinable.of_subtractive, Theorem 3.3 of the
paper): the witnesses of the minuend that are not witnesses of the subtrahend
are the witnesses of one kernel, the conjunction of the pulled kernel of the
first with the negated pulled kernel of the second. So this is the widest
notion of the library under which the class is closed, and the plain words go
to it, as on the decision side they go to reductions the classes are closed
under: DescriptiveComplexity.CountingClass.Hard and
DescriptiveComplexity.CountingClass.Complete are hardness and completeness
under subtractive reductions. Parsimonious hardness and completeness imply
them (DescriptiveComplexity.hard_sharpP_of_parsimoniousHard,
DescriptiveComplexity.complete_sharpP_of_parsimoniousComplete).
Witnesses at an interpreted instance #
The assignment ρ is a witness of the kernel φ at the instance drawn by
the interpretation I, ordered lexicographically. The universe of that
instance is Tag × A ^ dim whatever I is, so the witnesses at two
interpretations with the same tags and dimension are comparable.
Instances For
Dependency graph
A witness at an interpreted instance is a witness of the pulled kernel, at the pulled assignment.
Dependency graph
The witness count of the kernel at the interpreted instance, ordered lexicographically, is the number of witnesses there.
Dependency graph
Strong subtractive reductions #
A strong subtractive reduction: the target is presented as the witness count of a kernel, two interpretations with the same tags and dimension draw a subtrahend and a minuend, every witness at the first is a witness at the second, and the count of the source is the difference of the two counts.
- Tag : Type
The tags used by the two interpretations.
Tags are finite, so that finite structures map to finite structures.
Tags are nonempty, so that nonempty structures map to nonempty ones.
- tagOrder : LinearOrder self.Tag
Tags are linearly ordered: the order of the drawn instances is the lexicographic one.
- dim : ℕ
The dimension of the two interpretations.
- block : SOBlock
The second-order block of the presentation of the target.
The first-order kernel of the presentation of the target.
- present (A : Type) [L'.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : D.Count A = witnessCount self.block self.kernel A
The target counts the witnesses of its presentation, whatever the linear order.
- subtrahend : FOInterpretation (L.sum FirstOrder.Language.order) L' self.Tag self.dim
The interpretation drawing the subtrahend.
- minuend : FOInterpretation (L.sum FirstOrder.Language.order) L' self.Tag self.dim
The interpretation drawing the minuend.
- witness_le (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ρ : self.block.Assignment (self.Tag × (Fin self.dim → A))) : self.subtrahend.WitAt self.block self.kernel A ρ → self.minuend.WitAt self.block self.kernel A ρ
Every witness at the subtrahend is a witness at the minuend.
- correct (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : C.Count A + D.Count (self.subtrahend.Map A) = D.Count (self.minuend.Map A)
The count of the source and the count at the subtrahend add up to the count at the minuend.
Instances For
Dependency graph
The source of a strong subtractive reduction is in #P: it counts the
witnesses at the minuend that are not witnesses at the subtrahend, and those
are the witnesses of one kernel.
Dependency graph
Subtractive reductions #
Subtractive reducibility, C ≤ˢ D: a finite chain of steps, each a
strong subtractive reduction or a relativized ordered parsimonious
reduction.
- refl
{L : FirstOrder.Language}
[L.IsRelational]
(C : CountingProblem L)
: SubtractiveReducible C C
The empty chain.
- strong
{L₁ L₂ L₃ : FirstOrder.Language}
[L₁.IsRelational]
[L₂.IsRelational]
[L₃.IsRelational]
{C : CountingProblem L₁}
{D : CountingProblem L₂}
{E : CountingProblem L₃}
(f : StrongSubtractiveReduction C D)
(h : SubtractiveReducible D E)
: SubtractiveReducible C E
A strong subtractive step, then a chain.
- parsimonious
{L₁ L₂ L₃ : FirstOrder.Language}
[L₁.IsRelational]
[L₂.IsRelational]
[L₃.IsRelational]
{C : CountingProblem L₁}
{D : CountingProblem L₂}
{E : CountingProblem L₃}
(f : RelOrderedParsimoniousReduction C D)
(h : SubtractiveReducible D E)
: SubtractiveReducible C E
A parsimonious step, then a chain.
Instances For
Dependency graph
Subtractive reducibility, C ≤ˢ D: a finite chain of steps, each a
strong subtractive reduction or a relativized ordered parsimonious
reduction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
A strong subtractive reduction is a subtractive reduction.
Dependency graph
A relativized parsimonious reduction is a subtractive reduction.
Dependency graph
Subtractive reducibility is transitive (Proposition 3.2 of the paper): chains concatenate.
Dependency graph
#P is closed under subtractive reductions (Theorem 3.3 of
Durand, Hermann, Kolaitis 2005).
Dependency graph
Hardness and completeness #
A counting problem is hard for a class when every problem of the class reduces to it by a subtractive reduction.
Equations
- K.Hard C = ∀ {L'' : FirstOrder.Language} [inst : L''.IsRelational] (D : DescriptiveComplexity.CountingProblem L''), K.Mem D → DescriptiveComplexity.SubtractiveReducible D C
Instances For
Dependency graph
A counting problem is complete for a class when it belongs to it and is hard for it, under subtractive reductions.
Instances For
Dependency graph
Dependency graph
Dependency graph
Hardness travels forward along subtractive reductions.
Dependency graph
Membership in #P travels backward along subtractive reductions.
Dependency graph
Parsimonious #P-hardness implies #P-hardness: a relativized
parsimonious reduction is a subtractive reduction.
Dependency graph
A parsimoniously #P-complete problem is #P-complete.