Alternating machines with a logarithmic clock, at the level of bits

The machine side of the bottom of the ladder: an alternating random-access machine whose registers hold addresses of the instance, whose clock is the number of bit positions of those addresses – logarithmic in the size of the universe – and whose deterministic steps are bit operations, never a numeric predicate.

The three parts of a machine

• Guesses. A machine names regs registers and a polarity for each (DescriptiveComplexity.LTMachine.pol): the registers are filled in order, existentially or universally, by the two players. A register holds an element of the universe, that is, an address of posCount A bits, so filling one is a block of the classical Σₖ-TIME(log n) normal form – a logarithmic number of guessed bits – and an alternation is a change of polarity along the list.
• Queries. The instance is read only through DescriptiveComplexity.BaseTest.query: an input relation at a tuple of registers. This is the random access of the model, and in a structure-based framework it needs no index tape: reading the input at an address is evaluating a relation at a tuple.
• Sweeps. Everything the machine computes it computes bit by bit, with DescriptiveComplexity.Sweep: one pass over the bit positions, from the lowest to the highest, run by a finite automaton with σ state bits that reads, at each position, one bit of each register. A base test is a Boolean combination of sweeps, reads and queries, so a machine performs a constant number of passes over a logarithmic tape: a logarithmic clock, and a constant number of head reversals.
• Reads. DescriptiveComplexity.BaseTest.bit: the bit of one register at the position named by another register, that is, DescriptiveComplexity.BitIx. This is the second random access of the model – the machine addresses its own bits, not only the instance – and it is the one thing a sweep cannot do: finding the position orank i requires counting positions, which a finite automaton passing a constant number of bits cannot.

Why the base has to be this weak, and what it can still do

Letting the base evaluate an atom of ≤, + or × in one step would make the model a prenex FO(≤, +, ×) sentence in disguise, and the bridge to the logic vacuous. Sweeps and reads are the honest opposite: they see nothing but bits, and the arithmetic has to be built – DescriptiveComplexity.leSweep and DescriptiveComplexity.plusSweep (in DescriptiveComplexity.LogTime.Arith) are the comparison and the ripple-carry addition, exactly as DescriptiveComplexity.HeadArith builds them one resource bound higher. A read is an addressing operation, not an arithmetic one: it computes nothing, and the model still has no product.

Both restrictions are real, and their boundary is worth naming: a sweep carries σ bits of state past each position, so a constant number of sweeps carries a constant number of bits per position, that is, O(log n) bits of trace in total – which is what a first-order formula can guess, one element per bit vector (DescriptiveComplexity.LogTime.Simulate). A machine that could count its positions, or revisit them unboundedly often, would leave that budget, and with it the reach of the simulation.

Without the reads the model would be strictly weaker than AC⁰, and provably so: with a base of sweeps alone every atom is a regular relation of the bit tracks, alternating quantifiers over registers are projections, and the whole model collapses to what a finite automaton reading Nat.card A in binary can decide. That is the reason a read is a primitive here and not a convenience; see DescriptiveComplexity.LogTime.

Boolean expressions over bits

inductive DescriptiveComplexity.BitExpr (V : Type) : Type

A Boolean expression over bit variables: what a sweep computes in one step, and what its acceptance condition is. Expressions rather than functions, so that the translation into a formula is a recursion rather than an enumeration of a truth table.

• var {V : Type} (v : V) : BitExpr V

  A bit variable.

• tt {V : Type} : BitExpr V

  The constant true.

• ff {V : Type} : BitExpr V

  The constant false.

• not {V : Type} (e : BitExpr V) : BitExpr V

  Negation.

• and {V : Type} (e f : BitExpr V) : BitExpr V

  Conjunction.

• or {V : Type} (e f : BitExpr V) : BitExpr V

  Disjunction.

def DescriptiveComplexity.BitExpr.eval {V : Type} (val : V → Bool) : BitExpr V → Bool

