Documentation

DescriptiveComplexity.Exponential.Matrix

Translating a quantifier-free matrix #

DescriptiveComplexity.Exponential.PointAtoms writes each atom of a sentence over an expansion as a sentence of the quantifier prefix. This file closes the Boolean connectives over them: a quantifier-free formula whose free variables range over the points of the expanded universe becomes a sentence of the prefix, variable i read at round i.

Two points of technique.

The recursion is total, the correctness is not. IsQF is a Prop, so a definition cannot recurse on it. DescriptiveComplexity.ExpExpansion.translQF is therefore defined on every bounded formula, sending a quantifier node – and an atom mentioning a bound variable – to ⊥; correctness is then proved by induction on FirstOrder.Language.BoundedFormula.IsQF at n = 0, where no such node is reachable. This is the shape the abandoned quantifier-free-reduction track would have used too, and it is the standard way to recurse on a syntactic class carved out by a Prop.

Function symbols are impossible, not junk. The expanded vocabulary and the order vocabulary are both relational, so FirstOrder.Language.Term.func is eliminated by isEmptyElim rather than mapped to a default: a term is a variable (DescriptiveComplexity.ExpExpansion.termVar). Only the distinction between a free and a bound variable needs an Option.

Terms are variables #

source
def DescriptiveComplexity.ExpExpansion.termVar {L : FirstOrder.Language} {X : ExpExpansion L} {m n : ℕ} :
(X.E.sum FirstOrder.Language.order).Term (Fin m ⊕ Fin n) → Fin m ⊕ Fin n

The variable a term is. Over a relational vocabulary there is nothing else a term can be, so the function case is isEmptyElim.

Equations
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.ExpExpansion.realize_termVar {L : FirstOrder.Language} {X : ExpExpansion L} {m : ℕ} {A : Type} [(X.E.sum FirstOrder.Language.order).Structure A] {n : ℕ} (v : Fin m ⊕ Fin n → A) (t : (X.E.sum FirstOrder.Language.order).Term (Fin m ⊕ Fin n)) :
    FirstOrder.Language.Term.realize v t = v (termVar t)
    Dependency graph

    The atoms, selected by the relation symbol #

    source
    noncomputable def DescriptiveComplexity.ExpExpansion.atomOf {L : FirstOrder.Language} (X : ExpExpansion L) (m : ℕ) {k : ℕ} (r : (X.E.sum FirstOrder.Language.order).Relations k) (idx : Fin k → Fin m) :
    ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock m).lang).Sentence

    The prefix-level sentence of an atom, given the round each argument names: a relation of the expanded vocabulary, or the order.

    Equations
    Instances For
      Dependency graph

      The translation #

      The recursion carries a map bv sending each bound variable to a round. A quantifier node is sent to ⊥, so bv is never extended and never consulted at the depth the correctness proof works at – where it is finZeroElim, the empty map. Carrying it is what keeps the definition total without an Option in every atom.

      source
      noncomputable def DescriptiveComplexity.ExpExpansion.translQF {L : FirstOrder.Language} (X : ExpExpansion L) (m : ℕ) {n : ℕ} :
      (Fin n → Fin m) → (X.E.sum FirstOrder.Language.order).BoundedFormula (Fin m) n → ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock m).lang).Sentence

      The translation of a quantifier-free matrix. Total, so that it is a definition; correct on quantifier-free formulas, which is DescriptiveComplexity.ExpExpansion.realize_translQF.

      Equations
      Instances For
        Dependency graph

        Correctness #

        source
        theorem DescriptiveComplexity.ExpExpansion.elim_finZeroElim {L : FirstOrder.Language} {X : ExpExpansion L} {m : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (pts : Fin m → X.Map A) (x : Fin m ⊕ Fin 0) :
        Sum.elim pts default x = pts (Sum.elim id finZeroElim x)

        At no bound variables, a valuation of the free variables reads a variable through its round.

        Dependency graph
        source
        theorem DescriptiveComplexity.ExpExpansion.realize_translQF {L : FirstOrder.Language} {X : ExpExpansion L} {m : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (pts : Fin m → X.Map A) {φ : (X.E.sum FirstOrder.Language.order).Formula (Fin m)} (hqf : FirstOrder.Language.BoundedFormula.IsQF φ) :
        A ⊨ X.translQF m finZeroElim φ ↔ φ.Realize pts

        The matrix says what it should: on a quantifier-free formula, the translated sentence holds of the prefix exactly when the formula holds of the points the rounds carry.

        Dependency graph