Threshold and majority circuits in NC¹

Combining the logarithmic-depth carry-save Hamming weight circuit (weightCircuit) with the comparator (leCircuit) yields a fan-in-two De Morgan circuit thresholdDeMorganCircuit k j computing the k-bit threshold function threshold k j in size O(k log k) and depth O(log k) (computes_thresholdDeMorganCircuit, size_thresholdDeMorganCircuit_le, depth_thresholdDeMorganCircuit_le) Chandra et al., Vollmer, Chapter 4. Specializing to cutoff ⌈k / 2⌉ gives a De Morgan circuit majorityDeMorganCircuit k for majority k.

Consequently, any threshold slice family fun n => threshold n (t n) lies in NC¹ (threshold_mem_NC_one), and in particular MAJ ∈ NC¹ (majority_mem_NC_one) and strictMajority ∈ NC¹ (strictMajority_mem_NC_one). Replacing each gate of a fan-in-bounded threshold or majority circuit by thresholdDeMorganCircuit simulates depth d and fan-in F in De Morgan depth O(d log F) and size O(s F log F) (Threshold.exists_deMorgan_simulation_of_fanInAtMost, Unbounded.exists_deMorgan_simulation_majority_of_fanInAtMost).

Main definitions

• Cslib.Circuits.Boolean.wordConstCircuit: a constant w-bit word circuit of size 2 and depth at most 1.
• Cslib.Circuits.Boolean.thresholdDeMorganCircuit: a De Morgan circuit of size O(k log k) and depth O(log k) computing threshold k j.
• Cslib.Circuits.Boolean.majorityDeMorganCircuit: a De Morgan circuit of size O(k log k) and depth O(log k) computing majority k.
• Cslib.Circuits.Boolean.Threshold.Op.deMorganCircuit: a De Morgan circuit for each operation of the threshold basis.

Main results

• Cslib.Circuits.Boolean.computes_thresholdDeMorganCircuit, size_thresholdDeMorganCircuit_le, depth_thresholdDeMorganCircuit_le.
• Cslib.Circuits.Boolean.computes_majorityDeMorganCircuit, size_majorityDeMorganCircuit_le, depth_majorityDeMorganCircuit_le.
• Cslib.Circuits.Boolean.threshold_mem_NC_one, majority_mem_NC_one, strictMajority_mem_NC_one.
• Cslib.Circuits.Boolean.Threshold.exists_deMorgan_simulation_of_fanInAtMost, Cslib.Circuits.Boolean.Unbounded.exists_deMorgan_simulation_majority_of_fanInAtMost.
• Cslib.Circuits.Boolean.mem_NC_succ_of_threshold_fanInAtMost, Cslib.Circuits.Boolean.mem_NC_succ_of_majority_fanInAtMost.

References

• [A. K. Chandra, L. Stockmeyer, U. Vishkin, Constant depth reducibility] [CSV84]
• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• H. Vollmer, Introduction to Circuit Complexity

Constant word circuit

def Cslib.Circuits.Boolean.wordConstCircuit {w : ℕ} (n : ℕ) (y : BitString w) : Circuit signature n w

Constant w-bit word circuit on n inputs: computes false and true once and wires each output bit i to the corresponding constant gate.

@[simp]

theorem Cslib.Circuits.Boolean.eval_wordConstCircuit {n w : ℕ} (y : BitString w) (x : BitString n) : (wordConstCircuit n y).eval interpretation x = y

@[simp]

theorem Cslib.Circuits.Boolean.size_wordConstCircuit {w : ℕ} (n : ℕ) (y : BitString w) : (wordConstCircuit n y).size = 2

theorem Cslib.Circuits.Boolean.depth_wordConstCircuit_le {w : ℕ} (n : ℕ) (y : BitString w) : (wordConstCircuit n y).depth ≤ 1

Threshold and majority circuits in NC¹

def Cslib.Circuits.Boolean.thresholdDeMorganCircuit (k j : ℕ) : Circuit signature k 1

Logarithmic-depth threshold circuit: computes threshold k j over the De Morgan basis of fan-in two by computing the ⌈log₂ (k + 1)⌉-bit binary numeral of the input's Hamming weight (weightCircuit k) and comparing it against j (leCircuit). When k < j, the threshold cannot be met and a single false gate is used.

theorem Cslib.Circuits.Boolean.computes_thresholdDeMorganCircuit (k j : ℕ) : (thresholdDeMorganCircuit k j).Computes interpretation (single (threshold k j))

thresholdDeMorganCircuit k j computes threshold k j.

@[simp]

theorem Cslib.Circuits.Boolean.eval_thresholdDeMorganCircuit (k j : ℕ) (x : BitString k) : (thresholdDeMorganCircuit k j).eval interpretation x = single (threshold k j) x

