Aggregate gates

An operation of arity k aggregates in a commutative monoid T when its value is read off a product of contributions of its arguments: f x = ψ (∏ i, φ i (x i)). Every operation of the Boolean basis of unbounded fan-in (negation, and conjunction and disjunction of any number of arguments) aggregates in ZMod 2 under multiplication, and every function of the number of true arguments modulo m, such as parity and MOD_m, aggregates in ZMod m under addition.

If every special gate of a program aggregates in T, the special gates have a ledger in the monoid T ^ k of functions from the k special gates to T (Frontier.Ledger.ofAggregates): the contribution of a wire to a special gate is the product of its contributions to the argument slots of that gate that read it. So k aggregate gates cost k log |T| in the frontier lower bound.

Main definitions

• Cslib.Circuits.Frontier.Aggregates f T: the operation f aggregates in T.
• Cslib.Circuits.Frontier.Ledger.ofAggregates: the ledger of aggregate gates.

Main results

• Cslib.Circuits.Frontier.aggregates_unbounded: the operations of the Boolean basis of unbounded fan-in aggregate in ZMod 2.
• Cslib.Circuits.Frontier.aggregates_countMod: functions of the number of true arguments modulo m aggregate in ZMod m.

def Cslib.Circuits.Frontier.Aggregates {U : Type u_1} {k : ℕ} (f : (Fin k → U) → U) (T : Type u_2) [CommMonoid T] : Prop

An operation of arity k aggregates in a commutative monoid T when its value is read off a product of contributions of its arguments.

noncomputable def Cslib.Circuits.Frontier.Ledger.ofAggregates {U : Type u_1} {σ : Signature} {n s : ℕ} {special : Fin s → Prop} {p : Program σ n s} {I : Interpretation σ U} {T : Type u_2} [CommMonoid T] (h : ∀ (g : Fin s), special g → Aggregates (I (p.lines g).op) T) : Ledger special p I ({ g : Fin s // special g } → T)

Aggregate gates have a ledger. If every special gate of a program aggregates in T, the special gates have a ledger in the monoid of functions from the special gates to T: a wire contributes to a special gate the product of its contributions to the slots of that gate that read it, and each special gate reads off its own coordinate.

theorem Cslib.Circuits.Frontier.aggregates_unbounded (op : Boolean.Unbounded.Op) : Aggregates (Boolean.Unbounded.interpretation op) (ZMod 2)

The Boolean basis of unbounded fan-in aggregates. Negation, conjunction and disjunction of any number of arguments aggregate in ZMod 2 under multiplication: a conjunction is the product of its arguments read as 1 for true and 0 for false, and a disjunction is the negation of the product of the negations.

theorem Cslib.Circuits.Frontier.aggregates_countMod (k m : ℕ) (f : ZMod m → Bool) : Aggregates (fun (x : Fin k → Bool) => f ↑{i : Fin k | x i = true}.card) (Multiplicative (ZMod m))

Counting modulo m aggregates. Every function of the number of true arguments modulo m aggregates in ZMod m under addition: each true argument contributes 1 to the count. Parity and the MOD_m gates are of this form.