Documentation

Complexity.Computability.Circuit.Boolean.ConstDepth

Constant-depth circuit classes #

ConstDepth I is the class of languages decided, at every input length, by circuits over the Boolean basis I of polynomially bounded size and constant depth. AC⁰ Arora and Barak, Section 6.7.1, AC⁰[q] Arora and Barak, Section 14.2 and TC⁰ Vollmer, Chapter 4 are this class for their bases. A map of bases that keeps the meaning of every operation embeds the classes (ConstDepth.mono), and so does a basis computing every operation of another with a bounded number of gates in bounded depth (ConstDepth.subset_of_simulation).

The depth of a circuit counts every gate on a path, and its size counts every gate (cslib's Circuit.depth and Circuit.size); for a constant-depth class with polynomial size, the convention does not matter.

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Boolean.DepthClass {σ : Signature} (I : Interpretation σ Bool) (D : ℕ → ℕ) :
Set (Language Bool)

The languages over Bool decided, at every input length n, by circuits over the basis I of polynomially bounded size and depth at most c * D n for a constant c.

Instances For
    source
    theorem Cslib.Circuits.Boolean.DepthClass.mono {σ : Signature} {τ : Signature} {I : Interpretation σ Bool} {D : ℕ → ℕ} (φ : σ.Hom τ) {J : Interpretation τ Bool} [φ.Preserves I J] :
    DepthClass I D ⊆ DepthClass J D

    A map of bases keeping the meaning of every operation embeds the classes: translate the circuits gate by gate.

    source
    theorem Cslib.Circuits.Boolean.DepthClass.subset_of_simulation {σ : Signature} {τ : Signature} {I : Interpretation σ Bool} {D : ℕ → ℕ} {J : Interpretation τ Bool} {b c : ℕ} (h : ∀ (op : σ.Op), ∃ (C : Circuit τ (σ.Arity op) 1), C.Computes J (single (I op)) ∧ C.size ≤ b ∧ C.depth ≤ c) :
    DepthClass I D ⊆ DepthClass J D

    A simulation in bounded size and depth embeds the classes: if every operation of I is computed under J by a circuit of at most b gates and depth at most c, replacing every gate by its circuit multiplies sizes by at most b and depths by at most c.

    source
    theorem Cslib.Circuits.Boolean.DepthClass.mono_depth {σ : Signature} {I : Interpretation σ Bool} {D D' : ℕ → ℕ} (h : ∀ (n : ℕ), D n ≤ D' n) :
    DepthClass I D ⊆ DepthClass I D'

    A larger depth envelope gives a larger class.

    source
    def Cslib.Circuits.Boolean.ConstDepth {σ : Signature} (I : Interpretation σ Bool) :
    Set (Language Bool)

    The languages over Bool decided, at every input length, by circuits over the basis I of polynomially bounded size and constant depth.

    Instances For
      source
      theorem Cslib.Circuits.Boolean.ConstDepth.mem_iff {σ : Signature} {I : Interpretation σ Bool} {L : Language Bool} :
      L ∈ ConstDepth I ↔ ∃ (d : ℕ) (s : ℕ → ℕ), PolynomiallyBounded s ∧ ∀ (n : ℕ), ∃ (C : Circuit σ n 1), C.Computes I (single (L.slice n)) ∧ C.depth ≤ d ∧ C.size ≤ s n

      Membership in ConstDepth I: a depth bound and a polynomial size bound, and circuits for every slice within them.

      source
      theorem Cslib.Circuits.Boolean.ConstDepth.mono {σ : Signature} {τ : Signature} {I : Interpretation σ Bool} (φ : σ.Hom τ) {J : Interpretation τ Bool} [φ.Preserves I J] :
      ConstDepth I ⊆ ConstDepth J

      A map of bases keeping the meaning of every operation embeds the classes.

      source
      theorem Cslib.Circuits.Boolean.ConstDepth.subset_of_simulation {σ : Signature} {τ : Signature} {I : Interpretation σ Bool} {J : Interpretation τ Bool} {b c : ℕ} (h : ∀ (op : σ.Op), ∃ (C : Circuit τ (σ.Arity op) 1), C.Computes J (single (I op)) ∧ C.size ≤ b ∧ C.depth ≤ c) :
      ConstDepth I ⊆ ConstDepth J

      A simulation in bounded size and depth embeds the classes: if every operation of I is computed under J by a circuit of at most b gates and depth at most c.