Weighted threshold circuits and their input-reading transcripts

Real-weight threshold gates form a signature for CSLib's existing Program and Circuit. A gate returns true exactly when its weighted sum is at least its threshold. The model allows arbitrary real coefficients, repeated argument wires, and nullary gates.

Coefficients are aggregated by actual wire before determining which gates read original inputs. In particular, repeated weights may cancel. The values of these input-reading gates determine all internal gate values. Circuit outputs are therefore determined when they select gate wires; an output selecting an original input is not covered by that conclusion.

These are semantic results. Comparing arbitrary real numbers is noncomputable, and this module does not assert an algorithm for evaluating rationally encoded circuits.

Main definitions

• Cslib.Circuits.Boolean.WeightedThreshold.signature: the weighted threshold basis.
• Cslib.Circuits.Boolean.WeightedThreshold.inputGates: gates with a nonzero aggregated coefficient on an original input.
• Cslib.Circuits.Boolean.WeightedThreshold.transcript: the values of these gates.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.eval_gate_eq: the dense gate equation, with repeated wire coefficients aggregated.
• Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_transcript_eq: the restricted transcript determines every internal gate value.
• Cslib.Circuits.Boolean.WeightedThreshold.circuit_eval_eq_of_transcript_eq: the corresponding statement for circuits whose designated outputs are gates.

References

• [Threshold Circuits as Decision Trees and Finite-State Programs, Section 3] [26]

structure Cslib.Circuits.Boolean.WeightedThreshold.Op : Type

A real-weight threshold operation with arbitrary finite arity.

• arity : ℕ

  The number of argument slots.

• weight : Fin self.arity → ℝ

  The coefficient of each argument slot.

• threshold : ℝ

  Equality at the threshold returns true.

@[reducible, inline]

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

The signature of real-weight threshold gates.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.interpretation : Interpretation signature Bool

A gate is true exactly when its weighted sum is at least its threshold.

def Cslib.Circuits.Boolean.WeightedThreshold.ofThresholdOp : Threshold.Op → Op

Unweighted thresholds have unit coefficients, and negation has coefficient -1 and threshold zero.

def Cslib.Circuits.Boolean.WeightedThreshold.ofThreshold : Threshold.signature.Hom signature

The existing unweighted threshold basis embeds gate for gate.

instance Cslib.Circuits.Boolean.WeightedThreshold.preserves_ofThreshold : ofThreshold.Preserves Threshold.interpretation interpretation

Translating the existing threshold basis preserves its Boolean interpretation.

def Cslib.Circuits.Boolean.WeightedThreshold.lineWeight {n g : ℕ} (line : Line signature n g) (wire : Wire n g) : ℝ

The combined coefficient of an actual wire, summing all slots that read it.

theorem Cslib.Circuits.Boolean.WeightedThreshold.sum_lineWeight_mul {n g : ℕ} (line : Line signature n g) (values : Wire n g → ℝ) : ∑ a : Fin line.op.arity, line.op.weight a * values (line.wires a) = ∑ wire : Wire n g, lineWeight line wire * values wire

Regrouping argument slots by actual wire preserves their weighted sum.

theorem Cslib.Circuits.Boolean.WeightedThreshold.line_eval_eq {n g : ℕ} (line : Line signature n g) (x : Fin n → Bool) (z : Fin g → Bool) : line.eval interpretation x z = decide (line.op.threshold ≤ ∑ i : Fin n, lineWeight line (Wire.input i) * ↑(x i).toNat + ∑ j : Fin g, lineWeight line (Wire.gate j) * ↑(z j).toNat)

A line's value splits into its aggregated input and gate contributions.

def Cslib.Circuits.Boolean.WeightedThreshold.inputWeight {n g : ℕ} (p : Program signature n g) (gate : Fin g) (input : Fin n) : ℝ

The direct coefficient of an original input in a program gate.

def Cslib.Circuits.Boolean.WeightedThreshold.gateWeight {n g : ℕ} (p : Program signature n g) (gate prior : Fin g) : ℝ

The coefficient of an internal gate in another gate.

theorem Cslib.Circuits.Boolean.WeightedThreshold.eval_gate_eq {n g : ℕ} (p : Program signature n g) (x : Fin n → Bool) (gate : Fin g) : p.eval interpretation x gate = decide ((p.lines gate).op.threshold ≤ ∑ i : Fin n, inputWeight p gate i * ↑(x i).toNat + ∑ j : Fin g, gateWeight p gate j * ↑(p.eval interpretation x j).toNat)

A native program gate satisfies the usual dense threshold equation. Coefficients of the current gate and of later gates are zero by the program's topological order.

theorem Cslib.Circuits.Boolean.WeightedThreshold.gateWeight_eq_zero_of_le {n g : ℕ} (p : Program signature n g) (gate prior : Fin g) (h : gate ≤ prior) : gateWeight p gate prior = 0

A gate has zero coefficient on its own output and on later gate outputs.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.inputGates {n g : ℕ} (p : Program signature n g) : Finset (Fin g)

The gates with a nonzero aggregated direct-input coefficient. Gates that depend on inputs only through earlier gates are not counted.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.mem_inputGates {n g : ℕ} (p : Program signature n g) (gate : Fin g) : gate ∈ inputGates p ↔ ∃ (i : Fin n), inputWeight p gate i ≠ 0

theorem Cslib.Circuits.Boolean.WeightedThreshold.inputWeight_eq_zero_of_not_mem {n g : ℕ} (p : Program signature n g) {gate : Fin g} (h : gate ∉ inputGates p) (i : Fin n) : inputWeight p gate i = 0

Every input coefficient vanishes at a gate outside the input-reading set.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.transcript {n g : ℕ} (p : Program signature n g) (x : Fin n → Bool) : ↥(inputGates p) → Bool

The restricted activation transcript, indexed by the input-reading gates.

theorem Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_forall_mem_inputGates_lt {n g : ℕ} (p : Program signature n g) {x y : Fin n → Bool} (bound : ℕ) (h : ∀ gate ∈ inputGates p, ↑gate < bound → p.eval interpretation x gate = p.eval interpretation y gate) (gate : Fin g) : ↑gate < bound → p.eval interpretation x gate = p.eval interpretation y gate

Agreement on input-reading gates before a given bound forces agreement on every gate before that bound.

theorem Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_forall_mem_inputGates {n g : ℕ} (p : Program signature n g) {x y : Fin n → Bool} (h : ∀ gate ∈ inputGates p, p.eval interpretation x gate = p.eval interpretation y gate) : p.eval interpretation x = p.eval interpretation y

Agreement on all input-reading gates forces agreement on every gate.

theorem Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_transcript_eq {n g : ℕ} (p : Program signature n g) {x y : Fin n → Bool} (h : transcript p x = transcript p y) : p.eval interpretation x = p.eval interpretation y

The restricted transcript determines the complete gate valuation.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_eval_eq_of_transcript_eq {n m : ℕ} (c : Circuit signature n m) (houtputs : ∀ (output : Fin m), ∃ (gate : Fin c.size), c.outputs output = Wire.gate gate) {x y : Fin n → Bool} (h : transcript c.program x = transcript c.program y) : c.eval interpretation x = c.eval interpretation y

Gate-valued designated outputs are determined by the restricted transcript. The output hypothesis is necessary: native circuits may select original inputs without any gates.