P/poly

A language over Bool is in P/poly when it has circuits of polynomial size: for every input length n, a circuit over the De Morgan basis computing the slice of the language at n (Language.slice), with size bounded by a polynomially bounded function of n Arora and Barak, Definition 6.5. There is no requirement that the circuits for different lengths be related, so P/poly contains undecidable languages.

PPoly is defined through the minimal circuit size of each slice (Cslib.Circuits.complexity); mem_PPoly_iff_exists_circuits is the textbook formulation with an explicit family of circuits. Size counts gates, constants included, which changes sizes by at most a constant factor and so does not change the class.

Main definitions

• Cslib.Circuits.Boolean.SIZE: the languages with circuits of size at most s n at each length.
• Cslib.Circuits.Boolean.PPoly.

Main results

• Cslib.Circuits.Boolean.mem_PPoly_iff_exists_circuits: the formulation with circuit families.
• Cslib.Circuits.Boolean.mem_PPoly_iff_exists_mem_SIZE: P/poly is the union of the classes SIZE (c (n + 1) ^ c).
• Cslib.Circuits.Boolean.PPoly.of_synthesis: languages whose slices are synthesised within a polynomial budget are in P/poly.
• Cslib.Circuits.Boolean.PPoly.compl, PPoly.sup, PPoly.inf: closure under the Boolean operations.

References

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

def Cslib.Circuits.Boolean.SIZE (s : ℕ → ℕ) : Set (Language Bool)

The languages over Bool that have, for every input length n, a circuit of size at most s n Arora and Barak, Definition 6.2. Size counts gates (Cslib.Circuits.Circuit.size), while Arora and Barak count all vertices, inputs included, so SIZE s is their SIZE (s + n) up to the output vertex.

theorem Cslib.Circuits.Boolean.SIZE_mono : Monotone SIZE

def Cslib.Circuits.Boolean.PPoly : Set (Language Bool)

The languages over Bool whose slices have circuits of polynomial size.

theorem Cslib.Circuits.Boolean.mem_PPoly {L : Language Bool} : L ∈ PPoly ↔ PolynomiallyBounded fun (n : ℕ) => complexity interpretation (single (L.slice n))

theorem Cslib.Circuits.Boolean.mem_PPoly_iff_exists_circuits {L : Language Bool} : L ∈ PPoly ↔ ∃ (C : (n : ℕ) → Circuit signature n 1) (p : ℕ → ℕ), PolynomiallyBounded p ∧ ∀ (n : ℕ), (C n).size ≤ p n ∧ (C n).Computes interpretation (single (L.slice n))

P/poly with circuit families. A language is in P/poly exactly when it has a family of circuits, one for each input length, whose sizes are polynomially bounded.

theorem Cslib.Circuits.Boolean.mem_PPoly_iff_exists_mem_SIZE {L : Language Bool} : L ∈ PPoly ↔ ∃ (c : ℕ), L ∈ SIZE fun (n : ℕ) => c * (n + 1) ^ c

P/poly is the union of the classes SIZE (c (n + 1) ^ c).

theorem Cslib.Circuits.Boolean.PPoly.of_synthesis {L : Language Bool} {cost : ℕ → ℕ} (hcost : PolynomiallyBounded cost) (h : ∀ (n : ℕ), Synthesis interpretation (inputs n) {L.slice n} (cost n)) : L ∈ PPoly

A language whose slices are synthesised from the inputs within a polynomial budget is in P/poly.

theorem Cslib.Circuits.Boolean.PPoly.of_slice_const {L : Language Bool} (b : ℕ → Bool) (h : ∀ (n : ℕ) (x : Fin n → Bool), L.slice n x = b n) : L ∈ PPoly

A language whose slices are constant is in P/poly.

theorem Cslib.Circuits.Boolean.PPoly.zero_mem : 0 ∈ PPoly

theorem Cslib.Circuits.Boolean.PPoly.top_mem : ⊤ ∈ PPoly

theorem Cslib.Circuits.Boolean.PPoly.compl {L : Language Bool} (hL : L ∈ PPoly) : Lᶜ ∈ PPoly

P/poly is closed under complement.

theorem Cslib.Circuits.Boolean.PPoly.sup {L M : Language Bool} (hL : L ∈ PPoly) (hM : M ∈ PPoly) : L ⊔ M ∈ PPoly

P/poly is closed under union.

theorem Cslib.Circuits.Boolean.PPoly.inf {L M : Language Bool} (hL : L ∈ PPoly) (hM : M ∈ PPoly) : L ⊓ M ∈ PPoly

P/poly is closed under intersection.