Monoid programs

For a monoid M, a program over M reads an input x : ι → α, a word over the alphabet α with positions in ι. It is a word of instructions (MonoidProgram), each of which reads the letter at a position i and selects an element of M by a function α → M (Instruction). On an input the program computes the product of the selected elements, the first instruction leftmost (MonoidProgram.eval); evaluation is a monoid homomorphism from programs under concatenation (MonoidProgram.eval_mul) [BT88]. Programs are covariant in the monoid (MonoidProgram.map), and contravariant in the alphabet (MonoidProgram.comap) and in the positions (MonoidProgram.rename).

Branching programs of width w are the programs over Function.End (Fin w), and permutation branching programs those over Equiv.Perm (Fin w); since (σ * τ) a = σ (τ a), the last instruction acts first. A program σ-computes a Boolean-valued function f of its input when its value is σ where f is true and 1 elsewhere (MonoidProgram.Computes) [Bar89].

Programs over groups can be inverted (MonoidProgram.eval_inv), and every program can be pushed along a monoid homomorphism, for instance a conjugation (MonoidProgram.eval_map). So computed functions can be negated (MonoidProgram.Computes.not) and combined by commutators (MonoidProgram.Computes.and), the two steps of Barrington's theorem.

Main definitions

• Cslib.BranchingPrograms.Instruction: an instruction, a position and a function from the alphabet to the monoid; Cslib.BranchingPrograms.Instruction.cond: the instruction selecting one of two elements by a bit.
• Cslib.BranchingPrograms.MonoidProgram: a program over a monoid, a word of instructions.
• Cslib.BranchingPrograms.MonoidProgram.eval: the value of a program on an input.
• Cslib.BranchingPrograms.MonoidProgram.map, Cslib.BranchingPrograms.MonoidProgram.comap, Cslib.BranchingPrograms.MonoidProgram.rename: change of monoid, alphabet and positions.
• Cslib.BranchingPrograms.MonoidProgram.inv, Cslib.BranchingPrograms.MonoidProgram.mulLeft: the inverse of a program over a group, and left multiplication of its value.
• Cslib.BranchingPrograms.MonoidProgram.Computes: σ-computing a Boolean-valued function.

Main results

• Cslib.BranchingPrograms.MonoidProgram.Computes.not, Cslib.BranchingPrograms.MonoidProgram.Computes.and: negation and conjunction of computed functions.

Implementation notes

An instruction selects by a function α → M, as in [BT88], rather than by an element of M for each letter. Barrington's instructions over Boolean inputs, which select one of two elements according to the bit read [Bar89], are the instructions with α := Bool built by Instruction.cond, and every instruction over Bool is one of them (Instruction.cond_var_select). Barrington's programs over n Boolean variables are thus the programs over Fin n → Bool, the bit strings BitString n, with ι := Fin n and α := Bool.

References

• D. A. Barrington, Bounded-width polynomial-size branching programs recognize exactly those languages in NC¹
• D. A. Mix Barrington, D. Thérien, Finite monoids and the fine structure of NC¹

structure Cslib.BranchingPrograms.Instruction (ι : Type u_1) (α : Type u_2) (M : Type u_3) : Type (max (max u_1 u_2) u_3)

An instruction of a program over M on inputs x : ι → α: read the letter x var and select the element select (x var) of M.

• var : ι

  The position read.

• select : α → M

  The element selected for each letter.

def Cslib.BranchingPrograms.Instruction.eval {ι : Type u_1} {α : Type u_3} {M : Type u_5} (I : Instruction ι α M) (x : ι → α) : M

The element an instruction selects on an input.

@[simp]

theorem Cslib.BranchingPrograms.Instruction.eval_mk {ι : Type u_1} {α : Type u_3} {M : Type u_5} (i : ι) (f : α → M) (x : ι → α) : { var := i, select := f }.eval x = f (x i)

def Cslib.BranchingPrograms.Instruction.cond {ι : Type u_1} {M : Type u_5} (i : ι) (t e : M) : Instruction ι Bool M

The instruction over Boolean inputs that reads the bit at position i and selects t when it is true and e when it is false.

@[simp]

theorem Cslib.BranchingPrograms.Instruction.cond_var {ι : Type u_1} {M : Type u_5} (i : ι) (t e : M) : (cond i t e).var = i

@[simp]

theorem Cslib.BranchingPrograms.Instruction.cond_select {ι : Type u_1} {M : Type u_5} (i : ι) (t e : M) (b : Bool) : (cond i t e).select b = bif b then t else e

