Permutation branching programs

Width-w permutation branching programs: a program is a list of instructions, each of which reads one input variable and applies one of two permutations of Fin w accordingly; the program evaluates to the ordered product of the selected permutations (roadmap track M3, toward Barrington's theorem).

Main definitions and results

• BPInstr, BP — instructions and programs
• BP.eval — the evaluated permutation
• BP.eval_append, BP.eval_cons — the product (append/cons) semantics that Barrington's inductive construction rests on

structure Complexity.BPInstr (w : ℕ) : Type

A single width-w branching-program instruction: read variable var, and apply perm1 if it is true, perm0 if it is false.

• var : ℕ

  The input variable this instruction reads.

• perm0 : Equiv.Perm (Fin w)

  The permutation applied when the variable is false.

• perm1 : Equiv.Perm (Fin w)

  The permutation applied when the variable is true.

@[reducible, inline]

abbrev Complexity.BP (w : ℕ) : Type

A width-w permutation branching program is a list of instructions.

Equations

• Complexity.BP w = List (Complexity.BPInstr w)

def Complexity.BPInstr.eval {w : ℕ} (α : ℕ → Bool) (ins : BPInstr w) : Equiv.Perm (Fin w)

The permutation an instruction selects under an assignment.

Equations

• Complexity.BPInstr.eval α ins = if α ins.var = true then ins.perm1 else ins.perm0

def Complexity.BP.eval {w : ℕ} (α : ℕ → Bool) (p : BP w) : Equiv.Perm (Fin w)

Evaluate a branching program to a permutation: the ordered product of its instructions' selected permutations.

Equations

• Complexity.BP.eval α p = (List.map (Complexity.BPInstr.eval α) p).prod

@[simp]

theorem Complexity.BP.eval_nil {w : ℕ} (α : ℕ → Bool) : eval α [] = 1

theorem Complexity.BP.eval_append {w : ℕ} (α : ℕ → Bool) (p q : BP w) : eval α (p ++ q) = eval α p * eval α q

Product semantics. Concatenating programs multiplies their evaluated permutations — the compositional law underlying Barrington's construction.

theorem Complexity.BP.eval_cons {w : ℕ} (α : ℕ → Bool) (ins : BPInstr w) (p : BP w) : eval α (ins :: p) = BPInstr.eval α ins * eval α p

Evaluating a cons prepends the head instruction's permutation.

theorem Complexity.BP.eval_singleton {w : ℕ} (α : ℕ → Bool) (ins : BPInstr w) : eval α [ins] = BPInstr.eval α ins

A single-instruction program evaluates to that instruction's permutation.

def Complexity.BPInstr.rename {w : ℕ} (σ : ℕ → ℕ) (ins : BPInstr w) : BPInstr w

Rename the input variables of an instruction along σ.

Equations

• Complexity.BPInstr.rename σ ins = { var := σ ins.var, perm0 := ins.perm0, perm1 := ins.perm1 }

def Complexity.BP.rename {w : ℕ} (σ : ℕ → ℕ) (p : BP w) : BP w

Rename the input variables throughout a program.

Equations

• Complexity.BP.rename σ p = List.map (Complexity.BPInstr.rename σ) p

theorem Complexity.BPInstr.eval_rename {w : ℕ} (α : ℕ → Bool) (σ : ℕ → ℕ) (ins : BPInstr w) : eval α (rename σ ins) = eval (α ∘ σ) ins

Renaming an instruction's variables is a semantics-preserving relabeling: evaluating the renamed instruction at α equals evaluating the original at α ∘ σ.

theorem Complexity.BP.eval_rename {w : ℕ} (α : ℕ → Bool) (σ : ℕ → ℕ) (p : BP w) : eval α (rename σ p) = eval (α ∘ σ) p

Evaluation is invariant under a semantics-preserving variable rename: evaluating the renamed program at α equals evaluating the original at α ∘ σ.

def Complexity.BP.vars {w : ℕ} (p : BP w) : Finset ℕ

The set of input variables a branching program reads.

Equations

• p.vars = (List.map Complexity.BPInstr.var p).toFinset

theorem Complexity.BPInstr.eval_eq_of_agree {w : ℕ} (ins : BPInstr w) (α β : ℕ → Bool) (h : α ins.var = β ins.var) : eval α ins = eval β ins

Agreement on an instruction's variable fixes the permutation it selects.

theorem Complexity.BP.eval_eq_of_agree {w : ℕ} (p : BP w) (α β : ℕ → Bool) (h : ∀ (i : ℕ), i ∈ p.vars → α i = β i) : eval α p = eval β p

Locality. A branching program's value depends only on the variables it reads: if two assignments agree on BP.vars p, they yield the same permutation.