Claiming the block atoms of a quantifier-free matrix

The second of the two normal forms that let a machine evaluate a fixed first-order sentence with a finite control. DescriptiveComplexity.Exponential.AltQuant turned a sentence into an alternating prefix over a quantifier-free matrix; the matrix still mentions the block, whose atoms live on the machine's tape and are not available to a transition. This file removes them:

a quantifier-free matrix over two copies of a block is a base formula determined by the truth values of finitely many block atoms, whose addresses are read off the valuation.

DescriptiveComplexity.exists_blockClaims produces the finite list of occurrences (DescriptiveComplexity.BlockAtom: a copy, a relation variable, and where its arguments sit among the matrix's variables) and, for each vector of claimed truth values, the base formula the matrix becomes.

What a machine does with it

The claims are Bools and the statement is conditional on their correctness, which is exactly the shape of the standard alternating check: the existential player claims the whole vector b in one move – there are finitely many, so this is one nondeterministic transition – the universal player then either challenges one claim, which the machine settles by a single tape lookup at the address (copy, var, args) names, or lets the base formula be evaluated. The base formula has no block atoms left, so it is a condition on the source structure alone: a guard of the transition relation, written by the interpretation that emits the machine, and never something the machine has to compute.

Everything is stated for the two-copy structure DescriptiveComplexity.SOBlock.structure₂, the shape of an DescriptiveComplexity.SOGameSpec.move.

The relation symbols are named

A relation symbol of the two-copy language is a nested Sum, and a goal mentioning a raw Sum.inl (Sum.inl r) is ill-typed at implicit transparency – Language.sum has to be unfolded for it to typecheck – so rw and simp fail on it. The three shapes are therefore named (DescriptiveComplexity.twoBaseSym, DescriptiveComplexity.twoFstSym, DescriptiveComplexity.twoSndSym), the case analysis goes through DescriptiveComplexity.exists_symCase, and every realization lemma is stated at a named symbol.

An occurrence of a block atom

structure DescriptiveComplexity.BlockAtom (B : SOBlock) (n : ℕ) : Type

An occurrence of a block atom in a matrix: which of the two copies of the block it reads, which relation variable of the block, and where each of its arguments sits among the matrix's variables.

This is an address: on a machine's tape the cell it names is (copy, var, args applied to the valuation).

• copy : Bool

  The copy of the block the occurrence reads: false is the first copy.

• var : B.ι

  The relation variable of the block.

• args : Fin (B.arity self.var) → Fin n

  Where the arguments of the occurrence sit among the matrix's variables.

def DescriptiveComplexity.BlockAtom.Holds {B : SOBlock} {n : ℕ} {A : Type} (a : BlockAtom B n) (ρ σ : B.Assignment A) (v : Fin n → A) : Prop

The truth value of an occurrence, under two assignments and a valuation.

Equations

• a.Holds ρ σ v = (bif a.copy then σ else ρ) a.var fun (j : Fin (B.arity a.var)) => v (a.args j)

The relation symbols of the two-copy language

@[reducible, inline]

abbrev DescriptiveComplexity.twoBaseSym {K : FirstOrder.Language} {B : SOBlock} {l : ℕ} (r : K.Relations l) : ((K.sum B.lang).sum B.lang).Relations l

A relation symbol of the base vocabulary, read in the two-copy language.

Equations

• DescriptiveComplexity.twoBaseSym r = Sum.inl (Sum.inl r)

@[reducible, inline]

abbrev DescriptiveComplexity.twoFstSym {K : FirstOrder.Language} {B : SOBlock} {l : ℕ} (s : B.lang.Relations l) : ((K.sum B.lang).sum B.lang).Relations l

A relation variable of the first copy of the block.

Equations

• DescriptiveComplexity.twoFstSym s = Sum.inl (Sum.inr s)

@[reducible, inline]

abbrev DescriptiveComplexity.twoSndSym {K : FirstOrder.Language} {B : SOBlock} {l : ℕ} (s : B.lang.Relations l) : ((K.sum B.lang).sum B.lang).Relations l

A relation variable of the second copy of the block.

Equations

• DescriptiveComplexity.twoSndSym s = Sum.inr s

theorem DescriptiveComplexity.exists_symCase {K : FirstOrder.Language} {B : SOBlock} {l : ℕ} (R : ((K.sum B.lang).sum B.lang).Relations l) : (∃ (r : K.Relations l), R = twoBaseSym r) ∨ (∃ (s : B.lang.Relations l), R = twoFstSym s) ∨ ∃ (s : B.lang.Relations l), R = twoSndSym s

The three shapes of a relation symbol of the two-copy language.

Realization at the two-copy structure

def DescriptiveComplexity.twoRealize {K : FirstOrder.Language} {B : SOBlock} {A : Type} [K.Structure A] {n : ℕ} (mat : ((K.sum B.lang).sum B.lang).BoundedFormula Empty n) (ρ σ : B.Assignment A) (v : Fin n → A) : Prop

Realization of a formula over two stacked copies of a block, at the assignments ρ (first copy) and σ (second).

Equations

• DescriptiveComplexity.twoRealize mat ρ σ v = mat.Realize default v

theorem DescriptiveComplexity.twoRealize_bot {K : FirstOrder.Language} {B : SOBlock} {A : Type} [K.Structure A] {n : ℕ} (ρ σ : B.Assignment A) (v : Fin n → A) : ¬twoRealize ⊥ ρ σ v

theorem DescriptiveComplexity.twoRealize_imp {K : FirstOrder.Language} {B : SOBlock} {A : Type} [K.Structure A] {n : ℕ} (ρ σ : B.Assignment A) (v : Fin n → A) (φ₁ φ₂ : ((K.sum B.lang).sum B.lang).BoundedFormula Empty n) : twoRealize (φ₁.imp φ₂) ρ σ v ↔ twoRealize φ₁ ρ σ v → twoRealize φ₂ ρ σ v

Every quantifier-free matrix is a base formula plus claims

def DescriptiveComplexity.bvarOf {n : ℕ} (x : Empty ⊕ Fin n) : Fin n

The bound variable a term of a relational language over Empty ⊕ Fin n reads.

Equations

• DescriptiveComplexity.bvarOf x = Sum.elim (fun (e : Empty) => e.elim) id x

theorem DescriptiveComplexity.elim_bvarOf {n : ℕ} {A : Type} (v : Fin n → A) (d : Empty → A) (x : Empty ⊕ Fin n) : Sum.elim d v x = v (bvarOf x)

theorem DescriptiveComplexity.twoRealize_bdEqual {K : FirstOrder.Language} [K.IsRelational] {B : SOBlock} {n : ℕ} {A : Type} [K.Structure A] {ρ σ : B.Assignment A} {v : Fin n → A} (t₁ t₂ : ((K.sum B.lang).sum B.lang).Term (Empty ⊕ Fin n)) : twoRealize (t₁.bdEqual t₂) ρ σ v ↔ v (bvarOf t₁.varOf) = v (bvarOf t₂.varOf)

An equality of the matrix is an equality of two of its variables.

theorem DescriptiveComplexity.twoRealize_base {K : FirstOrder.Language} [K.IsRelational] {B : SOBlock} {n : ℕ} {A : Type} [K.Structure A] {ρ σ : B.Assignment A} {v : Fin n → A} {l : ℕ} (r : K.Relations l) (ts : Fin l → ((K.sum B.lang).sum B.lang).Term (Empty ⊕ Fin n)) : twoRealize ((twoBaseSym r).boundedFormula ts) ρ σ v ↔ FirstOrder.Language.Structure.RelMap r fun (q : Fin l) => v (bvarOf (ts q).varOf)

A base atom of the matrix is the same atom of the base structure.

theorem DescriptiveComplexity.twoRealize_fst {K : FirstOrder.Language} [K.IsRelational] {B : SOBlock} {n : ℕ} {A : Type} [K.Structure A] {ρ σ : B.Assignment A} {v : Fin n → A} {l : ℕ} (s : B.lang.Relations l) (ts : Fin l → ((K.sum B.lang).sum B.lang).Term (Empty ⊕ Fin n)) : twoRealize ((twoFstSym s).boundedFormula ts) ρ σ v ↔ ρ ↑s fun (j : Fin (B.arity ↑s)) => v (bvarOf (ts (Fin.cast ⋯ j)).varOf)

An atom of the first copy is the first assignment, read at the addresses its arguments name.

theorem DescriptiveComplexity.twoRealize_snd {K : FirstOrder.Language} [K.IsRelational] {B : SOBlock} {n : ℕ} {A : Type} [K.Structure A] {ρ σ : B.Assignment A} {v : Fin n → A} {l : ℕ} (s : B.lang.Relations l) (ts : Fin l → ((K.sum B.lang).sum B.lang).Term (Empty ⊕ Fin n)) : twoRealize ((twoSndSym s).boundedFormula ts) ρ σ v ↔ σ ↑s fun (j : Fin (B.arity ↑s)) => v (bvarOf (ts (Fin.cast ⋯ j)).varOf)

An atom of the second copy is the second assignment, read at the addresses its arguments name.

theorem DescriptiveComplexity.exists_blockClaims {K : FirstOrder.Language} [K.IsRelational] {B : SOBlock} {n : ℕ} {mat : ((K.sum B.lang).sum B.lang).BoundedFormula Empty n} : mat.IsQF → ∃ (m : ℕ) (atoms : Fin m → BlockAtom B n) (sub : (Fin m → Bool) → K.BoundedFormula Empty n), ∀ (A : Type) [inst : K.Structure A] (ρ σ : B.Assignment A) (v : Fin n → A) (b : Fin m → Bool), (∀ (j : Fin m), b j = true ↔ (atoms j).Holds ρ σ v) → (twoRealize mat ρ σ v ↔ (sub b).Realize default v)

A quantifier-free matrix over two copies of a block is a base formula determined by the truth values of finitely many block atoms.

The atoms are listed once and for all; the base formula depends on the vector of claimed values, and the equivalence holds as soon as the claims are correct. That conditional form is what a machine needs: it guesses b, has the claims challenged one at a time by tape lookups, and evaluates the base formula as a guard of its transition relation.