Documentation

Complexity.Computability.Circuit.Boolean.Formula.Poly

Formula-Size Complexity Classes (Formula[s] and Formula[poly]) #

A language over Bool lies in FormulaSIZE s (Formula[s] in Oliveira and Santhanam, Sections 1.2 and 3.1) when for every input length n, its n-bit slice (Language.slice) has a De Morgan formula of leaf size at most s n (Cslib.Circuits.Boolean.formulaSize) Jukna, Chapter 6. It lies in FormulaPoly (Formula[poly]) when the formula leaf size of its n-bit slice is polynomially bounded in n.

For decision problems over an arbitrary type α with encoding enc : α ↪ List Bool, FormulaSIZEOn enc s and FormulaPolyOn enc are the classes of problems whose image under enc agrees with a language in FormulaSIZE s or FormulaPoly, respectively, mirroring PPoly and PPolyOn (Complexity.Computability.Circuit.Boolean.PPoly).

Main definitions #

Main results #

References #

source
theorem Cslib.Circuits.Boolean.formulaSize_not_le {n : ℕ} (f : BooleanFunction n) :
(formulaSize fun (x : BitString n) => !f x) ≤ formulaSize f

Negating a Boolean function does not increase its De Morgan formula leaf size.

source
@[simp]
theorem Cslib.Circuits.Boolean.formulaSize_not {n : ℕ} (f : BooleanFunction n) :
(formulaSize fun (x : BitString n) => !f x) = formulaSize f

Negating a Boolean function preserves its De Morgan formula leaf size.

source
theorem Cslib.Circuits.Boolean.formulaSize_and_le {n : ℕ} (f g : BooleanFunction n) :
(formulaSize fun (x : BitString n) => f x && g x) ≤ formulaSize f + formulaSize g

The De Morgan formula leaf size of a conjunction is at most the sum of the leaf sizes of its conjuncts.

source
theorem Cslib.Circuits.Boolean.formulaSize_or_le {n : ℕ} (f g : BooleanFunction n) :
(formulaSize fun (x : BitString n) => f x || g x) ≤ formulaSize f + formulaSize g

The De Morgan formula leaf size of a disjunction is at most the sum of the leaf sizes of its disjuncts.

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

The languages over Bool that have, for every input length n, a De Morgan formula of leaf size at most s n (Formula[s] in [OliveiraSanthanam2018, Sections 1.2 and 3.1]).

