The basis of threshold gates

The threshold gate Th^m_j of m arguments says that at least j of them are true (Cslib.threshold m j). The threshold gates of every arity and every cutoff, together with negation, form the basis of threshold circuits Hajnal et al., Section 2. Here the gates are unweighted; a gate with weights ±1 is a threshold gate reading some of its arguments negated. As for AC⁰ circuits over the unbounded fan-in basis, negations are free in the depth that counts threshold gates (Threshold.thresholdCost).

Cutoff 0 is the constant true, a cutoff above the arity the constant false (Cslib.threshold_zero_right, Cslib.threshold_eq_false_of_lt), cutoff 1 the disjunction and cutoff m the conjunction of m arguments (Cslib.threshold_one_right, Cslib.threshold_self). So the unbounded fan-in basis maps into the threshold basis keeping the meaning of every operation (Threshold.ofUnbounded), and its AND/OR depth becomes the threshold depth (Threshold.thresholdCost_ofUnbounded). The majority gate of m arguments is the threshold gate Th^m_⌈m/2⌉ (Cslib.majority), so the basis of TC⁰ maps into the threshold basis too (Threshold.ofMajority).

Main definitions

• Cslib.Circuits.Boolean.Threshold.signature: negation, and the threshold gates of every arity and cutoff.
• Cslib.Circuits.Boolean.Threshold.interpretation: their Boolean meaning.
• Cslib.Circuits.Boolean.Threshold.thresholdCost: the costs of the threshold depth, in which negations are free.
• Cslib.Circuits.Boolean.Threshold.ofUnbounded: the unbounded fan-in basis inside the threshold basis.
• Cslib.Circuits.Boolean.Threshold.ofMajority: the basis of TC⁰, with majority gates, inside the threshold basis.

Main results

• Cslib.Circuits.Boolean.Threshold.preserves_ofUnbounded: conjunctions and disjunctions are threshold gates.
• Cslib.Circuits.Boolean.Threshold.thresholdCost_ofUnbounded: the AND/OR depth is the threshold depth.
• Cslib.Circuits.Boolean.Threshold.preserves_ofMajority: majority gates are threshold gates.

References

• A. Hajnal, W. Maass, P. Pudlák, M. Szegedy, G. Turán, Threshold circuits of bounded depth

inductive Cslib.Circuits.Boolean.Threshold.Op : Type

Negation, and the threshold gate of m arguments with cutoff j for every m and j.

• not : Op

  Negation.

• threshold (m j : ℕ) : Op

  The threshold gate Th^m_j: at least j of its m arguments are true.

def Cslib.Circuits.Boolean.Threshold.instDecidableEqOp.decEq (x✝ x✝¹ : Op) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Circuits.Boolean.Threshold.instDecidableEqOp : DecidableEq Op

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.Threshold.Op.arity : Op → ℕ

The arity of an operation.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.Threshold.signature : Signature

The signature of negation and of the threshold gates. It is reducible, so that case analysis on its operations sees their arities.

def Cslib.Circuits.Boolean.Threshold.interpretation : Interpretation signature Bool

The Boolean meaning of the operations.

@[simp]

theorem Cslib.Circuits.Boolean.Threshold.interpretation_not (x : Fin 1 → Bool) : interpretation Op.not x = !x 0

@[simp]

theorem Cslib.Circuits.Boolean.Threshold.interpretation_threshold (m j : ℕ) (x : Fin m → Bool) : interpretation (Op.threshold m j) x = threshold m j x

def Cslib.Circuits.Boolean.Threshold.thresholdCost : Op → ℕ

The cost of an operation in the threshold depth: negations are free. With these costs, Circuit.depthWith is the largest number of threshold gates on a path, as Unbounded.andOrCost counts the AND and OR gates of circuits over the unbounded fan-in basis.

@[simp]

theorem Cslib.Circuits.Boolean.Threshold.thresholdCost_not : thresholdCost Op.not = 0

@[simp]

theorem Cslib.Circuits.Boolean.Threshold.thresholdCost_threshold (m j : ℕ) : thresholdCost (Op.threshold m j) = 1

theorem Cslib.Circuits.Boolean.Threshold.thresholdCost_le_one (op : Op) : thresholdCost op ≤ 1

def Cslib.Circuits.Boolean.Threshold.ofUnboundedOp : Unbounded.Op → Op

The operations of the unbounded fan-in basis as threshold gates: the conjunction of m arguments is Th^m_m and their disjunction is Th^m_1.

def Cslib.Circuits.Boolean.Threshold.ofUnbounded : Unbounded.signature.Hom signature

The unbounded fan-in basis inside the threshold basis.

@[simp]

theorem Cslib.Circuits.Boolean.Threshold.ofUnbounded_apply (op : Unbounded.Op) : ofUnbounded op = ofUnboundedOp op

instance Cslib.Circuits.Boolean.Threshold.preserves_ofUnbounded : ofUnbounded.Preserves Unbounded.interpretation interpretation

Conjunctions and disjunctions are threshold gates.

@[simp]

theorem Cslib.Circuits.Boolean.Threshold.thresholdCost_ofUnbounded (op : Unbounded.Op) : thresholdCost (ofUnbounded op) = Unbounded.andOrCost op

The AND/OR depth of a circuit over the unbounded fan-in basis is the threshold depth of its translation.

def Cslib.Circuits.Boolean.Threshold.ofMajorityOp : Unbounded.ExtOp → Op

The operations of the basis of TC⁰ as threshold gates: the majority gate of m arguments is Th^m_⌈m/2⌉.

def Cslib.Circuits.Boolean.Threshold.ofMajority : Unbounded.extSignature.Hom signature

The basis of TC⁰, the unbounded fan-in basis with majority gates, inside the threshold basis.

@[simp]

theorem Cslib.Circuits.Boolean.Threshold.ofMajority_apply (op : Unbounded.ExtOp) : ofMajority op = ofMajorityOp op

instance Cslib.Circuits.Boolean.Threshold.preserves_ofMajority : ofMajority.Preserves (Unbounded.extInterpretation majority) interpretation

Majority gates are threshold gates.