Pulling SO-Horn definability back through an interpretation

SO-Horn definability is closed under (ordered) first-order reductions (DescriptiveComplexity.SigmaSOHornDefinable.of_orderedReduction). This is what makes the fragment a DescriptiveComplexity.ComplexityClass – the class DescriptiveComplexity.PTIME – rather than a mere definability predicate.

The closure is not an instance of the general pullback of DescriptiveComplexity.SecondOrderPull, which only says that the pulled-back kernel is some first-order formula: here the pulled-back kernel has to stay Horn. It does, and for a structural reason worth stating, since it is exactly what the Horn condition is careful about: the condition constrains the occurrences of the second-order variables only, while an interpretation rewrites the input-vocabulary atoms – which live in the guard, where anything is allowed. Concretely, pulling a clause back through a d-dimensional interpretation with tag type Tag:

• the block is pulled as in DescriptiveComplexity.SOBlock.pull: an n-ary relation variable on Tag × A^d becomes one (n·d)-ary relation variable on A per n-tuple of tags;
• a clause becomes one clause per assignment t : Fin k → Tag of tags to its universally quantified variables (DescriptiveComplexity.HornClause.pull), with the k variables replaced by k · d coordinates;
• its guard becomes the ordinary formula pullback DescriptiveComplexity.FOInterpretation.pull at the tag assignment t – an arbitrary first-order formula, which is fine, guards being unconstrained;
• each body and head atom becomes the atom of the corresponding pulled relation variable (DescriptiveComplexity.SOAtom.pull) – still an atom, which is what keeps the clause Horn.

The one place the order is needed is that the guards of the target may mention it: the pullback interprets the target's order by the lexicographic order on tagged tuples (DescriptiveComplexity.FOInterpretation.ordExtend), which is why the definability notion quantifies over ordered structures in the first place.

Pulling back a clause and a program

noncomputable def DescriptiveComplexity.HornClause.pull {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {d : ℕ} {B : SOBlock} {k : ℕ} [L₂.IsRelational] (I : FOInterpretation L₁ L₂ Tag d) (c : HornClause L₂ B k) (t : Fin k → Tag) : HornClause L₁ (SOBlock.pull Tag d B) (k * d)

The pullback of a Horn clause at a tag assignment: guards pull back as formulas, atoms as atoms – so the result is again a Horn clause.

Equations

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

theorem DescriptiveComplexity.HornClause.pull_holds {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {d : ℕ} {B : SOBlock} {k : ℕ} [L₂.IsRelational] {A : Type} [L₁.Structure A] (I : FOInterpretation L₁ L₂ Tag d) (c : HornClause L₂ B k) (t : Fin k → Tag) (ρ : B.Assignment (I.Map A)) (w : Fin (k * d) → A) : (pull I c t).Holds (B.pullAssign ρ) w ↔ c.Holds ρ (tagVal I t w)

noncomputable def DescriptiveComplexity.HornProgram.pull {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {d : ℕ} {B : SOBlock} {k : ℕ} [L₂.IsRelational] (I : FOInterpretation L₁ L₂ Tag d) (prog : HornProgram L₂ B k) : HornProgram L₁ (SOBlock.pull Tag d B) (k * d)

The pullback of a Horn program: one clause per clause of the program and per assignment of tags to its universally quantified variables.

Equations

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

theorem DescriptiveComplexity.HornProgram.pull_mem {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {d : ℕ} {B : SOBlock} {k : ℕ} [L₂.IsRelational] (I : FOInterpretation L₁ L₂ Tag d) {prog : HornProgram L₂ B k} {c : HornClause L₂ B k} (hc : c ∈ prog) (t : Fin k → Tag) : HornClause.pull I c t ∈ pull I prog

theorem DescriptiveComplexity.HornProgram.pull_cases {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {d : ℕ} {B : SOBlock} {k : ℕ} [L₂.IsRelational] (I : FOInterpretation L₁ L₂ Tag d) {prog : HornProgram L₂ B k} {c' : HornClause L₁ (SOBlock.pull Tag d B) (k * d)} (hc' : c' ∈ pull I prog) : ∃ c ∈ prog, ∃ (t : Fin k → Tag), c' = HornClause.pull I c t

Correctness of the pullback

theorem DescriptiveComplexity.HornProgram.pull_holds {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {d : ℕ} {B : SOBlock} {k : ℕ} [L₂.IsRelational] {A : Type} [L₁.Structure A] (I : FOInterpretation L₁ L₂ Tag d) (prog : HornProgram L₂ B k) (ρ : B.Assignment (I.Map A)) : (pull I prog).Holds (B.pullAssign ρ) ↔ prog.Holds ρ

An assignment satisfies a program on the interpreted structure iff its transfer satisfies the pulled program on the base structure.

theorem DescriptiveComplexity.exists_holds_pull {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {d : ℕ} {B : SOBlock} {k : ℕ} [L₂.IsRelational] {A : Type} [L₁.Structure A] (I : FOInterpretation L₁ L₂ Tag d) (prog : HornProgram L₂ B k) : (∃ (ρ : B.Assignment (I.Map A)), prog.Holds ρ) ↔ ∃ (σ : (SOBlock.pull Tag d B).Assignment A), (HornProgram.pull I prog).Holds σ

The pullback is correct: the program is satisfiable on the interpreted structure iff its pullback is satisfiable on the base structure.

Closure under reductions

theorem DescriptiveComplexity.SigmaSOHornDefinable.of_orderedReduction {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : OrderedFOReduction P Q) (h : SigmaSOHornDefinable Q) : SigmaSOHornDefinable P

SO-Horn definability is closed under ordered first-order reductions. The Horn shape survives the pullback because an interpretation only rewrites the input-vocabulary atoms, which live in the guards; the second-order atoms are merely re-indexed.

theorem DescriptiveComplexity.SigmaSOHornDefinable.of_foReduction {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : FOReduction P Q) (h : SigmaSOHornDefinable Q) : SigmaSOHornDefinable P

SO-Horn definability is closed under first-order reductions.