Boolean, modular, threshold, and symmetric aggregate gates

AND and OR use multiplication in the two-element ring as a commutative monoid. Their zero updates are noninvertible. Modular gates instead use its additive monoid (written multiplicatively through Multiplicative), with an arbitrary Boolean predicate on the residue. Slot-dependent contributions allow weighted modular sums. Saturating addition computes nonnegative weighted thresholds, and an arity-capped counter computes every predicate of the Hamming weight. Each operation has unrestricted finite fan-in.

def Algebraic.Aggregate.andGate (arity : ℕ) : Op fun (x : Unit) => ZMod 2

A two-state noncancellative aggregate computing conjunction.

Equations

• Algebraic.Aggregate.andGate arity = Algebraic.Aggregate.Op.special () arity (fun (x : Fin arity) (b : Bool) => if b = true then 1 else 0) fun (z : ZMod 2) => decide (z ≠ 0)

def Algebraic.Aggregate.orGate (arity : ℕ) : Op fun (x : Unit) => ZMod 2

A two-state noncancellative aggregate computing disjunction.

Equations

• Algebraic.Aggregate.orGate arity = Algebraic.Aggregate.Op.special () arity (fun (x : Fin arity) (b : Bool) => if b = true then 0 else 1) fun (z : ZMod 2) => decide (z = 0)

theorem Algebraic.Aggregate.andGate_eval (arity : ℕ) (x : Fin arity → Bool) : interpretation (andGate arity) x = decide (∀ (i : Fin arity), x i = true)

Conjunction has the expected semantics, including its nullary value true.

theorem Algebraic.Aggregate.orGate_eval (arity : ℕ) (x : Fin arity → Bool) : interpretation (orGate arity) x = decide (∃ (i : Fin arity), x i = true)

Disjunction has the expected semantics, including its nullary value false.

def Algebraic.Aggregate.modularGate (modulus arity : ℕ) (weight : Fin arity → ZMod modulus) (readout : ZMod modulus → Bool) : Op fun (x : Unit) => Multiplicative (ZMod modulus)

Any residue predicate on a slot-weighted modular sum is an aggregate gate.

Equations

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

theorem Algebraic.Aggregate.modularGate_eval (modulus arity : ℕ) (weight : Fin arity → ZMod modulus) (readout : ZMod modulus → Bool) (x : Fin arity → Bool) : interpretation (modularGate modulus arity weight readout) x = readout (∑ i : Fin arity, if x i = true then weight i else 0)

Modular gate evaluation is precisely the weighted modular sum.

theorem Algebraic.Aggregate.card_andGate_register (arity : ℕ) : Fintype.card (andGate arity).Register = 2

AND uses two aggregate states regardless of its fan-in.

theorem Algebraic.Aggregate.card_orGate_register (arity : ℕ) : Fintype.card (orGate arity).Register = 2

OR uses two aggregate states regardless of its fan-in.

structure Algebraic.Aggregate.Capped (cap : ℕ) : Type

A finite counter whose addition saturates at cap.

• toFin : Fin (cap + 1)

  The stored value lies between zero and the cap, inclusively.

theorem Algebraic.Aggregate.Capped.ext_iff {cap : ℕ} {x y : Capped cap} : x = y ↔ x.toFin = y.toFin

theorem Algebraic.Aggregate.Capped.ext {cap : ℕ} {x y : Capped cap} (toFin : x.toFin = y.toFin) : x = y

def Algebraic.Aggregate.instDecidableEqCapped.decEq {cap✝ : ℕ} (x✝ x✝¹ : Capped cap✝) : Decidable (x✝ = x✝¹)

Equations

