Barrington's theorem as a class equality

NC¹ is logarithmic formula depth: a language is in NC¹ exactly when its slice at length n has a De Morgan formula with O(log n) AND and OR gates on every path (Boolean.mem_NC_one_iff_formulaDepth_le). A circuit unfolds into formulas of its depth (Circuit.toFormula); conversely, a formula with d AND and OR gates on every path has a negation normal form of depth at most d + 1 (Formula.nnf), which is a circuit with fewer than 2 ^ (d + 1) gates.

Barrington's theorem [Bar89], Jukna, Section 15.4: NC¹ is the class of languages decided by permutation branching programs of width 5 and polynomial length (Boolean.NC_one_eq_polyLength_perm_five). A formula of depth O(log n) becomes a program of length 4 ^ O(log n), a polynomial (Boolean.exists_four_pow_formulaDepth_le_of_mem_NC_one), that σ-computes it for any 5-cycle σ (Boolean.exists_monoidProgram_alternatingGroup_computes_of_mem_NC_one, Boolean.exists_monoidProgram_computes_of_mem_NC_one). Conversely, a program over a finite monoid M is a branching program of width |M|, through the action of M on itself by left multiplication, and so a formula of depth logarithmic in its length [BT88]: the languages of polynomial-length programs over a finite monoid are in NC¹ (Boolean.polyLength_subset_NC_one). Five-cycles are even, so the programs of Barrington's theorem are programs over the alternating group A₅ (Boolean.NC_one_eq_polyLength_alternatingGroup), and NC¹ is the class of languages of polynomial-length programs over any finite monoid into which A₅ embeds (Boolean.NC_one_eq_polyLength_of_injective), for instance of polynomial-length permutation branching programs, and of polynomial-length branching programs, of any fixed width w ≥ 5 (Boolean.NC_one_eq_polyLength_perm, Boolean.NC_one_eq_polyLength_end). The classes of programs here are those of languages over Bool, PolyLength Bool M, and all these classes are nonuniform.

Main results

• Cslib.Circuits.Boolean.mem_NC_one_iff_formulaDepth_le: NC¹ is logarithmic formula depth.
• Cslib.Circuits.Boolean.exists_monoidProgram_alternatingGroup_computes_of_mem_NC_one, Cslib.Circuits.Boolean.exists_monoidProgram_computes_of_mem_NC_one: Barrington's theorem for the languages of NC¹, over A₅ and over S₅.
• Cslib.Circuits.Boolean.NC_one_subset_polyLength_alternatingGroup, Cslib.Circuits.Boolean.NC_one_subset_polyLength, Cslib.Circuits.Boolean.polyLength_subset_NC_one: the inclusions.
• Cslib.Circuits.Boolean.NC_one_eq_polyLength_perm_five, Cslib.Circuits.Boolean.NC_one_eq_polyLength_alternatingGroup: Barrington's theorem as a class equality, over S₅ and over A₅.
• Cslib.Circuits.Boolean.NC_one_eq_polyLength_perm, Cslib.Circuits.Boolean.NC_one_eq_polyLength_end: bounded-width branching programs of polynomial length decide exactly the languages of NC¹.

References

• D. A. Barrington, Bounded-width polynomial-size branching programs recognize exactly those languages in NC¹
• D. A. Mix Barrington, D. Thérien, Finite monoids and the fine structure of NC¹
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

NC¹ as logarithmic formula depth

theorem Cslib.Circuits.Boolean.mem_NC_one_iff_formulaDepth_le {L : Language Bool} : L ∈ NC 1 ↔ ∃ (c : ℕ), ∀ (n : ℕ), formulaDepth (L.slice n) ≤ c * (Nat.log 2 n + 1)

NC¹ is logarithmic formula depth. A language is in NC¹ exactly when, for a constant c, its slice at every length n has formula depth at most c (⌊log₂ n⌋ + 1): a De Morgan formula with at most that many AND and OR gates on every path.

Barrington's theorem

theorem Cslib.Circuits.Boolean.exists_four_pow_formulaDepth_le_of_mem_NC_one {L : Language Bool} (hL : L ∈ NC 1) : ∃ (s : ℕ → ℕ), PolynomiallyBounded s ∧ ∀ (n : ℕ), 4 ^ formulaDepth (L.slice n) ≤ s n

On a language in NC¹, 4 to the power of the formula depth is polynomially bounded.

