Tagged tuple interpretation semantics

Tagged FO interpretations have exact output size tags * card ^ dim and preserve isomorphisms. Consequently, pulling a query back through their structure map preserves isomorphism invariance. A two-copy graph construction demonstrates that this extends the expressive scope of universe-preserving interpretations.

Interpretation.Pullback proves general formula transport and closure of FO definability. Interpretation.Composition gives composition up to isomorphism, and TaggedReduction derives the reduction preorder on invariant problems.

@[simp]

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.apply_card {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (A : FinStruct V) : (I.apply A).card = tags * A.card ^ dim

The interpreted universe has exactly tags * card ^ dim elements.

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.mapElement {tags dim card₁ card₂ : ℕ} (f : Fin card₁ → Fin card₂) (x : Fin (tags * card₁ ^ dim)) : Fin (tags * card₂ ^ dim)

Map the coordinates of an interpreted element, keeping its tag.

Equations

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

@[simp]

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.elementEquiv_mapElement {tags dim card₁ card₂ : ℕ} (f : Fin card₁ → Fin card₂) (x : Fin (tags * card₁ ^ dim)) : (elementEquiv card₂ tags dim) (mapElement f x) = (((elementEquiv card₁ tags dim) x).1, f ∘ ((elementEquiv card₁ tags dim) x).2)

Decoding a mapped element exposes its unchanged tag and mapped coordinates.

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.relationEnv_mapElement {tags dim card₁ card₂ arity : ℕ} (f : Fin card₁ → Fin card₂) (args : Fin arity → Fin (tags * card₁ ^ dim)) : relationEnv (mapElement f ∘ args) = f ∘ relationEnv args

Coordinate mapping commutes with flattening relation arguments.

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.mapIso {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) {A B : FinStruct V} (f : Iso A B) : Iso (I.apply A) (I.apply B)

An input isomorphism acts coordinatewise on tagged tuples.

Equations

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

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.pullQuery {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (Q : BooleanQuery W) : BooleanQuery V

Pull back a query along the tagged structure map.

Equations

• I.pullQuery Q A = Q (I.apply A)

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.pullQuery_orderIndependent {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) {Q : BooleanQuery W} (hQ : Q.IsOrderIndependent) : (I.pullQuery Q).IsOrderIndependent

Isomorphism-invariant queries remain invariant under tagged interpretation.

def Complexity.DescriptiveComplexity.FOInterpretation.toTagged {V W : Vocabulary} (I : FOInterpretation V W) : TaggedFOInterpretation V W 1 1

Regard a universe-preserving interpretation as a one-tag, one-coordinate interpretation.

Equations

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

def Complexity.DescriptiveComplexity.FOInterpretation.toTaggedIso {V W : Vocabulary} (I : FOInterpretation V W) (A : FinStruct V) : Iso (I.toTagged.apply A) (I.apply A)

The old and new presentations of a dimension-one interpretation are isomorphic.

Equations

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

theorem Complexity.DescriptiveComplexity.FOInterpretation.toTagged_query {V W : Vocabulary} (I : FOInterpretation V W) (A : FinStruct V) {Q : BooleanQuery W} (hQ : Q.IsOrderIndependent) : Q (I.toTagged.apply A) ↔ Q (I.apply A)

An invariant query sees the same result through either dimension-one presentation.