The atoms of a step matrix, classified

The EXPSPACE program evaluates the matrix of a step formula atom by atom (DescriptiveComplexity.Draw.qfValue), and each atom gets a different subroutine: a point equality is one file test, an order comparison another, a relation of the expansion is an element-loop sub-fold, and a stage atom is a random access. So the program's call sites are indexed by the atoms with their kinds, and the kind must be data – computable from the formula when the program is defined, not merely known to exist.

This file is that data. Over the matrix vocabulary – the base X.E.sum Language.order expanded by the block, everything relational – a term is a variable (DescriptiveComplexity.Draw.matVar), an atom is one of four shapes (DescriptiveComplexity.Draw.MatAtom), the classifier DescriptiveComplexity.Draw.matAtom? reads the shape off the syntax – total on relation atoms, none only on non-atoms, which DescriptiveComplexity.Draw.qfAtoms never emits (DescriptiveComplexity.Draw.isSome_matAtom?_of_mem_qfAtoms) – and DescriptiveComplexity.Draw.realize_matAtom is the semantic reading: the atom holds at a valuation of the prefix exactly as its kind says, the stage atoms reading the assignment, the order atoms the chosen order on points, the expansion atoms the expanded structure.

Terms are variables

def DescriptiveComplexity.Draw.matVar {LM : FirstOrder.Language} [LM.IsRelational] {n : ℕ} : LM.Term (Empty ⊕ Fin n) → Fin n

The variable a matrix term is: over a relational vocabulary with no free names, nothing else is possible.

Equations

• DescriptiveComplexity.Draw.matVar (FirstOrder.Language.var (Sum.inl e)) = e.elim
• DescriptiveComplexity.Draw.matVar (FirstOrder.Language.var (Sum.inr j)) = j
• DescriptiveComplexity.Draw.matVar (FirstOrder.Language.func f _ts) = isEmptyElim f

theorem DescriptiveComplexity.Draw.realize_matVar {LM : FirstOrder.Language} [LM.IsRelational] {n : ℕ} {A : Type} [LM.Structure A] (xs : Empty → A) (w : Fin n → A) (t : LM.Term (Empty ⊕ Fin n)) : FirstOrder.Language.Term.realize (Sum.elim xs w) t = w (matVar t)

The four kinds of atoms

inductive DescriptiveComplexity.Draw.MatAtom {L : FirstOrder.Language} (X : ExpExpansion L) (B : SOBlock) (n : ℕ) : Type

An atom of a step matrix, classified: a point equality, an order comparison, a relation of the expansion, or a stage atom of the iteration – each with the prefix levels its arguments read. This is the index data of the program's per-atom call sites.

• eq {L : FirstOrder.Language} {X : ExpExpansion L} {B : SOBlock} {n : ℕ} : Fin n → Fin n → MatAtom X B n

  A point equality between two prefix levels.

• ord {L : FirstOrder.Language} {X : ExpExpansion L} {B : SOBlock} {n : ℕ} : Fin n → Fin n → MatAtom X B n

  An order comparison between two prefix levels.

• exp {L : FirstOrder.Language} {X : ExpExpansion L} {B : SOBlock} {n k : ℕ} : X.E.Relations k → (Fin k → Fin n) → MatAtom X B n

  A relation of the expansion, at the given prefix levels.

• stage {L : FirstOrder.Language} {X : ExpExpansion L} {B : SOBlock} {n : ℕ} (i : B.ι) : (Fin (B.arity i) → Fin n) → MatAtom X B n

  An atom of the block's relation variables, at the given prefix levels: a stage of the iteration for a fixed-point program, a guessed relation for a nondeterministic one.

def DescriptiveComplexity.Draw.relAtom {L : FirstOrder.Language} {X : ExpExpansion L} {B : SOBlock} {n k : ℕ} : ((X.E.sum FirstOrder.Language.order).sum B.lang).Relations k → (Fin k → ((X.E.sum FirstOrder.Language.order).sum B.lang).Term (Empty ⊕ Fin n)) → MatAtom X B n

