Documentation

DescriptiveComplexity.Counting.RelClosure

#P is closed under relativized parsimonious reductions #

Membership in #P travels backward along the relativized reductions C ≤ʳᵖ[≤] D, those whose target universe is a definable set of tagged tuples (DescriptiveComplexity.SharpPDefinable.of_relOrderedParsimonious). With the hardness half, which holds by definition, this makes the relativized reductions reductions of the class in the full sense.

From a retraction to a bijection #

DescriptiveComplexity.SecondOrderRelPull pulls a second-order sentence back through a relativized interpretation, and observes that the transfer of assignments is only a retraction: a relation variable of the pulled block ranges over all tagged tuples, and may hold of tuples that are not points of the target. That is harmless for deciding, and fatal for counting, every assignment of the target being counted once per way of filling in the tuples outside the domain.

The repair is one conjunct in the kernel, DescriptiveComplexity.supportSentence: every pulled relation variable holds only of tuples all of whose points are in the domain. On such supported assignments the read-back is injective (DescriptiveComplexity.SOBlock.pullAssignRel_readAssignRel), so the witnesses of the kernel in the target are, bijectively, the supported witnesses of the pulled kernel in the source (DescriptiveComplexity.witnessCount_mapRel).

Supported assignments #

source
def DescriptiveComplexity.SOBlock.Supported {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} {A : Type} [L₁.Structure A] (B : SOBlock) (J : RelFOInterpretation L₁ L₂ Tag dm) (σ : (pull Tag dm B).Assignment A) :
Prop

An assignment of the pulled block is supported by the domain of a relativized interpretation when each of its relations holds only of tuples all of whose points are in the domain.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.SOBlock.supported_pullAssignRel {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} {A : Type} [L₁.Structure A] (B : SOBlock) (J : RelFOInterpretation L₁ L₂ Tag dm) (ρ : B.Assignment (J.MapRel A)) :
    B.Supported J (B.pullAssignRel J ρ)

    A transferred assignment is supported.

    Dependency graph
    source
    theorem DescriptiveComplexity.SOBlock.pullAssignRel_readAssignRel {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} {A : Type} [L₁.Structure A] (B : SOBlock) (J : RelFOInterpretation L₁ L₂ Tag dm) {σ : (pull Tag dm B).Assignment A} (hσ : B.Supported J σ) :
    B.pullAssignRel J (B.readAssignRel J σ) = σ

    On supported assignments the read-back is injective: transferring the read-back of a supported assignment returns it.

    Dependency graph
    source
    noncomputable def DescriptiveComplexity.supportSentence {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} (J : RelFOInterpretation L₁ L₂ Tag dm) (B : SOBlock) :
    (L₁.sum (SOBlock.pull Tag dm B).lang).Sentence

    The sentence saying that the assignment of the pulled block is supported: for each relation variable, at each tuple it holds of, every point of the tuple satisfies the domain formula of its tag.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Dependency graph

      Witness counts through a relativized interpretation #

      source
      theorem DescriptiveComplexity.witnessCount_mapRel {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {dm : ℕ} [L₂.IsRelational] (J : RelFOInterpretation L₁ L₂ Tag dm) (B : SOBlock) (φ : (L₂.sum B.lang).Sentence) (A : Type) [L₁.Structure A] :
      witnessCount B φ (J.MapRel A) = witnessCount (SOBlock.pull Tag dm B) ((J.extendSORel B).pullRelSentence φ ⊓ supportSentence J B) A

      Pulling a witness count back through a relativized interpretation: the witnesses of a kernel in the definable structure are, bijectively, the supported witnesses of the pulled kernel in the base structure.

      Dependency graph

      Closure #

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

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

      Dependency graph