Documentation

Complexity.Computability.Circuit.Boolean.Parity

Circuits for parity #

Chaining x ⊕ y = (x ∨ y) ∧ ¬(x ∧ y) computes the parity of n + 1 bits with 4 n De Morgan gates, 3 n of them AND or OR gates (exists_computes_parity) Jukna, Section 1.6. The number of binary gates is optimal by Schnorr's bound, Cslib.Circuits.Boolean.three_mul_le_cost_of_computes_parity.

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Program.appendXor {n g : ℕ} (p : Program Boolean.signature n g) (u v : Wire n g) :
Program Boolean.signature n (g + 4)

Append u ⊕ v = (u ∨ v) ∧ ¬(u ∧ v) to a De Morgan program: four gates, three of them binary, the last of which computes the exclusive or of the wires u and v.

Instances For
    source
    theorem Cslib.Circuits.Program.trace_appendXor {n g : ℕ} (p : Program Boolean.signature n g) (u v : Wire n g) (x : BitString n) :
    (p.appendXor u v).trace Boolean.interpretation x (Wire.gate (Fin.last (g + 3))) = (p.trace Boolean.interpretation x u ^^ p.trace Boolean.interpretation x v)
    source
    @[simp]
    theorem Cslib.Circuits.Program.cost_appendXor {n g : ℕ} (p : Program Boolean.signature n g) (u v : Wire n g) :
    (p.appendXor u v).cost Boolean.binaryCost = p.cost Boolean.binaryCost + 3
    source
    def Cslib.Circuits.Boolean.parityProgram {n : ℕ} (k : ℕ) :
    k < n → Program signature n (4 * k) × Wire n (4 * k)

    A De Morgan program computing the parity of the bits 0, …, k, and its output wire: 4 k gates, 3 k of them binary.

    Instances For
      source
      theorem Cslib.Circuits.Boolean.trace_parityProgram {n : ℕ} (k : ℕ) (hk : k < n) (x : BitString n) :
      (parityProgram k hk).1.trace interpretation x (parityProgram k hk).2 = parityOn (Finset.Iic ⟨k, hk⟩) x
      source
      theorem Cslib.Circuits.Boolean.cost_parityProgram {n : ℕ} (k : ℕ) (hk : k < n) :
      (parityProgram k hk).1.cost binaryCost = 3 * k
      source
      theorem Cslib.Circuits.Boolean.exists_computes_parity (n : ℕ) :
      ∃ (C : Circuit signature (n + 1) 1), C.Computes interpretation (single (parity (n + 1))) ∧ C.program.cost binaryCost = 3 * n ∧ C.size = 4 * n

      Parity has circuits with 3 n binary gates. The parity of n + 1 bits has a De Morgan circuit with 3 n AND and OR gates, which matches Schnorr's lower bound, and 4 n gates in all.

      source
      theorem Cslib.Circuits.Boolean.exists_computes_parity_zero :
      ∃ (C : Circuit signature 0 1), C.Computes interpretation (single (parity 0)) ∧ C.program.cost binaryCost = 0

      The parity of no bits is computed by one constant gate, which is not binary.

      source
      theorem Cslib.Circuits.Boolean.complexity_parity_le (n : ℕ) :
      complexity interpretation (single (parity (n + 1))) ≤ 4 * n

      The circuit complexity of the parity of n + 1 bits is at most 4 n.