Documentation

DescriptiveComplexity.Invariant.EquivK

`k`-variable equivalence over a structure #

The instantiation of the abstract pebble refinement (DescriptiveComplexity.Invariant.Pebble) at a structure: the initial relation is agreement on the atomic type (DescriptiveComplexity.atomicAgreeOn – same equalities between coordinates, same base relations at every selection of coordinates), and DescriptiveComplexity.EquivK (atomicAgreeOn S A k) is k-variable equivalence ≡ᵏ of k-tuples over the structure A.

Agreement is relative to a family S of relation symbols: over an infinite vocabulary, full atomic agreement is not captured by any formula, and every consumer of the invariant layer – a DescriptiveComplexity.StepDef, whose formulas mention finitely many symbols (DescriptiveComplexity.StepDef.exists_usesRels) – needs the refinement relative to the finite family it actually reads, which is what makes the refinement itself definable. The full-agreement instance is DescriptiveComplexity.atomicAgree (S = Set.univ).

The theorem of this file is the k-variable invariance lemma (DescriptiveComplexity.realize_equivK): a first-order formula over a relational vocabulary, whose relation symbols lie in S (DescriptiveComplexity.RelsIn), cannot separate ≡ᵏ-equivalent tuples, when its free variables read the tuples through an arbitrary selection of coordinates, its bound variables are placed injectively outside that selection, and the positions not in use leave room for its quantifier depth (DescriptiveComplexity.qdepth). The proof is the textbook pebble argument (Ebbinghaus–Flum 1995, ch. 3): each quantifier spends one fresh pebble, placed by the game move DescriptiveComplexity.EquivK.update; atomic formulas are decided by the initial agreement. No syntactic k-variable fragment is ever defined – the budget hypothesis of the lemma is «this formula has at most k variables», in the only form the invariance argument needs.

A second consequence of the game formulation is inheritance by pair substructures (DescriptiveComplexity.equivK_atomicAgreeOn_of_pairSub, the structure instance of DescriptiveComplexity.equivK_of_pairSub): rearranging, selecting and repeating coordinates preserves ≡ᵏ – the well-definedness of every coordinate manipulation on ≡ᵏ-classes.

The vocabulary is required to be relational, as everywhere in the invariant layer: atomic agreement at selections of coordinates is only the atomic type when terms are variables. (Everything a StepDef runs on in the Abiteboul–Vianu development is relational or expanded from relational.)

Agreement on the atomic type #

def DescriptiveComplexity.atomicAgreeOn {L : FirstOrder.Language} (S : Set ((n : ℕ) × L.Relations n)) (A : Type) [L.Structure A] (k : ℕ) :

Agreement on the atomic type over the relation symbols of the family S: two k-tuples agree on all equalities between their coordinates and on all base relations of S at every selection of coordinates. This is the initial relation of the k-pebble refinement over a structure, relative to the finitely many symbols a definition mentions.

Equations

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

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.atomicAgree (L : FirstOrder.Language) (A : Type) [L.Structure A] (k : ℕ) :

Agreement on the full atomic type: the special case S = Set.univ of DescriptiveComplexity.atomicAgreeOn.

Equations

DescriptiveComplexity.atomicAgree L A k = DescriptiveComplexity.atomicAgreeOn Set.univ A k

Instances For

Dependency graph

theorem DescriptiveComplexity.atomicAgreeOn_equivalence {L : FirstOrder.Language} {A : Type} {k : ℕ} [L.Structure A] {S : Set ((n : ℕ) × L.Relations n)} :

Equivalence (atomicAgreeOn S A k)

Agreement on the atomic type is an equivalence.

Dependency graph

theorem DescriptiveComplexity.equivK_atomicAgreeOn_equivalence {L : FirstOrder.Language} {A : Type} {k : ℕ} [L.Structure A] {S : Set ((n : ℕ) × L.Relations n)} :

Equivalence (EquivK (atomicAgreeOn S A k))

≡ᵏ over a structure is an equivalence.

Dependency graph

theorem DescriptiveComplexity.atomicAgreeOn_of_pairSub {L : FirstOrder.Language} {A : Type} {k : ℕ} [L.Structure A] {S : Set ((n : ℕ) × L.Relations n)} {x y u v : Fin k → A} (hsub : ∀ (j : Fin k), ∃ (i : Fin k), x j = u i ∧ y j = v i) (h : atomicAgreeOn S A k u v) :

atomicAgreeOn S A k x y

Agreement on the atomic type passes to pair substructures: selecting, permuting and repeating coordinate pairs preserves it.

Dependency graph

theorem DescriptiveComplexity.equivK_atomicAgreeOn_of_pairSub {L : FirstOrder.Language} {A : Type} {k : ℕ} [L.Structure A] [Finite A] {S : Set ((n : ℕ) × L.Relations n)} {x y u v : Fin k → A} (hsub : ∀ (j : Fin k), ∃ (i : Fin k), x j = u i ∧ y j = v i) (huv : EquivK (atomicAgreeOn S A k) u v) :

