The bit-level logic is inside LOGSPACE

DescriptiveComplexity.BitDefinable.mem_LOGSPACE: every problem defined by a prenex sentence over ≤, + and the bit at an index – hence, by DescriptiveComplexity.ltDecidable_iff_bitDefinable, every problem decided by an alternating machine with a logarithmic clock – is decided by a deterministic multi-head automaton, so it is in LOGSPACE.

This is the fence the index naming cost, restored without either half of Immerman's mutual definability: nothing here goes through FO(≤, +, ×), so this route is independent of DescriptiveComplexity.powArithDef.

Why it is short

The bit logic is prenex, so there is no formula induction to redo: the evaluator is a recursion over DescriptiveComplexity.BitKernel, whose five constructors become branches (DescriptiveComplexity.HeadProgram.iteP), and a quantifier prefix, whose variables become sweeps (DescriptiveComplexity.HeadProgram.scanP for a universal register, its negation for an existential). The prefix peels its innermost variable first, which is exactly how a sweep wraps a body, so the induction matches the semantics step for step and the property a prefix decides depends on no head at all.

Only the atoms have content, and all of it is elsewhere: ≤ and an input relation are quantifier-free guards, + is DescriptiveComplexity.HeadProgram.plusP, and the bit is DescriptiveComplexity.HeadProgram.bitP – the halving loop of DescriptiveComplexity.HeadBit.

The head budget

2 * vars + 8: two heads per quantified variable, the register itself and the sweep's marker, then the eight the bit fragment needs (its five working heads and the addition's three). Where an arithmetic evaluation pays seven scratch heads (DescriptiveComplexity.HeadProgram.ArithScratch), a bit-level one pays eight, and it never needs a multiplication.

Negating a fragment

def DescriptiveComplexity.HeadProgram.notP {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) : HeadProgram L K

The negation of a fragment: run it and swap the exits.

Equations

• F.notP = F.iteP (DescriptiveComplexity.HeadProgram.exitP false) (DescriptiveComplexity.HeadProgram.exitP true)

theorem DescriptiveComplexity.HeadProgram.decides_notP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} {F : HeadProgram L K} {P : (Fin K → A) → Prop} (hF : F.Decides A m P) (hP : HeadLocal m P) : F.notP.Decides A m fun (x : Fin K → A) => ¬P x

theorem DescriptiveComplexity.HeadProgram.deterministic_notP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {F : HeadProgram L K} (hF : F.Deterministic A) : F.notP.Deterministic A

The scratch layout of a bit-level evaluation

structure DescriptiveComplexity.HeadProgram.BitScratch {K : ℕ} (y cnt cand w tmk a b mk : Fin K) (S : ℕ) : Prop

The eight heads a bit-level atom needs, pinned to the eight positions from S on: the bit fragment's five working heads, then the addition's three. S is the top of the quantifier region, so every level the evaluator reaches is at most S.

• hy : ↑y = S

  The working value 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.

• hw : ↑w = S + 3

  The candidate's successor sits at S + 3.

• htmk : ↑tmk = S + 4

  The scan's marker sits at S + 4.

• ha : ↑a = S + 5

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

• hb : ↑b = S + 6

  The addition's counter sits at S + 6.

• hmk : ↑mk = S + 7

  The addition's marker sits at S + 7.

theorem DescriptiveComplexity.HeadProgram.BitScratch.bitHeads {K : ℕ} {y cnt cand w tmk a b mk : Fin K} {S d : ℕ} (hs : BitScratch y cnt cand w tmk a b mk S) {ih xh : Fin K} (hih : ↑ih < d) (hxh : ↑xh < d) (hd : d ≤ S) : BitHeads ih xh y cnt cand w tmk a b mk d S (S + 5)

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

