Relativized parsimonious reductions

The counting counterpart of DescriptiveComplexity.RelOrderedFOReduction: an ordered parsimonious reduction through a relativized interpretation, whose target universe is the definable subset a domain formula carves out of Tag × A^dim (DescriptiveComplexity.RelOrderedParsimoniousReduction, notation C ≤ʳᵖ[≤] D).

It is needed for the same reason as on the decision side. A counting problem whose solutions span the universe – the Hamilton circuits of a graph – cannot be the target of an ordinary interpretation: the tagged tuples that stand for nothing would each have to lie on every circuit. With a definable domain they are simply not there.

• DescriptiveComplexity.OrderedParsimoniousReduction.toRel: an ordinary ordered parsimonious reduction is a relativized one, with domain ⊤;
• DescriptiveComplexity.RelOrderedParsimoniousReduction.trans: transitivity, by the guarded composition of DescriptiveComplexity.RelComposition;
• DescriptiveComplexity.RelOrderedParsimoniousReduction.toRelOrderedFOReduction: it is a relativized reduction between the supports.

Parsimonious hardness for the counting classes of DescriptiveComplexity.Counting.Class is hardness under these reductions, as hardness for the decision classes is hardness under ≤ʳᶠᵒ[≤].

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

An ordered parsimonious reduction through a relativized interpretation: the two counts agree, the target structure being carried by the definable subset of Tag × A^dim that the domain formula carves out.

• 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.

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

  The counts agree, whatever the linear order.

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

An ordered parsimonious reduction through a relativized interpretation: the two counts agree, the target structure being carried by the definable subset of Tag × A^dim that the domain formula carves out.

Equations

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

theorem DescriptiveComplexity.RelOrderedParsimoniousReduction.mapRel_nonempty {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : RelOrderedParsimoniousReduction 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.OrderedParsimoniousReduction.toRel {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : OrderedParsimoniousReduction C D) : RelOrderedParsimoniousReduction C D

An ordinary ordered parsimonious reduction is a relativized one with ⊤ domain.

Equations

• f.toRel = { Tag := f.Tag, tagFinite := ⋯, dim := f.dim, toRelInterpretation := f.toInterpretation.toRel, dom_nonempty := ⋯, correct := ⋯ }

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

A relativized parsimonious reduction is a relativized first-order reduction between the supports: equal counts are positive together.

Equations

• f.toRelOrderedFOReduction = { Tag := f.Tag, tagFinite := ⋯, dim := f.dim, toRelInterpretation := f.toRelInterpretation, dom_nonempty := ⋯, correct := ⋯ }

def DescriptiveComplexity.RelOrderedParsimoniousReduction.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 : RelOrderedParsimoniousReduction C D) : RelOrderedParsimoniousReduction C' D

Replacing the source of a relativized parsimonious 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.RelOrderedParsimoniousReduction.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 : RelOrderedParsimoniousReduction C D) : RelOrderedParsimoniousReduction C D'

Replacing the target of a relativized parsimonious 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.

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

Transitivity of relativized parsimonious reductions. The intermediate definable structure is ordered by the lexicographic order on tagged tuples, restricted to the domain.

Equations

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