Counting problems and parsimonious reductions

A decision problem is an isomorphism-invariant property of finite structures; a counting problem (DescriptiveComplexity.CountingProblem) is an isomorphism-invariant number attached to them – the number of satisfying assignments of a CNF formula, of proper colorings of a graph, of accepting runs of a machine. Vocabularies, tagged interpretations and the invariance discipline carry over unchanged from DescriptiveComplexity.Interpretation.

The reductions of this file are the parsimonious ones: a first-order interpretation under which the two counts are equal,

• DescriptiveComplexity.ParsimoniousReduction, notation C ≤ᵖ D, over the bare vocabulary, and
• DescriptiveComplexity.OrderedParsimoniousReduction, notation C ≤ᵖ[≤] D, over the ordered expansion, the equation holding whatever the linear order.

They are DescriptiveComplexity.FOReduction and DescriptiveComplexity.OrderedFOReduction with the equivalence of the correct field replaced by an equation, and they compose for the same reason: the composite interpretation is isomorphic to the twice-applied one, and a counting problem does not distinguish isomorphic structures.

Every counting problem has a decision problem underneath, its support (DescriptiveComplexity.CountingProblem.support): “is the count positive?”. A parsimonious reduction between two counting problems is in particular a first-order reduction between their supports (DescriptiveComplexity.ParsimoniousReduction.toFOReduction), which is how hardness results for counting problems yield hardness results for decision problems.

structure DescriptiveComplexity.CountingProblem (L : FirstOrder.Language) [L.IsRelational] : Type 1

A counting problem in the sense of descriptive complexity: an isomorphism-invariant natural number attached to every L-structure. As for DescriptiveComplexity.DecisionProblem, only the values on finite structures are ever read.

• Count (A : Type) [L.Structure A] : ℕ

  The count: C A (through the function coercion) is the number attached to the structure A.

• iso_invariant {A B : Type} [L.Structure A] [L.Structure B] : ∀ (a : L.Equiv A B), self.Count A = self.Count B

  Counting problems do not distinguish isomorphic structures.

@[instance_reducible]

instance DescriptiveComplexity.CountingProblem.instCoeFunForallForallStructureNat {L : FirstOrder.Language} [L.IsRelational] : CoeFun (CountingProblem L) fun (x : CountingProblem L) => (A : Type) → [L.Structure A] → ℕ

Equations

• DescriptiveComplexity.CountingProblem.instCoeFunForallForallStructureNat = { coe := DescriptiveComplexity.CountingProblem.Count }

theorem DescriptiveComplexity.CountingProblem.ext {L : FirstOrder.Language} [L.IsRelational] {C D : CountingProblem L} (h : ∀ (A : Type) [inst : L.Structure A], C.Count A = D.Count A) : C = D

theorem DescriptiveComplexity.CountingProblem.ext_iff {L : FirstOrder.Language} [L.IsRelational] {C D : CountingProblem L} : C = D ↔ ∀ (A : Type) [inst : L.Structure A], C.Count A = D.Count A

def DescriptiveComplexity.CountingProblem.support {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) : DecisionProblem L

The decision problem underneath a counting problem: is the count positive?

Equations

• C.support = { Holds := fun (A : Type) (inst : L.Structure A) => 0 < C.Count A, iso_invariant := ⋯ }

theorem DescriptiveComplexity.CountingProblem.support_iff {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) (A : Type) [L.Structure A] : C.support.Holds A ↔ 0 < C.Count A

Reading an interpretation over a larger source vocabulary

def DescriptiveComplexity.FOInterpretation.liftSource {L' L₀ L₁ : FirstOrder.Language} {Tag : Type} {dim : ℕ} (Φ : L₀ →ᴸ L₁) (I : FOInterpretation L₀ L' Tag dim) : FOInterpretation L₁ L' Tag dim

An interpretation read over a larger source vocabulary: every defining formula is transported along the vocabulary map.

Equations