The value of an expression under a Bool-valued assignment.

Equations

• DescriptiveComplexity.BitExpr.eval val (DescriptiveComplexity.BitExpr.var v) = val v
• DescriptiveComplexity.BitExpr.eval val DescriptiveComplexity.BitExpr.tt = true
• DescriptiveComplexity.BitExpr.eval val DescriptiveComplexity.BitExpr.ff = false
• DescriptiveComplexity.BitExpr.eval val e.not = !DescriptiveComplexity.BitExpr.eval val e
• DescriptiveComplexity.BitExpr.eval val (e.and f) = (DescriptiveComplexity.BitExpr.eval val e && DescriptiveComplexity.BitExpr.eval val f)
• DescriptiveComplexity.BitExpr.eval val (e.or f) = (DescriptiveComplexity.BitExpr.eval val e || DescriptiveComplexity.BitExpr.eval val f)

def DescriptiveComplexity.BitExpr.Holds {V : Type} (val : V → Prop) : BitExpr V → Prop

The value of an expression under a Prop-valued assignment: the reading a first-order formula gives it.

Equations

• DescriptiveComplexity.BitExpr.Holds val (DescriptiveComplexity.BitExpr.var v) = val v
• DescriptiveComplexity.BitExpr.Holds val DescriptiveComplexity.BitExpr.tt = True
• DescriptiveComplexity.BitExpr.Holds val DescriptiveComplexity.BitExpr.ff = False
• DescriptiveComplexity.BitExpr.Holds val e.not = ¬DescriptiveComplexity.BitExpr.Holds val e
• DescriptiveComplexity.BitExpr.Holds val (e.and f) = (DescriptiveComplexity.BitExpr.Holds val e ∧ DescriptiveComplexity.BitExpr.Holds val f)
• DescriptiveComplexity.BitExpr.Holds val (e.or f) = (DescriptiveComplexity.BitExpr.Holds val e ∨ DescriptiveComplexity.BitExpr.Holds val f)

def DescriptiveComplexity.BitExpr.mapVar {V W : Type} (f : V → W) : BitExpr V → BitExpr W

Renaming the bit variables of an expression.

Equations

• DescriptiveComplexity.BitExpr.mapVar f (DescriptiveComplexity.BitExpr.var v) = DescriptiveComplexity.BitExpr.var (f v)
• DescriptiveComplexity.BitExpr.mapVar f DescriptiveComplexity.BitExpr.tt = DescriptiveComplexity.BitExpr.tt
• DescriptiveComplexity.BitExpr.mapVar f DescriptiveComplexity.BitExpr.ff = DescriptiveComplexity.BitExpr.ff
• DescriptiveComplexity.BitExpr.mapVar f e.not = (DescriptiveComplexity.BitExpr.mapVar f e).not
• DescriptiveComplexity.BitExpr.mapVar f (e.and f_1) = (DescriptiveComplexity.BitExpr.mapVar f e).and (DescriptiveComplexity.BitExpr.mapVar f f_1)
• DescriptiveComplexity.BitExpr.mapVar f (e.or f_1) = (DescriptiveComplexity.BitExpr.mapVar f e).or (DescriptiveComplexity.BitExpr.mapVar f f_1)

Sweeps

structure DescriptiveComplexity.Sweep (ρ : ℕ) : Type

A sweep: one pass over the bit positions of the universe, from the lowest to the highest, by a finite automaton with σ state bits reading, at each position, one bit of each of the ρ registers.

• σ : ℕ

  The number of state bits.

• init : Fin self.σ → Bool

  The state before the lowest position.

• step : Fin self.σ → BitExpr (Fin self.σ ⊕ Fin ρ)

  The next state: one Boolean expression per state bit, over the old state and the register bits at the current position.

• acc : BitExpr (Fin self.σ)

  The acceptance condition, read from the state after the last position.