theorem Cslib.Circuits.Boolean.exists_monoidProgram_alternatingGroup_computes_of_mem_NC_one {L : Language Bool} (hL : L ∈ NC 1) : ∃ (s : ℕ → ℕ), PolynomiallyBounded s ∧ ∀ (n : ℕ) [NeZero n] (σ : ↥(alternatingGroup (Fin 5))), (↑σ).IsFiveCycle → ∃ (P : BranchingPrograms.MonoidProgram (Fin n) Bool ↥(alternatingGroup (Fin 5))), FreeMonoid.length P ≤ s n ∧ P.Computes σ (L.slice n)

Barrington's theorem for NC¹ over A₅. For a language in NC¹ there is a polynomially bounded s such that, at every length n ≠ 0 and for every 5-cycle σ, a program over the alternating group A₅ of length at most s n σ-computes the slice of the language at n.

theorem Cslib.Circuits.Boolean.exists_monoidProgram_computes_of_mem_NC_one {L : Language Bool} (hL : L ∈ NC 1) : ∃ (s : ℕ → ℕ), PolynomiallyBounded s ∧ ∀ (n : ℕ) [NeZero n] (σ : Equiv.Perm (Fin 5)), σ.IsFiveCycle → ∃ (P : BranchingPrograms.MonoidProgram (Fin n) Bool (Equiv.Perm (Fin 5))), FreeMonoid.length P ≤ s n ∧ P.Computes σ (L.slice n)

Barrington's theorem for NC¹. For a language in NC¹ there is a polynomially bounded s such that, at every length n ≠ 0 and for every 5-cycle σ, a permutation branching program of width 5 and length at most s n σ-computes the slice of the language at n.

theorem Cslib.Circuits.Boolean.NC_one_subset_polyLength_alternatingGroup : NC 1 ⊆ BranchingPrograms.PolyLength Bool ↥(alternatingGroup (Fin 5))

NC¹ is decided by polynomial-length programs over the alternating group A₅.

theorem Cslib.Circuits.Boolean.NC_one_subset_polyLength : NC 1 ⊆ BranchingPrograms.PolyLength Bool (Equiv.Perm (Fin 5))

NC¹ is decided by polynomial-length permutation branching programs of width 5.

theorem Cslib.Circuits.Boolean.polyLength_subset_NC_one (M : Type u_1) [Monoid M] [Finite M] : BranchingPrograms.PolyLength Bool M ⊆ NC 1

Polynomial-length programs over a finite monoid decide languages in NC¹ [BT88]: by left multiplication, a program over a finite monoid is a branching program of width its cardinality, which is a formula of depth logarithmic in its length.

theorem Cslib.Circuits.Boolean.NC_one_eq_polyLength_perm_five : NC 1 = BranchingPrograms.PolyLength Bool (Equiv.Perm (Fin 5))

Barrington's theorem [Bar89]: NC¹ is the class of languages decided by permutation branching programs of width 5 and polynomial length.

theorem Cslib.Circuits.Boolean.NC_one_eq_polyLength_of_injective {M : Type u_1} [Monoid M] [Finite M] {φ : ↥(alternatingGroup (Fin 5)) →* M} (hφ : Function.Injective ⇑φ) : NC 1 = BranchingPrograms.PolyLength Bool M

NC¹ is the class of languages decided by polynomial-length programs over any finite monoid into which the alternating group A₅ embeds.

theorem Cslib.Circuits.Boolean.NC_one_eq_polyLength_alternatingGroup : NC 1 = BranchingPrograms.PolyLength Bool ↥(alternatingGroup (Fin 5))

Barrington's theorem over A₅ [Bar89]: NC¹ is the class of languages decided by polynomial-length programs over the alternating group A₅.

theorem Cslib.Circuits.Boolean.NC_one_eq_polyLength_perm {w : ℕ} (hw : 5 ≤ w) : NC 1 = BranchingPrograms.PolyLength Bool (Equiv.Perm (Fin w))

For every w ≥ 5, NC¹ is the class of languages decided by permutation branching programs of width w and polynomial length, the programs over Equiv.Perm (Fin w).

theorem Cslib.Circuits.Boolean.NC_one_eq_polyLength_end {w : ℕ} (hw : 5 ≤ w) : NC 1 = BranchingPrograms.PolyLength Bool (Function.End (Fin w))

Bounded-width branching programs of polynomial length decide exactly the languages of NC¹ [Bar89]: for every w ≥ 5, NC¹ is the class of languages decided by branching programs of width w and polynomial length, the programs over Function.End (Fin w).