Simulating a k-variable induction on the invariant structure

The forward simulation of the Abiteboul–Vianu argument (DescriptiveComplexity.AbiteboulVianu): a simultaneous induction within the k-variable budget runs, step for step, on the invariant structure Iᵏ A (DescriptiveComplexity.InvMap). Its stage relations are ≡ᵏ-invariant (DescriptiveComplexity.Invariant.Stages), so they are unary relations on the classes; one application of a step formula is evaluated on the classes by the pebble compiler (DescriptiveComplexity.pebbleCompile), which translates a formula over the base vocabulary expanded by the block into a formula over the invariant vocabulary expanded by the unary copy of the block (DescriptiveComplexity.classBlock), one free class variable standing for the current pebble assignment:

• atomic formulas become atomic-type bits of the class;
• block atoms follow a rearrangement relation to the class of the reordered argument tuple, and read the unary relation variable there;
• a quantifier spends a fresh pebble: it becomes a quantifier over the classes reachable along that pebble's substitution relation.

The compiler is exact (DescriptiveComplexity.realize_pebbleCompile, the same pebble induction as the k-variable invariance lemma DescriptiveComplexity.realize_equivK, which also absorbs each re-choice of a representative); the induced induction on the invariant structure and the stage-by-stage tracking are DescriptiveComplexity.StepDef.invStepDef and its lemmas, further down.

The unary copy of a block

@[reducible]

def DescriptiveComplexity.classBlock (B : SOBlock) : SOBlock

