Documentation

Complexity.Computability.Complexity.Classes.Promise.Circuit

Promise problems solved by circuits #

PromiseSIZE s and PromisePPoly lift the circuit classes SIZE s and P/poly (Cslib.Circuits.Boolean.SIZE, Cslib.Circuits.Boolean.PPoly) to promise problems over words (Cslib.Complexity.promiseClass). A family of circuits, one for each input length, solves a promise problem when the circuit for each length gives the right answer on the promised words of that length; what it computes on the other words does not matter. The lifted classes consist exactly of the promise problems solved by circuit families of the given size (mem_PromiseSIZE_iff, mem_PromisePPoly_iff).

Main definitions #

Main results #

References #

source
def Cslib.Complexity.PromiseSIZE (s : ℕ → ℕ) :
Set (PromiseProblem (List Bool))

The promise problems over words solved by circuits of size at most s n on the inputs of length n: the lift of SIZE s.

Instances For
    source
    def Cslib.Complexity.PromisePPoly :
    Set (PromiseProblem (List Bool))

    The promise problems over words solved by circuits of polynomial size: the lift of P/poly.

    Instances For
      source
      theorem Cslib.Complexity.mem_PromiseSIZE_iff {Q : PromiseProblem (List Bool)} {s : ℕ → ℕ} :
      Q ∈ PromiseSIZE s ↔ ∃ (C : (n : ℕ) → Circuits.Circuit Circuits.Boolean.signature n 1), (∀ (n : ℕ), (C n).size ≤ s n) ∧ Q.SolvedBy fun (w : List Bool) => (C w.length).eval Circuits.Boolean.interpretation (fun (x : Fin w.length) => w[x]) 0

      Promise SIZE is solvability by circuits on the promise. A promise problem is in PromiseSIZE s exactly when a family of circuits of size at most s n on inputs of length n answers correctly on every promised word.

      source
      theorem Cslib.Complexity.mem_PromisePPoly_iff {Q : PromiseProblem (List Bool)} :
      Q ∈ PromisePPoly ↔ ∃ (C : (n : ℕ) → Circuits.Circuit Circuits.Boolean.signature n 1) (p : ℕ → ℕ), PolynomiallyBounded p ∧ (∀ (n : ℕ), (C n).size ≤ p n) ∧ Q.SolvedBy fun (w : List Bool) => (C w.length).eval Circuits.Boolean.interpretation (fun (x : Fin w.length) => w[x]) 0

      Promise P/poly is solvability by polynomial-size circuits on the promise. A promise problem is in PromisePPoly exactly when a family of circuits of polynomial size answers correctly on every promised word.

      source
      @[simp]
      theorem Cslib.Complexity.ofSet_mem_PromiseSIZE {L : Language Bool} {s : ℕ → ℕ} :
      PromiseProblem.ofSet L ∈ PromiseSIZE s ↔ L ∈ Circuits.Boolean.SIZE s

      A language is in the lift of SIZE s exactly when it is in SIZE s.

      source
      @[simp]
      theorem Cslib.Complexity.ofSet_mem_PromisePPoly {L : Language Bool} :
      PromiseProblem.ofSet L ∈ PromisePPoly ↔ L ∈ Circuits.Boolean.PPoly

      A language is in the lift of P/poly exactly when it is in P/poly.