noncomputable def DescriptiveComplexity.Sweep.state {ρ : ℕ} {A : Type} [LinearOrder A] (S : Sweep ρ) (x : Fin ρ → A) : ℕ → Fin S.σ → Bool

The state of a sweep before position i: the automaton starts in DescriptiveComplexity.Sweep.init and takes one step per position, reading the bits of the registers there.

Equations

• S.state x 0 = S.init
• S.state x i.succ = fun (j : Fin S.σ) => DescriptiveComplexity.BitExpr.eval (Sum.elim (S.state x i) fun (k : Fin ρ) => (DescriptiveComplexity.orank (x k)).testBit i) (S.step j)

@[simp]

theorem DescriptiveComplexity.Sweep.state_zero {ρ : ℕ} {A : Type} [LinearOrder A] (S : Sweep ρ) (x : Fin ρ → A) : S.state x 0 = S.init

theorem DescriptiveComplexity.Sweep.state_succ {ρ : ℕ} {A : Type} [LinearOrder A] (S : Sweep ρ) (x : Fin ρ → A) (i : ℕ) (j : Fin S.σ) : S.state x (i + 1) j = BitExpr.eval (Sum.elim (S.state x i) fun (k : Fin ρ) => (orank (x k)).testBit i) (S.step j)

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

A sweep accepts when its acceptance condition holds of the state left after the last bit position.

Equations

• S.Accepts x = (DescriptiveComplexity.BitExpr.eval (S.state x (DescriptiveComplexity.posCount A)) S.acc = true)

The deterministic base

inductive DescriptiveComplexity.BaseTest (L : FirstOrder.Language) (ρ : ℕ) : Type

The deterministic base of a machine: a Boolean combination of sweeps and of queries to the instance. Its cost is a constant number of passes over the bit positions, hence O(log n) steps; nothing here evaluates a numeric predicate.

• sweep {L : FirstOrder.Language} {ρ : ℕ} (S : Sweep ρ) : BaseTest L ρ

  Run a sweep on the registers.

• bit {L : FirstOrder.Language} {ρ : ℕ} (i x : Fin ρ) : BaseTest L ρ

  Read a bit: the bit of register x at the position named by register i. The addressing the model has over its own registers, and the one base operation that is not a pass over the positions.

• query {L : FirstOrder.Language} {ρ a : ℕ} (R : L.Relations a) (arg : Fin a → Fin ρ) : BaseTest L ρ

  Query the instance: an input relation at a tuple of registers.

• not {L : FirstOrder.Language} {ρ : ℕ} (t : BaseTest L ρ) : BaseTest L ρ

  Negation.

• and {L : FirstOrder.Language} {ρ : ℕ} (t u : BaseTest L ρ) : BaseTest L ρ

  Conjunction.

• or {L : FirstOrder.Language} {ρ : ℕ} (t u : BaseTest L ρ) : BaseTest L ρ

  Disjunction.

def DescriptiveComplexity.BaseTest.Holds {L : FirstOrder.Language} {ρ : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] : BaseTest L ρ → (Fin ρ → A) → Prop

What a base test says of a tuple of register values.

Equations

• (DescriptiveComplexity.BaseTest.sweep S).Holds x✝ = S.Accepts x✝
• (DescriptiveComplexity.BaseTest.bit i y).Holds x✝ = DescriptiveComplexity.BitIx (x✝ i) (x✝ y)
• (DescriptiveComplexity.BaseTest.query R arg).Holds x✝ = FirstOrder.Language.Structure.RelMap R fun (t : Fin a) => x✝ (arg t)
• t.not.Holds x✝ = ¬t.Holds x✝
• (t.and u).Holds x✝ = (t.Holds x✝ ∧ u.Holds x✝)
• (t.or u).Holds x✝ = (t.Holds x✝ ∨ u.Holds x✝)

Machines, and the class they decide

structure DescriptiveComplexity.LTMachine (L : FirstOrder.Language) : Type