theorem Cslib.Circuits.Boolean.size_thresholdDeMorganCircuit_le (k j : ℕ) : (thresholdDeMorganCircuit k j).size ≤ 4 + k + 40 * k * Nat.clog 2 (k + 1) + Nat.clog 2 (k + 1) * (20 * Nat.clog 2 (k + 1) + 6)

thresholdDeMorganCircuit k j uses O(k log k) gates.

theorem Cslib.Circuits.Boolean.depth_thresholdDeMorganCircuit_le (k j : ℕ) : (thresholdDeMorganCircuit k j).depth ≤ 2 + 23 * Nat.clog 2 (k + 1)

thresholdDeMorganCircuit k j has depth at most 2 + 23 ⌈log₂ (k + 1)⌉.

def Cslib.Circuits.Boolean.majorityDeMorganCircuit (k : ℕ) : Circuit signature k 1

Logarithmic-depth majority circuit: computes majority k over the De Morgan basis of fan-in two in size O(k log k) and depth O(log k).

theorem Cslib.Circuits.Boolean.computes_majorityDeMorganCircuit (k : ℕ) : (majorityDeMorganCircuit k).Computes interpretation (single (majority k))

majorityDeMorganCircuit k computes majority k.

@[simp]

theorem Cslib.Circuits.Boolean.eval_majorityDeMorganCircuit (k : ℕ) (x : BitString k) : (majorityDeMorganCircuit k).eval interpretation x = single (majority k) x

theorem Cslib.Circuits.Boolean.size_majorityDeMorganCircuit_le (k : ℕ) : (majorityDeMorganCircuit k).size ≤ 4 + k + 40 * k * Nat.clog 2 (k + 1) + Nat.clog 2 (k + 1) * (20 * Nat.clog 2 (k + 1) + 6)

majorityDeMorganCircuit k uses O(k log k) gates.

theorem Cslib.Circuits.Boolean.size_majorityDeMorganCircuit_le_sq (k : ℕ) : (majorityDeMorganCircuit k).size ≤ 65 * (k + 1) ^ 2

Quadratic upper bound on the size of majorityDeMorganCircuit k.

theorem Cslib.Circuits.Boolean.depth_majorityDeMorganCircuit_le (k : ℕ) : (majorityDeMorganCircuit k).depth ≤ 2 + 23 * Nat.clog 2 (k + 1)

majorityDeMorganCircuit k has depth at most 2 + 23 ⌈log₂ (k + 1)⌉.

theorem Cslib.Circuits.Boolean.threshold_mem_NC_one (t : ℕ → ℕ) : (Language.ofSlices fun (n : ℕ) => threshold n (t n)) ∈ NC 1

Every family of threshold functions fun n => threshold n (t n) belongs to NC¹.

theorem Cslib.Circuits.Boolean.majority_mem_NC_one : Language.ofSlices majority ∈ NC 1

Majority is in NC¹.

theorem Cslib.Circuits.Boolean.strictMajority_mem_NC_one : Language.ofSlices strictMajority ∈ NC 1

Strict majority is in NC¹.

Simulating fan-in-bounded threshold and majority circuits

def Cslib.Circuits.Boolean.Threshold.Op.deMorganCircuit (op : Op) : Circuit Boolean.signature op.arity 1

A De Morgan circuit of fan-in two for each operation of the threshold basis: one negation gate for .not, and thresholdDeMorganCircuit m j for .threshold m j.

theorem Cslib.Circuits.Boolean.Threshold.Op.computes_deMorganCircuit (op : Op) : op.deMorganCircuit.Computes Boolean.interpretation (single (interpretation op))

The De Morgan circuit of a threshold operation computes it.

theorem Cslib.Circuits.Boolean.Threshold.Op.size_deMorganCircuit_le (op : Op) : op.deMorganCircuit.size ≤ 4 + op.arity + 40 * op.arity * Nat.clog 2 (op.arity + 1) + Nat.clog 2 (op.arity + 1) * (20 * Nat.clog 2 (op.arity + 1) + 6)

The De Morgan circuit of a threshold operation of arity k uses O(k log k) gates.

theorem Cslib.Circuits.Boolean.Threshold.Op.depth_deMorganCircuit_le (op : Op) : op.deMorganCircuit.depth ≤ 2 + 23 * Nat.clog 2 (op.arity + 1)

The De Morgan circuit of a threshold operation of arity k has depth at most 2 + 23 ⌈log₂ (k + 1)⌉.

theorem Cslib.Circuits.Boolean.Threshold.exists_deMorgan_simulation_of_fanInAtMost {n m F : ℕ} (C : Circuit signature n m) (hF : C.FanInAtMost F) : ∃ (D : Circuit Boolean.signature n m), D.eval Boolean.interpretation = C.eval interpretation ∧ D.size ≤ C.size * (4 + F + 40 * F * Nat.clog 2 (F + 1) + Nat.clog 2 (F + 1) * (20 * Nat.clog 2 (F + 1) + 6)) ∧ D.depth ≤ (2 + 23 * Nat.clog 2 (F + 1)) * C.depth

