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):

• an atom of the input vocabulary, and an atom of ≤, stay guards, their terms carried across the two languages by DescriptiveComplexity.relTerm (both languages being relational, a term is a variable, so the map is the identity on variables; the three declarations live in DescriptiveComplexity.ArithmeticDefinable, low enough for the translation into the bit logic to share them);
• a plus atom becomes the program DescriptiveComplexity.HeadProgram.plusP on the three heads its arguments live in, and a times atom becomes DescriptiveComplexity.HeadProgram.timesP – the two deciders of DescriptiveComplexity.HeadArith, which is what DescriptiveComplexity.HeadProgram.wireP lets a node of a control graph be.

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

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

• DescriptiveComplexity.HeadProgram.qdepthA FirstOrder.Language.BoundedFormula.falsum = 0
• DescriptiveComplexity.HeadProgram.qdepthA (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = 0
• DescriptiveComplexity.HeadProgram.qdepthA (FirstOrder.Language.BoundedFormula.rel R ts) = 0
• DescriptiveComplexity.HeadProgram.qdepthA (φ₁.imp φ₂) = max (DescriptiveComplexity.HeadProgram.qdepthA φ₁) (DescriptiveComplexity.HeadProgram.qdepthA φ₂)
• DescriptiveComplexity.HeadProgram.qdepthA φ.all = DescriptiveComplexity.HeadProgram.qdepthA φ + 2

The layout of the arithmetic scratch heads

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.

The atoms

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.

The evaluator

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

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.evalArithP sh acc cnt cand tmk a b mk x✝¹ x✝ FirstOrder.Language.BoundedFormula.falsum = DescriptiveComplexity.HeadProgram.exitP false

Correctness

AC⁰ ⊆ LOGSPACE

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. Registered in the Lax archive as Lax895169.ACZeroInLogSpace.ac0Definable_dtcDefinable.

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. Registered in the Lax archive as Lax895169.ACZeroInLogSpace.ac0Definable_mem_LOGSPACE.

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. Registered in the Lax archive as Lax895169.ACZeroInLogSpace.ac0Definable_mem_NL.