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

The trace of a sweep

Definability of the machine

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⁰. Registered in the Lax archive as Lax895169.ACZeroIsLogTime.ltDecidable_bitDefinable.

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.