P ⊆ P/poly and BPP ⊆ P/poly

A problem decided in polynomial time has circuits of polynomial size Arora and Barak, Theorem 6.6: the machine deciding it writes [true] within polynomially many steps exactly on the encoded members, and the inputs on which a machine does so form a language in P/poly (MachineSimulation.acceptedWithin_mem_PPoly). With Adleman's theorem (PPoly.of_boundedError), the same holds for problems decided with bounded error Arora and Barak, Theorem 7.14: the verifier's circuits read frame x ++ r, whose bits are bits of x, bits of r or constants (frameWiring), so they are circuits for a function of x ++ r of the same size up to two gates.

Main definitions

• Cslib.Circuits.Boolean.frameWiring, Cslib.Circuits.Boolean.framedSlice: the input-and-constant substitution building frame x ++ r from x ++ r, and the slice of a language pulled back along that framing.
• Cslib.Circuits.Boolean.encodes, Cslib.Circuits.Boolean.encodesMember: the words of length n in the image of an encoding enc, and the indicator of encoded members of a set A.

Main results

• Cslib.Circuits.Boolean.PPoly.exists_of_polyTime: the instances on which a Boolean function computable in polynomial time is true are the preimage of a language in P/poly.
• Cslib.Circuits.Boolean.P_subset_PPolyOn: P ⊆ P/poly, for problems with any encoding of their instances.
• Cslib.Circuits.Boolean.BPP_subset_PPolyOn, Cslib.Circuits.Boolean.RP_subset_PPolyOn, Cslib.Circuits.Boolean.coRP_subset_PPolyOn: BPP, RP, coRP ⊆ P/poly, for problems with any encoding of their instances.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 7.5
• M. Sipser, Introduction to the Theory of Computation, Section 9.3

theorem Cslib.Circuits.Boolean.PPoly.exists_of_polyTime {α : Type u_1} {enc : α ↪ List Bool} {f : α → Bool} (hf : Turing.MultiTapeTM.ComputableInPolyTime f enc Turing.MultiTapeTM.encBool) : ∃ L ∈ PPoly, ∀ (a : α), f a = true ↔ enc a ∈ L

The instances on which a Boolean function computable in polynomial time is true are the preimage, under the encoding, of a language in P/poly.

theorem Cslib.Circuits.Boolean.P_subset_PPolyOn {α : Type u_1} {enc : α ↪ List Bool} : Complexity.P enc ⊆ PPolyOn enc

P ⊆ P/poly. A problem in P, with any encoding enc of its instances, is the preimage under enc of a language in P/poly.

Randomised classes

def Cslib.Circuits.Boolean.frameWiring (n P : ℕ) (j : Fin (2 * n + 1 + P)) : Fin (n + P) ⊕ Bool

The substitution feeding a function of 2 n + 1 + P variables with frame x ++ r, from the variables x ++ r.

theorem Cslib.Circuits.Boolean.ofFn_substitute_frameWiring {n P : ℕ} (x : Fin n → Bool) (r : Fin P → Bool) : List.ofFn (substitute (frameWiring n P) (Fin.append x r)) = Turing.MultiTapeTM.frame (List.ofFn x) ++ List.ofFn r

Substituting Fin.append x r along frameWiring n P produces the word frame (List.ofFn x) ++ List.ofFn r.

noncomputable def Cslib.Circuits.Boolean.framedSlice (L : Language Bool) (n P : ℕ) : BooleanFunction (n + P)

The function of x ++ r that tests frame x ++ r ∈ L.

theorem Cslib.Circuits.Boolean.framedSlice_append_eq_true {L : Language Bool} {n P : ℕ} (x : Fin n → Bool) (r : Fin P → Bool) : framedSlice L n P (Fin.append x r) = true ↔ Turing.MultiTapeTM.frame (List.ofFn x) ++ List.ofFn r ∈ L

def Cslib.Circuits.Boolean.encodes {α : Type} (enc : α ↪ List Bool) (n : ℕ) : Set (Fin n → Bool)

The words of length n that encode an instance.

noncomputable def Cslib.Circuits.Boolean.encodesMember {α : Type} (enc : α ↪ List Bool) (A : Set α) (n : ℕ) : BooleanFunction n

Whether the word x encodes a member of A.

theorem Cslib.Circuits.Boolean.encodesMember_eq_true_iff {α : Type} {enc : α ↪ List Bool} {A : Set α} {n : ℕ} {x : Fin n → Bool} {a : α} (ha : enc a = List.ofFn x) : encodesMember enc A n x = true ↔ a ∈ A

On a word x encoding a, encodesMember enc A n x is true iff a ∈ A.

theorem Cslib.Circuits.Boolean.mem_iff_of_slice_eq_encodesMember {α : Type} {enc : α ↪ List Bool} {L : Language Bool} {A : Set α} (h : ∀ (n : ℕ), ∀ x ∈ encodes enc n, L.slice n x = encodesMember enc A n x) (a : α) : a ∈ A ↔ enc a ∈ L

A language agreeing with encodesMember enc A on encoded words contains exactly the encodings of the members of A.

theorem Cslib.Circuits.Boolean.verifier_eq_true_iff {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} {L : Language Bool} (hVL : ∀ (y : α × List Bool), V y = true ↔ (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) y ∈ L) {n : ℕ} {x : Fin n → Bool} {a : α} (ha : enc a = List.ofFn x) (r : List Bool) {P : ℕ} (r' : Fin P → Bool) (hr : r = List.ofFn r') : V (a, r) = true ↔ framedSlice L n P (Fin.append x r') = true

The verifier on an encoded instance, as the framed slice of the language deciding it.

theorem Cslib.Circuits.Boolean.BPP_subset_PPolyOn {α : Type} {enc : α ↪ List Bool} : Complexity.BPP enc ⊆ PPolyOn enc

BPP ⊆ P/poly. A problem in BPP, with any encoding enc of its instances, is the preimage under enc of a language in P/poly.

theorem Cslib.Circuits.Boolean.RP_subset_PPolyOn {α : Type} {enc : α ↪ List Bool} : Complexity.RP enc ⊆ PPolyOn enc

RP ⊆ P/poly. A problem in RP, with any encoding enc of its instances, is the preimage under enc of a language in P/poly.

theorem Cslib.Circuits.Boolean.coRP_subset_PPolyOn {α : Type} {enc : α ↪ List Bool} : Complexity.coRP enc ⊆ PPolyOn enc

coRP ⊆ P/poly. A problem in coRP, with any encoding enc of its instances, is the preimage under enc of a language in P/poly.