Composition of relativized first-order reductions

Transitivity of P ≤ʳᶠᵒ[≤] Q (DescriptiveComplexity.RelOrderedFOReduction.trans), the relativized analogue of DescriptiveComplexity.OrderedFOReduction.trans. This is the one piece the hardness rewiring for relativized reductions needs that does not reduce to DescriptiveComplexity.OrderedFOReduction.toRel.

The plain composition of DescriptiveComplexity.Composition pulls the outer relation formulas back through the inner interpretation with quantifiers ranging over the whole inner universe Tag × A^dim. On the definable subset that is wrong: an outer quantifier must range over the in-domain points only. The fix is a guarded pullback DescriptiveComplexity.RelFOInterpretation.pullRel, which conjoins each quantifier block with the inner domain formula, and whose pullback theorem DescriptiveComplexity.RelFOInterpretation.realize_pullRel carries an “environment is in-domain” hypothesis. The composite domain formula is then the conjunction of the inner domains (one per outer coordinate) with the pulled-back outer domain, and the two decompose in exactly the way realize_pullRel needs.

Guarded pullback of a formula through a relativized interpretation

def DescriptiveComplexity.RelFOInterpretation.liftEnvRel {L₁ L₂ : FirstOrder.Language} {Tag : Type} {d : ℕ} (I : RelFOInterpretation L₁ L₂ Tag d) {A : Type} [L₁.Structure A] {γ : Type} (τ : γ → Tag) (v : γ × Fin d → A) (hv : ∀ (b : γ), (I.domFormula (τ b)).Realize fun (j : Fin d) => v (b, j)) (b : γ) : I.MapRel A

The in-domain environment of the relativized interpreted structure induced by tags τ, coordinates v, and a proof hv that each variable's coordinates satisfy its tag's domain formula.

Equations

• I.liftEnvRel τ v hv b = ⟨(τ b, fun (j : Fin d) => v (b, j)), ⋯⟩

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

Guarded pullback of an L₂-formula through the relativized interpretation I: as DescriptiveComplexity.FOInterpretation.pull, but each quantifier block is guarded by the domain formula of its tag, so that it ranges over the definable subset I.MapRel A rather than all of Tag × A^dim.

Equations

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

theorem DescriptiveComplexity.RelFOInterpretation.realize_pullRel {L₁ L₂ : FirstOrder.Language} {Tag : Type} {d : ℕ} {β : Type} (I : RelFOInterpretation L₁ L₂ Tag d) [L₂.IsRelational] [Finite Tag] {A : Type} [L₁.Structure A] {n : ℕ} (φ : L₂.BoundedFormula β n) (τ : β ⊕ Fin n → Tag) (v : (β ⊕ Fin n) × Fin d → A) (hv : ∀ (b : β ⊕ Fin n), (I.domFormula (τ b)).Realize fun (j : Fin d) => v (b, j)) : (I.pullRel φ τ).Realize v ↔ φ.Realize (I.liftEnvRel τ v hv ∘ Sum.inl) (I.liftEnvRel τ v hv ∘ Sum.inr)

Composition of relativized interpretations

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

The composite of two relativized interpretations: like DescriptiveComplexity.FOInterpretation.comp, but the relation formulas are pulled back with the guarded pullback, and the domain formula asks each outer coordinate's inner tuple to be in the inner domain and the outer tuple (of inner points) to be in the outer domain.

Equations

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

theorem DescriptiveComplexity.RelFOInterpretation.realize_compRel_domFormula {L₁ L₂ L₃ : FirstOrder.Language} {Tag₁ Tag₂ : Type} {d₁ d₂ : ℕ} [L₂.IsRelational] [Finite Tag₁] (J : RelFOInterpretation L₂ L₃ Tag₂ d₂) (I : RelFOInterpretation L₁ L₂ Tag₁ d₁) {A : Type} [L₁.Structure A] (T : Tag₂ × (Fin d₂ → Tag₁)) (coords : Fin (d₂ * d₁) → A) : ((J.compRel I).domFormula T).Realize coords ↔ ∃ (h : ∀ (k : Fin d₂), (I.domFormula (T.2 k)).Realize fun (j : Fin d₁) => coords (finProdFinEquiv (k, j))), (J.domFormula T.1).Realize fun (k : Fin d₂) => ⟨(T.2 k, fun (j : Fin d₁) => coords (finProdFinEquiv (k, j))), ⋯⟩

The composite domain decomposes: each outer coordinate is in the inner domain, and – given that – the outer tuple of inner points is in the outer domain.

