Documentation

Complexity.Computability.BranchingProgram.PolyLength

Languages of polynomial-length programs over a monoid #

A program over a monoid M decides a Boolean-valued function f of its input with an accepting set S of elements of M when f is true exactly on the inputs where the value of the program lies in S (MonoidProgram.Decides) [BT88]. PolyLength α M is the class of languages over the alphabet α decided, at every word length n, by programs over M of polynomially bounded length reading the words of length n as inputs Fin n → α. Over the alphabet Bool, the programs over Equiv.Perm (Fin w) are the permutation branching programs of width w, and those over Function.End (Fin w) the branching programs of width w [Bar89]. Like the circuit classes, PolyLength α M is nonuniform.

A program that σ-computes f, with σ ≠ 1, decides f with the accepting set {σ} (MonoidProgram.Computes.decides), and an injective homomorphism of monoids embeds the classes (PolyLength.subset_of_injective).

Main definitions #

Main results #

Implementation notes #

The languages of [BT88] are over a finite alphabet, and their monoids finite. Neither assumption is needed to state the class, so PolyLength α M takes any alphabet α and monoid M; the theorems that need finiteness assume it.

References #

source
def Cslib.BranchingPrograms.MonoidProgram.Decides {ι : Type u_1} {α : Type u_2} {M : Type u_3} [Monoid M] (P : MonoidProgram ι α M) (S : Set M) (f : (ι → α) → Bool) :
Prop

A program decides a Boolean-valued function f of its input with the accepting set S when f is true exactly on the inputs where the value of the program lies in S.

Instances For
    source
    theorem Cslib.BranchingPrograms.MonoidProgram.Computes.decides {ι : Type u_1} {α : Type u_2} {M : Type u_3} [Monoid M] {P : MonoidProgram ι α M} {f : (ι → α) → Bool} {σ : M} (h : P.Computes σ f) (hσ : σ ≠ 1) :
    P.Decides {σ} f

    A program that σ-computes f, with σ ≠ 1, decides f with the accepting set {σ}.

    source
    theorem Cslib.BranchingPrograms.MonoidProgram.Decides.map {ι : Type u_1} {α : Type u_2} {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] {P : MonoidProgram ι α M} {S : Set M} {f : (ι → α) → Bool} (h : P.Decides S f) {φ : M →* N} (hφ : Function.Injective ⇑φ) :
    (MonoidProgram.map φ P).Decides (⇑φ '' S) f

    Pushing a program along an injective homomorphism keeps what it decides, with the image of the accepting set.

    source
    theorem Cslib.BranchingPrograms.MonoidProgram.decides_one {ι : Type u_1} {α : Type u_2} {M : Type u_3} [Monoid M] [IsEmpty ι] (f : (ι → α) → Bool) :
    Decides 1 {_m : M | (f fun (a : ι) => isEmptyElim a) = true} f

    On inputs with no positions, the empty program decides every function, accepting everything when the function is true and nothing when it is false.

    source
    def Cslib.BranchingPrograms.PolyLength (α : Type u_5) (M : Type u_6) [Monoid M] :
    Set (Language α)

    The languages over α decided, at every word length n, by a program over M of length at most s n, with an accepting set, for a polynomially bounded s.

    The class is meant for finite monoids, as in [BT88]. Over an infinite monoid it can contain every language: in the free monoid on ℕ × α, the program of length n that selects the generator (i, x i) at each position i sends different inputs to different elements.

    Instances For
      source
      theorem Cslib.BranchingPrograms.PolyLength.subset_of_injective {α : Type u_2} {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] {φ : M →* N} (hφ : Function.Injective ⇑φ) :
      PolyLength α M ⊆ PolyLength α N

      An injective homomorphism of monoids embeds the classes: push the programs along it.