Counting the witnesses of a second-order block: `#P`-definability #

Fagin's theorem reads NP as the problems defined by a sentence ∃X̄. φ with φ first-order. The counting analog, due to Saluja, Subrahmanyam and Thakur (1995), reads #P as the functions counting the witnesses of such a sentence, over ordered structures: the number of assignments of the block X̄ under which the first-order kernel φ holds. This is also the prenex normal form ΣX̄. φ of the logic ΣQSO(FO) of Arenas, Muñoz and Riveros (2020), who show that every formula of that logic can be brought to it.

This file sets up that notion:

DescriptiveComplexity.witnessCount B φ A is the number of assignments of the block B on A satisfying the kernel φ;
DescriptiveComplexity.SharpPDefinable C states that the counting problem C is the witness count of some kernel over the ordered expansion, whatever the linear order of the instance. The order is a parameter here and not a guessed relation as in DescriptiveComplexity.SigmaSODefinable: guessing it would multiply every count by the number of linear orders;
DescriptiveComplexity.CountingProblem.ofKernel B φ is the witness-counting problem of an order-free kernel, the counting version of the decision problem the kernel defines.

The closure theorem, DescriptiveComplexity.SharpPDefinable.of_orderedParsimonious, pulls a kernel back through a parsimonious reduction. The decision-side pullback of DescriptiveComplexity.SecondOrderPull only needs each assignment of the pulled block to come from one of the original block; counting needs the correspondence to be a bijection (DescriptiveComplexity.SOBlock.pullAssignEquiv), which it is because the interpreted universe is all of Tag × A^d.

Counting witnesses #

source

noncomputable def DescriptiveComplexity.witnessCount {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) (A : Type) [inst : L.Structure A] :

ℕ

The number of assignments of the block B on the structure A under which the first-order kernel φ holds.

Equations

DescriptiveComplexity.witnessCount B φ A = Nat.card { ρ : B.Assignment A // A ⊨ φ }

Instances For

Dependency graph

source

def DescriptiveComplexity.SOBlock.mapAssignEquiv (B : SOBlock) {A A' : Type} (e : A ≃ A') :

B.Assignment A ≃ B.Assignment A'

Transport of block assignments along an equivalence, as an equivalence.

Equations

B.mapAssignEquiv e = { toFun := B.mapAssign e, invFun := B.mapAssign e.symm, left_inv := ⋯, right_inv := ⋯ }

Instances For

Dependency graph

source

theorem DescriptiveComplexity.witnessCount_iso {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) {A A' : Type} [L.Structure A] [L.Structure A'] (e : L.Equiv A A') :

witnessCount B φ A = witnessCount B φ A'

The witness count is isomorphism-invariant.

Dependency graph

source

instance DescriptiveComplexity.SOBlock.finite_assignment (B : SOBlock) (A : Type) [Finite A] :

Finite (B.Assignment A)

Block assignments on a finite universe are finitely many.

Dependency graph

Pulling a witness count back through an interpretation #

source

theorem DescriptiveComplexity.witnessCount_map {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {d : ℕ} [L₂.IsRelational] (I : FOInterpretation L₁ L₂ Tag d) (B : SOBlock) (φ : (L₂.sum B.lang).Sentence) (A : Type) [instA : L₁.Structure A] :

witnessCount B φ (I.Map A) = witnessCount (SOBlock.pull Tag d B) ((I.extendSO B).pullSentence φ) A

Pulling a witness count back through an interpretation: the witnesses of a kernel in the interpreted structure are, bijectively, the witnesses of the pulled kernel, over the pulled block, in the base structure.

Dependency graph

`#P`-definability #

source

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

Prop

A counting problem is #P-definable if, on nonempty finite structures, it counts the witnesses of an existential second-order sentence over the ordered expansion: for some block B and first-order kernel φ, its value is the number of assignments of B satisfying φ, whatever the linear order of the instance.

Equations

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

Instances For

Dependency graph

source

theorem DescriptiveComplexity.sharpPDefinable_congr {L : FirstOrder.Language} [L.IsRelational] {C C' : CountingProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], C.Count A = C'.Count A) (hC : SharpPDefinable C) :

SharpPDefinable C'

Dependency graph

source

theorem DescriptiveComplexity.SharpPDefinable.of_orderedParsimonious {L : FirstOrder.Language} [L.IsRelational] {L' : FirstOrder.Language} [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : OrderedParsimoniousReduction C D) (h : SharpPDefinable D) :

SharpPDefinable C

#P-definability is closed under ordered parsimonious reductions. Registered in the Lax archive as Lax366625.SharpPClosure.SharpP_mem_of_orderedParsimonious.

Dependency graph

source

theorem DescriptiveComplexity.SharpPDefinable.of_parsimonious {L : FirstOrder.Language} [L.IsRelational] {L' : FirstOrder.Language} [L'.IsRelational] {C : CountingProblem L} {D : CountingProblem L'} (f : ParsimoniousReduction C D) (h : SharpPDefinable D) :

SharpPDefinable C

#P-definability is closed under parsimonious reductions.

Dependency graph

The witness-counting problem of an order-free kernel #

source

noncomputable def DescriptiveComplexity.CountingProblem.ofKernel {L : FirstOrder.Language} [L.IsRelational] (B : SOBlock) (φ : (L.sum B.lang).Sentence) :

CountingProblem L

The counting problem of an existential second-order sentence: the number of witnesses of the block B for the first-order kernel φ. It is the counting version of the decision problem ∃B. φ, which is its support (DescriptiveComplexity.CountingProblem.ofKernel_support_iff).

Equations