Documentation

Complexity.Computability.Circuit.Boolean.AtLeast

Threshold functions by De Morgan circuits of quadratic size #

Given Boolean functions f 0, f 1, … that are already available, the functions "at least j of f 0, …, f (i - 1) are true" satisfy the recursion

atLeast (i + 1) (j + 1) = atLeast i (j + 1) ∨ (f i ∧ atLeast i j),

so all of them for i, j ≤ k are synthesised with O(k ^ 2) gates over the De Morgan basis. In particular every threshold function, and the majority, of k available functions has a circuit of size O(k ^ 2) on top of them.

Main definitions #

Main results #

source
def Cslib.Circuits.Boolean.atLeast {n : ℕ} (f : ℕ → BooleanFunction n) (i j : ℕ) :
BooleanFunction n

atLeast f i j x: at least j of f 0 x, …, f (i - 1) x are true.

Instances For
    source
    @[simp]
    theorem Cslib.Circuits.Boolean.atLeast_zero_right {n : ℕ} (f : ℕ → BooleanFunction n) (i : ℕ) :
    atLeast f i 0 = fun (x : BitString n) => true
    source
    theorem Cslib.Circuits.Boolean.atLeast_zero_succ {n : ℕ} (f : ℕ → BooleanFunction n) (j : ℕ) :
    atLeast f 0 (j + 1) = fun (x : BitString n) => false
    source
    theorem Cslib.Circuits.Boolean.atLeast_succ_succ {n : ℕ} (f : ℕ → BooleanFunction n) (i j : ℕ) (x : Fin n → Bool) :
    atLeast f (i + 1) (j + 1) x = (atLeast f i (j + 1) x || f i x && atLeast f i j x)

    The counting recursion.

    source
    def Cslib.Circuits.Boolean.atLeastUpTo {n : ℕ} (f : ℕ → BooleanFunction n) (k i : ℕ) :
    Set (BooleanFunction n)

    The counting functions of levels 0, …, i.

    Instances For
      source
      theorem Cslib.Circuits.Boolean.synthesis_atLeastUpTo {n : ℕ} (f : ℕ → BooleanFunction n) {s : Set (BooleanFunction n)} (k : ℕ) (hf : ∀ i < k, f i ∈ s) (i : ℕ) :
      i ≤ k → Synthesis interpretation s (atLeastUpTo f k i) (2 + i * (2 * (k + 2)))

      All counting functions of levels 0, …, i ≤ k, if f 0, …, f (k - 1) are available in s: two constants, and two gates for each pair (i', j) with 0 < i' ≤ i and j ≤ k + 1.

      source
      theorem Cslib.Circuits.Boolean.synthesis_atLeast {n : ℕ} (f : ℕ → BooleanFunction n) {s : Set (BooleanFunction n)} {k j : ℕ} (hf : ∀ i < k, f i ∈ s) (hj : j ≤ k + 1) :
      Synthesis interpretation s {atLeast f k j} (2 + k * (2 * (k + 2)))

      The threshold function "at least j of f 0, …, f (k - 1) are true", for j ≤ k + 1, on top of available functions, within O(k ^ 2) gates.

      source
      theorem Cslib.Circuits.Boolean.atLeast_eq_threshold (m j : ℕ) :
      atLeast (fun (l : ℕ) (y : BitString m) => if h : l < m then y ⟨l, h⟩ else false) m j = threshold m j
      source
      theorem Cslib.Circuits.Boolean.complexity_threshold_le (m j : ℕ) :
      complexity interpretation (single (threshold m j)) ≤ 2 + m * (2 * (m + 2))

      The threshold functions on m variables have circuits with O(m ^ 2) gates.