Polynomial advice

A machine takes advice when, on an input x of length n, it also reads a string α n that depends only on n Arora and Barak, Section 6.3. With the advice placed in front of the input as the pair (α |x|, x), encoded as frame (α |x|) ++ x, a language is in PAdvice when it consists of the inputs whose pair lies in a problem decidable in polynomial time, for advice of polynomial length. This is the class ⋃ DTIME(n ^ c) / n ^ d of Arora and Barak, Theorem 6.18, the original definition of P/poly Karp and Lipton.

Hardwiring the advice into circuits for the pairs gives circuits for the language: at each length n the first 2 |α n| + 1 inputs are fixed to the bits of frame (α n), which costs two gates for the constants (PPoly.of_advice). With P ⊆ P/poly (P_subset_PPolyOn), every language in PAdvice is in PPoly (PAdvice_subset_PPoly). The machine enters only through the hypothesis that the problem of pairs is in Complexity.P. Conversely, evaluating circuits from an advice string listing their certificates (familyAdvice, evalAdvice) in polynomial time (computableInPolyTime_evalAdvice) shows PPoly ⊆ PAdvice (PPoly_subset_PAdvice), establishing PPoly = PAdvice (PPoly_eq_PAdvice).

Main definitions

• Cslib.Circuits.Boolean.familyAdvice: the advice string listing circuits up to a given length.
• Cslib.Circuits.Boolean.evalAdvice: circuit evaluation from an advice string.
• Cslib.Circuits.Boolean.PAdvice: polynomial time with polynomial advice.

Main results

• Cslib.Circuits.Boolean.PPoly.of_advice: hardwiring advice of polynomial length into circuits of polynomial size.
• Cslib.Circuits.Boolean.PPoly.exists_evalAdvice: advice strings of polynomial length deciding a language in P/poly up to any polynomial input-length bound.
• Cslib.Circuits.Boolean.computableInPolyTime_evalAdvice, Cslib.Circuits.Boolean.computableInPolyTime_evalAdvice_eval: circuit evaluation from advice is polynomial-time, also with the polynomial bounds of PPoly.exists_evalAdvice.
• Cslib.Circuits.Boolean.PAdvice_subset_PPoly: P/advice ⊆ P/poly.
• Cslib.Circuits.Boolean.PPoly_subset_PAdvice: P/poly ⊆ P/advice.
• Cslib.Circuits.Boolean.PPoly_eq_PAdvice: P/poly = P/advice.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.3
• R. M. Karp, R. J. Lipton, Some connections between nonuniform and uniform complexity classes

theorem Cslib.Circuits.Boolean.PPoly.of_advice {L M : Language Bool} (hM : M ∈ PPoly) (α : ℕ → List Bool) (hα : PolynomiallyBounded fun (n : ℕ) => (α n).length) (h : ∀ (x : List Bool), x ∈ L ↔ Turing.MultiTapeTM.frame (α x.length) ++ x ∈ M) : L ∈ PPoly

Hardwiring advice. If x ∈ L exactly when frame (α |x|) ++ x ∈ M, with M in P/poly and advice α of polynomial length, then L is in P/poly: fixing the first inputs of the circuits for M to the bits of frame (α n) costs two gates.

Advice strings for circuit families

def Cslib.Circuits.Boolean.familyAdvice (N s : ℕ) (C : (m : ℕ) → Circuit signature m 1) : List Bool

The advice string listing the circuits C 0, …, C N, each with at most s gates: block m holds the certificate of C m (certificate), padded with false to certLength N s bits.

def Cslib.Circuits.Boolean.evalAdvice (s width : ℕ) (w x : List Bool) : Bool

The value on x of the circuit for inputs of length x.length, read with at most s gates from the block at position x.length of an advice string w whose blocks have width bits. Every advice string gives a value.

theorem Cslib.Circuits.Boolean.length_familyAdvice {N s : ℕ} {C : (m : ℕ) → Circuit signature m 1} (hs : ∀ m ≤ N, (C m).size ≤ s) : (familyAdvice N s C).length = (N + 1) * certLength N s

The advice string of circuits with at most s gates has N + 1 blocks of certLength N s bits.

