The atoms of a defining sentence, classified

The element loops of the EXPSPACE program evaluate the matrices of the expansion's defining sentences – X.relSentence, over the base vocabulary expanded by a replicated block (one copy per argument point), and X.dom, over the same expanded by the block itself. Both are the same shape, so the classification is stated at an arbitrary block: the base-vocabulary atoms – equalities, base relations, order – are guards, evaluated on the control-held elements by the transition table itself; the block atoms are the read leaves, one named-bit trip each, at the cell of the point whose payload the loop variables spell.

This file mirrors DescriptiveComplexity.Problems.Wide.DrawAtoms at that language: DescriptiveComplexity.Draw.BlkAtom is the kind, DescriptiveComplexity.Draw.blkAtom? the total-on-atoms classifier, DescriptiveComplexity.Draw.BlkAtom.holds the semantic reading at a block assignment, and DescriptiveComplexity.Draw.realize_iff_qfValue_blkHolds the capstone: a quantifier-free matrix realizes as its Boolean function at the kinds' readings. For a defining sentence the assignment is DescriptiveComplexity.SOBlock.replicateAssign, so a block atom's index splits into the copy – which argument point – and the point's own relation variable.

The kinds

inductive DescriptiveComplexity.Draw.BlkAtom (L : FirstOrder.Language) (B : SOBlock) (n : ℕ) : Type

An atom of a defining sentence, classified: the base-vocabulary kinds are guards, the block kind is a read leaf.

• eqA {L : FirstOrder.Language} {B : SOBlock} {n : ℕ} : Fin n → Fin n → BlkAtom L B n

  An equality between two prefix levels: a guard.

• baseA {L : FirstOrder.Language} {B : SOBlock} {n m : ℕ} : L.Relations m → (Fin m → Fin n) → BlkAtom L B n

  A base-vocabulary relation at prefix levels: a guard.

• ordA {L : FirstOrder.Language} {B : SOBlock} {n : ℕ} : Fin n → Fin n → BlkAtom L B n

  An order comparison between two prefix levels: a guard.

• blkA {L : FirstOrder.Language} {B : SOBlock} {n : ℕ} (i : B.ι) : (Fin (B.arity i) → Fin n) → BlkAtom L B n

  A relation variable of the block at prefix levels: a read leaf.