The unary copy of a block: the same relation variables, all unary – on the invariant structure, an invariant relation is a set of classes. (Reducible so that numerals elaborate at the block's arities.)

Equations

• DescriptiveComplexity.classBlock B = { ι := B.ι, ιFinite := ⋯, arity := fun (x : B.ι) => 1 }

@[reducible, inline]

abbrev DescriptiveComplexity.invRelSym (L : FirstOrder.Language) (k : ℕ) (B : SOBlock) {n : ℕ} (r : InvRel L k n) : ((invLang L k).sum (classBlock B).lang).Relations n

The relation symbol of an invariant-vocabulary relation, in the expansion by the unary block.

Equations

• DescriptiveComplexity.invRelSym L k B r = Sum.inl r

The pebble compiler

def DescriptiveComplexity.blockSel {k l : ℕ} (sel : Fin l → Fin k) : Fin k → Fin k

The coordinate selection of a block atom, extended to a rearrangement of all k pebbles (fixing the pebbles beyond the atom's arity).

Equations

• DescriptiveComplexity.blockSel sel q = if hq : ↑q < l then sel ⟨↑q, hq⟩ else q

theorem DescriptiveComplexity.blockSel_castLE {k l : ℕ} (sel : Fin l → Fin k) {a : ℕ} (ha : a ≤ k) (hal : a = l) (j : Fin a) : blockSel sel (Fin.castLE ha j) = sel (Fin.cast hal j)

noncomputable def DescriptiveComplexity.pebbleCompile {L : FirstOrder.Language} {k : ℕ} {B : SOBlock} [L.IsRelational] {m : ℕ} (g : Fin m → Fin k) {n : ℕ} : (L.sum B.lang).BoundedFormula (Fin m) n → (Fin n → Fin k) → ((invLang L k).sum (classBlock B).lang).Formula (Fin 1)

The pebble compiler: a formula over the base vocabulary expanded by the block, its free variables read through the selection g and its bound variables through h, becomes a formula over the invariant vocabulary expanded by the unary block, with one free class variable. Atomic formulas read the atomic-type bits of the class; block atoms follow a rearrangement to the class of their argument tuple; each quantifier spends a fresh pebble, quantifying over the classes along its substitution relation. (When no fresh pebble is left the compiled formula is ⊥; the budget hypothesis of DescriptiveComplexity.realize_pebbleCompile rules the case out.)

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.pebbleCompile g FirstOrder.Language.BoundedFormula.falsum x✝ = ⊥
• DescriptiveComplexity.pebbleCompile g (f₁.imp f₂) x✝ = FirstOrder.Language.BoundedFormula.imp (DescriptiveComplexity.pebbleCompile g f₁ x✝) (DescriptiveComplexity.pebbleCompile g f₂ x✝)

Exactness of the compiler

theorem DescriptiveComplexity.realize_pebbleCompile {L : FirstOrder.Language} {k : ℕ} {B : SOBlock} [L.IsRelational] {S : Set ((n : ℕ) × L.Relations n)} {A : Type} [L.Structure A] [Finite A] {X : (classBlock B).Assignment (InvMap S k A)} {m : ℕ} {ρ : B.Assignment A} (hρ : AssignInvariant S A k ρ) (harity : ∀ (i : B.ι), B.arity i ≤ k) (hX : ∀ (i : B.ι) (w : Fin k → A), (X i fun (x : Fin ((classBlock B).arity i)) => InvMap.mk S w) ↔ ρ i fun (p : Fin (B.arity i)) => w (Fin.castLE ⋯ p)) {n : ℕ} (φ : (L.sum B.lang).BoundedFormula (Fin m) n) (g : Fin m → Fin k) (h : Fin n → Fin k) : Function.Injective h → (∀ (i : Fin m) (j : Fin n), g i ≠ h j) → (Finset.image g Finset.univ ∪ Finset.image h Finset.univ).card + qdepth φ ≤ k → RelsIn (blockRelsExtend S B) φ → ∀ (v : Fin k → A), ((pebbleCompile g φ h).Realize fun (x : Fin 1) => InvMap.mk S v) ↔ φ.Realize (fun (i : Fin m) => v (g i)) fun (j : Fin n) => v (h j)

Exactness of the pebble compiler: over an invariant block assignment ρ on A and its unary image X on the classes, the compiled formula holds at the class of v exactly when the original formula holds at the pebble assignment v. The induction is the one of the k-variable invariance lemma: each quantifier spends a fresh pebble, and re-choosing a representative is absorbed by the invariance lemma itself (DescriptiveComplexity.realize_equivK).

Sentences over an empty variable supply

def DescriptiveComplexity.sentenceFin0 {L' : FirstOrder.Language} (φ : L'.Sentence) : L'.Formula (Fin 0)

A sentence, re-typed over an empty supply of Fin-indexed variables, so that the pebble compiler applies to it.

Equations

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

theorem DescriptiveComplexity.qdepth_sentenceFin0 {L' : FirstOrder.Language} (φ : L'.Sentence) : qdepth (sentenceFin0 φ) = qdepth φ

theorem DescriptiveComplexity.relsIn_sentenceFin0 {L' : FirstOrder.Language} {S' : Set ((n : ℕ) × L'.Relations n)} {φ : L'.Sentence} (h : RelsIn S' φ) : RelsIn S' (sentenceFin0 φ)

theorem DescriptiveComplexity.realize_sentenceFin0 {L' : FirstOrder.Language} {M : Type} {instM : L'.Structure M} (φ : L'.Sentence) (v : Fin 0 → M) : (sentenceFin0 φ).Realize v ↔ M ⊨ φ

The induced induction on the invariant structure

def DescriptiveComplexity.invAssign {L : FirstOrder.Language} {k : ℕ} {B : SOBlock} (S : Set ((n : ℕ) × L.Relations n)) {A : Type} [L.Structure A] (harity : ∀ (i : B.ι), B.arity i ≤ k) (ρ : B.Assignment A) : (classBlock B).Assignment (InvMap S k A)

The unary image on the classes of a block assignment: the class of w is in the image of variable i when ρ holds at the initial coordinates of w.

Equations

• DescriptiveComplexity.invAssign S harity ρ i x = ∃ (w : Fin k → A), x 0 = DescriptiveComplexity.InvMap.mk S w ∧ ρ i fun (p : Fin (B.arity i)) => w (Fin.castLE ⋯ p)

theorem DescriptiveComplexity.invAssign_mk {L : FirstOrder.Language} {k : ℕ} {B : SOBlock} {S : Set ((n : ℕ) × L.Relations n)} {A : Type} [L.Structure A] {harity : ∀ (i : B.ι), B.arity i ≤ k} {ρ : B.Assignment A} (hρ : AssignInvariant S A k ρ) (i : B.ι) (w : Fin k → A) : (invAssign S harity ρ i fun (x : Fin ((classBlock B).arity i)) => InvMap.mk S w) ↔ ρ i fun (p : Fin (B.arity i)) => w (Fin.castLE ⋯ p)

theorem DescriptiveComplexity.invAssign_injOn {L : FirstOrder.Language} {k : ℕ} {B : SOBlock} {S : Set ((n : ℕ) × L.Relations n)} {A : Type} [L.Structure A] [Nonempty A] {harity : ∀ (i : B.ι), B.arity i ≤ k} {ρ₁ ρ₂ : B.Assignment A} (h₁ : AssignInvariant S A k ρ₁) (h₂ : AssignInvariant S A k ρ₂) (h : invAssign S harity ρ₁ = invAssign S harity ρ₂) : ρ₁ = ρ₂

The unary image determines an invariant assignment: read any tuple at an extension of its arguments.

theorem DescriptiveComplexity.StepDef.VarBound.arity_le {L : FirstOrder.Language} {d : StepDef L} {k : ℕ} (h : d.VarBound k) (i : d.B.ι) : d.B.arity i ≤ k

The arity part of the variable budget.

@[reducible]

noncomputable def DescriptiveComplexity.StepDef.invStepDef {L : FirstOrder.Language} [L.IsRelational] (d : StepDef L) (k : ℕ) (harity : ∀ (i : d.B.ι), d.B.arity i ≤ k) : StepDef (invLang L k)

The induced induction on the invariant structure: the same relation variables, unary; the step formulas and the output, compiled by the pebble compiler.

Equations

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

theorem DescriptiveComplexity.StepDef.partStage_invStepDef {L : FirstOrder.Language} {k : ℕ} [L.IsRelational] (d : StepDef L) {S : Set ((n : ℕ) × L.Relations n)} {A : Type} [L.Structure A] [Finite A] {harity : ∀ (i : d.B.ι), d.B.arity i ≤ k} (hbound : d.VarBound k) (hrels : d.UsesRels S) (n : ℕ) : (d.invStepDef k harity).partStage (InvMap S k A) n = invAssign S harity (d.partStage A n)

The partial stages of the induced induction are the images of the original ones: the pebble compiler tracks the iteration stage by stage.

theorem DescriptiveComplexity.StepDef.isFixedPt_invStepDef_iff {L : FirstOrder.Language} {k : ℕ} [L.IsRelational] (d : StepDef L) {S : Set ((n : ℕ) × L.Relations n)} {A : Type} [L.Structure A] [Finite A] {harity : ∀ (i : d.B.ι), d.B.arity i ≤ k} [Nonempty A] (hbound : d.VarBound k) (hrels : d.UsesRels S) (n : ℕ) : Function.IsFixedPt (d.invStepDef k harity).next ((d.invStepDef k harity).partStage (InvMap S k A) n) ↔ Function.IsFixedPt d.next (d.partStage A n)

Convergence transfers between the induction and its image on the invariant structure.

theorem DescriptiveComplexity.StepDef.pfpHolds_invStepDef {L : FirstOrder.Language} {k : ℕ} [L.IsRelational] (d : StepDef L) {S : Set ((n : ℕ) × L.Relations n)} {A : Type} [L.Structure A] [Finite A] {harity : ∀ (i : d.B.ι), d.B.arity i ≤ k} [Nonempty A] (hbound : d.VarBound k) (hrels : d.UsesRels S) (houtd : qdepth d.out ≤ k) : (d.invStepDef k harity).PFPHolds (InvMap S k A) ↔ d.PFPHolds A

The forward simulation: the partial value of the induced induction on the invariant structure is the partial value of the original induction.