The k-pebble refinement, over an abstract initial relation

The combinatorial core of k-variable equivalence ≡ᵏ (Abiteboul–Vianu 1991; Ebbinghaus–Flum 1995, ch. 3), with no logic in sight: positions are k-tuples over a bare type A, an initial relation E₀ stands in for «same atomic type», and one round of the k-pebble game refines a relation E to DescriptiveComplexity.pebbleRefine E₀ E – the pairs that are in E₀ and survive one exchange of a pebble (DescriptiveComplexity.PebbleBackForth).

DescriptiveComplexity.EquivK E₀ is the limit of the descending refinement chain DescriptiveComplexity.pebbleStage, that is, the greatest fixed point of the refinement:

• the chain plateaus within the number of pairs of tuples (DescriptiveComplexity.exists_pebbleStage_succ_eq, the antitone half of DescriptiveComplexity.exists_succ_eq_of_antitone_subset), so on a finite type the limit is a stage and is itself a fixed point (DescriptiveComplexity.equivK_iff, the interface characterization);
• any relation below E₀ that survives its own back-and-forth condition is below the limit (DescriptiveComplexity.le_equivK, the coinduction principle), which is what «greatest» means and how anything is ever proved ≡ᵏ-equivalent;
• the limit is an equivalence relation whenever E₀ is (DescriptiveComplexity.equivK_equivalence);
• refining the initial relation by anything the limit already refines does not change the limit (DescriptiveComplexity.equivK_inf_eq) – read with E₀' the agreement on a ≡ᵏ-invariant relation, this is the expansion lemma: ≡ᵏ is unchanged when the structure is expanded by an ≡ᵏ-invariant relation. It is the lemma that carries the ≡ᵏ-invariance of fixed-point logics, each stage of an induction being such an expansion.

Keeping E₀ abstract keeps the vocabulary out: the instantiation at «same atomic type over a structure» – necessarily over the finitely many symbols a definition actually mentions – is where the logic enters, and lives with the invariance results for the fixed-point logics, not here. The same skeleton with rounds in place of pebbles is the Ehrenfeucht–Fraïssé refinement, a second consumer this file is stated to serve.

Relations on k-tuples

@[reducible, inline]

abbrev DescriptiveComplexity.PebbleRel (A : Type) (k : ℕ) : Type

A relation between k-tuples over A: the positions of the k-pebble game.

Equations

• DescriptiveComplexity.PebbleRel A k = ((Fin k → A) → (Fin k → A) → Prop)

