Threshold circuits -- definitions

A threshold operation carries a natural cutoff and returns true exactly when at least that many inputs are true. The operation has unbounded fan-in. As in the rest of the circuit library, per-edge negation remains free; this is the standard nonuniform threshold-circuit convention with NOT gates available at no asymptotic cost.

structure Complexity.ThresholdOp : Type

An unweighted threshold operation with a natural cutoff.

• cutoff : ℕ

  Minimum number of true inputs required.

@[implicit_reducible]

instance Complexity.instReprThresholdOp : Repr ThresholdOp

Equations

• Complexity.instReprThresholdOp = { reprPrec := Complexity.instReprThresholdOp.repr }

def Complexity.instReprThresholdOp.repr : ThresholdOp → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Complexity.instDecidableEqThresholdOp.decEq (x✝ x✝¹ : ThresholdOp) : Decidable (x✝ = x✝¹)

Equations

• Complexity.instDecidableEqThresholdOp.decEq { cutoff := a } { cutoff := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.instDecidableEqThresholdOp : DecidableEq ThresholdOp

Equations

• Complexity.instDecidableEqThresholdOp = Complexity.instDecidableEqThresholdOp.decEq

def Complexity.ThresholdOp.trueCount {n : ℕ} (inputs : BitString n) : ℕ

Count the true inputs to an n-ary threshold gate.

Equations

• Complexity.ThresholdOp.trueCount inputs = Fin.countP inputs

def Complexity.ThresholdOp.eval (op : ThresholdOp) (n : ℕ) (inputs : BitString n) : Bool

Evaluate an unweighted threshold gate.

Equations

• op.eval n inputs = decide (op.cutoff ≤ Complexity.ThresholdOp.trueCount inputs)

def Complexity.ThresholdOp.conjunction (n : ℕ) : ThresholdOp

The threshold operation computing conjunction at arity n.

Equations

• Complexity.ThresholdOp.conjunction n = { cutoff := n }

def Complexity.ThresholdOp.disjunction : ThresholdOp

The threshold operation computing disjunction.

Equations

• Complexity.ThresholdOp.disjunction = { cutoff := 1 }

def Complexity.ThresholdOp.majority (n : ℕ) : ThresholdOp

Strict majority at arity n.

Equations

• Complexity.ThresholdOp.majority n = { cutoff := n / 2 + 1 }

def Complexity.Basis.threshold : Basis

The basis of unbounded-fan-in, unweighted threshold operations.

Equations

• One or more equations did not get rendered due to their size.