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. For decision problems over an arbitrary type α with encoding enc : α ↪ List Bool, PPolyOn enc is the class of problems whose image under enc agrees with a language in PPoly.

Main definitions

• Cslib.Circuits.Boolean.SIZE: the languages with circuits of size at most s n at each length.
• Cslib.Circuits.Boolean.PPoly: the languages over Bool with circuits of polynomial size.
• Cslib.Circuits.Boolean.PPolyOn: problems with circuits of polynomial size under an encoding.

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.
• Cslib.Circuits.Boolean.mem_PPolyOn_encBits_iff, Cslib.Circuits.Boolean.PPolyOn.compl, Cslib.Circuits.Boolean.PPolyOn.sup, Cslib.Circuits.Boolean.PPolyOn.inf: agreement with PPoly on encBits and closure of PPolyOn 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

SIZE is monotone in the size bound.

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))

A language is in P/poly if and only if the circuit complexity of its slices is polynomially bounded.

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

The empty language is in P/poly.

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

The universal language is in P/poly.

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.

def Cslib.Circuits.Boolean.PPolyOn {α : Type u_1} (enc : α ↪ List Bool) : Set (Set α)

Problems with circuits of polynomial size. A decision problem A : Set α, with encoding enc : α ↪ List Bool of its instances, lies in PPolyOn enc when some language L ∈ PPoly agrees with A along enc.

theorem Cslib.Circuits.Boolean.mem_PPolyOn {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} : A ∈ PPolyOn enc ↔ ∃ L ∈ PPoly, ∀ (a : α), a ∈ A ↔ enc a ∈ L

A problem is in PPolyOn enc if and only if some language in P/poly agrees with it along enc.

@[simp]

theorem Cslib.Circuits.Boolean.mem_PPolyOn_encBits_iff {A : Language Bool} : A ∈ PPolyOn Turing.MultiTapeTM.encBits ↔ A ∈ PPoly

Over bitstrings (encBits), membership in PPolyOn encBits is membership in PPoly.

theorem Cslib.Circuits.Boolean.PPolyOn.compl {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ PPolyOn enc) : Aᶜ ∈ PPolyOn enc

PPolyOn is closed under complement.

@[simp]

theorem Cslib.Circuits.Boolean.compl_mem_PPolyOn_iff {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} : Aᶜ ∈ PPolyOn enc ↔ A ∈ PPolyOn enc

A complement lies in PPolyOn enc if and only if the problem does.

theorem Cslib.Circuits.Boolean.PPolyOn.sup {α : Type u_1} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ PPolyOn enc) (hB : B ∈ PPolyOn enc) : A ∪ B ∈ PPolyOn enc

PPolyOn is closed under union.

theorem Cslib.Circuits.Boolean.PPolyOn.inf {α : Type u_1} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ PPolyOn enc) (hB : B ∈ PPolyOn enc) : A ∩ B ∈ PPolyOn enc

PPolyOn is closed under intersection.