Documentation

Complexitylib.DescriptiveComplexity.Interpretation.Composition

Composition and identity for tagged interpretations #

Composition preserves the interpreted structure up to isomorphism. Its tag count is t₂ * t₁ ^ d₂, its dimension is d₂ * d₁, and invariant queries give the same answer under composition or successive application. The one-tag, dimension-one identity is likewise an identity up to isomorphism.

These are the semantic laws needed for first-order reductions, following Immerman, Chapter 3, and the tagged presentation of Senellart--Gnatenko (2026).

source
def Complexity.DescriptiveComplexity.TaggedFOInterpretation.idInterp (V : Vocabulary) :
TaggedFOInterpretation V V 1 1

The identity tagged interpretation has one tag and one coordinate.

Equations
Instances For
    source
    def Complexity.DescriptiveComplexity.TaggedFOInterpretation.idIso {V : Vocabulary} (A : FinStruct V) :
    Iso ((idInterp V).apply A) A

    The identity interpreted structure is canonically isomorphic to its input.

    Equations
    Instances For
      source
      theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.comp_query {U V W : Vocabulary} {t₁ d₁ t₂ d₂ : ℕ} (I₂ : TaggedFOInterpretation V W t₂ d₂) (I₁ : TaggedFOInterpretation U V t₁ d₁) (A : FinStruct U) {Q : BooleanQuery W} (hQ : Q.IsOrderIndependent) :
      Q ((I₂.comp I₁).apply A) ↔ Q (I₂.apply (I₁.apply A))

      Invariant queries cannot distinguish composition from successive application.

      source
      theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.translateSentence_comp_models {U V W : Vocabulary} {t₁ d₁ t₂ d₂ : ℕ} (I₂ : TaggedFOInterpretation V W t₂ d₂) (I₁ : TaggedFOInterpretation U V t₁ d₁) (A : FinStruct U) (φ : Sentence W) :
      Sentence.Models A ((I₂.comp I₁).translateSentence φ) ↔ Sentence.Models A (I₁.translateSentence (I₂.translateSentence φ))

      Translating along a composite agrees semantically with successive translations.