The NC, AC and TC hierarchies

PolylogDepth I i is the class of languages decided, at every input length n, by circuits over the Boolean basis I of polynomially bounded size and depth O((log n) ^ i), with the explicit envelope c (⌊log₂ n⌋ + 1) ^ i. Over the De Morgan basis of fan-in two this is NCⁱ, over the unbounded fan-in basis ACⁱ, with majority gates TCⁱ, and with MOD_q gates ACⁱ[q] Arora and Barak, Section 6.7, Vollmer, Chapter 4. For i = 0 these are the constant-depth classes (polylogDepth_zero). Every hierarchy is monotone in i (PolylogDepth.mono_exponent), and a meaning-preserving map of bases embeds the classes (PolylogDepth.mono), so NCⁱ ⊆ ACⁱ ⊆ TCⁱ and ACⁱ ⊆ ACⁱ[q]. These classes are nonuniform.

Main definitions

• Cslib.Circuits.Boolean.PolylogDepth: polynomial size and depth O((log n) ^ i).
• Cslib.Circuits.Boolean.NC, AC, TC, ACMod: the hierarchies.

Main results

• Cslib.Circuits.Boolean.NC_subset_AC, AC_subset_TC, AC_subset_ACMod: the inclusions.
• Cslib.Circuits.Boolean.AC_zero, TC_zero, ACMod_zero: the constant-depth classes.
• Cslib.Circuits.Boolean.NC_subset_PPoly: NCⁱ ⊆ P/poly.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• H. Vollmer, Introduction to Circuit Complexity

def Cslib.Circuits.Boolean.PolylogDepth {σ : Signature} (I : Interpretation σ Bool) (i : ℕ) : Set (Language Bool)

The languages over Bool decided, at every input length n, by circuits over I of polynomially bounded size and depth at most c (⌊log₂ n⌋ + 1) ^ i for a constant c.

theorem Cslib.Circuits.Boolean.PolylogDepth.mono_exponent {σ : Signature} {I : Interpretation σ Bool} {i j : ℕ} (hij : i ≤ j) : PolylogDepth I i ⊆ PolylogDepth I j

The hierarchy is monotone in the exponent.

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

A meaning-preserving map of bases embeds the classes.

theorem Cslib.Circuits.Boolean.polylogDepth_zero {σ : Signature} (I : Interpretation σ Bool) : PolylogDepth I 0 = ConstDepth I

For exponent zero, polynomial size and constant depth.

def Cslib.Circuits.Boolean.NC (i : ℕ) : Set (Language Bool)

NCⁱ: polynomial size and depth O((log n) ^ i) over the De Morgan basis of fan-in two.

def Cslib.Circuits.Boolean.AC (i : ℕ) : Set (Language Bool)

ACⁱ: polynomial size and depth O((log n) ^ i) with unbounded fan-in.

def Cslib.Circuits.Boolean.TC (i : ℕ) : Set (Language Bool)

TCⁱ: polynomial size and depth O((log n) ^ i) with majority gates.

def Cslib.Circuits.Boolean.ACMod (q i : ℕ) : Set (Language Bool)

ACⁱ[q]: polynomial size and depth O((log n) ^ i) with MOD_q gates.

theorem Cslib.Circuits.Boolean.AC_zero : AC 0 = AC0

theorem Cslib.Circuits.Boolean.TC_zero : TC 0 = TC0

theorem Cslib.Circuits.Boolean.ACMod_zero (q : ℕ) : ACMod q 0 = AC0Mod q

theorem Cslib.Circuits.Boolean.NC_subset_AC (i : ℕ) : NC i ⊆ AC i

NCⁱ ⊆ ACⁱ.

theorem Cslib.Circuits.Boolean.AC_subset_TC (i : ℕ) : AC i ⊆ TC i

ACⁱ ⊆ TCⁱ.

theorem Cslib.Circuits.Boolean.AC_subset_ACMod (q i : ℕ) : AC i ⊆ ACMod q i

ACⁱ ⊆ ACⁱ[q].

theorem Cslib.Circuits.Boolean.NC_mono {i j : ℕ} (hij : i ≤ j) : NC i ⊆ NC j

theorem Cslib.Circuits.Boolean.AC_mono {i j : ℕ} (hij : i ≤ j) : AC i ⊆ AC j

theorem Cslib.Circuits.Boolean.TC_mono {i j : ℕ} (hij : i ≤ j) : TC i ⊆ TC j

theorem Cslib.Circuits.Boolean.ACMod_mono (q : ℕ) {i j : ℕ} (hij : i ≤ j) : ACMod q i ⊆ ACMod q j

theorem Cslib.Circuits.Boolean.NC_subset_PPoly (i : ℕ) : NC i ⊆ PPoly

NCⁱ ⊆ P/poly for every i: a language decided by polynomial-size De Morgan circuits of polylogarithmic depth has polynomially bounded circuit complexity.