Documentation

Cslib.Computability.Circuit.Boolean.Family

Size classes of De Morgan circuit families #

SIZE s is the class of languages decided by De Morgan circuit families with at most s n gates on n inputs, following [Arora and Barak, Definition 6.1][AroraBarak09], and PPoly is the class P/poly of languages decided by such families of polynomial size, following their Definition 6.5. The bound in P/poly is n ^ k + k rather than n ^ k because of the slice at length 0: a circuit with no inputs has no wire to designate as its output until it has a gate, so that slice costs at least one constant gate, which 0 ^ k does not allow when k > 0.

Lupanov's and Shannon's bounds carry over to families: every language has a family with at most (1 + ε) 2ⁿ/n gates at all large lengths, while some language defeats every family with at most 2ⁿ/n gates at all large lengths and so lies outside P/poly. Since the circuits of a family need not be related, P/poly also contains every unary language, including languages that no Turing machine decides.

References #

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

SIZE(s): the languages decided by De Morgan circuit families with at most s n gates on n inputs.

Equations
Instances For
    source
    theorem Cslib.Circuits.Boolean.mem_SIZE_iff {L : Language Bool} {s : ℕ → ℕ} :
    L ∈ SIZE s ↔ DecidableInSize L interpretation id s
    source
    theorem Cslib.Circuits.Boolean.SIZE_mono :
    Monotone SIZE
    source
    theorem Cslib.Circuits.Boolean.mem_SIZE_iff_complexity_le {L : Language Bool} {s : ℕ → ℕ} :
    L ∈ SIZE s ↔ ∀ (n : ℕ), (complexity interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => L.slice n x) ≤ s n

    A language is in SIZE s exactly when every slice has complexity at most the bound.

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

    P/poly: the languages decided by De Morgan circuit families of polynomial size.

    Equations
    Instances For
      source
      theorem Cslib.Circuits.Boolean.mem_PPoly_iff {L : Language Bool} :
      L ∈ PPoly ↔ ∃ (k : ℕ), L ∈ SIZE fun (n : ℕ) => n ^ k + k
      source
      theorem Cslib.Circuits.Boolean.SIZE_subset_PPoly (k : ℕ) :
      (SIZE fun (n : ℕ) => n ^ k + k) ⊆ PPoly
      source
      theorem Cslib.Circuits.Boolean.mem_PPoly_of_le {L : Language Bool} {s : ℕ → ℕ} (hL : L ∈ SIZE s) (c k d : ℕ) (h : ∀ (n : ℕ), s n ≤ c * n ^ k + d) :
      L ∈ PPoly

      The bounds n ^ k + k are cofinal among polynomials, so a language decided within any polynomial bound is in P/poly.

      source
      theorem Cslib.Circuits.Boolean.exists_decides_size_le (ε : ℝ) (hε : 0 < ε) :
      ∃ (N : ℕ), ∀ (L : Language Bool), ∃ (F : CircuitFamily signature), F.Decides interpretation id L ∧ ∀ n ≥ N, ↑(F n).size ≤ (1 + ε) * 2 ^ n / ↑n

      Lupanov's bound for families: for every ε > 0 there is a length beyond which every language is decided by a family with at most (1 + ε) 2ⁿ/n gates per circuit.

      source
      theorem Cslib.Circuits.Boolean.exists_language_lt_size :
      ∃ (L : Language Bool) (N : ℕ), ∀ (F : CircuitFamily signature), F.Decides interpretation id L → ∀ n ≥ N, 2 ^ n / ↑n < ↑(F n).size

      Shannon's bound for families: some language defeats, at all large lengths, every family with at most 2ⁿ/n gates per circuit.

      source
      theorem Cslib.Circuits.Boolean.exists_not_mem_PPoly :
      ∃ (L : Language Bool), L ∉ PPoly

      Some language is not in P/poly.

      source
      theorem Cslib.Circuits.Boolean.mem_SIZE_of_unary {L : Language Bool} (hL : ∀ w ∈ L, ∀ b ∈ w, b = true) :
      L ∈ SIZE fun (n : ℕ) => n + 1

      A unary language, whose words consist only of trues, is decided by a family with at most n + 1 gates on n inputs: a constant when the word of length n is not in the language, and otherwise a conjunction of the inputs, whose extra gate supplies the empty conjunction.

      source
      theorem Cslib.Circuits.Boolean.mem_PPoly_of_unary {L : Language Bool} (hL : ∀ w ∈ L, ∀ b ∈ w, b = true) :
      L ∈ PPoly

      Every unary language is in P/poly.