Composition of first-order reductions (transitivity)

The composite of two FO interpretations is an FO interpretation (DescriptiveComplexity.FOInterpretation.comp), and hence FO reducibility is transitive (DescriptiveComplexity.FOReduction.trans): from P ≤ᶠᵒ Q and Q ≤ᶠᵒ R one gets P ≤ᶠᵒ R.

The composite of an interpretation I : FOInterpretation L₁ L₂ Tag₁ d₁ with J : FOInterpretation L₂ L₃ Tag₂ d₂ has tags Tag₂ × (Fin d₂ → Tag₁) and dimension d₂ * d₁: an element of the composite universe carries the outer tag, one inner tag per outer coordinate, and a d₂ × d₁ matrix of elements. Its defining formulas are obtained by pulling back the defining L₂-formulas of J through I (DescriptiveComplexity.FOInterpretation.pull): atoms become the defining formulas of I, equality becomes componentwise equality (with tags compared statically), and a quantifier over the universe of I.Map A becomes a finite conjunction/disjunction over Tag₁ of a block of d₁ quantifiers over A.

Two points deserve attention:

• the composite's universe (Tag₂ × (Fin d₂ → Tag₁)) × A^(d₂·d₁) is only isomorphic (DescriptiveComplexity.FOInterpretation.compLEquiv), not equal, to the twice-interpreted J.Map (I.Map A); transitivity therefore uses the isomorphism-invariance of the target problem, which is part of the notion of DecisionProblem;
• pulling back quantifiers requires enumerating the (finitely many) inner tags, so composite formulas are noncomputable (they are built with BoundedFormula.iInf); this does not affect any of the theorems.

Terms of a relational language are variables

These extend Mathlib's FirstOrder.Language.Term and live in its namespace (where Mathlib would want them, and where dot notation finds them).

def FirstOrder.Language.Term.varOf {L₂ : Language} [L₂.IsRelational] {γ : Type u_1} : L₂.Term γ → γ

In a relational language, every term is a variable.

Equations

• (FirstOrder.Language.var x_1).varOf = x_1
• (FirstOrder.Language.func f _ts).varOf = isEmptyElim f

@[simp]

theorem FirstOrder.Language.Term.varOf_var {L₂ : Language} [L₂.IsRelational] {γ : Type u_1} (x : γ) : (var x).varOf = x

@[simp]

theorem FirstOrder.Language.Term.realize_varOf {L₂ : Language} [L₂.IsRelational] {γ : Type u_1} {M : Type u_2} [L₂.Structure M] {v : γ → M} (t : L₂.Term γ) : realize v t = v t.varOf

Pulling back a formula through an interpretation

def DescriptiveComplexity.FOInterpretation.liftEnv {L₁ L₂ : FirstOrder.Language} {Tag : Type} {d : ℕ} (I : FOInterpretation L₁ L₂ Tag d) {A γ : Type} (τ : γ → Tag) (v : γ × Fin d → A) (b : γ) : I.Map A

The environment of the interpreted structure induced by tags τ and an environment v for the individual coordinates.

Equations

• I.liftEnv τ v b = (τ b, fun (j : Fin d) => v (b, j))

noncomputable def DescriptiveComplexity.FOInterpretation.pull {L₁ L₂ : FirstOrder.Language} {Tag : Type} {d : ℕ} {β : Type} (I : FOInterpretation L₁ L₂ Tag d) [L₂.IsRelational] [Finite Tag] {n : ℕ} : L₂.BoundedFormula β n → (β ⊕ Fin n → Tag) → L₁.Formula ((β ⊕ Fin n) × Fin d)

Pullback of an L₂-formula through the interpretation I, given a static assignment of tags to its (free and bound) variables: an L₁-formula on the coordinates which realizes in A exactly as the original formula realizes in I.Map A (see FOInterpretation.realize_pull). Quantified variables are expanded into a conjunction over the (finitely many) tags of a block of d quantifiers.

Equations

• One or more equations did not get rendered due to their size.
• I.pull FirstOrder.Language.BoundedFormula.falsum x✝ = ⊥
• I.pull (φ.imp ψ) x✝ = (I.pull φ x✝).imp (I.pull ψ x✝)

theorem DescriptiveComplexity.FOInterpretation.realize_pull {L₁ L₂ : FirstOrder.Language} {Tag : Type} {d : ℕ} (I : FOInterpretation L₁ L₂ Tag d) {β : Type} [L₂.IsRelational] [Finite Tag] {A : Type} [L₁.Structure A] {n : ℕ} (φ : L₂.BoundedFormula β n) (τ : β ⊕ Fin n → Tag) (v : (β ⊕ Fin n) × Fin d → A) : (I.pull φ τ).Realize v ↔ φ.Realize (I.liftEnv τ v ∘ Sum.inl) (I.liftEnv τ v ∘ Sum.inr)

Composition of interpretations

noncomputable def DescriptiveComplexity.FOInterpretation.comp {L₁ L₂ L₃ : FirstOrder.Language} {Tag₁ Tag₂ : Type} {d₁ d₂ : ℕ} [L₂.IsRelational] [Finite Tag₁] (J : FOInterpretation L₂ L₃ Tag₂ d₂) (I : FOInterpretation L₁ L₂ Tag₁ d₁) : FOInterpretation L₁ L₃ (Tag₂ × (Fin d₂ → Tag₁)) (d₂ * d₁)

