The upper fence: a machine's acceptance is a sentence of the bit-level logic

Every problem decided by an alternating machine with a logarithmic clock and a bit-level base is defined by a prenex sentence of FO(≤, +, BIT) (DescriptiveComplexity.LTDecidable.bitDefinable). With DescriptiveComplexity.BitDefinable.ltDecidable this makes the model exactly that logic.

The four moving parts

• The guesses are quantifiers. A register holds an element of the universe, and filling it existentially or universally is ∃ or ∀ – the alternation structure of the machine is the quantifier prefix of the sentence, on the nose.
• A query is an atom. Reading the instance at a tuple of registers is an atomic formula of the input vocabulary; no encoding of addresses is involved, which is the whole reason the model fits a structure-based framework.
• A read is an atom too. DescriptiveComplexity.BaseTest.bit is the bit atom of the logic and nothing more: both name a bit position by an element, so the translation has nothing to do.
• A sweep is a guessed trace. This is the content. A sweep carries σ bits of state past each of the posCount A bit positions, so its entire history is σ bit vectors over the positions – and a bit vector over the positions is an element of the universe. The formula therefore guesses σ elements, says with DescriptiveComplexity.BitIx that the bit of the j-th at each index is what the transition of the sweep produces there, and reads acceptance off the top. Determinism of the sweep makes the guess unique, so the existential is faithful.

Two places the index naming pays

The trace is pinned by a condition relating the bit at an index to the bit at the index below, and under the index naming that is the cover relation of the order (DescriptiveComplexity.stepAt), where naming positions by their place value made it a doubling. The end of the tape is likewise read rather than computed: DescriptiveComplexity.IsTopIx is “the highest index carrying a bit of the greatest element”, an order condition on the bit atom (DescriptiveComplexity.isTopIx_iff_bits).

The one asymmetry: the last position

A bit vector over all the positions need not be a rank – the universe need not have a power of two elements – so the trace elements can only carry the state up to the index below the top (DescriptiveComplexity.exists_orank_testBit). The state after the top position is therefore carried by σ further elements used as flags, one bit each, read as “nonzero rank”. Everything else in the construction is uniform.

Two statements, one construction

Landing in FO(≤, +, BIT) is what the construction below does; landing in FO(≤, +, ×) is that plus one lemma – DescriptiveComplexity.powArithDef, the definability of i ↦ 2 ^ i. Both are unconditional, and the statement of record here is the first, DescriptiveComplexity.LTDecidable.bitDefinable: it is the classical logic for AC⁰, and it is what the converse direction reads.

Boolean expressions, read as formulas

theorem DescriptiveComplexity.bitDef_bitExpr {L : FirstOrder.Language} {α V : Type} {val : V → ArithRel L α} (h : ∀ (z : V), BitDef (val z)) (e : BitExpr V) : BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : α → A) => BitExpr.Holds (fun (z : V) => val z A v) e

A Boolean expression of definable bits is definable: the translation is a recursion over the expression, not an enumeration of its truth table.

The trace of a sweep

def DescriptiveComplexity.stepAt {ρ : ℕ} {A : Type} [LinearOrder A] (S : Sweep ρ) (x : Fin ρ → A) (t : Fin S.σ → A) (i : A) (j : Fin S.σ) : Prop

The transition of a sweep at an index, as a statement about a guessed trace: the state bits before the position are the initial ones at the lowest index, and the trace bits at the index covered by this one otherwise. Under the index naming the previous position is the predecessor in the order, so nothing but ≤ is needed to find it.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.SweepWitness {ρ : ℕ} {A : Type} [LinearOrder A] [Finite A] (S : Sweep ρ) (x : Fin ρ → A) (t f : Fin S.σ → A) : Prop

What the formula asks of the guessed trace and flags: the trace records the state after each index below the top, the flags record the state after the top position, and the acceptance condition holds of the flags – of the initial state, if the universe has no bit position at all.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.storedAfter {ρ : ℕ} {A : Type} [LinearOrder A] [Finite A] (S : Sweep ρ) (t f : Fin S.σ → A) (i : ℕ) (j : Fin S.σ) : Prop

The state the witnesses record after position i: a trace bit below the top, a flag at the top.

Equations

• DescriptiveComplexity.storedAfter S t f i j = if i + 1 < DescriptiveComplexity.posCount A then (DescriptiveComplexity.orank (t j)).testBit i = true else DescriptiveComplexity.orank (f j) ≠ 0

