Barrington's theorem

Barrington's theorem: a De Morgan formula of depth d, with negations free, becomes a permutation branching program of width 5 and length at most 4 ^ d, which is a fixed 5-cycle on the inputs where the formula is true and the identity elsewhere (Formula.exists_monoidProgram_computes) [Bar89], Jukna, Section 15.4. The programs here are the programs over Boolean inputs BitString n = Fin n → Bool, those of MonoidProgram (Fin n) Bool M.

The construction works for every 5-cycle σ at once. An input xᵢ reads xᵢ and selects σ or the identity (Instruction.cond i σ 1). A negation σ⁻¹-computes its argument and multiplies by σ. For a conjunction, σ is the commutator ⁅α, β⁆ = α β α⁻¹ β⁻¹ of two 5-cycles (Equiv.Perm.IsFiveCycle.exists_commutator); running the programs for the arguments with α and β, then their inverses, gives σ exactly when both arguments are true. A disjunction is the negation of the conjunction of the negations. This works in any group with a set of elements closed under inverses in which every element is a commutator of two of them (Formula.exists_monoidProgram_computes_of_forall_commutator). Five-cycles are even, so the programs select only elements of the alternating group A₅ (Formula.exists_monoidProgram_alternatingGroup_computes); mapped into S₅, they are permutation branching programs of width 5 (Formula.exists_monoidProgram_computes).

Conversely, whether a branching program of width w, a program over Function.End (Fin w), maps a to b is a formula of depth O(log w · log L): split the program in halves and take the disjunction over the middle values (MonoidProgram.entryFormulaMul), recursively along a balanced tree (MonoidProgram.entryFormula, by List.balancedFold). So a branching program of width w and length L is a formula of depth (⌈log₂ w⌉ + 1) ⌈log₂ L⌉ + ⌈log₂ w⌉ (MonoidProgram.exists_formula), with negations only at the leaves, and constant-width polynomial-length branching programs and logarithmic-depth formulas compute the same functions.

Main definitions

• Cslib.BranchingPrograms.MonoidProgram.entryFormula: the formula saying that a branching program maps a to b.
• Cslib.BranchingPrograms.MonoidProgram.entryFormulaMul: the formulas of a program from those of its two halves.

Main results

• Cslib.Circuits.Formula.exists_monoidProgram_computes_of_forall_commutator: Barrington's construction in a group.
• Cslib.Circuits.Formula.exists_monoidProgram_alternatingGroup_computes, Cslib.Circuits.Formula.exists_monoidProgram_computes: Barrington's theorem, with programs over A₅ and over S₅.
• Cslib.Circuits.Boolean.exists_monoidProgram_alternatingGroup_computes_of_formulaDepth, Cslib.Circuits.Boolean.exists_monoidProgram_computes_of_formulaDepth: the same for Boolean functions, in terms of their formula depth.
• Cslib.BranchingPrograms.MonoidProgram.exists_formula: branching programs give formulas of logarithmic depth.
• Cslib.BranchingPrograms.MonoidProgram.Computes.exists_formula: so do permutation branching programs.

References

• D. A. Barrington, Bounded-width polynomial-size branching programs recognize exactly those languages in NC¹
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

Barrington's theorem

theorem Cslib.Circuits.Formula.exists_monoidProgram_computes_of_forall_commutator {n : ℕ} {G : Type u_1} [Group G] [NeZero n] {C : Set G} (hinv : ∀ σ ∈ C, σ⁻¹ ∈ C) (hcomm : ∀ σ ∈ C, ∃ α ∈ C, ∃ β ∈ C, ⁅α, β⁆ = σ) (F : Formula Boolean.signature n) {σ : G} (hσ : σ ∈ C) : ∃ (P : BranchingPrograms.MonoidProgram (Fin n) Bool G), FreeMonoid.length P ≤ 4 ^ depthWith Boolean.binaryCost F ∧ P.Computes σ (F.eval Boolean.interpretation)

Barrington's construction in a group G. Let C be a set of elements of G, closed under inverses, in which every element is the commutator of two elements of C. For every σ ∈ C, a De Morgan formula of depth d, with negations and constants free, has a program over G of length at most 4 ^ d that σ-computes it.