De Morgan circuits simulate fan-in-bounded threshold circuits: a circuit over the threshold basis of n inputs, s gates, depth d, and fan-in at most F has an equivalent De Morgan circuit of fan-in two with at most s (4 + F + 40 F ⌈log₂ (F + 1)⌉ + ⌈log₂ (F + 1)⌉ (20 ⌈log₂ (F + 1)⌉ + 6)) gates and depth at most (2 + 23 ⌈log₂ (F + 1)⌉) d.

def Cslib.Circuits.Boolean.Unbounded.ExtOp.majorityDeMorganCircuit (op : ExtOp) : Circuit Boolean.signature op.arity 1

A De Morgan circuit of fan-in two for each operation of the TC basis: balanced trees for the unbounded fan-in operations, and majorityDeMorganCircuit m for .gate m.

theorem Cslib.Circuits.Boolean.Unbounded.ExtOp.computes_majorityDeMorganCircuit (op : ExtOp) : op.majorityDeMorganCircuit.Computes Boolean.interpretation (single (extInterpretation majority op))

The De Morgan circuit of a TC operation computes it.

theorem Cslib.Circuits.Boolean.Unbounded.ExtOp.size_majorityDeMorganCircuit_le (op : ExtOp) : op.majorityDeMorganCircuit.size ≤ 4 + op.arity + 40 * op.arity * Nat.clog 2 (op.arity + 1) + Nat.clog 2 (op.arity + 1) * (20 * Nat.clog 2 (op.arity + 1) + 6)

The De Morgan circuit of a TC operation of arity k uses O(k log k) gates.

theorem Cslib.Circuits.Boolean.Unbounded.ExtOp.depth_majorityDeMorganCircuit_le (op : ExtOp) : op.majorityDeMorganCircuit.depth ≤ 2 + 23 * Nat.clog 2 (op.arity + 1)

The De Morgan circuit of a TC operation of arity k has depth at most 2 + 23 ⌈log₂ (k + 1)⌉.

theorem Cslib.Circuits.Boolean.Unbounded.exists_deMorgan_simulation_majority_of_fanInAtMost {n m F : ℕ} (C : Circuit extSignature n m) (hF : C.FanInAtMost F) : ∃ (D : Circuit Boolean.signature n m), D.eval Boolean.interpretation = C.eval (extInterpretation majority) ∧ D.size ≤ C.size * (4 + F + 40 * F * Nat.clog 2 (F + 1) + Nat.clog 2 (F + 1) * (20 * Nat.clog 2 (F + 1) + 6)) ∧ D.depth ≤ (2 + 23 * Nat.clog 2 (F + 1)) * C.depth

De Morgan circuits simulate fan-in-bounded majority circuits: a circuit over the TC basis (unbounded AND, OR, NOT, and MAJ gates) of n inputs, s gates, depth d, and fan-in at most F has an equivalent De Morgan circuit of fan-in two of size O(s F log F) and depth O(d log F).

theorem Cslib.Circuits.Boolean.mem_NC_succ_of_threshold_fanInAtMost {L : Language Bool} {i c : ℕ} {s F : ℕ → ℕ} (hs : PolynomiallyBounded s) (hF : PolynomiallyBounded F) (hC : ∀ (n : ℕ), ∃ (C : Circuit Threshold.signature n 1), C.Computes Threshold.interpretation (single (L.slice n)) ∧ C.depth ≤ c * (Nat.log 2 n + 1) ^ i ∧ C.size ≤ s n ∧ C.FanInAtMost (F n)) : L ∈ NC (i + 1)

Any language decided by polynomial-size, polynomially fan-in-bounded threshold circuits of depth O((log n) ^ i) belongs to NCⁱ⁺¹ Vollmer, Theorem 4.22.

theorem Cslib.Circuits.Boolean.mem_NC_succ_of_majority_fanInAtMost {L : Language Bool} {i c : ℕ} {s F : ℕ → ℕ} (hs : PolynomiallyBounded s) (hF : PolynomiallyBounded F) (hC : ∀ (n : ℕ), ∃ (C : Circuit Unbounded.extSignature n 1), C.Computes (Unbounded.extInterpretation majority) (single (L.slice n)) ∧ C.depth ≤ c * (Nat.log 2 n + 1) ^ i ∧ C.size ≤ s n ∧ C.FanInAtMost (F n)) : L ∈ NC (i + 1)

Any language decided by polynomial-size, polynomially fan-in-bounded TC circuits of depth O((log n) ^ i) belongs to NCⁱ⁺¹ Vollmer, Theorem 4.22.