Documentation

Complexity.Computability.Circuit.Boolean.TC0

TC⁰ #

TC⁰ is the class of languages decided, at every input length, by circuits of polynomial size and constant depth whose gates are negations, conjunctions and disjunctions of unbounded fan-in, and majority gates of unbounded fan-in Vollmer, Chapter 4: the unbounded fan-in basis extended by majority (Unbounded.extInterpretation majority). Every AC⁰ circuit is a TC⁰ circuit (AC0_subset_TC0), and majority is a single gate, so majority is in TC⁰ (majority_mem_TC0) but not in AC⁰: AC⁰ is strictly contained in TC⁰ (AC0_ssubset_TC0).

TC⁰ is also the class of the threshold circuits of polynomial size and constant depth (TC0_eq_constDepth_threshold) Hajnal et al., Section 2. A majority gate is a threshold gate (Threshold.ofMajority). Conversely, a threshold gate Th^m_j is a majority gate on its m arguments padded with m + 2 constants, m + 1 - j of them true, read from two constant gates (thresholdCircuitOfMajority): three gates in depth two, whatever the fan-in. So parity, which has threshold circuits of depth three and linear size (Threshold.parity_mem_constDepth), is in TC⁰ (parity_mem_TC0).

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Boolean.TC0 :
Set (Language Bool)

TC⁰: the languages over Bool decided, at every input length, by circuits with majority gates of polynomially bounded size and constant depth.

Instances For
    source
    theorem Cslib.Circuits.Boolean.AC0_subset_TC0 :
    AC0 ⊆ TC0

    AC⁰ ⊆ TC⁰: every AC⁰ circuit is a circuit with majority gates.

    source
    theorem Cslib.Circuits.Boolean.majority_mem_TC0 :
    Language.ofSlices majority ∈ TC0

    Majority is in TC⁰: it is a single gate.

    source
    theorem Cslib.Circuits.Boolean.AC0_ssubset_TC0 :
    AC0 ⊂ TC0

    AC⁰ is strictly contained in TC⁰.

    source
    def Cslib.Circuits.Boolean.Threshold.majorityCircuit (op : Op) :
    Circuit Unbounded.extSignature (signature.Arity op) 1

    A gate of the threshold basis as a circuit over the basis of TC⁰: a negation is a negation, and the threshold gate Th^m_j is a majority gate of 2 m + 2 arguments, its m arguments padded with m + 1 - j copies of true and the rest copies of false.

    Instances For
      source
      theorem Cslib.Circuits.Boolean.Threshold.computes_majorityCircuit (op : Op) :
      (majorityCircuit op).Computes (Unbounded.extInterpretation majority) (single (interpretation op))

      The circuit of a gate computes the gate.

      source
      theorem Cslib.Circuits.Boolean.Threshold.size_majorityCircuit_le (op : Op) :
      (majorityCircuit op).size ≤ 3

      The circuit of a gate has at most three gates.

      source
      theorem Cslib.Circuits.Boolean.Threshold.depth_majorityCircuit_le (op : Op) :
      (majorityCircuit op).depth ≤ 2

      The circuit of a gate has depth at most two.

      source
      theorem Cslib.Circuits.Boolean.TC0_eq_constDepth_threshold :
      TC0 = ConstDepth Threshold.interpretation

      TC⁰ is the class of threshold circuits of polynomial size and constant depth: majority gates are threshold gates, and a threshold gate is a majority gate with constants.

      source
      theorem Cslib.Circuits.Boolean.parity_mem_TC0 :
      Language.ofSlices parity ∈ TC0

      Parity is in TC⁰: it has threshold circuits of depth three and linear size.