An alternating machine with a logarithmic clock: a list of registers, each filled by one of the two players, and a deterministic bit-level test of the tuple they leave behind.

Registers are filled in order, DescriptiveComplexity.LTMachine.pol i telling which player fills the i-th; a block of the classical normal form is a maximal run of equal polarities, and the number of alternations is the number of changes along the list.

• regs : ℕ

  The number of registers, that is, of guessed addresses.

• pol : Fin self.regs → Bool

  Who fills each register: true existentially, false universally.

• base : BaseTest L self.regs

  The deterministic base test.

def DescriptiveComplexity.prefixHolds {A : Type} (m : ℕ) : (Fin m → Bool) → ((Fin m → A) → Prop) → Prop

The quantifier prefix of a machine, peeled from the innermost register outwards.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.prefixHolds 0 x_3 P = P Fin.elim0

Prenexing: what a quantifier prefix does to the connectives

The three lemmas a bit-level definability API needs, so that a construction built from the connectives and the quantifiers can be read off as a single prefix over a quantifier-free kernel. They are about prefixHolds alone, and they are what replaces a normal-form theorem: negation dualizes a prefix, a prefix absorbs a side condition it does not mention, and two prefixes concatenate.

theorem DescriptiveComplexity.prefixHolds_not {A : Type} (m : ℕ) (pol : Fin m → Bool) (P : (Fin m → A) → Prop) : ¬prefixHolds m pol P ↔ prefixHolds m (fun (j : Fin m) => !pol j) fun (v : Fin m → A) => ¬P v

Negating a prefix dualizes it: every quantifier flips, and the body is negated. Classical, as prenexing is.

theorem DescriptiveComplexity.prefixHolds_and_const {A : Type} [Nonempty A] (m : ℕ) (pol : Fin m → Bool) (P : (Fin m → A) → Prop) (Q : Prop) : (prefixHolds m pol fun (v : Fin m → A) => P v ∧ Q) ↔ prefixHolds m pol P ∧ Q

A prefix absorbs a side condition it does not mention. The universal steps are what needs the universe to be nonempty.

theorem DescriptiveComplexity.prefixHolds_add {A : Type} (k₁ k₂ : ℕ) (pol : Fin (k₁ + k₂) → Bool) (P : (Fin k₁ → A) → (Fin k₂ → A) → Prop) : (prefixHolds (k₁ + k₂) pol fun (u : Fin (k₁ + k₂) → A) => P (fun (i : Fin k₁) => u (Fin.castAdd k₂ i)) fun (j : Fin k₂) => u (Fin.natAdd k₁ j)) ↔ prefixHolds k₁ (fun (i : Fin k₁) => pol (Fin.castAdd k₂ i)) fun (v : Fin k₁ → A) => prefixHolds k₂ (fun (j : Fin k₂) => pol (Fin.natAdd k₁ j)) (P v)

Two prefixes concatenate: a prefix of k₁ + k₂ variables, read on a body that splits its valuation into the first k₁ and the last k₂, is the first prefix wrapped around the second. This is the only place the index arithmetic of Fin appears; everything downstream uses it as a black box.

def DescriptiveComplexity.LTMachine.Accepts {L : FirstOrder.Language} (M : LTMachine L) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] : Prop

The machine accepts the instance when the two players, filling the registers in order, leave a tuple passing the base test.

Equations

• M.Accepts A = DescriptiveComplexity.prefixHolds M.regs M.pol fun (x : Fin M.regs → A) => M.base.Holds x

def DescriptiveComplexity.LTDecidable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : Prop

The class decided by the machines of this section: the analogue, at the bottom of the ladder, of DescriptiveComplexity.LOGSPACE's automata. A problem is decidable in constant-alternation logarithmic time – the level Σₖ-TIME(log n) of the logarithmic-time hierarchy fixed by the machine's own polarities – when one machine decides it on every nonempty finite ordered structure.

Equations

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