theorem Cslib.Circuits.Boolean.evalAdvice_familyAdvice {N s : ℕ} {C : (m : ℕ) → Circuit signature m 1} (hs : ∀ m ≤ N, (C m).size ≤ s) {x : List Bool} (hx : x.length ≤ N) : evalAdvice s (certLength N s) (familyAdvice N s C) x = (C x.length).eval interpretation (fun (i : Fin x.length) => x[i]) 0

Evaluation from the advice string of a family is evaluation of its circuits, on inputs of length at most N.

theorem Cslib.Circuits.Boolean.computableInPolyTime_evalAdvice {γ : Type} {encIn : γ ↪ List Bool} {s width : γ → ℕ} {w x : γ → List Bool} (hs : Turing.MultiTapeTM.ComputableInPolyTime s encIn Turing.MultiTapeTM.encUnary) (hwidth : Turing.MultiTapeTM.ComputableInPolyTime width encIn Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w encIn Turing.MultiTapeTM.encBits) (hx : Turing.MultiTapeTM.ComputableInPolyTime x encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => evalAdvice (s a) (width a) (w a) (x a)) encIn Turing.MultiTapeTM.encBool

Evaluation from advice strings is polynomial-time, for the number of gates and the block width in unary.

theorem Cslib.Circuits.Boolean.computableInPolyTime_evalAdvice_eval {γ : Type} {encIn : γ ↪ List Bool} (S W : Polynomial ℕ) {n : γ → ℕ} {w x : γ → List Bool} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w encIn Turing.MultiTapeTM.encBits) (hx : Turing.MultiTapeTM.ComputableInPolyTime x encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => evalAdvice (Polynomial.eval (n a) S) (Polynomial.eval (n a) W) (w a) (x a)) encIn Turing.MultiTapeTM.encBool

Evaluation from advice is polynomial-time with S.eval n gates in blocks of W.eval n bits, for polynomials S and W of a length n in unary, the bounds of PPoly.exists_evalAdvice.

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

Polynomial time with polynomial advice Arora and Barak, Section 6.3: the languages L with advice α of polynomial length and a problem A of pairs, decidable in polynomial time for the encoding frame u ++ x of (u, x), such that x ∈ L exactly when (α |x|, x) ∈ A.

theorem Cslib.Circuits.Boolean.PAdvice_subset_PPoly : PAdvice ⊆ PPoly

P/advice ⊆ P/poly Arora and Barak, Theorem 6.18: a language decided in polynomial time with polynomial advice has circuits of polynomial size.

theorem Cslib.Circuits.Boolean.PPoly.exists_evalAdvice {L : Language Bool} (hL : L ∈ PPoly) (N : Polynomial ℕ) : ∃ (S : Polynomial ℕ) (W : Polynomial ℕ) (P : Polynomial ℕ) (α : ℕ → List Bool), (∀ (n : ℕ), (α n).length = Polynomial.eval n P) ∧ (PolynomiallyBounded fun (n : ℕ) => (α n).length) ∧ ∀ (n : ℕ) (x : List Bool), x.length ≤ Polynomial.eval n N → (evalAdvice (Polynomial.eval n S) (Polynomial.eval n W) (α n) x = true ↔ x ∈ L)

Advice strings for P/poly up to a polynomial length bound. For any language L ∈ P/poly and polynomial N : Polynomial ℕ, there exist polynomials S W P : Polynomial ℕ (for the circuit size bound, block width, and total advice length) and an advice family α : ℕ → List Bool of polynomial length (α n).length = P.eval n such that evalAdvice (S.eval n) (W.eval n) (α n) x decides x ∈ L for every n and every word x of length at most N.eval n.

theorem Cslib.Circuits.Boolean.PPoly_subset_PAdvice : PPoly ⊆ PAdvice

P/poly ⊆ P/advice Arora and Barak, Theorem 6.18: a language decided in polynomial size has polynomial advice.

theorem Cslib.Circuits.Boolean.PPoly_eq_PAdvice : PPoly = PAdvice

P/poly = P/advice Arora and Barak, Theorem 6.18: the circuit class P/poly equals the advice class P/advice.