def DescriptiveComplexity.Draw.blkRelAtom {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {n m : ℕ} : ((L.sum FirstOrder.Language.order).sum B.lang).Relations m → (Fin m → ((L.sum FirstOrder.Language.order).sum B.lang).Term (Empty ⊕ Fin n)) → BlkAtom L 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.blkRelAtom (Sum.inl (Sum.inl r)) x✝ = DescriptiveComplexity.Draw.BlkAtom.baseA r fun (j : Fin x✝¹) => DescriptiveComplexity.Draw.matVar (x✝ j)
• DescriptiveComplexity.Draw.blkRelAtom (Sum.inr b) x✝ = DescriptiveComplexity.Draw.BlkAtom.blkA ↑b fun (j : Fin (B.arity ↑b)) => DescriptiveComplexity.Draw.matVar (x✝ (Fin.cast ⋯ j))

def DescriptiveComplexity.Draw.blkAtom? {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {n : ℕ} : ((L.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n → Option (BlkAtom L 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.blkAtom? (FirstOrder.Language.BoundedFormula.rel r ts) = some (DescriptiveComplexity.Draw.blkRelAtom r ts)
• DescriptiveComplexity.Draw.blkAtom? FirstOrder.Language.BoundedFormula.falsum = none
• DescriptiveComplexity.Draw.blkAtom? (f₁.imp f₂) = none
• DescriptiveComplexity.Draw.blkAtom? f.all = none

theorem DescriptiveComplexity.Draw.isSome_blkAtom?_of_mem_qfAtoms {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {n : ℕ} (ψ φ : ((L.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n) : φ ∈ qfAtoms ψ → (blkAtom? φ).isSome = true

Every atom of a matrix classifies.

The atoms that need a tape

Only the block atoms are read leaves: an equality, a base relation or an order comparison on the loop's own elements is a guard, evaluated by the transition table where it stands. So a round of an element loop makes one trip per block atom and no more – which matters, because a defining sentence may well have no block atom at all, and there is in general no cell a harmless trip could be sent to.

def DescriptiveComplexity.Draw.isBlkAtom {L : FirstOrder.Language} {B : SOBlock} {n : ℕ} : ((L.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n → Bool

Is this atom a read leaf? – decided by the relation symbol's summand, so no term analysis and no relationality is needed.

Equations

• DescriptiveComplexity.Draw.isBlkAtom (FirstOrder.Language.BoundedFormula.rel (Sum.inr val) ts) = true
• DescriptiveComplexity.Draw.isBlkAtom x✝ = false

def DescriptiveComplexity.Draw.blkAtoms {L : FirstOrder.Language} {B : SOBlock} {n : ℕ} (mat : ((L.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n) : List (((L.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n)

The read leaves of a matrix, in evaluation order.

Equations

• DescriptiveComplexity.Draw.blkAtoms mat = List.filter DescriptiveComplexity.Draw.isBlkAtom (DescriptiveComplexity.Draw.qfAtoms mat)

theorem DescriptiveComplexity.Draw.mem_qfAtoms_of_mem_blkAtoms {L : FirstOrder.Language} {B : SOBlock} {n : ℕ} {mat φ : ((L.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n} (h : φ ∈ blkAtoms mat) : φ ∈ qfAtoms mat

theorem DescriptiveComplexity.Draw.isBlkAtom_of_mem_blkAtoms {L : FirstOrder.Language} {B : SOBlock} {n : ℕ} {mat φ : ((L.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n} (h : φ ∈ blkAtoms mat) : isBlkAtom φ = true

The semantic reading

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

What an atom says, at a block assignment and a valuation of the prefix.

Equations

• DescriptiveComplexity.Draw.BlkAtom.holds ρ w (DescriptiveComplexity.Draw.BlkAtom.eqA j₁ j₂) = (w j₁ = w j₂)
• DescriptiveComplexity.Draw.BlkAtom.holds ρ w (DescriptiveComplexity.Draw.BlkAtom.baseA r ts) = FirstOrder.Language.Structure.RelMap r fun (j : Fin m) => w (ts j)
• DescriptiveComplexity.Draw.BlkAtom.holds ρ w (DescriptiveComplexity.Draw.BlkAtom.ordA j₁ j₂) = (w j₁ ≤ w j₂)
• DescriptiveComplexity.Draw.BlkAtom.holds ρ w (DescriptiveComplexity.Draw.BlkAtom.blkA i ts) = ρ i fun (j : Fin (B.arity i)) => w (ts j)

theorem DescriptiveComplexity.Draw.realize_blkAtom {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] (ρ : B.Assignment A) {n : ℕ} {φ : ((L.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n} {κ : BlkAtom L B n} (h : blkAtom? φ = some κ) (w : Fin n → A) : φ.Realize default w ↔ BlkAtom.holds ρ w κ

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

theorem DescriptiveComplexity.Draw.exists_blkA_of_isBlkAtom {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {n : ℕ} {φ : ((L.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n} (h : isBlkAtom φ = true) : ∃ (i : B.ι) (ts : Fin (B.arity i) → Fin n), blkAtom? φ = some (BlkAtom.blkA i ts)

A read leaf is a block atom: the syntactic test and the classifier agree, so an element loop's r-th trip has a relation variable, a copy and a tuple of levels to read.

theorem DescriptiveComplexity.Draw.isBlkAtom_of_blkA {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {n : ℕ} {φ : ((L.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n} {i : B.ι} {ts : Fin (B.arity i) → Fin n} (h : blkAtom? φ = some (BlkAtom.blkA i ts)) : isBlkAtom φ = true

The converse test: a classified block atom passes the syntactic one.

theorem DescriptiveComplexity.Draw.realize_iff_qfValue_blkHolds {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {n : ℕ} {mat : ((L.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n} (hqf : mat.IsQF) (ρ : B.Assignment A) (w : Fin n → A) : mat.Realize default w ↔ qfValue mat fun (a : ((L.sum FirstOrder.Language.order).sum B.lang).BoundedFormula Empty n) => (blkAtom? a).elim False (BlkAtom.holds ρ w)

The matrix through its classified atoms: a quantifier-free matrix realizes exactly as its Boolean function at the kinds' readings.