@[simp]

theorem Cslib.BranchingPrograms.Instruction.eval_cond {ι : Type u_1} {M : Type u_5} (i : ι) (t e : M) (x : ι → Bool) : (cond i t e).eval x = bif x i then t else e

theorem Cslib.BranchingPrograms.Instruction.cond_var_select {ι : Type u_1} {M : Type u_5} (I : Instruction ι Bool M) : cond I.var (I.select true) (I.select false) = I

Every instruction over Boolean inputs selects one of two elements by the bit it reads.

def Cslib.BranchingPrograms.Instruction.const {ι : Type u_1} {α : Type u_3} {M : Type u_5} (i : ι) (m : M) : Instruction ι α M

The instruction that reads position i and selects m whatever the letter.

@[simp]

theorem Cslib.BranchingPrograms.Instruction.const_var {ι : Type u_1} {α : Type u_3} {M : Type u_5} (i : ι) (m : M) : (const i m).var = i

@[simp]

theorem Cslib.BranchingPrograms.Instruction.const_select {ι : Type u_1} {α : Type u_3} {M : Type u_5} (i : ι) (m : M) (x✝ : α) : (const i m).select x✝ = m

@[simp]

theorem Cslib.BranchingPrograms.Instruction.eval_const {ι : Type u_1} {α : Type u_3} {M : Type u_5} (i : ι) (m : M) (x : ι → α) : (const i m).eval x = m

def Cslib.BranchingPrograms.Instruction.map {ι : Type u_1} {α : Type u_3} {M : Type u_5} {N : Type u_6} (φ : M → N) (I : Instruction ι α M) : Instruction ι α N

The instruction selecting φ m instead of each m.

@[simp]

theorem Cslib.BranchingPrograms.Instruction.map_select {ι : Type u_1} {α : Type u_3} {M : Type u_5} {N : Type u_6} (φ : M → N) (I : Instruction ι α M) (a✝ : α) : (map φ I).select a✝ = (φ ∘ I.select) a✝

@[simp]

theorem Cslib.BranchingPrograms.Instruction.map_var {ι : Type u_1} {α : Type u_3} {M : Type u_5} {N : Type u_6} (φ : M → N) (I : Instruction ι α M) : (map φ I).var = I.var

@[simp]

theorem Cslib.BranchingPrograms.Instruction.eval_map {ι : Type u_1} {α : Type u_3} {M : Type u_5} {N : Type u_6} (φ : M → N) (I : Instruction ι α M) (x : ι → α) : (map φ I).eval x = φ (I.eval x)

def Cslib.BranchingPrograms.Instruction.comap {ι : Type u_1} {α : Type u_3} {β : Type u_4} {M : Type u_5} (g : β → α) (I : Instruction ι α M) : Instruction ι β M

The instruction on inputs over β that reads each letter b as g b.

@[simp]

theorem Cslib.BranchingPrograms.Instruction.comap_var {ι : Type u_1} {α : Type u_3} {β : Type u_4} {M : Type u_5} (g : β → α) (I : Instruction ι α M) : (comap g I).var = I.var

@[simp]

theorem Cslib.BranchingPrograms.Instruction.comap_select {ι : Type u_1} {α : Type u_3} {β : Type u_4} {M : Type u_5} (g : β → α) (I : Instruction ι α M) (a✝ : β) : (comap g I).select a✝ = (I.select ∘ g) a✝

@[simp]

theorem Cslib.BranchingPrograms.Instruction.eval_comap {ι : Type u_1} {α : Type u_3} {β : Type u_4} {M : Type u_5} (g : β → α) (I : Instruction ι α M) (x : ι → β) : (comap g I).eval x = I.eval (g ∘ x)

def Cslib.BranchingPrograms.Instruction.rename {ι : Type u_1} {κ : Type u_2} {α : Type u_3} {M : Type u_5} (f : ι → κ) (I : Instruction ι α M) : Instruction κ α M

The instruction that reads position f I.var instead of I.var.

@[simp]

theorem Cslib.BranchingPrograms.Instruction.rename_select {ι : Type u_1} {κ : Type u_2} {α : Type u_3} {M : Type u_5} (f : ι → κ) (I : Instruction ι α M) (a✝ : α) : (rename f I).select a✝ = I.select a✝

@[simp]

theorem Cslib.BranchingPrograms.Instruction.rename_var {ι : Type u_1} {κ : Type u_2} {α : Type u_3} {M : Type u_5} (f : ι → κ) (I : Instruction ι α M) : (rename f I).var = f I.var

