Pulling an ordered induction on the invariant structure back to the base

The backward simulation of the Abiteboul–Vianu argument (DescriptiveComplexity.AbiteboulVianu): an induction over the ordered invariant vocabulary – as produced by the PTIME capture applied on the invariant structure – runs on the base structure A, once the canonical order on k-tuples is available as a converged relation variable. The class compiler (DescriptiveComplexity.backCompile) translates a formula over ((invLang L k).sum Language.order).sum B'.lang into a formula over the base vocabulary expanded by the order block and by a k-fold copy of B' (DescriptiveComplexity.backBlock):

• every class variable becomes k element variables – a representative tuple; equality of classes becomes incomparability in the order variable (≡ᵏ);
• the invariant vocabulary's relations become their defining formulas – bits as atomic formulas, substitution and rearrangement as incomparability at manipulated tuples, the order symbol as «strictly below or equivalent»;
• a relation variable on classes becomes its k-fold pullback, one flat arity · k-tuple read through DescriptiveComplexity.backFlatten;
• a quantifier over classes becomes k quantifiers over elements.

The compiler is exact (DescriptiveComplexity.realize_backCompile), the compiled induction DescriptiveComplexity.StepDef.backStepDef tracks the original stage by stage over the pulled-back assignments (DescriptiveComplexity.backAssign), and the values agree (DescriptiveComplexity.StepDef.ifpHolds_backStepDef). Stratified over the definable refinement (DescriptiveComplexity.Invariant.OrderDef, DescriptiveComplexity.FixedPointStratify), this is what turns an ordered induction on Iᵏ A into an order-free induction on A.

The pulled-back block

@[reducible]

def DescriptiveComplexity.backBlock (B' : SOBlock) (k : ℕ) : SOBlock

The k-fold pullback of a block: each relation variable on classes becomes one on representative tuples, its arity multiplied by k.

Equations

• DescriptiveComplexity.backBlock B' k = { ι := B'.ι, ιFinite := ⋯, arity := fun (i : B'.ι) => B'.arity i * k }

def DescriptiveComplexity.backFlatten {k : ℕ} {A : Type} {m : ℕ} (t : Fin m → Fin k → A) : Fin (m * k) → A

Reading a tuple of k-tuples as one flat tuple.

Equations

• DescriptiveComplexity.backFlatten t p = t (finProdFinEquiv.symm p).1 (finProdFinEquiv.symm p).2

theorem DescriptiveComplexity.backFlatten_apply {k : ℕ} {A : Type} {m : ℕ} (t : Fin m → Fin k → A) (a : Fin m) (q : Fin k) : backFlatten t (finProdFinEquiv (a, q)) = t a q

def DescriptiveComplexity.backAssign {L : FirstOrder.Language} {k : ℕ} {S : Set ((n : ℕ) × L.Relations n)} {A : Type} [L.Structure A] {B' : SOBlock} (X' : B'.Assignment (InvMap S k A)) : (backBlock B' k).Assignment A

The pullback along the quotient map of an assignment on classes.

Equations

• DescriptiveComplexity.backAssign X' i flat = X' i fun (a : Fin (B'.arity i)) => DescriptiveComplexity.InvMap.mk S fun (q : Fin k) => flat (finProdFinEquiv (a, q))

theorem DescriptiveComplexity.backAssign_backFlatten {L : FirstOrder.Language} {k : ℕ} {S : Set ((n : ℕ) × L.Relations n)} {A : Type} [L.Structure A] {B' : SOBlock} (X' : B'.Assignment (InvMap S k A)) (i : B'.ι) (t : Fin (B'.arity i) → Fin k → A) : backAssign X' i (backFlatten t) ↔ X' i fun (a : Fin (B'.arity i)) => InvMap.mk S (t a)

Symbols and atoms over the doubly expanded vocabulary

@[reducible, inline]

abbrev DescriptiveComplexity.backPrecSym (L : FirstOrder.Language) (k : ℕ) (B' : SOBlock) : ((L.sum (ordBlock k).lang).sum (backBlock B' k).lang).Relations (k + k)

The order variable, inside the second expansion.

Equations

• DescriptiveComplexity.backPrecSym L k B' = Sum.inl (DescriptiveComplexity.ordVSym L k)

@[reducible, inline]

abbrev DescriptiveComplexity.backBaseSym (L : FirstOrder.Language) (k : ℕ) (B' : SOBlock) {l : ℕ} (R : L.Relations l) : ((L.sum (ordBlock k).lang).sum (backBlock B' k).lang).Relations l

A base relation symbol, inside the second expansion.

Equations

• DescriptiveComplexity.backBaseSym L k B' R = Sum.inl (DescriptiveComplexity.ordBaseSym L k R)

noncomputable def DescriptiveComplexity.bPrecF (L : FirstOrder.Language) (k : ℕ) {B' : SOBlock} {γ : Type} (f g : Fin k → γ) : ((L.sum (ordBlock k).lang).sum (backBlock B' k).lang).Formula γ

The ≺-atom between two k-tuples of variables, inside the second expansion.

Equations

• DescriptiveComplexity.bPrecF L k f g = (DescriptiveComplexity.backPrecSym L k B').formula fun (p : Fin (k + k)) => FirstOrder.Language.var (Fin.addCases f g p)

noncomputable def DescriptiveComplexity.bEquivF (L : FirstOrder.Language) (k : ℕ) {B' : SOBlock} {γ : Type} (f g : Fin k → γ) : ((L.sum (ordBlock k).lang).sum (backBlock B' k).lang).Formula γ

The ≡ᵏ-atom: incomparability.

Equations

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

