The converse direction of Barrington's theorem -- definitions

This file defines balanced Boolean formulas for evaluating permutation branching programs. A depth parameter d describes a block of at most 2 ^ d instructions. Two half-blocks are composed by existentially selecting their intermediate state.

It also fixes the semantic family classes used by the nonuniform Barrington equivalence. They follow the existing Barrington convention: formulas and programs are evaluated on total assignments ℕ → Bool, while the family index records the input-length parameter controlling depth and program length.

def Complexity.BoolFormula.disjoin : List BoolFormula → BoolFormula

Disjoin a list of Boolean formulas. The empty disjunction is false.

Equations

• Complexity.BoolFormula.disjoin [] = Complexity.BoolFormula.fls
• Complexity.BoolFormula.disjoin (φ :: fs) = φ.disj (Complexity.BoolFormula.disjoin fs)

def Complexity.BPInstr.reachesFormula {w : ℕ} (ins : BPInstr w) (x y : Fin w) : BoolFormula

A formula saying that this instruction maps state x to state y.

Equations

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

def Complexity.BP.reachesFormula {w : ℕ} : ℕ → BP w → Fin w → Fin w → BoolFormula

A balanced formula saying that a program block maps state x to state y.

At depth zero the formula reads the first instruction, if present. At depth d + 1 it splits after 2 ^ d instructions and disjoins over every possible intermediate state. Its semantic theorem assumes p.length ≤ 2 ^ d.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.BP.reachesFormula 0 [] x✝¹ x✝ = if x✝¹ = x✝ then Complexity.BoolFormula.tru else Complexity.BoolFormula.fls
• Complexity.BP.reachesFormula 0 (ins :: tail) x✝¹ x✝ = ins.reachesFormula x✝¹ x✝

def Complexity.BP.decisionFormula {w : ℕ} (p : BP w) (x : Fin w) : BoolFormula

The canonical balanced formula deciding whether p moves the query point x. Its recursion depth is the least d with p.length ≤ 2 ^ d.

Equations

• p.decisionFormula x = (Complexity.BP.reachesFormula (Nat.clog 2 (List.length p)) p x x).neg

def Complexity.BPFamily (w : ℕ) : Type

A family of width-w permutation branching programs.

Equations

• Complexity.BPFamily w = (ℕ → Complexity.BP w)

def Complexity.BPFamily.PolynomialLength {w : ℕ} (R : BPFamily w) : Prop

A branching-program family has polynomial length.

Equations

• R.PolynomialLength = ∃ (C : ℕ) (p : ℕ), ∀ (n : ℕ), List.length (R n) ≤ C * (n + 1) ^ p

def Complexity.BPFamily.DecidesOnTotalAssignments {w : ℕ} (R : BPFamily w) (x : ℕ → Fin w) (f : ℕ → (ℕ → Bool) → Bool) : Prop

A branching-program family decides a total-assignment family by whether its designated query point is moved by the evaluated permutation.

Equations

• R.DecidesOnTotalAssignments x f = ∀ (n : ℕ) (α : ℕ → Bool), (Complexity.BP.eval α (R n)) (x n) ≠ x n ↔ f n α = true

@[reducible, inline]

abbrev Complexity.BPFamily.Decides {w : ℕ} (R : BPFamily w) (x : ℕ → Fin w) (f : ℕ → (ℕ → Bool) → Bool) : Prop

Compatibility alias for the original total-assignment decision predicate. New statements should use DecidesOnTotalAssignments explicitly.

Equations

• R.Decides x f = R.DecidesOnTotalAssignments x f

def Complexity.BPFamily.toFormulaFamily {w : ℕ} (R : BPFamily w) (x : ℕ → Fin w) : FormulaFamily

Convert a branching-program family into its balanced decision-formula family.

Equations

• R.toFormulaFamily x n = (R n).decisionFormula (x n)

def Complexity.FormulaFamily.ComputesOnTotalAssignments (F : FormulaFamily) (f : ℕ → (ℕ → Bool) → Bool) : Prop

A formula family computes f when it agrees at every family index and on every total assignment.

Equations

• F.ComputesOnTotalAssignments f = ∀ (n : ℕ) (α : ℕ → Bool), Complexity.BoolFormula.eval α (F n) = f n α

@[reducible, inline]

abbrev Complexity.FormulaFamily.Computes (F : FormulaFamily) (f : ℕ → (ℕ → Bool) → Bool) : Prop

Compatibility alias for the original total-assignment computation predicate. New statements should use ComputesOnTotalAssignments explicitly.

Equations

• F.Computes f = F.ComputesOnTotalAssignments f

def Complexity.FormulaNC1OnTotalAssignments : Set (ℕ → (ℕ → Bool) → Bool)

Total-assignment families computed by logarithmic-depth formula families.

The family index controls the depth bound, but assignments have the full domain ℕ → Bool; no assertion is made here that the length-n member only reads variables below n.

Equations

• Complexity.FormulaNC1OnTotalAssignments = {f : ℕ → (ℕ → Bool) → Bool | ∃ (F : Complexity.FormulaFamily), F.LogDepth ∧ F.ComputesOnTotalAssignments f}

def Complexity.Width5BPOnTotalAssignments : Set (ℕ → (ℕ → Bool) → Bool)

Total-assignment families decided by polynomial-length width-5 permutation branching programs.

The family index controls the length bound, but programs may query any natural variable index.

Equations

• Complexity.Width5BPOnTotalAssignments = {f : ℕ → (ℕ → Bool) → Bool | ∃ (R : Complexity.BPFamily 5) (x : ℕ → Fin 5), R.PolynomialLength ∧ R.DecidesOnTotalAssignments x f}