The lower fence: a bit-level prenex logic, compiled into machines

DescriptiveComplexity.LTDecidable.bitDefinable puts the machine model inside the bit-level logic. This file puts that logic back inside the machine model, so that the fence is an equality and the picture is

prenex FO(≤, +, BIT) = constant-alternation logarithmic time.

DescriptiveComplexity.ltDecidable_iff_bitDefinable is that equality: the machine model of this development is exactly characterized by a logic, with no normal form left to apply and no gap left to name on either side of it.

The logic

DescriptiveComplexity.BitSentence: a quantifier prefix – a polarity per variable, exactly the shape a machine's registers have – over a quantifier-free kernel built from four atoms (DescriptiveComplexity.BitAtom): the order, the addition of ranks, an input relation at a tuple of variables, and the bit BitIx i x of x at the index i.

That last atom is where the model gets its power, and it is a read rather than a computation: the machine has the index in a register and addresses the bit there (DescriptiveComplexity.BaseTest.bit). No sweep can do it – locating the position orank i means counting positions, and an automaton carrying a constant number of bits cannot – which is exactly why it is a primitive and not a construction.

The addition is a derived predicate

DescriptiveComplexity.bitDef_plus_free: the atom DescriptiveComplexity.BitAtom.plus is redundant. orank x + orank y = orank z is bit-definable from the order and the bit atom alone, by carry-lookahead (DescriptiveComplexity.plus_iff_bits), so the logic of this file is FO(≤, BIT) under another name – its classical name, and in the sharpest sense, since ≤ is itself first-order definable from BIT alone, whence FO(BIT) = FO(≤, BIT) (Dawar, Doets, Lindell & Weinstein 1998 Thm. 2.1 and Cor. 2.3: BIT is Ackermann membership, (A, BIT) is an ∈-initial segment of the hereditarily finite sets, and one formula defines the order on all of them – it guesses the order relation itself as an element, a set of pairs, and checks it is a post-fixed point of the “greatest differing member” operator). That elimination is neither used nor proved here: every structure in this library carries its order anyway. The atom stays all the same: DescriptiveComplexity.plusSweep_accepts is half of what shows the machine has to build its arithmetic rather than read it, and deleting the atom would delete that demonstration for no theorem.

The lookahead is also where the index naming shows: the carry into position i is “some j < i generates one, and every k strictly between propagates it”, with j and k ordinary elements compared by ≤. Under the place-value naming each of those quantifiers had to be relativized to the powers of two.

The compilation

Atom by atom, with the sweeps already built: ≤ is leSweep, + is plusSweep, the bit atom is the machine's read, and an input relation is a query. DescriptiveComplexity.Sweep.relabel is what lets a sweep written once for two or three registers be run on any registers of the machine. The Boolean structure of the kernel becomes the Boolean structure of the base test, and the quantifier prefix becomes the register list unchanged – there is nothing to prenexify, because the source syntax is prenex by construction.

What is closed, and what is not

The equality with the logic is closed on both sides. The identification of that logic with FO(≤, +, ×), that is, with DescriptiveComplexity.AC0Definable, is Immerman 1999 Thm 1.17, one named theorem per direction:

• FO(≤, +, BIT) ⊆ FO(≤, +, ×) is DescriptiveComplexity.powArithDef, the definability of i ↦ 2 ^ i, which is proved (DescriptiveComplexity.LogTime.Pow), so DescriptiveComplexity.BitDefinable.ac0Definable is unconditional;
• FO(≤, +, ×) ⊆ FO(≤, +, BIT) is the Bit Sum Lemma, the counting argument that eliminates × in favor of the bit atom, and it is not built.

Neither is a defect of the machine: they are statements about two vocabularies, and the machine is exactly the one of them that a machine can be.

def DescriptiveComplexity.BitAtom.compile {L : FirstOrder.Language} {m : ℕ} : BitAtom L (Fin m) → BaseTest L m

The base test an atom compiles to.

Equations

• (DescriptiveComplexity.BitAtom.le x_1 y).compile = DescriptiveComplexity.BaseTest.sweep (DescriptiveComplexity.leSweep.relabel ![x_1, y])
• (DescriptiveComplexity.BitAtom.plus x_1 y z).compile = DescriptiveComplexity.BaseTest.sweep (DescriptiveComplexity.plusSweep.relabel ![x_1, y, z])
• (DescriptiveComplexity.BitAtom.bit i x_1).compile = DescriptiveComplexity.BaseTest.bit i x_1
• (DescriptiveComplexity.BitAtom.rel R arg).compile = DescriptiveComplexity.BaseTest.query R arg

