Documentation

DescriptiveComplexity.Problems.Wide.DrawMatrix

A quantifier-free matrix is a Boolean function of its atoms #

The machine evaluates the matrix of its step formula atom by atom: a subroutine per atom, each ending in a state that records whether that atom holds, the accumulating assignment kept in the coordinates of the state – one coordinate per atom, holding one of the two designated elements the tracks of DescriptiveComplexity.Problems.Wide.DrawTracks carry. When every atom has been evaluated, one transition reads off the answer.

For that to be correct the matrix must be a function of its atoms' truths, and this file says so:

The last two are what make the phase count linear in the number of atoms rather than exponential in it: the machine visits qfAtoms once and the final transition is a disjunction over the assignments that satisfy qfValue, a finite list a defining formula can write out.

The recursion is total, the correctness is not. IsQF is a Prop, so a definition cannot recurse on it; qfValue and qfAtoms are therefore defined on every bounded formula, sending a quantifier node to False and to [], and correctness is proved by induction on FirstOrder.Language.BoundedFormula.IsQF, where no such node is reachable. This is the shape of DescriptiveComplexity.ExpExpansion.translQF in Exponential/Matrix.lean, and it is the standard way to recurse on a syntactic class carved out by a Prop. Discarding the quantifier node is also why the list stays at one depth: a quantifier-free formula never changes it.

source
def DescriptiveComplexity.Draw.qfAtoms {L : FirstOrder.Language} {α : Type} {n : ℕ} :
L.BoundedFormula α n → List (L.BoundedFormula α n)

The atoms of a formula, left to right. Total on every bounded formula: a quantifier node contributes none, which is what keeps the list at one depth.

Equations
Instances For
    Dependency graph
    source
    def DescriptiveComplexity.Draw.qfValue {L : FirstOrder.Language} {α : Type} {n : ℕ} :
    L.BoundedFormula α n → (L.BoundedFormula α n → Prop) → Prop

    The value of a formula given a truth value for each atom: the Boolean function a machine computes once its subroutines have evaluated the atoms. Total, for the reason in the module docstring.

    Equations
    Instances For
      Dependency graph
      source
      theorem DescriptiveComplexity.Draw.qfValue_congr {L : FirstOrder.Language} {α : Type} {n : ℕ} (φ : L.BoundedFormula α n) (val val' : L.BoundedFormula α n → Prop) :
      (∀ a ∈ qfAtoms φ, val a ↔ val' a) → (qfValue φ val ↔ qfValue φ val')

      Only the atoms matter. Two assignments agreeing on the atoms of a formula give it the same value – so a machine that has evaluated qfAtoms has evaluated the matrix, and the finitely many assignments to those atoms are what the final transition is a disjunction over.

      Dependency graph
      source
      theorem DescriptiveComplexity.Draw.realize_qfValue {L : FirstOrder.Language} {α M : Type} [L.Structure M] {n : ℕ} {φ : L.BoundedFormula α n} :
      φ.IsQF → ∀ (v : α → M) (xs : Fin n → M), φ.Realize v xs ↔ qfValue φ fun (a : L.BoundedFormula α n) => a.Realize v xs

      A quantifier-free formula is the Boolean function of its atoms. Its realization is DescriptiveComplexity.Draw.qfValue at the assignment that reads each atom off the structure – which is exactly what the machine's subroutines compute, one atom at a time.

      Dependency graph