An executable Barrington compiler -- definitions

The original existence proof chooses conjugators and commutator factors inside Prop. This module instead searches the finite group S₅ explicitly, making the target-cycle decomposition and the resulting formula compiler executable.

def Complexity.allPermutationsFin (n : ℕ) : List (Equiv.Perm (Fin n))

A computable enumeration of every permutation of Fin n, obtained from the recursive decomposition S_(n+1) ≃ Fin (n+1) × S_n.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.allPermutationsFin 0 = [1]

def Complexity.isConjugator5 (source target g : Equiv.Perm (Fin 5)) : Bool

Test whether g conjugates source to target.

Equations

• Complexity.isConjugator5 source target g = decide (g * source * g⁻¹ = target)

def Complexity.firstConjugator5 (source target : Equiv.Perm (Fin 5)) : Equiv.Perm (Fin 5)

The first conjugator in the canonical finite enumeration of S₅, or the identity if no conjugator exists.

Equations

• Complexity.firstConjugator5 source target = (List.find? (Complexity.isConjugator5 source target) (Complexity.allPermutationsFin 5)).getD 1

def Complexity.barringtonLeftBase : Equiv.Perm (Fin 5)

The first fixed 5-cycle in the explicit Barrington commutator.

Equations

• Complexity.barringtonLeftBase = finRotate 5

def Complexity.barringtonRightBase : Equiv.Perm (Fin 5)

The second fixed 5-cycle in the explicit Barrington commutator.

Equations

• Complexity.barringtonRightBase = [0, 2, 4, 3, 1].formPerm

def Complexity.barringtonTargetBase : Equiv.Perm (Fin 5)

The fixed target cycle obtained as the commutator of the two base cycles.

Equations

• Complexity.barringtonTargetBase = ⁅Complexity.barringtonLeftBase, Complexity.barringtonRightBase⁆

def Complexity.barringtonConjugator (target : Equiv.Perm (Fin 5)) : Equiv.Perm (Fin 5)

Canonically search for a permutation conjugating the fixed target cycle to target.

Equations

• Complexity.barringtonConjugator target = Complexity.firstConjugator5 Complexity.barringtonTargetBase target

def Complexity.barringtonLeft (target : Equiv.Perm (Fin 5)) : Equiv.Perm (Fin 5)

The left factor in the canonical commutator decomposition of target.

Equations

• Complexity.barringtonLeft target = Complexity.barringtonConjugator target * Complexity.barringtonLeftBase * (Complexity.barringtonConjugator target)⁻¹

def Complexity.barringtonRight (target : Equiv.Perm (Fin 5)) : Equiv.Perm (Fin 5)

The right factor in the canonical commutator decomposition of target.

Equations

• Complexity.barringtonRight target = Complexity.barringtonConjugator target * Complexity.barringtonRightBase * (Complexity.barringtonConjugator target)⁻¹

def Complexity.BP.commutatorProgram {w : ℕ} (p q : BP w) : BP w

The four-block program commutator p q p⁻¹ q⁻¹.

Equations

• p.commutatorProgram q = p ++ q ++ p.inverse ++ q.inverse

def Complexity.barringtonCompile : BoolFormula → Equiv.Perm (Fin 5) → BP 5

Compile a Boolean formula to a width-5 permutation branching program representing it through target.

The definition is total for every target permutation. Its correctness theorem assumes that target is a 5-cycle. Binary gates use the executable canonical commutator decomposition above; no choice from an existential proof remains.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.barringtonCompile (Complexity.BoolFormula.var i) x✝ = [{ var := i, perm0 := 1, perm1 := x✝ }]
• Complexity.barringtonCompile Complexity.BoolFormula.tru x✝ = [Complexity.BPInstr.const x✝]
• Complexity.barringtonCompile Complexity.BoolFormula.fls x✝ = []
• Complexity.barringtonCompile formula.neg x✝ = (Complexity.barringtonCompile formula x✝⁻¹).postMul x✝