noncomputable def DescriptiveComplexity.RelFOInterpretation.compEquivRel {L₁ L₂ L₃ : FirstOrder.Language} {Tag₁ Tag₂ : Type} {d₁ d₂ : ℕ} [L₂.IsRelational] [Finite Tag₁] (J : RelFOInterpretation L₂ L₃ Tag₂ d₂) (I : RelFOInterpretation L₁ L₂ Tag₁ d₁) {A : Type} [L₁.Structure A] : (J.compRel I).MapRel A ≃ J.MapRel (I.MapRel A)

The universe of the composite relativized interpretation is equivalent to the twice-interpreted universe, as subtypes.

Equations

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

theorem DescriptiveComplexity.RelFOInterpretation.relMap_compRel {L₁ L₂ L₃ : FirstOrder.Language} {Tag₁ Tag₂ : Type} {d₁ d₂ : ℕ} [L₂.IsRelational] [L₃.IsRelational] [Finite Tag₁] (J : RelFOInterpretation L₂ L₃ Tag₂ d₂) (I : RelFOInterpretation L₁ L₂ Tag₁ d₁) {A : Type} [L₁.Structure A] {n : ℕ} (R : L₃.Relations n) (x : Fin n → (J.compRel I).MapRel A) : FirstOrder.Language.Structure.RelMap R x ↔ FirstOrder.Language.Structure.RelMap R (⇑(J.compEquivRel I) ∘ x)

noncomputable def DescriptiveComplexity.RelFOInterpretation.compLEquivRel {L₁ L₂ L₃ : FirstOrder.Language} {Tag₁ Tag₂ : Type} {d₁ d₂ : ℕ} [L₂.IsRelational] [L₃.IsRelational] [Finite Tag₁] (J : RelFOInterpretation L₂ L₃ Tag₂ d₂) (I : RelFOInterpretation L₁ L₂ Tag₁ d₁) {A : Type} [L₁.Structure A] : L₃.Equiv ((J.compRel I).MapRel A) (J.MapRel (I.MapRel A))

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

Equations

• J.compLEquivRel I = { toEquiv := J.compEquivRel I, map_fun' := ⋯, map_rel' := ⋯ }

Extending a relativized interpretation with the lexicographic order

noncomputable def DescriptiveComplexity.RelFOInterpretation.ordExtendRel {L₁ L₂ : FirstOrder.Language} {T : Type} [LinearOrder T] {d : ℕ} (I : RelFOInterpretation (L₁.sum FirstOrder.Language.order) L₂ T d) : RelFOInterpretation (L₁.sum FirstOrder.Language.order) (L₂.sum FirstOrder.Language.order) T d

Extension of a relativized interpretation over an ordered base to one whose target carries the order vocabulary, interpreted by the lexicographic order on tagged tuples. The domain formula is unchanged.

Equations

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

@[instance_reducible]

noncomputable def DescriptiveComplexity.RelFOInterpretation.mapRelLinearOrder {L₁ L₂ : FirstOrder.Language} {T : Type} [LinearOrder T] {d : ℕ} (I : RelFOInterpretation (L₁.sum FirstOrder.Language.order) L₂ T d) (A : Type) [L₁.Structure A] [LinearOrder A] : LinearOrder (I.MapRel A)

The lexicographic linear order on the relativized interpreted universe, restricted from the tagged-tuple order along Subtype.val.

Equations

• I.mapRelLinearOrder A = LinearOrder.lift' Subtype.val ⋯

noncomputable def DescriptiveComplexity.RelFOInterpretation.ordExtendRelLEquiv {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {T : Type} [LinearOrder T] {d : ℕ} (I : RelFOInterpretation (L₁.sum FirstOrder.Language.order) L₂ T d) (A : Type) [L₁.Structure A] [LinearOrder A] : (L₂.sum FirstOrder.Language.order).Equiv (I.ordExtendRel.MapRel A) (I.MapRel A)

The order-extended relativized interpretation produces exactly the original relativized interpreted structure equipped with the lexicographic order.

Equations

• I.ordExtendRelLEquiv A = { toEquiv := Equiv.refl (I.ordExtendRel.MapRel A), map_fun' := ⋯, map_rel' := ⋯ }

Transitivity of relativized ordered reductions

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

Transitivity of relativized ordered FO reductions: if P ≤ʳᶠᵒ[≤] Q and Q ≤ʳᶠᵒ[≤] R, then P ≤ʳᶠᵒ[≤] R. The intermediate definable structure is ordered by the lexicographic order on tagged tuples, restricted to the domain.

Equations

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

@[instance_reducible]

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

Trans instance for relativized ordered FO reductions.

Equations

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