Documentation

DescriptiveComplexity.HeadEvalArith

Evaluating an arithmetic formula with heads, and AC⁰ ⊆ LOGSPACE #

The last step of the machine route to the bottom class: a deterministic multi-head automaton decides any fixed sentence of FO(≤, +, ×), whence DescriptiveComplexity.ac0Definable_mem_LOGSPACE.

What is new here, against HeadEval #

DescriptiveComplexity.HeadProgram.evalP already evaluates a first-order formula of the head positions: atoms are quantifier-free guards, implication is a branch, and a quantifier is a sweep of two fresh heads. It cannot be used as it stands, for the reason the whole file exists: the formula to evaluate lives over L.sum Language.arith, while the machine's guards live over L.sum Language.order. A guard may not read plus or times – they are not relations of the instance at all, but functions of the order – so those two atoms must be computed, not read.

So this is evalP with one case split four ways (DescriptiveComplexity.HeadProgram.arithAtomP):

Everything else – the sweep, the branch, the head accounting – is reused from HeadEval unchanged, which is why this file is short.

The head layout #

DescriptiveComplexity.HeadProgram.ArithScratch pins the seven heads the arithmetic needs to the seven positions above the quantifier region: the four working heads of a multiplication first, then the three scratch heads of an addition. It has to be above the quantifier region because the fragments' own protection level is the evaluator's current level d, which grows as the evaluation enters quantifiers – and the invariant that makes the induction go through is that d + qdepth does not change.

The result, and what it does not say #

DescriptiveComplexity.ac0Definable_mem_LOGSPACE: everything AC⁰ definable is in DescriptiveComplexity.LOGSPACE. With DescriptiveComplexity.exists_ac0Definable_not_foDefinable and DescriptiveComplexity.parity_mem_LOGSPACE this pins the bottom of the ladder:

FO(≤) ⊊ AC⁰ ⊆ LOGSPACE ⊆ NL ⊆ PTIME

with the first inclusion strict and the second's strictness exactly the switching lemma (PARITY is in LOGSPACE here, and outside AC⁰ classically), which this library does not prove. It also supersedes DescriptiveComplexity.ac0Definable_mem_PTIME, which the fixed-point route gave for a tenth of the work; that route is kept, both because it is the cheap way to the same corollaries and because the two together say something the machine route alone does not – that the numeric predicates are simultaneously one induction and one deterministic walk.

The quantifier budget of an arithmetic formula #

source
def DescriptiveComplexity.HeadProgram.qdepthA {L : FirstOrder.Language} {α : Type} {n : ℕ} :
(L.sum FirstOrder.Language.arith).BoundedFormula α n → ℕ

How many heads an arithmetic evaluation needs: two per nested quantifier, exactly as for DescriptiveComplexity.HeadProgram.qdepth, the arithmetic atoms needing none of their own (they have their scratch heads at the top).