theorem DescriptiveComplexity.BitAtom.holds_compile {L : FirstOrder.Language} {m : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (a : BitAtom L (Fin m)) (v : Fin m → A) : a.compile.Holds v ↔ a.Holds v

The compilation of an atom is correct.

def DescriptiveComplexity.BitKernel.compile {L : FirstOrder.Language} {m : ℕ} : BitKernel L (Fin m) → BaseTest L m

The base test a kernel compiles to: the Boolean structure is carried over unchanged.

Equations

• (DescriptiveComplexity.BitKernel.atom a).compile = a.compile
• DescriptiveComplexity.BitKernel.tt.compile = DescriptiveComplexity.BaseTest.sweep (DescriptiveComplexity.trueSweep.relabel Fin.elim0)
• k.not.compile = k.compile.not
• (k.and k').compile = k.compile.and k'.compile
• (k.or k').compile = k.compile.or k'.compile

theorem DescriptiveComplexity.BitKernel.holds_compile {L : FirstOrder.Language} {m : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (k : BitKernel L (Fin m)) (v : Fin m → A) : k.compile.Holds v ↔ k.Holds v

The compilation of a kernel is correct.

The logic decided by the machines

def DescriptiveComplexity.BitSentence.compile {L : FirstOrder.Language} (φ : BitSentence L) : LTMachine L

The machine a sentence compiles to: the prefix is the register list.

Equations

• φ.compile = { regs := φ.vars, pol := φ.pol, base := φ.kernel.compile }

theorem DescriptiveComplexity.BitSentence.accepts_compile {L : FirstOrder.Language} (φ : BitSentence L) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] : φ.compile.Accepts A ↔ φ.Holds A

The compilation of a sentence is correct: the machine accepts exactly the instances the sentence holds of.

The addition is a derived predicate

FO(≤, +, BIT) = FO(≤, BIT): the addition of ranks is expressed by the carry-lookahead formula, a condition on the bits with no addition in it. The atom is kept all the same – plusSweep_accepts is half of what shows the model has to build its arithmetic rather than read it – so what this section settles is a name, not an API.

theorem DescriptiveComplexity.lt_iff_orank_lt {A : Type} [LinearOrder A] [Finite A] {i i' : A} : i < i' ↔ orank i < orank i'

The order of the elements is the order of their ranks.

def DescriptiveComplexity.CarryAt {A : Type} [LinearOrder A] (x y i : A) : Prop

The carry into a position, first-order in the bits: a lower position generates a carry, and every position between propagates it.

Equations

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

theorem DescriptiveComplexity.carryAt_iff {A : Type} [LinearOrder A] [Finite A] (x y i : A) : CarryAt x y i ↔ 2 ^ orank i ≤ orank x % 2 ^ orank i + orank y % 2 ^ orank i

The carry into a position is the arithmetic carry at its index.

theorem DescriptiveComplexity.plus_iff_bits {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x y z : A) : orank x + orank y = orank z ↔ ∀ (i : A), BitIx i z ↔ ((BitIx i x ↔ BitIx i y) ↔ CarryAt x y i)

The addition of ranks is the carry-lookahead formula. orank x + orank y = orank z says that at every index the output bit is the exclusive or of the two input bits and the carry – written as an iff-chain, which for three propositions is the parity of their truth values. Nothing on the right-hand side is an addition: this is the sense in which FO(≤, +, BIT) is FO(≤, BIT).

There is no separate clause for the carry out of the last position: the equation at the index above the top one says exactly that, all three bits being clear there, and that index is a rank of the universe (DescriptiveComplexity.posCount_lt_card).

theorem DescriptiveComplexity.bitDef_carryAt {L : FirstOrder.Language} {α : Type} (x y : α) : BitDef fun (x_1 : Type) (x_2 : L.Structure x_1) (x_3 : LinearOrder x_1) (x_4 : Finite x_1) (x_5 : Nonempty x_1) (u : α ⊕ Fin 1 → x_1) => CarryAt (u (Sum.inl x)) (u (Sum.inl y)) (u (Sum.inr 0))

The carry into a bound index, bit-definably: three variables, j guessed and k universal, and nothing but the order to bound them.

theorem DescriptiveComplexity.bitDef_plus_free {L : FirstOrder.Language} {α : Type} (x y z : α) : BitDef fun (x_1 : Type) (x_2 : L.Structure x_1) (x_3 : LinearOrder x_1) (x_4 : Finite x_1) (x_5 : Nonempty x_1) (v : α → x_1) => orank (v x) + orank (v y) = orank (v z)

The addition atom is redundant: orank x + orank y = orank z is bit-definable with no plus atom in the construction – only the order and the bit at an index – which is the sense in which the logic of this file is FO(≤, BIT). The atom stays: plusSweep_accepts is half of what shows the machine has to build its arithmetic rather than read it.

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

The lower fence: every prenex FO(≤, +, BIT) sentence is decided by a machine with a logarithmic clock and a bit-level base. The order and the addition are the sweeps of DescriptiveComplexity.LogTime.Arith, the bit is a read, and the quantifiers are the registers.

theorem DescriptiveComplexity.ltDecidable_iff_bitDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} : LTDecidable P ↔ BitDefinable P

The machine model is exactly a logic. Constant-alternation logarithmic time – a machine whose registers are guessed addresses, in a list whose polarities are fixed, and whose base sees nothing but bits – decides exactly the problems defined by a prenex sentence over ≤, + and the bit at an index, that is, by FO(≤, BIT). The forward direction guesses each sweep's trace, one element per bit vector over the positions (DescriptiveComplexity.LTDecidable.bitDefinable); the backward one compiles atom by atom into the sweeps of DescriptiveComplexity.LogTime.Arith and the machine's read.