Documentation

Complexity.Computability.Circuit.Boolean.Threshold.Parity

Parity in depth two with threshold gates #

Every symmetric function has threshold circuits of depth two and linear size Hajnal et al., Proposition 2.1. For parity, alternating signs give such a circuit with n + 1 threshold gates. On n bits, let g_j, for j < n, be the threshold gate "at least j + 1 of the bits are true". If w of the bits are true, g_j is true exactly when j < w. Negating g_j for every odd j, exactly n / 2 + w % 2 of the n signed values are true (Threshold.weight_signedLayer), so the threshold gate "at least n / 2 + 1 of them are true" computes the parity of w.

This circuit (Threshold.parityCircuit) has n + 1 threshold gates and threshold depth two, the n / 2 negations being free; with them it has n + n / 2 + 1 gates and depth three (Threshold.exists_computes_parity). So parity has threshold circuits of polynomial size and constant depth (Threshold.parity_mem_constDepth), and is in TC⁰ (Cslib.Circuits.Boolean.parity_mem_TC0).

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Boolean.Threshold.negIf :
Bool → Circuit signature 1 1

A negation if b is true, and no gate otherwise.

Instances For
    source
    @[simp]
    theorem Cslib.Circuits.Boolean.Threshold.eval_negIf (b : Bool) (y : Fin 1 → Bool) (o : Fin 1) :
    (negIf b).eval interpretation y o = (b ^^ y 0)
    source
    theorem Cslib.Circuits.Boolean.Threshold.cost_program_negIf (b : Bool) :
    (negIf b).program.cost thresholdCost = 0
    source
    @[simp]
    theorem Cslib.Circuits.Boolean.Threshold.size_negIf (b : Bool) :
    (negIf b).size = b.toNat
    source
    @[simp]
    theorem Cslib.Circuits.Boolean.Threshold.depthWith_negIf (b : Bool) :
    Circuit.depthWith thresholdCost (negIf b) = 0
    source
    theorem Cslib.Circuits.Boolean.Threshold.depth_negIf_le (b : Bool) :
    (negIf b).depth ≤ 1
    source
    def Cslib.Circuits.Boolean.Threshold.signedLayerGate (n : ℕ) (j : Fin n) :
    Circuit signature n 1

    The j-th input of the output gate of parityCircuit n: the threshold gate "at least j + 1 of the n bits are true", negated when j is odd.

    Instances For
      source
      def Cslib.Circuits.Boolean.Threshold.parityCircuit (n : ℕ) :
      Circuit signature n 1

      The depth-two threshold circuit for parity: the threshold gate "at least n / 2 + 1 of them are true" on the signed layer gates signedLayerGate n j.

      Instances For
        source
        theorem Cslib.Circuits.Boolean.Threshold.eval_signedLayerGate {n : ℕ} (j : Fin n) (x : BitString n) :
        (signedLayerGate n j).eval interpretation x 0 = (decide (↑j % 2 = 1) ^^ threshold n (↑j + 1) x)
        source
        theorem Cslib.Circuits.Boolean.Threshold.weight_signedLayer {n : ℕ} (x : BitString n) :
        (BitString.weight fun (j : Fin n) => decide (↑j % 2 = 1) ^^ threshold n (↑j + 1) x) = n / 2 + BitString.weight x % 2

        If w of the bits are true, exactly n / 2 + w % 2 of the signed layer values are true.

        source
        theorem Cslib.Circuits.Boolean.Threshold.computes_parityCircuit {n : ℕ} :
        (parityCircuit n).Computes interpretation (single (parity n))

        The circuit computes parity.

        source
        theorem Cslib.Circuits.Boolean.Threshold.cost_parityCircuit {n : ℕ} :
        (parityCircuit n).program.cost thresholdCost = n + 1

        The circuit has n + 1 threshold gates.

        source
        theorem Cslib.Circuits.Boolean.Threshold.size_parityCircuit {n : ℕ} :
        (parityCircuit n).size = n + n / 2 + 1

        The circuit has n + 1 threshold gates and n / 2 negations.

        source
        theorem Cslib.Circuits.Boolean.Threshold.depthWith_parityCircuit_le {n : ℕ} :
        Circuit.depthWith thresholdCost (parityCircuit n) ≤ 2

        The circuit has threshold depth two: negations are free.

        source
        theorem Cslib.Circuits.Boolean.Threshold.depth_parityCircuit_le {n : ℕ} :
        (parityCircuit n).depth ≤ 3

        The circuit has depth three, counting the negations.

        source
        theorem Cslib.Circuits.Boolean.Threshold.exists_computes_parity (n : ℕ) :
        ∃ (C : Circuit signature n 1), C.Computes interpretation (single (parity n)) ∧ C.program.cost thresholdCost = n + 1 ∧ Circuit.depthWith thresholdCost C ≤ 2 ∧ C.size = n + n / 2 + 1 ∧ C.depth ≤ 3

        Parity in depth two: the parity of n bits has a circuit of n + 1 threshold gates and threshold depth two, with n / 2 negations, so of n + n / 2 + 1 gates and depth three in all. Every symmetric function has threshold circuits of depth two and linear size Hajnal et al., Proposition 2.1.

        source
        theorem Cslib.Circuits.Boolean.Threshold.parity_mem_constDepth :
        Language.ofSlices parity ∈ ConstDepth interpretation

        Parity has threshold circuits of polynomial size and constant depth.