Equations
Instances For
    Dependency graph

    The layout of the arithmetic scratch heads #

    source
    structure DescriptiveComplexity.HeadProgram.ArithScratch {K : ℕ} (acc cnt cand tmk a b mk : Fin K) (S : ℕ) :
    Prop

    The seven heads the arithmetic fragments need, pinned to the seven positions from S on: a multiplication's four working heads, then an addition's three scratch heads. S is the top of the quantifier region, so every level the evaluator reaches is at most S.

    • hacc : ↑acc = S

      The accumulator sits at S.

    • hcnt : ↑cnt = S + 1

      The round counter sits at S + 1.

    • hcand : ↑cand = S + 2

      The scan's candidate sits at S + 2.

    • htmk : ↑tmk = S + 3

      The scan's marker sits at S + 3.

    • ha : ↑a = S + 4

      The addition's running head sits at S + 4.

    • hb : ↑b = S + 5

      The addition's counter sits at S + 5.

    • hmk : ↑mk = S + 6

      The addition's marker sits at S + 6.

    Instances For
      Dependency graph
      source
      theorem DescriptiveComplexity.HeadProgram.ArithScratch.plusHeads {K : ℕ} {acc cnt cand tmk a b mk : Fin K} {S d : ℕ} (hs : ArithScratch acc cnt cand tmk a b mk S) {i j k : Fin K} (hi : ↑i < d) (hj : ↑j < d) (hk : ↑k < d) (hd : d ≤ S) :
      PlusHeads i j k a b mk d

      The layout gives an addition the head discipline it asks for, at any level the evaluator can reach.

      Dependency graph
      source
      theorem DescriptiveComplexity.HeadProgram.ArithScratch.timesHeads {K : ℕ} {acc cnt cand tmk a b mk : Fin K} {S d : ℕ} (hs : ArithScratch acc cnt cand tmk a b mk S) {i j k : Fin K} (hi : ↑i < d) (hj : ↑j < d) (hk : ↑k < d) (hd : d ≤ S) :
      TimesHeads i j k acc cnt cand tmk a b mk d (S + 4)

      The layout gives a multiplication the three-level head discipline it asks for, the middle level being the top of its four working heads.

      Dependency graph

      The atoms #

      source
      noncomputable def DescriptiveComplexity.HeadProgram.arithAtomP {L : FirstOrder.Language} [L.IsRelational] {K : ℕ} {α : Type} (acc cnt cand tmk a b mk : Fin K) {n l : ℕ} (hv : α ⊕ Fin l → Fin K) (_R : (L.sum FirstOrder.Language.arith).Relations n) :
      (Fin n → (L.sum FirstOrder.Language.arith).Term (α ⊕ Fin l)) → HeadProgram L K

      An arithmetic atom, as a program: the input vocabulary and ≤ are read as guards, plus and times are computed by the deciders of DescriptiveComplexity.HeadArith.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Dependency graph

        The evaluator #

        source
        noncomputable def DescriptiveComplexity.HeadProgram.evalArithP {L : FirstOrder.Language} [L.IsRelational] {K : ℕ} {α : Type} (sh : ℕ → Fin K) (acc cnt cand tmk a b mk : Fin K) {n : ℕ} :
        ℕ → (α ⊕ Fin n → Fin K) → (L.sum FirstOrder.Language.arith).BoundedFormula α n → HeadProgram L K

        The evaluator of an arithmetic formula: evalP with the arithmetic atoms computed instead of read.

        Equations
        Instances For
          Dependency graph

          Correctness #

          source
          theorem DescriptiveComplexity.HeadProgram.headLocalA_realize {L : FirstOrder.Language} {K : ℕ} {α A : Type} [L.Structure A] [LinearOrder A] {n d : ℕ} (hv : α ⊕ Fin n → Fin K) (ψ : (L.sum FirstOrder.Language.arith).BoundedFormula α n) (hlow : ∀ (v : α ⊕ Fin n), ↑(hv v) < d) :
          HeadLocal d fun (x : Fin K → A) => ψ.Realize (fun (v : α) => x (hv (Sum.inl v))) fun (i : Fin n) => x (hv (Sum.inr i))

          What an arithmetic formula says of the heads depends only on the heads its variables live in – the arithmetic twin of DescriptiveComplexity.HeadProgram.headLocal_realize.

          Dependency graph
          source
          theorem DescriptiveComplexity.HeadProgram.decides_arithAtomP {L : FirstOrder.Language} [L.IsRelational] {K : ℕ} {α A : Type} [L.Structure A] [LinearOrder A] [Finite A] {acc cnt cand tmk a b mk : Fin K} {S : ℕ} (hs : ArithScratch acc cnt cand tmk a b mk S) (hSK : S + 7 ≤ K) {n l d : ℕ} (hv : α ⊕ Fin l → Fin K) (hlow : ∀ (v : α ⊕ Fin l), ↑(hv v) < d) (hd : d ≤ S) (R : (L.sum FirstOrder.Language.arith).Relations n) (ts : Fin n → (L.sum FirstOrder.Language.arith).Term (α ⊕ Fin l)) :
          (arithAtomP acc cnt cand tmk a b mk hv R ts).Decides A d fun (x : Fin K → A) => (FirstOrder.Language.BoundedFormula.rel R ts).Realize (fun (v : α) => x (hv (Sum.inl v))) fun (i : Fin l) => x (hv (Sum.inr i))

          An arithmetic atom is decided: read as a guard where it is an input relation or the order, computed by a fragment where it is plus or times.

          Dependency graph
          source
          theorem DescriptiveComplexity.HeadProgram.decides_evalArithP {L : FirstOrder.Language} [L.IsRelational] {K : ℕ} {α A : Type} [L.Structure A] [LinearOrder A] [Finite A] {acc cnt cand tmk a b mk : Fin K} {S : ℕ} (sh : ℕ → Fin K) (hsh : ∀ i < K, ↑(sh i) = i) (hs : ArithScratch acc cnt cand tmk a b mk S) (hSK : S + 7 ≤ K) {n : ℕ} (ψ : (L.sum FirstOrder.Language.arith).BoundedFormula α n) (d : ℕ) (hv : α ⊕ Fin n → Fin K) :
          (∀ (v : α ⊕ Fin n), ↑(hv v) < d) → d + qdepthA ψ ≤ S → (evalArithP sh acc cnt cand tmk a b mk d hv ψ).Decides A d fun (x : Fin K → A) => ψ.Realize (fun (v : α) => x (hv (Sum.inl v))) fun (i : Fin n) => x (hv (Sum.inr i))

          The arithmetic evaluator is correct: it decides the formula, reading its variables off the heads they live in, and gives those heads back untouched.

          Dependency graph
          source
          theorem DescriptiveComplexity.HeadProgram.deterministic_evalArithP {L : FirstOrder.Language} [L.IsRelational] {K : ℕ} {α A : Type} [L.Structure A] [LinearOrder A] {acc cnt cand tmk a b mk : Fin K} (sh : ℕ → Fin K) {n : ℕ} (ψ : (L.sum FirstOrder.Language.arith).BoundedFormula α n) (d : ℕ) (hv : α ⊕ Fin n → Fin K) :
          (evalArithP sh acc cnt cand tmk a b mk d hv ψ).Deterministic A

          The arithmetic evaluator is deterministic: it sweeps and it computes, it does not guess – the two arithmetic fragments being deterministic too.

          Dependency graph

          AC⁰ ⊆ LOGSPACE #

          source
          theorem DescriptiveComplexity.AC0Definable.dtcDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : AC0Definable P) :
          DTCDefinable P

          AC⁰ ⊆ FO(DTC): the sentence is evaluated by a deterministic multi-head automaton – the quantifiers swept, the input atoms and the order read as guards, and the two numeric atoms computed by DescriptiveComplexity.HeadProgram.plusP and DescriptiveComplexity.HeadProgram.timesP.

          The machine has qdepthA φ + 7 heads: two per nested quantifier, then the four working heads of a multiplication and the three scratch heads of an addition.

          Dependency graph
          source
          theorem DescriptiveComplexity.ac0Definable_mem_LOGSPACE {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : AC0Definable P) :
          LOGSPACE.Mem P

          AC⁰ ⊆ LOGSPACE. The bottom of the ladder, pinned: with DescriptiveComplexity.FODefinable.ac0Definable and DescriptiveComplexity.exists_ac0Definable_not_foDefinable on one side and DescriptiveComplexity.LOGSPACE_subset_NL on the other,

          FO(≤) ⊊ AC⁰ ⊆ LOGSPACE ⊆ NL ⊆ PTIME,

          with the first inclusion strict and the strictness of the second exactly the switching lemma – DescriptiveComplexity.PARITY is in LOGSPACE here and outside AC⁰ classically, which this library does not prove.

          Dependency graph
          source
          theorem DescriptiveComplexity.ac0Definable_mem_NL {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : AC0Definable P) :
          NL.Mem P

          AC⁰ ⊆ NL, by the inclusion of LOGSPACE.

          Dependency graph