• Algebraic.Aggregate.instDecidableEqCapped.decEq { toFin := a } { toFin := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Algebraic.Aggregate.instDecidableEqCapped {cap✝ : ℕ} : DecidableEq (Capped cap✝)

Equations

• Algebraic.Aggregate.instDecidableEqCapped = Algebraic.Aggregate.instDecidableEqCapped.decEq

def Algebraic.Aggregate.Capped.equivFin (cap : ℕ) : Capped cap ≃ Fin (cap + 1)

Capped counters enumerate exactly the integers from zero through the cap.

Equations

• Algebraic.Aggregate.Capped.equivFin cap = { toFun := Algebraic.Aggregate.Capped.toFin, invFun := Algebraic.Aggregate.Capped.mk, left_inv := ⋯, right_inv := ⋯ }

@[instance_reducible]

instance Algebraic.Aggregate.Capped.instFintype (cap : ℕ) : Fintype (Capped cap)

Equations

• Algebraic.Aggregate.Capped.instFintype cap = Fintype.ofEquiv (Fin (cap + 1)) (Algebraic.Aggregate.Capped.equivFin cap).symm

def Algebraic.Aggregate.Capped.val {cap : ℕ} (x : Capped cap) : ℕ

The natural number stored in a capped counter.

Equations

• x.val = ↑x.toFin

def Algebraic.Aggregate.Capped.ofNat (cap value : ℕ) : Capped cap

Insert a natural number, saturating at the cap.

Equations

• Algebraic.Aggregate.Capped.ofNat cap value = { toFin := ⟨min cap value, ⋯⟩ }

theorem Algebraic.Aggregate.Capped.ext_val {cap : ℕ} {x y : Capped cap} (h : x.val = y.val) : x = y

Equality of capped counters is equality of their stored values.

@[instance_reducible]

instance Algebraic.Aggregate.Capped.instCommMonoid (cap : ℕ) : CommMonoid (Capped cap)

Capped addition, written multiplicatively for the aggregate interface.

Equations

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

theorem Algebraic.Aggregate.Capped.card (cap : ℕ) : Fintype.card (Capped cap) = cap + 1

The register has exactly cap + 1 states.

theorem Algebraic.Aggregate.Capped.ofNat_add (cap a b : ℕ) : ofNat cap (a + b) = ofNat cap a * ofNat cap b

Saturation commutes with addition.

theorem Algebraic.Aggregate.Capped.prod_ofNat {ι : Type u_1} (cap : ℕ) (s : Finset ι) (f : ι → ℕ) : ∏ i ∈ s, ofNat cap (f i) = ofNat cap (∑ i ∈ s, f i)

A product of inserted values is their capped sum.

def Algebraic.Aggregate.thresholdGate (threshold arity : ℕ) (weight : Fin arity → ℕ) : Op fun (x : Unit) => Capped threshold

A nonnegative weighted threshold uses a counter capped at the threshold.

Equations

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

theorem Algebraic.Aggregate.thresholdGate_eval (threshold arity : ℕ) (weight : Fin arity → ℕ) (x : Fin arity → Bool) : interpretation (thresholdGate threshold arity weight) x = decide (threshold ≤ ∑ i : Fin arity, if x i = true then weight i else 0)

A capped counter computes the threshold predicate exactly.

def Algebraic.Aggregate.symmetricGate (arity : ℕ) (readout : ℕ → Bool) : Op fun (x : Unit) => Capped arity

A symmetric gate stores the exact Hamming weight in an arity-capped counter.

Equations

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

theorem Algebraic.Aggregate.symmetricGate_eval (arity : ℕ) (readout : ℕ → Bool) (x : Fin arity → Bool) : interpretation (symmetricGate arity readout) x = readout (∑ i : Fin arity, if x i = true then 1 else 0)

No saturation occurs when at most arity Boolean contributions are counted.

theorem Algebraic.Aggregate.card_thresholdGate_register (threshold arity : ℕ) (weight : Fin arity → ℕ) : Fintype.card (thresholdGate threshold arity weight).Register = threshold + 1

Threshold register size depends on the threshold, not the fan-in or weights.

theorem Algebraic.Aggregate.card_symmetricGate_register (arity : ℕ) (readout : ℕ → Bool) : Fintype.card (symmetricGate arity readout).Register = arity + 1

An arbitrary symmetric predicate uses exactly arity + 1 aggregate states.

theorem Algebraic.Aggregate.card_modularGate_register (modulus arity : ℕ) [NeZero modulus] (weight : Fin arity → ZMod modulus) (readout : ZMod modulus → Bool) : Fintype.card (modularGate modulus arity weight readout).Register = modulus

A positive-modulus weighted modular gate has exactly modulus states.