• DescriptiveComplexity.FOInterpretation.liftSource Φ I = { relFormula := fun {n : ℕ} (R : L'.Relations n) (t : Fin n → Tag) => Φ.onFormula (I.relFormula R t) }

def DescriptiveComplexity.FOInterpretation.liftSourceLEquiv {L' L₀ L₁ : FirstOrder.Language} {Tag : Type} {dim : ℕ} [L'.IsRelational] (Φ : L₀ →ᴸ L₁) (I : FOInterpretation L₀ L' Tag dim) (A : Type) [L₀.Structure A] [L₁.Structure A] [Φ.IsExpansionOn A] : L'.Equiv ((liftSource Φ I).Map A) (I.Map A)

On a structure that is an expansion along the vocabulary map, the lifted interpretation produces the same structure as the original one: the identity on tagged tuples is an isomorphism.

Equations

• DescriptiveComplexity.FOInterpretation.liftSourceLEquiv Φ I A = { toEquiv := Equiv.refl ((DescriptiveComplexity.FOInterpretation.liftSource Φ I).Map A), map_fun' := ⋯, map_rel' := ⋯ }

Parsimonious reductions

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

A parsimonious first-order reduction from the counting problem C to the counting problem D: a first-order interpretation under which the two counts agree.

• Tag : Type

  The tags (copies of A^dim) used by the underlying interpretation.

• tagFinite : Finite self.Tag

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

• tagNonempty : Nonempty self.Tag

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

• dim : ℕ

  The dimension of the underlying interpretation.

• toInterpretation : FOInterpretation L L' self.Tag self.dim

  The underlying first-order interpretation.

• correct (A : Type) [L.Structure A] [Finite A] [Nonempty A] : C.Count A = D.Count (self.toInterpretation.Map A)

  The counts agree, on the finite nonempty structures.

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

A parsimonious first-order reduction from the counting problem C to the counting problem D: a first-order interpretation under which the two counts agree.

Equations

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

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

An ordered parsimonious reduction: a first-order interpretation over the ordered expansion of the source vocabulary under which the two counts agree, for every linear order of the (finite) input structure.

• Tag : Type

  The tags (copies of A^dim) used by the underlying interpretation.

• tagFinite : Finite self.Tag

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

• tagNonempty : Nonempty self.Tag

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

• dim : ℕ

  The dimension of the underlying interpretation.

• toInterpretation : FOInterpretation (L.sum FirstOrder.Language.order) L' self.Tag self.dim

  The underlying first-order interpretation, over the ordered expansion.

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

  The counts agree, whatever the linear order.

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

An ordered parsimonious reduction: a first-order interpretation over the ordered expansion of the source vocabulary under which the two counts agree, for every linear order of the (finite) input structure.

Equations

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

def DescriptiveComplexity.ParsimoniousReduction.toFOReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : ParsimoniousReduction C D) : FOReduction C.support D.support

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

Equations

• f.toFOReduction = { Tag := f.Tag, tagFinite := ⋯, tagNonempty := ⋯, dim := f.dim, toInterpretation := f.toInterpretation, correct := ⋯ }

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

An ordered parsimonious reduction is an ordered first-order reduction between the supports.

Equations

• f.toOrderedFOReduction = { Tag := f.Tag, tagFinite := ⋯, tagNonempty := ⋯, dim := f.dim, toInterpretation := f.toInterpretation, correct := ⋯ }

Reflexivity and transitivity

def DescriptiveComplexity.ParsimoniousReduction.refl {L₁ : FirstOrder.Language} [L₁.IsRelational] (C : CountingProblem L₁) : ParsimoniousReduction C C

Every counting problem parsimoniously reduces to itself, via the identity interpretation.

Equations

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

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

Transitivity of parsimonious reductions. The composite interpretation is only isomorphic to the twice-applied one, so the isomorphism-invariance built into DescriptiveComplexity.CountingProblem concludes.

Equations

• g.trans f = { Tag := f.Tag × (Fin f.dim → g.Tag), tagFinite := ⋯, tagNonempty := ⋯, dim := f.dim * g.dim, toInterpretation := f.toInterpretation.comp g.toInterpretation, correct := ⋯ }

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

Transitivity of ordered parsimonious reductions. The intermediate structure is ordered by the lexicographic order on tagged tuples, which is first-order definable from the order of the input.

Equations

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

noncomputable def DescriptiveComplexity.ParsimoniousReduction.toOrdered {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {C : CountingProblem L₁} {D : CountingProblem L₂} (g : ParsimoniousReduction C D) : OrderedParsimoniousReduction C D

A parsimonious reduction is in particular an ordered one: lift its defining formulas to the ordered expansion, where they ignore the order.

Equations

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

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

Mixed transitivity: an ordered parsimonious reduction followed by a plain one.

Equations

• g.trans_pars f = g.trans f.toOrdered

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

Mixed transitivity: a plain parsimonious reduction followed by an ordered one.

Equations

• g.trans_ordered f = g.toOrdered.trans f

@[instance_reducible]

noncomputable instance DescriptiveComplexity.instTransCountingProblemParsimoniousReduction {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] : Trans ParsimoniousReduction ParsimoniousReduction ParsimoniousReduction

Trans instance for parsimonious reductions, enabling calc chains.

Equations

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

@[instance_reducible]

noncomputable instance DescriptiveComplexity.instTransCountingProblemOrderedParsimoniousReduction {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] : Trans OrderedParsimoniousReduction OrderedParsimoniousReduction OrderedParsimoniousReduction

Trans instance for ordered parsimonious reductions.

Equations

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

@[instance_reducible]

noncomputable instance DescriptiveComplexity.instTransCountingProblemOrderedParsimoniousReductionParsimoniousReduction {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] : Trans OrderedParsimoniousReduction ParsimoniousReduction OrderedParsimoniousReduction

Mixed transitivity: an ordered parsimonious reduction followed by a plain one.

Equations

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

@[instance_reducible]

noncomputable instance DescriptiveComplexity.instTransCountingProblemParsimoniousReductionOrderedParsimoniousReduction {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] : Trans ParsimoniousReduction OrderedParsimoniousReduction OrderedParsimoniousReduction

Mixed transitivity: a plain parsimonious reduction followed by an ordered one.

Equations

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

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

Replacing the source of an ordered parsimonious reduction by a counting problem with the same values on finite structures.

Equations

• DescriptiveComplexity.OrderedParsimoniousReduction.congrSource h g = { Tag := g.Tag, tagFinite := ⋯, tagNonempty := ⋯, dim := g.dim, toInterpretation := g.toInterpretation, correct := ⋯ }