@[simp]

theorem Cslib.BranchingPrograms.Instruction.eval_rename {ι : Type u_1} {κ : Type u_2} {α : Type u_3} {M : Type u_5} (f : ι → κ) (I : Instruction ι α M) (x : κ → α) : (rename f I).eval x = I.eval (x ∘ f)

@[reducible, inline]

abbrev Cslib.BranchingPrograms.MonoidProgram (ι : Type u_1) (α : Type u_2) (M : Type u_3) : Type (max (max u_3 u_2) u_1)

A program over M on inputs ι → α: a word of instructions.

def Cslib.BranchingPrograms.MonoidProgram.eval {ι : Type u_1} {α : Type u_3} {M : Type u_5} [Monoid M] (P : MonoidProgram ι α M) (x : ι → α) : M

The product of the elements a program selects on an input, the first instruction leftmost.

theorem Cslib.BranchingPrograms.MonoidProgram.eval_eq_prod {ι : Type u_1} {α : Type u_3} {M : Type u_5} [Monoid M] (P : MonoidProgram ι α M) (x : ι → α) : P.eval x = (List.map (fun (x_1 : Instruction ι α M) => x_1.eval x) (FreeMonoid.toList P)).prod

@[simp]

theorem Cslib.BranchingPrograms.MonoidProgram.eval_one {ι : Type u_1} {α : Type u_3} {M : Type u_5} [Monoid M] (x : ι → α) : eval 1 x = 1

@[simp]

theorem Cslib.BranchingPrograms.MonoidProgram.eval_of {ι : Type u_1} {α : Type u_3} {M : Type u_5} [Monoid M] (I : Instruction ι α M) (x : ι → α) : eval (FreeMonoid.of I) x = I.eval x

@[simp]

theorem Cslib.BranchingPrograms.MonoidProgram.eval_mul {ι : Type u_1} {α : Type u_3} {M : Type u_5} [Monoid M] (P Q : MonoidProgram ι α M) (x : ι → α) : (P * Q).eval x = P.eval x * Q.eval x

def Cslib.BranchingPrograms.MonoidProgram.Computes {ι : Type u_1} {α : Type u_3} {M : Type u_5} [Monoid M] (P : MonoidProgram ι α M) (σ : M) (f : (ι → α) → Bool) : Prop

A program σ-computes a Boolean-valued function f of its input when its value is σ on the inputs where f is true and 1 elsewhere.

def Cslib.BranchingPrograms.MonoidProgram.map {ι : Type u_1} {α : Type u_3} {M : Type u_5} {N : Type u_6} [Monoid M] [Monoid N] (φ : M →* N) (P : MonoidProgram ι α M) : MonoidProgram ι α N

The program selecting φ m instead of each m.

@[simp]

theorem Cslib.BranchingPrograms.MonoidProgram.length_map {ι : Type u_1} {α : Type u_3} {M : Type u_5} {N : Type u_6} [Monoid M] [Monoid N] (φ : M →* N) (P : MonoidProgram ι α M) : FreeMonoid.length (map φ P) = FreeMonoid.length P

@[simp]

theorem Cslib.BranchingPrograms.MonoidProgram.eval_map {ι : Type u_1} {α : Type u_3} {M : Type u_5} {N : Type u_6} [Monoid M] [Monoid N] (φ : M →* N) (P : MonoidProgram ι α M) (x : ι → α) : (map φ P).eval x = φ (P.eval x)

theorem Cslib.BranchingPrograms.MonoidProgram.Computes.map {ι : Type u_1} {α : Type u_3} {M : Type u_5} {N : Type u_6} [Monoid M] [Monoid N] {P : MonoidProgram ι α M} {σ : M} {f : (ι → α) → Bool} (h : P.Computes σ f) (φ : M →* N) : (MonoidProgram.map φ P).Computes (φ σ) f

def Cslib.BranchingPrograms.MonoidProgram.comap {ι : Type u_1} {α : Type u_3} {β : Type u_4} {M : Type u_5} (g : β → α) (P : MonoidProgram ι α M) : MonoidProgram ι β M

The program on inputs over β that reads each letter b as g b.

@[simp]

theorem Cslib.BranchingPrograms.MonoidProgram.length_comap {ι : Type u_1} {α : Type u_3} {β : Type u_4} {M : Type u_5} (g : β → α) (P : MonoidProgram ι α M) : FreeMonoid.length (comap g P) = FreeMonoid.length P

@[simp]