The classification of a relation atom, by its symbol's summand.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.relAtom (Sum.inl (Sum.inl e)) x✝ = DescriptiveComplexity.Draw.MatAtom.exp e fun (j : Fin x✝¹) => DescriptiveComplexity.Draw.matVar (x✝ j)
• DescriptiveComplexity.Draw.relAtom (Sum.inr b) x✝ = DescriptiveComplexity.Draw.MatAtom.stage ↑b fun (j : Fin (B.arity ↑b)) => DescriptiveComplexity.Draw.matVar (x✝ (Fin.cast ⋯ j))

def DescriptiveComplexity.Draw.matAtom? {L : FirstOrder.Language} {X : ExpExpansion L} {B : SOBlock} {n : ℕ} : ((X.E.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n → Option (MatAtom X B n)

The classifier: the kind of an atom, read off the syntax; none only on non-atoms.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.matAtom? (FirstOrder.Language.BoundedFormula.rel r ts) = some (DescriptiveComplexity.Draw.relAtom r ts)
• DescriptiveComplexity.Draw.matAtom? FirstOrder.Language.BoundedFormula.falsum = none
• DescriptiveComplexity.Draw.matAtom? (f₁.imp f₂) = none
• DescriptiveComplexity.Draw.matAtom? f.all = none

theorem DescriptiveComplexity.Draw.isSome_matAtom?_of_mem_qfAtoms {L : FirstOrder.Language} {X : ExpExpansion L} {B : SOBlock} {n : ℕ} (ψ φ : ((X.E.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n) : φ ∈ qfAtoms ψ → (matAtom? φ).isSome = true

Every atom of a matrix classifies: the members of DescriptiveComplexity.Draw.qfAtoms are equality and relation atoms, on which the classifier is total.

The semantic reading

def DescriptiveComplexity.Draw.MatAtom.holds {L : FirstOrder.Language} {X : ExpExpansion L} {B : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] [LinearOrder (X.Map A)] (σ : B.Assignment (X.Map A)) {n : ℕ} (w : Fin n → X.Map A) : MatAtom X B n → Prop

What an atom says, at a stage of the iteration and a valuation of the prefix: the machine subroutine of the atom computes exactly this.

Equations

• DescriptiveComplexity.Draw.MatAtom.holds σ w (DescriptiveComplexity.Draw.MatAtom.eq j₁ j₂) = (w j₁ = w j₂)
• DescriptiveComplexity.Draw.MatAtom.holds σ w (DescriptiveComplexity.Draw.MatAtom.ord j₁ j₂) = (w j₁ ≤ w j₂)
• DescriptiveComplexity.Draw.MatAtom.holds σ w (DescriptiveComplexity.Draw.MatAtom.exp e ts) = FirstOrder.Language.Structure.RelMap e fun (j : Fin k) => w (ts j)
• DescriptiveComplexity.Draw.MatAtom.holds σ w (DescriptiveComplexity.Draw.MatAtom.stage i ts) = σ i fun (j : Fin (B.arity i)) => w (ts j)

theorem DescriptiveComplexity.Draw.realize_matAtom {L : FirstOrder.Language} {X : ExpExpansion L} {B : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] [LinearOrder (X.Map A)] (σ : B.Assignment (X.Map A)) {n : ℕ} {φ : ((X.E.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n} {κ : MatAtom X B n} (h : matAtom? φ = some κ) (w : Fin n → X.Map A) : φ.Realize default w ↔ MatAtom.holds σ w κ

The reading is correct: a classified atom realizes at a valuation of the prefix exactly as its kind says.

theorem DescriptiveComplexity.Draw.realize_iff_qfValue_holds {L : FirstOrder.Language} {X : ExpExpansion L} {B : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] [LinearOrder (X.Map A)] {n : ℕ} {mat : ((X.E.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n} (hqf : mat.IsQF) (σ : B.Assignment (X.Map A)) (w : Fin n → X.Map A) : mat.Realize default w ↔ qfValue mat fun (a : ((X.E.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n) => (matAtom? a).elim False (MatAtom.holds σ w)

The matrix through its classified atoms: a quantifier-free matrix realizes exactly as its Boolean function at the kinds' readings – which is what the machine computes once its per-atom subroutines have filled the verdict slots.