noncomputable def DescriptiveComplexity.bLeF (L : FirstOrder.Language) (k : ℕ) {B' : SOBlock} {γ : Type} (f g : Fin k → γ) : ((L.sum (ordBlock k).lang).sum (backBlock B' k).lang).Formula γ

The ≤-atom on classes: strictly below or equivalent.

Equations

• DescriptiveComplexity.bLeF L k f g = DescriptiveComplexity.bPrecF L k f g ⊔ DescriptiveComplexity.bEquivF L k f g

The class compiler

@[irreducible]

noncomputable def DescriptiveComplexity.backCompile (L : FirstOrder.Language) (k : ℕ) {B' : SOBlock} (S : Set ((n : ℕ) × L.Relations n)) {γ α : Type} {n : ℕ} : (((invLang L k).sum FirstOrder.Language.order).sum B'.lang).BoundedFormula α n → (α → Fin k → γ) → (Fin n → Fin k → γ) → ((L.sum (ordBlock k).lang).sum (backBlock B' k).lang).Formula γ

The class compiler: a formula over the ordered invariant vocabulary expanded by a block, read on representative k-tuples over the base vocabulary expanded by the order block and the pulled-back block. Each free or bound class variable is a selection of k context variables.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.backCompile L k S FirstOrder.Language.BoundedFormula.falsum x✝¹ x✝ = ⊥
• DescriptiveComplexity.backCompile L k S (FirstOrder.Language.BoundedFormula.equal t₁ t₂) x✝¹ x✝ = DescriptiveComplexity.bEquivF L k (Sum.elim x✝¹ x✝ t₁.varOf) (Sum.elim x✝¹ x✝ t₂.varOf)

Exactness of the class compiler

theorem DescriptiveComplexity.realize_backCompile {L : FirstOrder.Language} {k : ℕ} {B' : SOBlock} {S : Set ((n : ℕ) × L.Relations n)} {A : Type} [L.Structure A] [Finite A] {σ : (ordBlock k).Assignment A} {Y : (backBlock B' k).Assignment A} (lo : LinearOrder (InvMap S k A)) {X' : B'.Assignment (InvMap S k A)} (h1 : IncompRel (toPebble σ) = EquivK (atomicAgreeOn S A k)) (h2 : ∀ (u v : Fin k → A), toPebble σ u v ∨ EquivK (atomicAgreeOn S A k) u v ↔ InvMap.mk S u ≤ InvMap.mk S v) (hY : ∀ (i : B'.ι) (t : Fin (B'.arity i) → Fin k → A), Y i (backFlatten t) ↔ X' i fun (a : Fin (B'.arity i)) => InvMap.mk S (t a)) {α : Type} {n : ℕ} (φ : (((invLang L k).sum FirstOrder.Language.order).sum B'.lang).BoundedFormula α n) {γ : Type} (E : α → Fin k → γ) (H : Fin n → Fin k → γ) (W : γ → A) : (backCompile L k S φ E H).Realize W ↔ φ.Realize (fun (a : α) => InvMap.mk S fun (q : Fin k) => W (E a q)) fun (j : Fin n) => InvMap.mk S fun (q : Fin k) => W (H j q)

Exactness of the class compiler: over an order variable whose incomparability is ≡ᵏ and an assignment corresponding to one on classes, the compiled formula holds at representative tuples exactly when the original formula holds at their classes on the ordered invariant structure.

The pulled-back induction

noncomputable def DescriptiveComplexity.StepDef.backStepDef {L : FirstOrder.Language} {k : ℕ} (e : StepDef ((invLang L k).sum FirstOrder.Language.order)) (S : Set ((n : ℕ) × L.Relations n)) : StepDef (L.sum (ordBlock k).lang)

The pulled-back induction: the induction over the ordered invariant vocabulary, compiled onto representative tuples over the base vocabulary expanded by the (frozen) order block.

Equations

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

theorem DescriptiveComplexity.StepDef.inflStage_backStepDef {L : FirstOrder.Language} {k : ℕ} (e : StepDef ((invLang L k).sum FirstOrder.Language.order)) {S : Set ((n : ℕ) × L.Relations n)} {A : Type} [L.Structure A] [Finite A] {σ : (ordBlock k).Assignment A} (lo : LinearOrder (InvMap S k A)) (h1 : IncompRel (toPebble σ) = EquivK (atomicAgreeOn S A k)) (h2 : ∀ (u v : Fin k → A), toPebble σ u v ∨ EquivK (atomicAgreeOn S A k) u v ↔ InvMap.mk S u ≤ InvMap.mk S v) (n : ℕ) : (e.backStepDef S).inflStage A n = backAssign (e.inflStage (InvMap S k A) n)

The stages of the pulled-back induction are the pullbacks of the original stages.

theorem DescriptiveComplexity.StepDef.ifpHolds_backStepDef {L : FirstOrder.Language} {k : ℕ} (e : StepDef ((invLang L k).sum FirstOrder.Language.order)) {S : Set ((n : ℕ) × L.Relations n)} {A : Type} [L.Structure A] [Finite A] {σ : (ordBlock k).Assignment A} (lo : LinearOrder (InvMap S k A)) (h1 : IncompRel (toPebble σ) = EquivK (atomicAgreeOn S A k)) (h2 : ∀ (u v : Fin k → A), toPebble σ u v ∨ EquivK (atomicAgreeOn S A k) u v ↔ InvMap.mk S u ≤ InvMap.mk S v) : (e.backStepDef S).IFPHolds A ↔ e.IFPHolds (InvMap S k A)

The value of the pulled-back induction is the original value: an ordered induction over the invariant structure runs on the base structure, over the frozen canonical order.