AC⁰ ⊆ PTIME: the numeric predicates are an induction

AC⁰ ⊆ PTIME (DescriptiveComplexity.ac0Definable_mem_PTIME): first-order logic with + and × on the ranks is inside polynomial time, because the two numeric predicates are themselves defined by one simultaneous induction over the order, and DescriptiveComplexity.StepDef puts an unrestricted first-order sentence on top of the relations it computes.

Why the fixed-point layer, and not the machine

The tempting route is FO(DTC): x + y = z is a walk (step two heads in lockstep), which is deterministic, so addition is one operator. But DescriptiveComplexity.TCSpec is a single operator over first-order kernels, with no relation variables; multiplication is a walk whose step needs addition, and the sentence on top needs both, so the route requires nesting that the specification-as-data logic does not have. DescriptiveComplexity.StepDef has exactly the two features that are wanted instead:

• the step formulas may read the variables being computed, so plus and times are one simultaneous induction – times reads plus positively, and no stratification (DescriptiveComplexity.StepDef.stratify) is needed;
• the output is an arbitrary first-order sentence over the expanded vocabulary, free to negate fixed-point atoms – which is what an AC⁰ sentence needs, its numeric atoms sitting anywhere.

Since the numeric predicates are symbols, no formula recursion is involved either: the translation of an AC⁰ sentence is a language map (DescriptiveComplexity.arithToBlock) sending plus and times to the two relation variables, and FirstOrder.Language.LHom.realize_onSentence does the rest, once the limit of the induction is proved to be the arithmetic.

The induction

Two variables of arity 3, plus and times, with the clauses

• plus x y z ← y is least and x = z; or y' ⋖ y, z' ⋖ z, plus x y' z';
• times x y z ← y and z are least; or y' ⋖ y, times x y' w, plus w x z

read inflationarily. Soundness is an induction on the stages (DescriptiveComplexity.inflStage_arith_sound); completeness needs no stage count at all, only that the limit is closed under the step (DescriptiveComplexity.StepDef.isFixedPt_inflStep_inflLimit), and then an induction along the order (DescriptiveComplexity.inflLimit_plus_of_eq, DescriptiveComplexity.inflLimit_times_of_eq).

What this does and does not give

It gives the inclusion in PTIME, hence in NP and everything above, and it gives every consumer that a closure of AC⁰ under first-order reductions would (a problem reducing to an AC⁰ problem is in PTIME, PTIME being closed under reductions). It does not give the sharper AC⁰ ⊆ LOGSPACE, which needs the arithmetic computed by a deterministic multi-head automaton (DescriptiveComplexity.HeadProgram) rather than by an induction.

The block of the two numeric predicates

@[reducible, inline]

abbrev DescriptiveComplexity.arithBlock : SOBlock

The relation variables computing the numeric predicates: two of arity 3, false for addition and true for multiplication. The index type is Bool rather than Fin 2 because numerals do not elaborate at a block's ι.

Equations

• DescriptiveComplexity.arithBlock = { ι := Bool, ιFinite := Bool.instFinite, arity := fun (x : Bool) => 3 }

@[reducible, inline]

abbrev DescriptiveComplexity.plusVarSym (L : FirstOrder.Language) : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Relations 3

The addition variable, as a symbol of the expanded vocabulary.

Equations

• DescriptiveComplexity.plusVarSym L = DescriptiveComplexity.varOutSym L DescriptiveComplexity.arithBlock false

@[reducible, inline]

abbrev DescriptiveComplexity.timesVarSym (L : FirstOrder.Language) : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Relations 3

The multiplication variable, as a symbol of the expanded vocabulary.

Equations

• DescriptiveComplexity.timesVarSym L = DescriptiveComplexity.varOutSym L DescriptiveComplexity.arithBlock true

noncomputable def DescriptiveComplexity.arithOrdF {L : FirstOrder.Language} {α : Type} (φ : (L.sum FirstOrder.Language.order).Formula α) : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Formula α

An order formula, transported to the vocabulary expanded by the block.

Equations