theorem Cslib.Circuits.Formula.exists_monoidProgram_alternatingGroup_computes {n : ℕ} [NeZero n] (F : Formula Boolean.signature n) {σ : ↥(alternatingGroup (Fin 5))} (hσ : (↑σ).IsFiveCycle) : ∃ (P : BranchingPrograms.MonoidProgram (Fin n) Bool ↥(alternatingGroup (Fin 5))), FreeMonoid.length P ≤ 4 ^ depthWith Boolean.binaryCost F ∧ P.Computes σ (F.eval Boolean.interpretation)

Barrington's theorem in A₅. For every 5-cycle σ, a De Morgan formula of depth d, with negations and constants free, is σ-computed by a program of length at most 4 ^ d over the alternating group A₅: five-cycles are even.

theorem Cslib.Circuits.Formula.exists_monoidProgram_computes {n : ℕ} [NeZero n] (F : Formula Boolean.signature n) {σ : Equiv.Perm (Fin 5)} (hσ : σ.IsFiveCycle) : ∃ (P : BranchingPrograms.MonoidProgram (Fin n) Bool (Equiv.Perm (Fin 5))), FreeMonoid.length P ≤ 4 ^ depthWith Boolean.binaryCost F ∧ P.Computes σ (F.eval Boolean.interpretation)

Barrington's theorem. For every 5-cycle σ, a De Morgan formula of depth d, with negations and constants free, has a permutation branching program of width 5 and length at most 4 ^ d that σ-computes it: the program over A₅ mapped into S₅.

theorem Cslib.Circuits.Boolean.exists_monoidProgram_alternatingGroup_computes_of_formulaDepth {n : ℕ} [NeZero n] (f : BooleanFunction n) {σ : ↥(alternatingGroup (Fin 5))} (hσ : (↑σ).IsFiveCycle) : ∃ (P : BranchingPrograms.MonoidProgram (Fin n) Bool ↥(alternatingGroup (Fin 5))), FreeMonoid.length P ≤ 4 ^ formulaDepth f ∧ P.Computes σ f

A function of formula depth d is σ-computed, for every 5-cycle σ, by a program over the alternating group A₅ of length at most 4 ^ d.

theorem Cslib.Circuits.Boolean.exists_monoidProgram_computes_of_formulaDepth {n : ℕ} [NeZero n] (f : BooleanFunction n) {σ : Equiv.Perm (Fin 5)} (hσ : σ.IsFiveCycle) : ∃ (P : BranchingPrograms.MonoidProgram (Fin n) Bool (Equiv.Perm (Fin 5))), FreeMonoid.length P ≤ 4 ^ formulaDepth f ∧ P.Computes σ f

A function of formula depth d is σ-computed, for every 5-cycle σ, by a permutation branching program of width 5 and length at most 4 ^ d.

The converse

def Cslib.BranchingPrograms.Instruction.entryFormula {n w : ℕ} (I : Instruction (Fin n) Bool (Function.End (Fin w))) (a b : Fin w) : Circuits.Formula Circuits.Boolean.signature n

The formula saying that an instruction of a width-w branching program maps a to b: a constant or a literal.

@[simp]

theorem Cslib.BranchingPrograms.Instruction.eval_entryFormula {n w : ℕ} (I : Instruction (Fin n) Bool (Function.End (Fin w))) (a b : Fin w) (x : BitString n) : (I.entryFormula a b).eval Circuits.Boolean.interpretation x = decide (I.eval x a = b)

@[simp]

theorem Cslib.BranchingPrograms.Instruction.depthWith_entryFormula {n w : ℕ} (I : Instruction (Fin n) Bool (Function.End (Fin w))) (a b : Fin w) : Circuits.Formula.depthWith Circuits.Boolean.binaryCost (I.entryFormula a b) = 0

theorem Cslib.BranchingPrograms.Instruction.isNNF_entryFormula {n w : ℕ} (I : Instruction (Fin n) Bool (Function.End (Fin w))) (a b : Fin w) : (I.entryFormula a b).IsNNF

