Nonuniform circuit classes — definitions

This module defines language semantics for circuit families, pointwise circuit size classes, and PPoly, the class conventionally written P/poly.

PPoly is initially specialized to the library's fan-in-two AND/OR basis with free per-gate-input negation flags. Primary input vertices are also excluded from Circuit.size. These choices preserve the usual polynomial-size class after elementary overhead simulations, but exact SIZE bounds are convention-dependent. Basis/size invariance must be proved rather than treated as definitional.

def Complexity.BoolFunFamily.toLanguage (f : BoolFunFamily) : Language

The language whose characteristic function is f, using the canonical list-to-fixed-length representation.

Equations

• f.toLanguage = {x : List Bool | f x.length x.get = true}

def Complexity.CircuitFamily.language {B : Basis} (F : CircuitFamily B) : Language

The language recognized by a circuit family.

Equations

• F.language = F.function.toLanguage

def Complexity.CircuitFamily.Decides {B : Basis} (F : CircuitFamily B) (L : Language) : Prop

F decides L when its recognized language is exactly L.

Equations

• F.Decides L = (F.language = L)

def Complexity.SIZEWithBasis (B : Basis) (s : ℕ → ℕ) : Set Language

Languages decided by B-circuit families with the pointwise size bound s, using this library's non-input-gate count.

Equations

• Complexity.SIZEWithBasis B s = {L : Complexity.Language | ∃ (F : Complexity.CircuitFamily B), F.Decides L ∧ F.SizeBoundedBy s}

def Complexity.SIZE (s : ℕ → ℕ) : Set Language

The fan-in-two AND/OR circuit-size class under the library's free-negation, non-input-gate convention.

Equations

• Complexity.SIZE s = Complexity.SIZEWithBasis Complexity.Basis.andOr2 s

def Complexity.PPoly : Set Language

P/poly: languages decided by polynomial-size nonuniform fan-in-two AND/OR circuit families under the library's size convention, expressed through the SIZE class as the union of the pointwise size classes over all natural-coefficient polynomials. Equivalent to the pointwise PolynomialSize formulation; see PPoly_eq_iUnion_SIZE (definitional) and the big-O characterization mem_PPoly_iff.

Equations

• Complexity.PPoly = ⋃ (p : Polynomial ℕ), Complexity.SIZE fun (n : ℕ) => Polynomial.eval n p