• DescriptiveComplexity.arithOrdF φ = FirstOrder.Language.LHom.sumInl.onFormula φ

noncomputable def DescriptiveComplexity.arithVarF {L : FirstOrder.Language} {α : Type} (i : Bool) (a b c : α) : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Formula α

An atom of one of the two numeric relation variables.

Equations

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

noncomputable def DescriptiveComplexity.plusStepF (L : FirstOrder.Language) : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Formula (Fin 3)

The clause of addition: either y is least and z is x, or y and z both step down and the smaller triple is already there.

Stated at Fin 3 and only then read at Fin (arithBlock.arity i): numerals do not elaborate through the arity projection of a block.

Equations

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

noncomputable def DescriptiveComplexity.timesStepF (L : FirstOrder.Language) : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Formula (Fin 3)

The clause of multiplication: either y and z are least, or y steps down, x * y' is already there, and one more x is added to it – the addition variable of the same simultaneous induction.

Equations

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

noncomputable def DescriptiveComplexity.arithStep (L : FirstOrder.Language) (i : arithBlock.ι) : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Formula (Fin (arithBlock.arity i))

The step formulas of the numeric induction, indexed by the block.

Equations

• DescriptiveComplexity.arithStep L false = DescriptiveComplexity.plusStepF L
• DescriptiveComplexity.arithStep L true = DescriptiveComplexity.timesStepF L

@[simp]

theorem DescriptiveComplexity.realize_arithOrdF {L : FirstOrder.Language} {α A : Type} [L.Structure A] [LinearOrder A] (ρ : arithBlock.Assignment A) (φ : (L.sum FirstOrder.Language.order).Formula α) (v : α → A) : (arithOrdF φ).Realize v ↔ φ.Realize v

@[simp]

theorem DescriptiveComplexity.realize_arithVarF {L : FirstOrder.Language} {α A : Type} [L.Structure A] [LinearOrder A] (ρ : arithBlock.Assignment A) (i : Bool) (a b c : α) (v : α → A) : (arithVarF i a b c).Realize v ↔ ρ i ![v a, v b, v c]

The definition, and what it is meant to compute

@[reducible]

noncomputable def DescriptiveComplexity.arithStepDef {L : FirstOrder.Language} (out : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Sentence) : StepDef (L.sum FirstOrder.Language.order)

The numeric induction, with an arbitrary first-order output: the two variables of DescriptiveComplexity.arithBlock, the clauses of DescriptiveComplexity.arithStep, and a sentence over the expanded vocabulary.

Reducible, so that the arity of a variable of its block still reduces to 3 where rw works at implicit transparency.

Equations

• DescriptiveComplexity.arithStepDef out = { B := DescriptiveComplexity.arithBlock, step := DescriptiveComplexity.arithStep L, out := out }

theorem DescriptiveComplexity.next_arithStepDef_iff {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (out : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Sentence) (ρ : arithBlock.Assignment A) (i : arithBlock.ι) (v : Fin (arithBlock.arity i) → A) : (arithStepDef out).next ρ i v ↔ (arithStep L i).Realize v

One application of the numeric clauses, unfolded: the step formula realized at the current assignment. Stated because DescriptiveComplexity.StepDef.next is a def whose equation theorems do not rewrite.

theorem DescriptiveComplexity.next_plus_iff {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (out : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Sentence) (ρ : arithBlock.Assignment A) (v : Fin 3 → A) : (arithStepDef out).next ρ false v ↔ (∀ (a : A), v 1 ≤ a) ∧ v 0 = v 2 ∨ ∃ (y' : A) (z' : A), (y' < v 1 ∧ ∀ (a : A), ¬(y' < a ∧ a < v 1)) ∧ (z' < v 2 ∧ ∀ (a : A), ¬(z' < a ∧ a < v 2)) ∧ ρ false ![v 0, y', z']

What the addition clause derives: either the base case, or a step down on both y and z from a triple already there.