def DescriptiveComplexity.PebbleRel.Le {A : Type} {k : ℕ} (E E' : PebbleRel A k) : Prop

Pointwise implication of relations on k-tuples, spelled out (the lattice order, kept explicit per the conventions of this library).

Equations

• E.Le E' = ∀ (a b : Fin k → A), E a b → E' a b

One round of the game

def DescriptiveComplexity.PebbleBackForth {A : Type} {k : ℕ} (E : PebbleRel A k) : PebbleRel A k

The back-and-forth condition of the k-pebble game relative to a relation E: whichever pebble the spoiler moves, on whichever side, the duplicator can move the same pebble on the other side and stay in E.

Equations

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

def DescriptiveComplexity.pebbleRefine {A : Type} {k : ℕ} (E₀ E : PebbleRel A k) : PebbleRel A k

One round of refinement: agree initially, and survive one exchange of a pebble relative to E.

Equations

• DescriptiveComplexity.pebbleRefine E₀ E a b = (E₀ a b ∧ DescriptiveComplexity.PebbleBackForth E a b)

theorem DescriptiveComplexity.pebbleBackForth_mono {A : Type} {k : ℕ} {E E' : PebbleRel A k} (h : E.Le E') : (PebbleBackForth E).Le (PebbleBackForth E')

The back-and-forth condition is monotone in the relation it is relative to.

theorem DescriptiveComplexity.pebbleRefine_mono {A : Type} {k : ℕ} (E₀ : PebbleRel A k) {E E' : PebbleRel A k} (h : E.Le E') : (pebbleRefine E₀ E).Le (pebbleRefine E₀ E')

One round of refinement is monotone in the refined relation.

The refinement chain and its limit

def DescriptiveComplexity.pebbleStage {A : Type} {k : ℕ} (E₀ : PebbleRel A k) : ℕ → PebbleRel A k

The descending refinement chain, from the all-relation: what one round cannot yet tell apart, twice refined, thrice refined …

Equations

• DescriptiveComplexity.pebbleStage E₀ 0 = fun (x x_1 : Fin k → A) => True
• DescriptiveComplexity.pebbleStage E₀ n.succ = DescriptiveComplexity.pebbleRefine E₀ (DescriptiveComplexity.pebbleStage E₀ n)

def DescriptiveComplexity.EquivK {A : Type} {k : ℕ} (E₀ : PebbleRel A k) : PebbleRel A k

k-equivalence relative to an initial relation: the limit of the refinement chain – equivalently (DescriptiveComplexity.equivK_iff, DescriptiveComplexity.le_equivK) the greatest fixed point of one round of refinement.

Equations

• DescriptiveComplexity.EquivK E₀ a b = ∀ (n : ℕ), DescriptiveComplexity.pebbleStage E₀ n a b

theorem DescriptiveComplexity.pebbleStage_succ_le {A : Type} {k : ℕ} (E₀ : PebbleRel A k) (n : ℕ) : (pebbleStage E₀ (n + 1)).Le (pebbleStage E₀ n)

The refinement chain descends.

theorem DescriptiveComplexity.pebbleStage_le_of_le {A : Type} {k : ℕ} (E₀ : PebbleRel A k) {m n : ℕ} (hmn : m ≤ n) : (pebbleStage E₀ n).Le (pebbleStage E₀ m)

The refinement chain descends, monotonically.

theorem DescriptiveComplexity.EquivK.stage {A : Type} {k : ℕ} {E₀ : PebbleRel A k} {a b : Fin k → A} (h : EquivK E₀ a b) (n : ℕ) : pebbleStage E₀ n a b

The limit is below every stage.

theorem DescriptiveComplexity.EquivK.initial {A : Type} {k : ℕ} {E₀ : PebbleRel A k} {a b : Fin k → A} (h : EquivK E₀ a b) : E₀ a b

The limit is below the initial relation.

Coinduction: the limit is the greatest post-fixed point

theorem DescriptiveComplexity.le_equivK {A : Type} {k : ℕ} {E₀ E : PebbleRel A k} (h : E.Le (pebbleRefine E₀ E)) : E.Le (EquivK E₀)

The coinduction principle: a relation below its own refinement is below the limit. This is how tuples are ever proved ≡ᵏ-equivalent – exhibit a back-and-forth system containing the pair.

Stabilization on a finite type

theorem DescriptiveComplexity.exists_pebbleStage_succ_eq {A : Type} {k : ℕ} [Finite A] (E₀ : PebbleRel A k) : ∃ N ≤ Nat.card ((Fin k → A) × (Fin k → A)), pebbleStage E₀ (N + 1) = pebbleStage E₀ N

The refinement chain plateaus within the number of pairs of k-tuples: consecutive stages agree from there on.

theorem DescriptiveComplexity.pebbleRefine_equivK {A : Type} {k : ℕ} [Finite A] (E₀ : PebbleRel A k) : pebbleRefine E₀ (EquivK E₀) = EquivK E₀

On a finite type the limit is a fixed point of the refinement – the greatest one, by DescriptiveComplexity.le_equivK.

theorem DescriptiveComplexity.equivK_iff {A : Type} {k : ℕ} [Finite A] (E₀ : PebbleRel A k) (a b : Fin k → A) : EquivK E₀ a b ↔ E₀ a b ∧ PebbleBackForth (EquivK E₀) a b

The interface characterization of ≡ᵏ on a finite type: initial agreement together with the back-and-forth condition relative to ≡ᵏ itself. Consumers should use this, never the stages.

theorem DescriptiveComplexity.EquivK.update {A : Type} {k : ℕ} {E₀ : PebbleRel A k} [Finite A] {a b : Fin k → A} (h : EquivK E₀ a b) (i : Fin k) (c : A) : ∃ (d : A), EquivK E₀ (Function.update a i c) (Function.update b i d)

The game move: from an equivalent pair, moving a pebble on the left can be answered on the right.

theorem DescriptiveComplexity.EquivK.update_right {A : Type} {k : ℕ} {E₀ : PebbleRel A k} [Finite A] {a b : Fin k → A} (h : EquivK E₀ a b) (i : Fin k) (d : A) : ∃ (c : A), EquivK E₀ (Function.update a i c) (Function.update b i d)

The game move, from the right.

Pair substructures

A tuple pair obtained by selecting, permuting and repeating coordinate pairs of an equivalent pair is equivalent: duplicated pebbles only make the duplicator's task easier. This is the well-definedness lemma behind every operation on ≡ᵏ-classes that rearranges coordinates – the substitution and rearrangement relations of the invariant structure.

theorem DescriptiveComplexity.equivK_of_pairSub {A : Type} {k : ℕ} {E₀ : PebbleRel A k} [Finite A] (hE₀ : ∀ {x y u v : Fin k → A}, (∀ (j : Fin k), ∃ (i : Fin k), x j = u i ∧ y j = v i) → E₀ u v → E₀ x y) {x y u v : Fin k → A} (hsub : ∀ (j : Fin k), ∃ (i : Fin k), x j = u i ∧ y j = v i) (huv : EquivK E₀ u v) : EquivK E₀ x y

Equivalence is inherited by pair substructures: if every coordinate pair of (x, y) is a coordinate pair of (u, v), and the initial relation is closed under this passage, then u ≡ᵏ v forces x ≡ᵏ y. Coinduction: the spoiler's move on (x, y) frees a pebble of (u, v) (at most k - 1 pairs are still needed), where the duplicator answers via the game move.

Equivalence

theorem DescriptiveComplexity.pebbleBackForth_refl {A : Type} {k : ℕ} {E : PebbleRel A k} (h : ∀ (a : Fin k → A), E a a) (a : Fin k → A) : PebbleBackForth E a a

The back-and-forth condition preserves reflexivity.

theorem DescriptiveComplexity.pebbleBackForth_symm {A : Type} {k : ℕ} {E : PebbleRel A k} (h : ∀ (a b : Fin k → A), E a b → E b a) {a b : Fin k → A} (hab : PebbleBackForth E a b) : PebbleBackForth E b a

The back-and-forth condition preserves symmetry.

theorem DescriptiveComplexity.pebbleBackForth_trans {A : Type} {k : ℕ} {E : PebbleRel A k} (h : ∀ (a b c : Fin k → A), E a b → E b c → E a c) {a b c : Fin k → A} (hab : PebbleBackForth E a b) (hbc : PebbleBackForth E b c) : PebbleBackForth E a c

The back-and-forth condition preserves transitivity.

theorem DescriptiveComplexity.pebbleStage_equivalence {A : Type} {k : ℕ} {E₀ : PebbleRel A k} (hE₀ : Equivalence E₀) (n : ℕ) : Equivalence (pebbleStage E₀ n)

Every stage of the refinement chain of an equivalence is an equivalence.

theorem DescriptiveComplexity.equivK_equivalence {A : Type} {k : ℕ} {E₀ : PebbleRel A k} (hE₀ : Equivalence E₀) : Equivalence (EquivK E₀)

≡ᵏ is an equivalence whenever the initial relation is one.

Monotonicity and the expansion lemma

theorem DescriptiveComplexity.pebbleStage_mono {A : Type} {k : ℕ} {E₀ E₀' : PebbleRel A k} (h : E₀'.Le E₀) (n : ℕ) : (pebbleStage E₀' n).Le (pebbleStage E₀ n)

The stages are monotone in the initial relation.

theorem DescriptiveComplexity.equivK_mono {A : Type} {k : ℕ} {E₀ E₀' : PebbleRel A k} (h : E₀'.Le E₀) : (EquivK E₀').Le (EquivK E₀)

≡ᵏ is monotone in the initial relation.

theorem DescriptiveComplexity.equivK_inf_eq {A : Type} {k : ℕ} [Finite A] {E₀ E₀' : PebbleRel A k} (hle : E₀'.Le E₀) (hinv : (EquivK E₀).Le E₀') : EquivK E₀' = EquivK E₀

The expansion lemma: refining the initial relation by anything ≡ᵏ already refines does not change ≡ᵏ. Read with E₀' the conjunction of E₀ and agreement on an ≡ᵏ-invariant relation, this says ≡ᵏ is unchanged when the structure is expanded by an ≡ᵏ-invariant relation – the lemma that carries the ≡ᵏ-invariance of the fixed-point logics, stage by stage.