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 #

source

@[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 }

Instances For

Dependency graph

source

@[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

Instances For

Dependency graph

The pebble compiler #

source

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

Instances For

Dependency graph

source

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✝)

Instances For

Dependency graph

Exactness of the compiler #

source

theorem DescriptiveComplexity.realize_rearrBody {L : FirstOrder.Language} {k : ℕ} {B : SOBlock} {S : Set ((n : ℕ) × L.Relations n)} {A : Type} [L.Structure A] [Finite A] {X : (classBlock B).Assignment (InvMap S k A)} (σ : Fin k → Fin k) (i : B.ι) (val c : Fin 1 → InvMap S k A) :

((invRelSym L k B (InvRel.rearr σ)).formula ![FirstOrder.Language.var (Sum.inl 0), FirstOrder.Language.var (Sum.inr 0)] ⊓ (varInSym (invLang L k) (classBlock B) i).formula fun (x : Fin ((classBlock B).arity i)) => FirstOrder.Language.var (Sum.inr 0)).Realize (Sum.elim val c) ↔ InvMap.rearrRel σ (val 0) (c 0) ∧ X i fun (x : Fin ((classBlock B).arity i)) => c 0

Dependency graph

source

theorem DescriptiveComplexity.realize_subAtom {L : FirstOrder.Language} {k : ℕ} {B : SOBlock} {S : Set ((n : ℕ) × L.Relations n)} {A : Type} [L.Structure A] [Finite A] {X : (classBlock B).Assignment (InvMap S k A)} (p : Fin k) (val c : Fin 1 → InvMap S k A) :

((invRelSym L k B (InvRel.sub p)).formula ![FirstOrder.Language.var (Sum.inl 0), FirstOrder.Language.var (Sum.inr 0)]).Realize (Sum.elim val c) ↔ InvMap.subRel p (val 0) (c 0)

Dependency graph

source

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).

Dependency graph

Sentences over an empty variable supply #

source

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.

Instances For

Dependency graph

The induced induction on the invariant structure #

source

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)

Instances For

Dependency graph

source

@[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