theorem DescriptiveComplexity.exists_isTopIx_iff {A : Type} [LinearOrder A] [Finite A] : (∃ (i : A), IsTopIx i) ↔ 0 < posCount A

A top index exists exactly when the universe has more than one element.

theorem DescriptiveComplexity.stepAt_iff {ρ : ℕ} {A : Type} [LinearOrder A] [Finite A] (S : Sweep ρ) (x : Fin ρ → A) (t : Fin S.σ → A) (i : A) (j : Fin S.σ) : stepAt S x t i j ↔ BitExpr.eval (Sum.elim (fun (j' : Fin S.σ) => if orank i = 0 then S.init j' else (orank (t j')).testBit (orank i - 1)) fun (k : Fin ρ) => (orank (x k)).testBit (orank i)) (S.step j) = true

The transition read from the trace is the transition of the sweep: at the index i, the guessed bits say exactly what the automaton computes from the state before that position.

theorem DescriptiveComplexity.storedAfter_iff_state {ρ : ℕ} {A : Type} [LinearOrder A] [Finite A] (S : Sweep ρ) (x : Fin ρ → A) (t f : Fin S.σ → A) (hw : SweepWitness S x t f) (i : ℕ) : i < posCount A → ∀ (j : Fin S.σ), storedAfter S t f i j ↔ S.state x (i + 1) j = true

The guessed trace is the run: the witnesses of the formula record, position by position, the states of the sweep. Determinism does the work – the local conditions pin the trace by induction along the indices.

theorem DescriptiveComplexity.sweepWitness_iff {ρ : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (S : Sweep ρ) (x : Fin ρ → A) : (∃ (t : Fin S.σ → A) (f : Fin S.σ → A), SweepWitness S x t f) ↔ S.Accepts x

The formula says what the sweep does.

Definability of the machine

theorem DescriptiveComplexity.bitDef_stepAt {L : FirstOrder.Language} {α : Type} {ρ : ℕ} (S : Sweep ρ) (reg : Fin ρ → α) (tr : Fin S.σ → α) (p : α) (j : Fin S.σ) : BitDef fun (_A : Type) (x : L.Structure _A) (x_1 : LinearOrder _A) (x_2 : Finite _A) (x_3 : Nonempty _A) (v : α → _A) => stepAt S (fun (k : Fin ρ) => v (reg k)) (fun (j' : Fin S.σ) => v (tr j')) (v p) j

The transition condition at an index is definable.

theorem DescriptiveComplexity.bitDef_sweep {L : FirstOrder.Language} {α : Type} {ρ : ℕ} (S : Sweep ρ) (reg : Fin ρ → α) : BitDef fun (_A : Type) (x : L.Structure _A) (x_1 : LinearOrder _A) (x_2 : Finite _A) (x_3 : Nonempty _A) (v : α → _A) => S.Accepts fun (k : Fin ρ) => v (reg k)

A sweep is definable: the formula guesses the trace and the flags, and asks that they be the run.

theorem DescriptiveComplexity.bitDef_baseTest {L : FirstOrder.Language} {α : Type} {ρ : ℕ} (t : BaseTest L ρ) (reg : Fin ρ → α) : BitDef fun (_A : Type) (x : L.Structure _A) (x_1 : LinearOrder _A) (x_2 : Finite _A) (x_3 : Nonempty _A) (v : α → _A) => t.Holds fun (k : Fin ρ) => v (reg k)

A base test is definable: sweeps by the construction above, reads and queries as atoms, and the Boolean structure by the closure lemmas.

The inclusion

theorem DescriptiveComplexity.LTDecidable.bitDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : LTDecidable P) : BitDefinable P

The machine model is inside the bit-level logic: every problem decided by an alternating machine with a logarithmic clock and a bit-level base is defined by a prenex sentence over ≤, + and the bit at an index. The guesses are the quantifier prefix, the queries and the reads are atoms, and each sweep is a guessed trace pinned by its transition.

With DescriptiveComplexity.BitDefinable.ltDecidable this makes the fence an equality: the machine model is exactly characterized by a logic, and by the logic that is classically AC⁰.

theorem DescriptiveComplexity.LTDecidable.ac0Definable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : LTDecidable P) : AC0Definable P

The machine model is inside AC⁰: a corollary of the statement above and of the translation of the bit-level logic into FO(≤, +, ×), whose bit atom is DescriptiveComplexity.powArithDef and whose other atoms are numeric predicates outright.