Uniform P/poly

The logspace-uniform polynomial-size circuit class (Arora–Barak Section 6.2). A circuit family is logspace-uniform when its tagged code map 1ⁿ ↦ (code of the length-n member) is computable by a deterministic log-space transducer (FL). UniformPPoly restricts PPoly to such families.

Uniformity is what makes a nonuniform circuit class comparable to a uniform machine class: the headline UniformPPoly = P (UniformPPoly_eq_P, the logspace-uniform characterization of P in Arora–Barak Section 6.2) rests on this definition — the easy containment UniformPPoly ⊆ P runs the log-space generator (FL ⊆ FP) and evaluates the produced code, and P ⊆ UniformPPoly unrolls a time-bounded DTM into a logspace-uniform tableau family.

Logspace-uniformity (rather than the weaker P-uniformity) is the Arora–Barak convention and is what lets the same uniformity notion later scale down to NC/AC.

Main definitions and results

• unaryList — the unary input 1ⁿ.
• CircuitFamily.Uniform — logspace-uniformity of a family (its encodeAt code map is in FL).
• UniformPPoly — the logspace-uniform polynomial-size class.
• UniformPPoly_subset_PPoly — uniform P/poly is contained in nonuniform P/poly.

The circuits-to-machines containment is exposed separately as UniformPPoly_subset_P in Complexitylib.Classes.PPoly.Uniform.Containment.

def Complexity.unaryList (n : ℕ) : List Bool

The unary encoding of n as 1ⁿ (n true bits): the standard generator input that keeps generator time polynomial in n rather than in log n.

Equations

• Complexity.unaryList n = List.replicate n true

def Complexity.CircuitFamily.Uniform (F : CircuitFamily Basis.andOr2) : Prop

A circuit family is logspace-uniform (Arora–Barak Section 6.2) when its tagged code map 1ⁿ ↦ (code of the length-n member) is computable by a deterministic log-space transducer. The tagged encodeAt codec already carries the length-zero answer explicitly, so a single generator function produces the whole family.

Equations

• F.Uniform = ∃ gen ∈ Complexity.FL, ∀ (n : ℕ), gen (Complexity.unaryList n) = F.encodeAt n

def Complexity.UniformPPoly : Set Language

Uniform P/poly: languages decided by a logspace-uniform polynomial-size fan-in-two AND/OR circuit family. The uniform companion of PPoly; its headline is UniformPPoly = P (UniformPPoly_eq_P, Arora–Barak Section 6.2).

Equations

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

theorem Complexity.UniformPPoly_subset_PPoly : UniformPPoly ⊆ PPoly

Uniform P/poly is contained in nonuniform P/poly. Forgetting the uniformity generator leaves exactly a polynomial-size family deciding the language.