theorem DescriptiveComplexity.HeadProgram.BitScratch.plusHeads {K : ℕ} {y cnt cand w tmk a b mk : Fin K} {S d : ℕ} (hs : BitScratch y cnt cand w 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.

The atoms

@[reducible, inline]

abbrev DescriptiveComplexity.HeadProgram.inOrdSym {L : FirstOrder.Language} {a : ℕ} (R : L.Relations a) : (L.sum FirstOrder.Language.order).Relations a

An input relation symbol, in the ordered expansion of its vocabulary. Named, as every symbol of a sum vocabulary in this library is, so that rw matches it.

Equations

• DescriptiveComplexity.HeadProgram.inOrdSym R = Sum.inl R

noncomputable def DescriptiveComplexity.HeadProgram.bitAtomP {L : FirstOrder.Language} {K : ℕ} (y cnt cand w tmk a b mk : Fin K) {γ : Type} (hv : γ → Fin K) : BitAtom L γ → HeadProgram L K

A bit-level atom, as a program: the order and an input relation are read as guards, the addition and the bit are computed, by plusP and by the halving loop bitP.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.bitAtomP y cnt cand w tmk a b mk hv (DescriptiveComplexity.BitAtom.le u v) = DescriptiveComplexity.HeadProgram.leafP (DescriptiveComplexity.leF (hv u) (hv v)) ⋯
• DescriptiveComplexity.HeadProgram.bitAtomP y cnt cand w tmk a b mk hv (DescriptiveComplexity.BitAtom.plus u v z) = DescriptiveComplexity.HeadProgram.plusP (hv u) (hv v) (hv z) a b mk
• DescriptiveComplexity.HeadProgram.bitAtomP y cnt cand w tmk a b mk hv (DescriptiveComplexity.BitAtom.bit u v) = DescriptiveComplexity.HeadProgram.bitP (hv u) (hv v) y cnt cand w tmk a b mk

noncomputable def DescriptiveComplexity.HeadProgram.bitKernelP {L : FirstOrder.Language} {K : ℕ} (y cnt cand w tmk a b mk : Fin K) {γ : Type} (hv : γ → Fin K) : BitKernel L γ → HeadProgram L K

The quantifier-free kernel, as a program: the Boolean structure becomes branches.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.bitKernelP y cnt cand w tmk a b mk hv (DescriptiveComplexity.BitKernel.atom at') = DescriptiveComplexity.HeadProgram.bitAtomP y cnt cand w tmk a b mk hv at'
• DescriptiveComplexity.HeadProgram.bitKernelP y cnt cand w tmk a b mk hv DescriptiveComplexity.BitKernel.tt = DescriptiveComplexity.HeadProgram.exitP true
• DescriptiveComplexity.HeadProgram.bitKernelP y cnt cand w tmk a b mk hv k.not = (DescriptiveComplexity.HeadProgram.bitKernelP y cnt cand w tmk a b mk hv k).notP

noncomputable def DescriptiveComplexity.HeadProgram.quantP {L : FirstOrder.Language} {K : ℕ} (pol : Bool) (h hm : Fin K) (F : HeadProgram L K) : HeadProgram L K

A quantified register, as a sweep: universally the sweep itself, and existentially its double negation.

Equations

• DescriptiveComplexity.HeadProgram.quantP pol h hm F = if pol = true then (DescriptiveComplexity.HeadProgram.scanP h hm F.notP).notP else DescriptiveComplexity.HeadProgram.scanP h hm F

noncomputable def DescriptiveComplexity.HeadProgram.prefixP {L : FirstOrder.Language} {K : ℕ} (sh : ℕ → Fin K) (n : ℕ) : (Fin n → Bool) → HeadProgram L K → HeadProgram L K

The quantifier prefix, as nested sweeps: the innermost variable wraps the body first, which is how DescriptiveComplexity.prefixHolds peels it. Variable j lives in head sh (2 * j), its sweep's marker in sh (2 * j + 1).

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.prefixP sh 0 x_3 x✝ = x✝

Correctness

theorem DescriptiveComplexity.HeadProgram.headLocal_of_heads {K : ℕ} {A γ : Type} {d : ℕ} (hv : γ → Fin K) (hlow : ∀ (v : γ), ↑(hv v) < d) (R : (γ → A) → Prop) : HeadLocal d fun (x : Fin K → A) => R fun (v : γ) => x (hv v)

A property read off a fixed tuple of heads only sees those heads.

theorem DescriptiveComplexity.HeadProgram.decides_bitAtomP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {y cnt cand w tmk a b mk : Fin K} {S : ℕ} (hs : BitScratch y cnt cand w tmk a b mk S) (hSK : S + 8 ≤ K) {γ : Type} {d : ℕ} (hv : γ → Fin K) (hlow : ∀ (v : γ), ↑(hv v) < d) (hd : d ≤ S) (at' : BitAtom L γ) : (bitAtomP y cnt cand w tmk a b mk hv at').Decides A d fun (x : Fin K → A) => at'.Holds fun (v : γ) => x (hv v)

An atom is decided: as a guard where it is the order or an input relation, by a fragment where it is the addition or the bit.

theorem DescriptiveComplexity.HeadProgram.decides_bitKernelP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {y cnt cand w tmk a b mk : Fin K} {S : ℕ} (hs : BitScratch y cnt cand w tmk a b mk S) (hSK : S + 8 ≤ K) {γ : Type} {d : ℕ} (hv : γ → Fin K) (hlow : ∀ (v : γ), ↑(hv v) < d) (hd : d ≤ S) (k : BitKernel L γ) : (bitKernelP y cnt cand w tmk a b mk hv k).Decides A d fun (x : Fin K → A) => k.Holds fun (v : γ) => x (hv v)

A kernel is decided, by recursion on its Boolean structure.

theorem DescriptiveComplexity.HeadProgram.decides_quantP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {pol : Bool} {h hm : Fin K} {lvl : ℕ} (hh : ↑h = lvl) (hhm : ↑hm = lvl + 1) {F : HeadProgram L K} {P : (Fin K → A) → Prop} (hF : F.Decides A (lvl + 2) P) (hP : HeadLocal (lvl + 1) P) : (quantP pol h hm F).Decides A lvl fun (x : Fin K → A) => if pol = true then ∃ (v : A), P (Function.update x h v) else ∀ (v : A), P (Function.update x h v)

A quantified register is decided: universally by the sweep, existentially by its double negation.

theorem DescriptiveComplexity.HeadProgram.snoc_update {K : ℕ} {A : Type} {n : ℕ} {sh : ℕ → Fin K} (hsh : ∀ i < K, ↑(sh i) = i) (hK : 2 * n + 1 < K) (x : Fin K → A) (v : A) : (fun (j : Fin (n + 1)) => Function.update x (sh (2 * n)) v (sh (2 * ↑j))) = Fin.snoc (fun (j : Fin n) => x (sh (2 * ↑j))) v

Reading a valuation off the registers, one variable per even head.

theorem DescriptiveComplexity.HeadProgram.decides_prefixP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {sh : ℕ → Fin K} (hsh : ∀ i < K, ↑(sh i) = i) (n : ℕ) (pol : Fin n → Bool) (F : HeadProgram L K) (R : (Fin n → A) → Prop) : 2 * n ≤ K → (F.Decides A (2 * n) fun (x : Fin K → A) => R fun (j : Fin n) => x (sh (2 * ↑j))) → (prefixP sh n pol F).Decides A 0 fun (x : Fin K → A) => prefixHolds n pol R

The prefix is decided: nested sweeps, one per variable, innermost first – and what they decide depends on no head at all, the prefix binding every variable.

Determinism

theorem DescriptiveComplexity.HeadProgram.deterministic_bitAtomP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {y cnt cand w tmk a b mk : Fin K} {γ : Type} (hv : γ → Fin K) (at' : BitAtom L γ) : (bitAtomP y cnt cand w tmk a b mk hv at').Deterministic A

theorem DescriptiveComplexity.HeadProgram.deterministic_bitKernelP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {y cnt cand w tmk a b mk : Fin K} {γ : Type} (hv : γ → Fin K) (k : BitKernel L γ) : (bitKernelP y cnt cand w tmk a b mk hv k).Deterministic A

theorem DescriptiveComplexity.HeadProgram.deterministic_quantP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {pol : Bool} {h hm : Fin K} {F : HeadProgram L K} (hF : F.Deterministic A) : (quantP pol h hm F).Deterministic A

theorem DescriptiveComplexity.HeadProgram.deterministic_prefixP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (sh : ℕ → Fin K) (n : ℕ) (pol : Fin n → Bool) (F : HeadProgram L K) : F.Deterministic A → (prefixP sh n pol F).Deterministic A

The inclusion

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

The bit-level logic is inside FO(DTC): a prenex sentence over ≤, + and the bit at an index is evaluated by a deterministic multi-head automaton – the registers swept, the order and the input atoms read as guards, the addition and the bit computed by DescriptiveComplexity.HeadProgram.plusP and DescriptiveComplexity.HeadProgram.bitP.

The machine has 2 * vars + 8 heads: two per quantified register, then the eight the bit fragment needs.

theorem DescriptiveComplexity.BitDefinable.mem_LOGSPACE {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : BitDefinable P) : LOGSPACE.Mem P

The bit-level logic is inside LOGSPACE, and with it the machine model of DescriptiveComplexity.LogTime. No part of Immerman's mutual definability is used: the route through AC⁰ (DescriptiveComplexity.powArithDef, then DescriptiveComplexity.ac0Definable_mem_LOGSPACE) is a different one, and longer.

theorem DescriptiveComplexity.LTDecidable.mem_LOGSPACE {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : LTDecidable P) : LOGSPACE.Mem P

Constant-alternation logarithmic time is inside LOGSPACE, through the logic it is equal to.