Composition of tagged interpretations

Composing (t₁, d₁) with (t₂, d₂) gives tag count t₂ * t₁ ^ d₂ and dimension d₂ * d₁. A composite tag records an outer tag and one inner tag for each outer coordinate. Coordinates are flattened with finProdFinEquiv. The outer relation formulas are pulled back through the inner interpretation.

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.compTags {t₁ t₂ d₂ arity : ℕ} (τ : Fin arity → Fin (t₂ * t₁ ^ d₂)) : Fin (arity * d₂) → Fin t₁

Expand composite tags to the tags of the inner elements of each argument.

Equations

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

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.compCoords (U : Vocabulary) (arity d₁ d₂ : ℕ) : Fin (arity * d₂) → Fin d₁ → Term U (arity * (d₂ * d₁))

Source variables for the inner coordinates, in flattened argument-coordinate order.

Equations

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

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.comp {U V W : Vocabulary} {t₁ d₁ t₂ d₂ : ℕ} (I₂ : TaggedFOInterpretation V W t₂ d₂) (I₁ : TaggedFOInterpretation U V t₁ d₁) : TaggedFOInterpretation U W (t₂ * t₁ ^ d₂) (d₂ * d₁)

Compose tagged interpretations, recording all inner tags in the composite tag.

Equations

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

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.unflattenElement (card t₁ d₁ t₂ d₂ : ℕ) (x : Fin (t₂ * t₁ ^ d₂ * card ^ (d₂ * d₁))) : Fin (t₂ * (t₁ * card ^ d₁) ^ d₂)

Decode a composite element as an outer element whose coordinates are inner elements.

Equations

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

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.flattenElement (card t₁ d₁ t₂ d₂ : ℕ) (x : Fin (t₂ * (t₁ * card ^ d₁) ^ d₂)) : Fin (t₂ * t₁ ^ d₂ * card ^ (d₂ * d₁))

Flatten an outer element, retaining every inner tag and coordinate.

Equations

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