The composite of two FO interpretations: tags are an outer tag together with one inner tag per outer coordinate, and dimensions multiply. Its interpretation of a structure A is isomorphic to J.Map (I.Map A) (FOInterpretation.compLEquiv).

Equations

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

def DescriptiveComplexity.FOInterpretation.compEquiv {L₁ L₂ L₃ : FirstOrder.Language} {Tag₁ Tag₂ : Type} {d₁ d₂ : ℕ} [L₂.IsRelational] [Finite Tag₁] (J : FOInterpretation L₂ L₃ Tag₂ d₂) (I : FOInterpretation L₁ L₂ Tag₁ d₁) (A : Type) : (J.comp I).Map A ≃ J.Map (I.Map A)

The universe of the composite interpretation is equivalent to the twice-interpreted universe.

Equations

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

theorem DescriptiveComplexity.FOInterpretation.relMap_comp {L₁ L₂ L₃ : FirstOrder.Language} {Tag₁ Tag₂ : Type} {d₁ d₂ : ℕ} [L₂.IsRelational] [L₃.IsRelational] [Finite Tag₁] (J : FOInterpretation L₂ L₃ Tag₂ d₂) (I : FOInterpretation L₁ L₂ Tag₁ d₁) (A : Type) [L₁.Structure A] {n : ℕ} (R : L₃.Relations n) (x : Fin n → (J.comp I).Map A) : FirstOrder.Language.Structure.RelMap R x ↔ FirstOrder.Language.Structure.RelMap R (⇑(J.compEquiv I A) ∘ x)

Transitivity of FO reductions

noncomputable def DescriptiveComplexity.FOInterpretation.compLEquiv {L₁ L₂ L₃ : FirstOrder.Language} {Tag₁ Tag₂ : Type} {d₁ d₂ : ℕ} [L₂.IsRelational] [L₃.IsRelational] [Finite Tag₁] (J : FOInterpretation L₂ L₃ Tag₂ d₂) (I : FOInterpretation L₁ L₂ Tag₁ d₁) (A : Type) [L₁.Structure A] : L₃.Equiv ((J.comp I).Map A) (J.Map (I.Map A))

The universe equivalence of the composite interpretation is an L₃-isomorphism.

Equations

• J.compLEquiv I A = { toEquiv := J.compEquiv I A, map_fun' := ⋯, map_rel' := ⋯ }

noncomputable def DescriptiveComplexity.FOReduction.trans {L₁ L₂ L₃ : FirstOrder.Language} [L₂.IsRelational] [L₃.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {R : DecisionProblem L₃} (g : FOReduction P Q) (f : FOReduction Q R) : FOReduction P R

Transitivity of FO reductions: if P ≤ᶠᵒ Q and Q ≤ᶠᵒ R, then P ≤ᶠᵒ R. The composite interpretation is only isomorphic, not equal, to the twice-applied one, so the isomorphism-invariance built into DecisionProblem is used to conclude.

Equations

• g.trans f = { Tag := f.Tag × (Fin f.dim → g.Tag), tagFinite := ⋯, tagNonempty := ⋯, dim := f.dim * g.dim, toInterpretation := f.toInterpretation.comp g.toInterpretation, correct := ⋯ }

@[instance_reducible]

noncomputable instance DescriptiveComplexity.instTransDecisionProblemFOReduction {L₁ L₂ L₃ : FirstOrder.Language} [L₂.IsRelational] [L₃.IsRelational] : Trans FOReduction FOReduction FOReduction

Trans instance for FO reductions, enabling calc chains P ≤ᶠᵒ Q ≤ᶠᵒ R.

Equations

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

Reflexivity and the preorder structure

def DescriptiveComplexity.FOInterpretation.refl (L : FirstOrder.Language) : FOInterpretation L L Unit 1

The identity interpretation of a language in itself (one tag, dimension one).

Equations

• DescriptiveComplexity.FOInterpretation.refl L = { relFormula := fun {_n : ℕ} (R : L.Relations _n) (x : Fin _n → Unit) => R.formula fun (i : Fin _n) => FirstOrder.Language.var (i, 0) }

def DescriptiveComplexity.FOInterpretation.reflLEquiv (L : FirstOrder.Language) [L.IsRelational] (A : Type) [L.Structure A] : L.Equiv ((refl L).Map A) A

The identity interpretation of a structure is isomorphic to the structure itself.

Equations

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

def DescriptiveComplexity.FOReduction.refl {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : FOReduction P P

Reflexivity of FO reductions: every decision problem (over a relational language) reduces to itself, via the identity interpretation.

Equations

• DescriptiveComplexity.FOReduction.refl P = { Tag := Unit, tagFinite := ⋯, tagNonempty := ⋯, dim := 1, toInterpretation := DescriptiveComplexity.FOInterpretation.refl L, correct := ⋯ }

@[instance_reducible]

instance DescriptiveComplexity.instPreorderDecisionProblem {L : FirstOrder.Language} [L.IsRelational] : Preorder (DecisionProblem L)

FO reducibility is a preorder on the decision problems over a fixed relational language, with P ≤ Q the propositional truncation of P ≤ᶠᵒ Q. (Across different languages, reflexivity FOReduction.refl and transitivity FOReduction.trans express the same fact in heterogeneous form.)

Equations

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

theorem DescriptiveComplexity.DecisionProblem.le_def {L : FirstOrder.Language} [L.IsRelational] {P Q : DecisionProblem L} : P ≤ Q ↔ Nonempty (FOReduction P Q)