The formula of an instruction is a constant or a literal, so in negation normal form.

def Cslib.BranchingPrograms.MonoidProgram.entryFormulaMul {n w : ℕ} (u v : Fin w → Fin w → Circuits.Formula Circuits.Boolean.signature n) (a b : Fin w) : Circuits.Formula Circuits.Boolean.signature n

The formulas saying that two pieces of a branching program of width w, run one after the other, map a to b, from the formulas u and v of the two pieces: the second piece, which acts first, maps a to some c that the first piece maps to b.

def Cslib.BranchingPrograms.MonoidProgram.entryFormula {n w : ℕ} (P : MonoidProgram (Fin n) Bool (Function.End (Fin w))) (a b : Fin w) : Circuits.Formula Circuits.Boolean.signature n

The formula saying that a branching program of width w maps a to b: split the program in halves, and say that the second half maps a to some c that the first half maps to b (List.balancedFold).

@[simp]

theorem Cslib.BranchingPrograms.MonoidProgram.eval_entryFormula {n w : ℕ} (P : MonoidProgram (Fin n) Bool (Function.End (Fin w))) (a b : Fin w) (x : BitString n) : (P.entryFormula a b).eval Circuits.Boolean.interpretation x = decide (P.eval x a = b)

theorem Cslib.BranchingPrograms.MonoidProgram.isNNF_entryFormula {n w : ℕ} (P : MonoidProgram (Fin n) Bool (Function.End (Fin w))) (a b : Fin w) : (P.entryFormula a b).IsNNF

The formula saying that a branching program maps a to b has negations only at the leaves.

theorem Cslib.BranchingPrograms.MonoidProgram.depthWith_entryFormula_le {n w : ℕ} (P : MonoidProgram (Fin n) Bool (Function.End (Fin w))) (a b : Fin w) : Circuits.Formula.depthWith Circuits.Boolean.binaryCost (P.entryFormula a b) ≤ (Nat.clog 2 w + 1) * Nat.clog 2 (FreeMonoid.length P)

theorem Cslib.BranchingPrograms.MonoidProgram.exists_formula {n w : ℕ} (P : MonoidProgram (Fin n) Bool (Function.End (Fin w))) (a : Fin w) (acc : Finset (Fin w)) : ∃ (F : Circuits.Formula Circuits.Boolean.signature n), (∀ (x : Fin n → Bool), F.eval Circuits.Boolean.interpretation x = decide (P.eval x a ∈ acc)) ∧ Circuits.Formula.depthWith Circuits.Boolean.binaryCost F ≤ (Nat.clog 2 w + 1) * Nat.clog 2 (FreeMonoid.length P) + Nat.clog 2 w ∧ F.IsNNF

Branching programs give formulas. A branching program of width w and length L, started at a and accepting at the states of acc, is computed by a De Morgan formula of depth at most (⌈log₂ w⌉ + 1) ⌈log₂ L⌉ + ⌈log₂ w⌉, with negations only at the leaves (Formula.IsNNF).

theorem Cslib.BranchingPrograms.MonoidProgram.Computes.exists_formula {n w : ℕ} {P : MonoidProgram (Fin n) Bool (Equiv.Perm (Fin w))} {σ : Equiv.Perm (Fin w)} {f : BooleanFunction n} (hP : P.Computes σ f) (hσ : σ ≠ 1) : ∃ (F : Circuits.Formula Circuits.Boolean.signature n), F.Computes Circuits.Boolean.interpretation f ∧ Circuits.Formula.depthWith Circuits.Boolean.binaryCost F ≤ (Nat.clog 2 w + 1) * Nat.clog 2 (FreeMonoid.length P) + Nat.clog 2 (w * w) ∧ F.IsNNF

Permutation branching programs give formulas. A permutation branching program of width w and length L that σ-computes f, with σ ≠ 1, is turned into a De Morgan formula computing f of depth at most (⌈log₂ w⌉ + 1) ⌈log₂ L⌉ + ⌈log₂ (w ^ 2)⌉, with negations only at the leaves (Formula.IsNNF): f is true where some a is mapped to some b ≠ a.