EquivK (atomicAgreeOn S A k) x y

≡ᵏ is inherited by pair substructures over a structure: the instance of DescriptiveComplexity.equivK_of_pairSub at atomic agreement. This is the well-definedness of every coordinate manipulation on ≡ᵏ-classes – substitution and rearrangement relations included.

Dependency graph

Quantifier depth and the relation symbols of a formula #

def DescriptiveComplexity.qdepth {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} :

L.BoundedFormula α n → ℕ

The quantifier depth of a bounded formula: the number of pebbles the invariance argument spends on it.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.RelsIn {L : FirstOrder.Language} (S : Set ((n : ℕ) × L.Relations n)) {α : Type u_1} {n : ℕ} :

L.BoundedFormula α n → Prop

The relation symbols of a bounded formula all lie in the family S.

Equations

Instances For

Dependency graph

theorem DescriptiveComplexity.RelsIn.mono {L : FirstOrder.Language} {S S' : Set ((n : ℕ) × L.Relations n)} (hS : S ⊆ S') {α : Type u_1} {n : ℕ} {φ : L.BoundedFormula α n} (h : RelsIn S φ) :

RelsIn S' φ

Containment of relation symbols is monotone in the family.

Dependency graph

def DescriptiveComplexity.relsOf {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} :

L.BoundedFormula α n → Set ((n : ℕ) × L.Relations n)

The set of relation symbols occurring in a bounded formula.

Equations

Instances For

Dependency graph

theorem DescriptiveComplexity.relsOf_finite {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormula α n) :

(relsOf φ).Finite

A formula mentions finitely many relation symbols.

Dependency graph

theorem DescriptiveComplexity.relsIn_relsOf {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormula α n) :

RelsIn (relsOf φ) φ

A formula's relation symbols lie in the set of its relation symbols.

Dependency graph

Terms of a relational vocabulary are variables #

theorem DescriptiveComplexity.exists_eq_var_of_isRelational {L : FirstOrder.Language} [L.IsRelational] {α : Type u_1} (t : L.Term α) :

∃ (x : α), t = FirstOrder.Language.var x

In a relational vocabulary, every term is a variable.

Dependency graph

Placing a fresh pebble #

theorem DescriptiveComplexity.snoc_injective {k n : ℕ} {h : Fin n → Fin k} {p : Fin k} (hinj : Function.Injective h) (hp : ∀ (j : Fin n), h j ≠ p) :

Function.Injective (Fin.snoc h p)

Dependency graph

theorem DescriptiveComplexity.image_snoc_subset {k n : ℕ} {h : Fin n → Fin k} {p : Fin k} :

Finset.image (Fin.snoc h p) Finset.univ ⊆ insert p (Finset.image h Finset.univ)

Dependency graph

The `k`-variable invariance lemma #

theorem DescriptiveComplexity.realize_equivK {L : FirstOrder.Language} {A : Type} {k : ℕ} [L.IsRelational] [L.Structure A] [Finite A] {S : Set ((n : ℕ) × L.Relations n)} {m n : ℕ} (φ : L.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 S φ → ∀ (v w : Fin k → A), EquivK (atomicAgreeOn S A k) v w → ((φ.Realize (fun (i : Fin m) => v (g i)) fun (j : Fin n) => v (h j)) ↔ φ.Realize (fun (i : Fin m) => w (g i)) fun (j : Fin n) => w (h j))

The k-variable invariance lemma. A first-order formula over a relational vocabulary, with relation symbols in the family S, cannot separate tuples ≡ᵏ-equivalent relative to S: its free variables read the tuples through an arbitrary selection g of coordinates, its bound variables through an injective selection h disjoint from g, and the coordinates not in use leave room for its quantifier depth. Each quantifier spends one fresh pebble, placed by the game move (DescriptiveComplexity.EquivK.update); atomic formulas are decided by the initial agreement (DescriptiveComplexity.atomicAgreeOn).

Dependency graph

theorem DescriptiveComplexity.realize_formula_equivK {L : FirstOrder.Language} {A : Type} {k : ℕ} [L.IsRelational] [L.Structure A] [Finite A] {S : Set ((n : ℕ) × L.Relations n)} {m : ℕ} (φ : L.Formula (Fin m)) (g : Fin m → Fin k) (hroom : (Finset.image g Finset.univ).card + qdepth φ ≤ k) (hS : RelsIn S φ) {v w : Fin k → A} (hvw : EquivK (atomicAgreeOn S A k) v w) :

(φ.Realize fun (i : Fin m) => v (g i)) ↔ φ.Realize fun (i : Fin m) => w (g i)

The k-variable invariance lemma, for formulas: a formula over a relational vocabulary, with relation symbols in S and room for its quantifier depth beyond the selection of coordinates its free variables read, cannot separate ≡ᵏ-equivalent tuples.

Dependency graph