Pulling SO-Krom definability back through an interpretation

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

The argument is the one of DescriptiveComplexity.SecondOrderHornPull, and it works for the same structural reason: the Krom 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. 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.KromClause.pull), with the k variables replaced by k · d coordinates;
• its guard becomes the ordinary formula pullback DescriptiveComplexity.guardPull at the tag assignment t – an arbitrary first-order formula, which is fine, guards being unconstrained;
• each literal keeps its sign and its atom becomes the atom of the corresponding pulled relation variable (DescriptiveComplexity.SOAtom.pull), so the clause still has at most two second-order literals – which is what keeps it Krom.

The shared pieces (DescriptiveComplexity.SOAtom.pull, DescriptiveComplexity.guardPull, DescriptiveComplexity.tagVal, DescriptiveComplexity.allTagAssign) are in DescriptiveComplexity.SecondOrderPull, and the order enters exactly as it does for SO-Horn: the pullback interprets the target's order by the lexicographic order on tagged tuples (DescriptiveComplexity.FOInterpretation.ordExtend).

Pulling back a literal, a clause and a program

def DescriptiveComplexity.KromLit.pull {Tag : Type} [Finite Tag] {B : SOBlock} {k : ℕ} (l : KromLit B k) (d : ℕ) (t : Fin k → Tag) : KromLit (SOBlock.pull Tag d B) (k * d)

The pullback of a literal: same sign, pulled atom.

Equations

• l.pull d t = { atom := l.atom.pull d t, positive := l.positive }

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

theorem DescriptiveComplexity.KromLit.slotHolds_pull {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {d : ℕ} {B : SOBlock} {k : ℕ} {A : Type} (I : FOInterpretation L₁ L₂ Tag d) (o : Option (KromLit B k)) (t : Fin k → Tag) (ρ : B.Assignment (I.Map A)) (w : Fin (k * d) → A) : slotHolds (Option.map (fun (l : KromLit B k) => l.pull d t) o) (B.pullAssign ρ) w ↔ slotHolds o ρ (tagVal I t w)

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

The pullback of a Krom clause at a tag assignment: guards pull back as formulas, literals keep their signs – so the result is again a Krom clause.

Equations

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

theorem DescriptiveComplexity.KromClause.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 : KromClause 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.KromProgram.pull {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {d : ℕ} {B : SOBlock} {k : ℕ} [L₂.IsRelational] (I : FOInterpretation L₁ L₂ Tag d) (prog : KromProgram L₂ B k) : KromProgram L₁ (SOBlock.pull Tag d B) (k * d)

The pullback of a Krom 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.KromProgram.pull_mem {L₁ L₂ : FirstOrder.Language} {Tag : Type} [Finite Tag] {d : ℕ} {B : SOBlock} {k : ℕ} [L₂.IsRelational] (I : FOInterpretation L₁ L₂ Tag d) {prog : KromProgram L₂ B k} {c : KromClause L₂ B k} (hc : c ∈ prog) (t : Fin k → Tag) : KromClause.pull I c t ∈ pull I prog

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

Correctness of the pullback

theorem DescriptiveComplexity.KromProgram.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 : KromProgram 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.KromProgram.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 : KromProgram L₂ B k) : (∃ (ρ : B.Assignment (I.Map A)), prog.Holds ρ) ↔ ∃ (σ : (SOBlock.pull Tag d B).Assignment A), (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.SigmaSOKromDefinable.of_orderedReduction {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : OrderedFOReduction P Q) (h : SigmaSOKromDefinable Q) : SigmaSOKromDefinable P

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

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

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