theorem Cslib.BranchingPrograms.MonoidProgram.eval_comap {ι : Type u_1} {α : Type u_3} {β : Type u_4} {M : Type u_5} [Monoid M] (g : β → α) (P : MonoidProgram ι α M) (x : ι → β) : (comap g P).eval x = P.eval (g ∘ x)

def Cslib.BranchingPrograms.MonoidProgram.rename {ι : Type u_1} {κ : Type u_2} {α : Type u_3} {M : Type u_5} (f : ι → κ) (P : MonoidProgram ι α M) : MonoidProgram κ α M

The program that reads position f i wherever P reads position i.

@[simp]

theorem Cslib.BranchingPrograms.MonoidProgram.length_rename {ι : Type u_1} {κ : Type u_2} {α : Type u_3} {M : Type u_5} (f : ι → κ) (P : MonoidProgram ι α M) : FreeMonoid.length (rename f P) = FreeMonoid.length P

@[simp]

theorem Cslib.BranchingPrograms.MonoidProgram.eval_rename {ι : Type u_1} {κ : Type u_2} {α : Type u_3} {M : Type u_5} [Monoid M] (f : ι → κ) (P : MonoidProgram ι α M) (x : κ → α) : (rename f P).eval x = P.eval (x ∘ f)

def Cslib.BranchingPrograms.MonoidProgram.inv {ι : Type u_1} {α : Type u_3} {G : Type u_7} [Group G] (P : MonoidProgram ι α G) : MonoidProgram ι α G

The program with the instructions in reverse order and their elements inverted.

theorem Cslib.BranchingPrograms.MonoidProgram.toList_inv {ι : Type u_1} {α : Type u_3} {G : Type u_7} [Group G] (P : MonoidProgram ι α G) : FreeMonoid.toList P.inv = (List.map (Instruction.map fun (x : G) => x⁻¹) (FreeMonoid.toList P)).reverse

@[simp]

theorem Cslib.BranchingPrograms.MonoidProgram.length_inv {ι : Type u_1} {α : Type u_3} {G : Type u_7} [Group G] (P : MonoidProgram ι α G) : FreeMonoid.length P.inv = FreeMonoid.length P

@[simp]

theorem Cslib.BranchingPrograms.MonoidProgram.eval_inv {ι : Type u_1} {α : Type u_3} {G : Type u_7} [Group G] (P : MonoidProgram ι α G) (x : ι → α) : P.inv.eval x = (P.eval x)⁻¹

def Cslib.BranchingPrograms.MonoidProgram.mulLeft {ι : Type u_1} {α : Type u_3} {M : Type u_5} [Monoid M] [Inhabited ι] (g : M) (P : MonoidProgram ι α M) : MonoidProgram ι α M

Multiply the value of a program by g on the left, without making it longer unless it is empty.

@[simp]

theorem Cslib.BranchingPrograms.MonoidProgram.eval_mulLeft {ι : Type u_1} {α : Type u_3} {M : Type u_5} [Monoid M] [Inhabited ι] (g : M) (P : MonoidProgram ι α M) (x : ι → α) : (mulLeft g P).eval x = g * P.eval x

theorem Cslib.BranchingPrograms.MonoidProgram.length_mulLeft {ι : Type u_1} {α : Type u_3} {M : Type u_5} [Monoid M] [Inhabited ι] (g : M) (P : MonoidProgram ι α M) : FreeMonoid.length (mulLeft g P) = 1 ⊔ FreeMonoid.length P

theorem Cslib.BranchingPrograms.MonoidProgram.Computes.not {ι : Type u_1} {α : Type u_3} {G : Type u_7} [Group G] [Inhabited ι] {σ : G} {f : (ι → α) → Bool} {P : MonoidProgram ι α G} (h : P.Computes σ⁻¹ f) : (mulLeft σ P).Computes σ fun (x : ι → α) => !f x

If P σ⁻¹-computes f, multiplying by σ makes it σ-compute the negation of f.

theorem Cslib.BranchingPrograms.MonoidProgram.Computes.and {ι : Type u_1} {α : Type u_3} {G : Type u_7} [Group G] {σ τ : G} {f g : (ι → α) → Bool} {P Q : MonoidProgram ι α G} (hP : P.Computes σ f) (hQ : Q.Computes τ g) : (P * Q * P.inv * Q.inv).Computes (σ * τ * σ⁻¹ * τ⁻¹) fun (x : ι → α) => f x && g x

The commutator of programs σ- and τ-computing f and g computes f ∧ g with the commutator σ τ σ⁻¹ τ⁻¹.