Instances For
    source
    theorem Cslib.Circuits.Boolean.FormulaSIZE_mono :
    Monotone FormulaSIZE

    FormulaSIZE is monotone in the leaf-size bound.

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

    The languages over Bool whose slices have De Morgan formulas of polynomial leaf size (Formula[poly] in [OliveiraSanthanam2018, Sections 1.2 and 3.1]).

    Instances For
      source
      theorem Cslib.Circuits.Boolean.mem_FormulaPoly {L : Language Bool} :
      L ∈ FormulaPoly ↔ PolynomiallyBounded fun (n : ℕ) => formulaSize (L.slice n)

      A language is in FormulaPoly if and only if the formula leaf size of its slices is polynomially bounded.

      source
      theorem Cslib.Circuits.Boolean.mem_FormulaPoly_iff_exists_formulas {L : Language Bool} :
      L ∈ FormulaPoly ↔ ∃ (F : (n : ℕ) → Formula signature n) (p : ℕ → ℕ), PolynomiallyBounded p ∧ ∀ (n : ℕ), (F n).leafSize ≤ p n ∧ (F n).Computes interpretation (L.slice n)

      FormulaPoly with formula families. A language is in FormulaPoly exactly when it has a family of De Morgan formulas, one for each input length, whose leaf sizes are polynomially bounded.

      source
      theorem Cslib.Circuits.Boolean.mem_FormulaPoly_iff_exists_mem_FormulaSIZE {L : Language Bool} :
      L ∈ FormulaPoly ↔ ∃ (c : ℕ), L ∈ FormulaSIZE fun (n : ℕ) => c * (n + 1) ^ c

      FormulaPoly is the union of the classes FormulaSIZE (fun n => c * (n + 1) ^ c).

      source
      theorem Cslib.Circuits.Boolean.FormulaPoly.of_slice_const {L : Language Bool} (b : ℕ → Bool) (h : ∀ (n : ℕ) (x : Fin n → Bool), L.slice n x = b n) :
      L ∈ FormulaPoly

      A language whose slices are constant is in FormulaPoly.

      source
      theorem Cslib.Circuits.Boolean.FormulaPoly.zero_mem :
      0 ∈ FormulaPoly

      The empty language is in FormulaPoly.

      source
      theorem Cslib.Circuits.Boolean.FormulaPoly.top_mem :
      ⊤ ∈ FormulaPoly

      The universal language is in FormulaPoly.

      source
      theorem Cslib.Circuits.Boolean.FormulaPoly.compl {L : Language Bool} (hL : L ∈ FormulaPoly) :
      Lᶜ ∈ FormulaPoly

      FormulaPoly is closed under complement.

      source
      theorem Cslib.Circuits.Boolean.FormulaPoly.sup {L M : Language Bool} (hL : L ∈ FormulaPoly) (hM : M ∈ FormulaPoly) :
      L ⊔ M ∈ FormulaPoly

      FormulaPoly is closed under union.

      source
      theorem Cslib.Circuits.Boolean.FormulaPoly.inf {L M : Language Bool} (hL : L ∈ FormulaPoly) (hM : M ∈ FormulaPoly) :
      L ⊓ M ∈ FormulaPoly

      FormulaPoly is closed under intersection.

      source
      def Cslib.Circuits.Boolean.FormulaSIZEOn {α : Type u_1} (enc : α ↪ List Bool) (s : ℕ → ℕ) :
      Set (Set α)

      Problems with De Morgan formulas of leaf size s. A decision problem A : Set α, with encoding enc : α ↪ List Bool of its instances, lies in FormulaSIZEOn enc s when some language L ∈ FormulaSIZE s agrees with A along enc.

      Instances For
        source
        theorem Cslib.Circuits.Boolean.mem_FormulaSIZEOn {α : Type u_1} {enc : α ↪ List Bool} {s : ℕ → ℕ} {A : Set α} :
        A ∈ FormulaSIZEOn enc s ↔ ∃ L ∈ FormulaSIZE s, ∀ (a : α), a ∈ A ↔ enc a ∈ L

        Membership in FormulaSIZEOn enc s unfolds to agreement with a language in FormulaSIZE s.

        source
        @[simp]
        theorem Cslib.Circuits.Boolean.mem_FormulaSIZEOn_encBits_iff {s : ℕ → ℕ} {A : Language Bool} :
        A ∈ FormulaSIZEOn Turing.MultiTapeTM.encBits s ↔ A ∈ FormulaSIZE s

        Over bitstrings (encBits), membership in FormulaSIZEOn encBits s is membership in FormulaSIZE s.

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

        Problems with De Morgan formulas of polynomial leaf size. A decision problem A : Set α, with encoding enc : α ↪ List Bool of its instances, lies in FormulaPolyOn enc when some language L ∈ FormulaPoly agrees with A along enc.

        Instances For
          source
          theorem Cslib.Circuits.Boolean.mem_FormulaPolyOn {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} :
          A ∈ FormulaPolyOn enc ↔ ∃ L ∈ FormulaPoly, ∀ (a : α), a ∈ A ↔ enc a ∈ L

          A problem is in FormulaPolyOn enc if and only if some language in FormulaPoly agrees with it along enc.

          source
          theorem Cslib.Circuits.Boolean.mem_FormulaPolyOn_iff_exists_mem_FormulaSIZEOn {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} :
          A ∈ FormulaPolyOn enc ↔ ∃ (c : ℕ), A ∈ FormulaSIZEOn enc fun (n : ℕ) => c * (n + 1) ^ c

          FormulaPolyOn enc is the union of FormulaSIZEOn enc (fun n => c * (n + 1) ^ c).

          source
          @[simp]
          theorem Cslib.Circuits.Boolean.mem_FormulaPolyOn_encBits_iff {A : Language Bool} :
          A ∈ FormulaPolyOn Turing.MultiTapeTM.encBits ↔ A ∈ FormulaPoly

          Over bitstrings (encBits), membership in FormulaPolyOn encBits is membership in FormulaPoly.

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

          FormulaPolyOn is closed under complement.

          source
          @[simp]
          theorem Cslib.Circuits.Boolean.compl_mem_FormulaPolyOn_iff {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} :
          Aᶜ ∈ FormulaPolyOn enc ↔ A ∈ FormulaPolyOn enc

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