Circuit depth classes -- definitions

This module defines exact depth classes for Boolean-function families using the library's CircuitFamily convention. In particular, the unique length-zero input is represented by CircuitFamily.emptyOutput rather than omitted.

NC i uses fan-in-two AND/OR circuits, while AC i uses unbounded-fan-in AND/OR circuits. Both require polynomial size and depth O((log n + 1)^i) in an explicit pointwise form.

def Complexity.polylogDepth (i c n : ℕ) : ℕ

A concrete O((log₂ n + 1)^i) depth envelope with multiplicative constant c. The + 1 makes the base positive and gives constant depth when i = 0.

Equations

• Complexity.polylogDepth i c n = c * (Nat.log 2 n + 1) ^ i

def Complexity.DEPTHWithBasis (B : Basis) (d : ℕ → ℕ) : Set BoolFunFamily

Boolean-function families computed by B-circuit families under the pointwise depth bound d. No size restriction is implicit in DEPTHWithBasis.

Equations

• Complexity.DEPTHWithBasis B d = {f : Complexity.BoolFunFamily | ∃ (F : Complexity.CircuitFamily B), F.Computes f ∧ F.DepthBoundedBy d}

def Complexity.DEPTH (d : ℕ → ℕ) : Set BoolFunFamily

The bounded-fan-in AND/OR depth class under the pointwise bound d.

Equations

• Complexity.DEPTH d = Complexity.DEPTHWithBasis Complexity.Basis.andOr2 d

def Complexity.NC (i : ℕ) : Set BoolFunFamily

NC^i, in its nonuniform circuit-family form: polynomial-size, fan-in-two AND/OR circuits of depth O((log n + 1)^i).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.AC (i : ℕ) : Set BoolFunFamily

AC^i, in its nonuniform circuit-family form: polynomial-size, unbounded-fan-in AND/OR circuits of depth O((log n + 1)^i).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TC (i : ℕ) : Set BoolFunFamily

TC^i, in its nonuniform circuit-family form: polynomial-size, unbounded-fan-in threshold circuits of depth O((log n + 1)^i).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.NC0 : Set BoolFunFamily

Constant-depth, polynomial-size bounded-fan-in circuits.

Equations

• Complexity.NC0 = Complexity.NC 0

def Complexity.NC1 : Set BoolFunFamily

Logarithmic-depth, polynomial-size bounded-fan-in circuits.

Equations

• Complexity.NC1 = Complexity.NC 1

def Complexity.AC0 : Set BoolFunFamily

Constant-depth, polynomial-size unbounded-fan-in circuits.

Equations

• Complexity.AC0 = Complexity.AC 0

def Complexity.TC0 : Set BoolFunFamily

Constant-depth, polynomial-size threshold circuits.

Equations

• Complexity.TC0 = Complexity.TC 0