theorem DescriptiveComplexity.next_times_iff {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (out : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Sentence) (ρ : arithBlock.Assignment A) (v : Fin 3 → A) : (arithStepDef out).next ρ true v ↔ ((∀ (a : A), v 1 ≤ a) ∧ ∀ (a : A), v 2 ≤ a) ∨ ∃ (y' : A) (w : A), (y' < v 1 ∧ ∀ (a : A), ¬(y' < a ∧ a < v 1)) ∧ ρ true ![v 0, y', w] ∧ ρ false ![w, v 0, v 2]

What the multiplication clause derives: either the base case, or one copy of x peeled off y and added back with the addition variable.

Soundness: every stage holds only true facts

theorem DescriptiveComplexity.inflStage_arith_sound {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (out : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Sentence) [Finite A] (n : ℕ) : (∀ (v : Fin 3 → A), (arithStepDef out).inflStage A n false v → orank (v 0) + orank (v 1) = orank (v 2)) ∧ ∀ (v : Fin 3 → A), (arithStepDef out).inflStage A n true v → orank (v 0) * orank (v 1) = orank (v 2)

Every stage of the numeric induction is sound: the addition variable holds only triples whose ranks add up, and the multiplication variable only triples whose ranks multiply.

Completeness: the limit is closed under the clauses

theorem DescriptiveComplexity.next_inflLimit_le {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (out : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Sentence) [Finite A] {i : arithBlock.ι} {v : Fin (arithBlock.arity i) → A} (h : (arithStepDef out).next ((arithStepDef out).inflLimit A) i v) : (arithStepDef out).inflLimit A i v

The limit of the numeric induction is closed under the step formulas: what one clause derives from it is already in it.

theorem DescriptiveComplexity.inflLimit_plus_of_eq {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (out : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Sentence) [Finite A] (x y z : A) (h : orank x + orank y = orank z) : (arithStepDef out).inflLimit A false ![x, y, z]

The addition variable holds every true triple, by induction along the order: the clause is applied to the limit, which is closed under it.

theorem DescriptiveComplexity.inflLimit_times_of_eq {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (out : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Sentence) [Finite A] (x y z : A) (h : orank x * orank y = orank z) : (arithStepDef out).inflLimit A true ![x, y, z]

The multiplication variable holds every true triple: the same argument, one copy of x at a time, using the addition variable for the accumulation.

theorem DescriptiveComplexity.inflLimit_arith_iff {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (out : ((L.sum FirstOrder.Language.order).sum arithBlock.lang).Sentence) [Finite A] (i : arithBlock.ι) (v : Fin (arithBlock.arity i) → A) : (arithStepDef out).inflLimit A i v ↔ (if i = true then orank (v 0) * orank (v 1) else orank (v 0) + orank (v 1)) = orank (v 2)

The limit of the numeric induction is the arithmetic of the order: the two variables hold exactly the true triples.

Reading an AC⁰ sentence at the limit

def DescriptiveComplexity.arithToBlock (L : FirstOrder.Language) [L.IsRelational] : L.sum FirstOrder.Language.arith →ᴸ (L.sum FirstOrder.Language.order).sum arithBlock.lang

The translation of an AC⁰ sentence: the numeric symbols go to the two relation variables of the induction, the order symbol and the input symbols to themselves. Being a language map, it needs no recursion over formulas.

Equations

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

The inclusion

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

AC⁰ ⊆ FO(IFP): the numeric predicates are the limit of the simultaneous induction of DescriptiveComplexity.arithStep, and an AC⁰ sentence is its output, translated by DescriptiveComplexity.arithToBlock.

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

AC⁰ ⊆ FO(LFP), through the equivalence of the inflationary and the least fixed point.

theorem DescriptiveComplexity.ac0Definable_mem_PTIME {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : AC0Definable P) : PTIME.Mem P

AC⁰ ⊆ PTIME. With DescriptiveComplexity.FODefinable.ac0Definable and DescriptiveComplexity.exists_ac0Definable_not_foDefinable this places the arithmetic logic strictly above FO(≤) and inside polynomial time; the sharper AC⁰ ⊆ LOGSPACE needs the multi-head automaton instead.