Sparse and unary languages have circuits of polynomial size

A slice with at most k words of length n is the disjunction of the minterms of its words, so it has a circuit of k (2 n + 2) + 1 gates (complexity_slice_le_of_card_le). A language with polynomially many words of each length, a sparse language, is therefore in P/poly (PPoly.of_sparse). A unary language, whose words consist only of trues, has at most one word of each length, and its slice at n is a constant or the conjunction of the n inputs, so it has circuits of n + 1 gates (mem_SIZE_of_unary). Since the circuits at different lengths need not be related, unary languages that no machine decides are in P/poly Arora and Barak, Section 6.1.

Main results

• Cslib.Circuits.Boolean.complexity_slice_le_of_card_le: a slice with few words has a small circuit.
• Cslib.Circuits.Boolean.PPoly.of_sparse: sparse languages are in P/poly.
• Cslib.Circuits.Boolean.mem_SIZE_of_unary, Cslib.Circuits.Boolean.PPoly.of_unary: unary languages have circuits of n + 1 gates, so they are in P/poly.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

theorem Cslib.Circuits.Boolean.complexity_slice_le_of_card_le {L : Language Bool} {n k : ℕ} (h : {x : BitString n | L.slice n x = true}.card ≤ k) : complexity interpretation (single (L.slice n)) ≤ k * (2 * n + 2) + 1

A slice with at most k words of length n has a circuit of k (2 n + 2) + 1 gates: the disjunction of the minterms of its words.

theorem Cslib.Circuits.Boolean.PPoly.of_sparse {L : Language Bool} {s : ℕ → ℕ} (hs : PolynomiallyBounded s) (h : ∀ (n : ℕ), {x : BitString n | L.slice n x = true}.card ≤ s n) : L ∈ PPoly

Sparse languages are in P/poly. A language with at most s n words of each length n, for a polynomially bounded s, has circuits of polynomial size.

theorem Cslib.Circuits.Boolean.mem_SIZE_of_unary {L : Language Bool} (hL : ∀ w ∈ L, ∀ b ∈ w, b = true) : L ∈ SIZE fun (n : ℕ) => n + 1

Unary languages have linear-size circuits. A language whose words consist only of trues has, at every length n, a circuit of n + 1 gates: a constant when the word of length n is not in the language, and the conjunction of the inputs otherwise.

theorem Cslib.Circuits.Boolean.PPoly.of_unary {L : Language Bool} (hL : ∀ w ∈ L, ∀ b ∈ w, b = true) : L ∈ PPoly

Unary languages are in P/poly, including those that no machine decides.