Fixed-arity nonuniform Barrington families -- definitions

The earlier Barrington family layer evaluates syntax on total assignments ℕ → Bool. This file defines the fixed-arity objects needed for an actual class of typed Boolean-function families:

• the formula selected at arity n may mention only variables below n;
• the positive-arity branching program selected at arity n + 1 may query only variables below n + 1;
• the unique zero-bit answer of a branching-program family is stored separately, because a nonempty instruction necessarily carries a variable index.

Both objects denote BoolFunFamily, so the eventual equivalence has the correct fixed-arity semantic domain.

structure Complexity.FixedArityFormulaFamily : Type

A nonuniform family of formulas with an explicit arity bound on every member.

• formula : ℕ → BoolFormula

  The formula selected at each input length.

• variables_lt (n index : ℕ) : index ∈ (self.formula n).vars → index < n

  Every variable mentioned by the length-n formula is below n.

def Complexity.FixedArityFormulaFamily.function (F : FixedArityFormulaFamily) : BoolFunFamily

The typed Boolean-function family denoted by a fixed-arity formula family. Out-of-range variables are canonically set to false, though variables_lt ensures they are not read.

Equations

• F.function n input = Complexity.BoolFormula.eval input.toTotal (F.formula n)

def Complexity.FixedArityFormulaFamily.depth (F : FixedArityFormulaFamily) (n : ℕ) : ℕ

The formula depth at each input length.

Equations

• F.depth n = (F.formula n).depth

def Complexity.FixedArityFormulaFamily.LogDepth (F : FixedArityFormulaFamily) : Prop

A fixed-arity formula family has logarithmic depth.

Equations

• F.LogDepth = ∃ (c : ℕ), ∀ (n : ℕ), F.depth n ≤ c * Nat.log 2 n + c

def Complexity.FixedArityFormulaFamily.Computes (F : FixedArityFormulaFamily) (f : BoolFunFamily) : Prop

A fixed-arity formula family computes a typed Boolean-function family.

Equations

• F.Computes f = (F.function = f)

structure Complexity.FixedArityBPFamily (w : ℕ) : Type

A nonuniform width-w branching-program family with explicit positive input arities and a separate zero-input answer.

• emptyOutput : Bool

  The answer on the unique zero-bit input.

• positiveProgram : ℕ → BP w

  The program at input length n + 1.

• positiveQuery : ℕ → Fin w

  The point whose movement decides acceptance at input length n + 1.

• variables_lt (n : ℕ) (instruction : BPInstr w) : instruction ∈ self.positiveProgram n → instruction.var < n + 1

  The length-n + 1 program queries only variables below n + 1.

def Complexity.FixedArityBPFamily.length {w : ℕ} (R : FixedArityBPFamily w) : ℕ → ℕ

The program length at each typed input length. The separately stored zero-input answer has length zero.

Equations

• R.length 0 = 0
• R.length n.succ = List.length (R.positiveProgram n)

def Complexity.FixedArityBPFamily.function {w : ℕ} (R : FixedArityBPFamily w) : BoolFunFamily

The typed Boolean-function family decided by movement of the designated query point.

Equations

• R.function 0 x_2 = R.emptyOutput
• R.function n.succ input = decide ((Complexity.BP.eval input.toTotal (R.positiveProgram n)) (R.positiveQuery n) ≠ R.positiveQuery n)

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

A fixed-arity branching-program family has polynomial length.

Equations

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

def Complexity.FixedArityBPFamily.Decides {w : ℕ} (R : FixedArityBPFamily w) (f : BoolFunFamily) : Prop

A fixed-arity branching-program family decides a typed Boolean-function family.

Equations

• R.Decides f = (R.function = f)

def Complexity.FormulaNC1 : Set BoolFunFamily

Typed Boolean-function families computed by variable-bounded, logarithmic-depth formula families.

Equations

• Complexity.FormulaNC1 = {f : Complexity.BoolFunFamily | ∃ (F : Complexity.FixedArityFormulaFamily), F.LogDepth ∧ F.Computes f}

def Complexity.Width5BP : Set BoolFunFamily

Typed Boolean-function families decided by variable-bounded, polynomial-length width-5 permutation branching-program families.

Equations

• Complexity.Width5BP = {f : Complexity.BoolFunFamily | ∃ (R : Complexity.FixedArityBPFamily 5), R.PolynomialLength ∧ R.Decides f}