Binary gates and finite commutative aggregates

A special operation multiplies one contribution for each ordered input slot and applies a Boolean readout. Slots may repeat wires. Commutativity permits partitioning the contributions; no cancellation, inverse, or group structure is required.

inductive Algebraic.Aggregate.Op {J : Type} (State : J → Type) : Type

A full binary Boolean operation or a finite-arity aggregate operation.

• binary {J : Type} {State : J → Type} (function : Bool → Bool → Bool) : Op State
• special {J : Type} {State : J → Type} (kind : J) (arity : ℕ) (contribution : Fin arity → Bool → State kind) (readout : State kind → Bool) : Op State

@[reducible, inline]

abbrev Algebraic.Aggregate.signature {J : Type} (State : J → Type) : Signature

The mixed signature retains the special operation's ordered slots.

Equations

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

def Algebraic.Aggregate.Op.isSpecial {J : Type} {State : J → Type} : Op State → Bool

Whether an operation needs an aggregate consistency check.

Equations

• (Algebraic.Aggregate.Op.binary function).isSpecial = false
• (Algebraic.Aggregate.Op.special kind arity contribution readout).isSpecial = true

@[reducible, inline]

abbrev Algebraic.Aggregate.Op.Register {J : Type} {State : J → Type} : Op State → Type

The register carried by an operation; binary operations need no register.

Equations

• (Algebraic.Aggregate.Op.binary function).Register = PUnit.{1}
• (Algebraic.Aggregate.Op.special kind arity contribution readout).Register = State kind

@[instance_reducible]

instance Algebraic.Aggregate.instCommMonoidRegister {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] (op : Op State) : CommMonoid op.Register

Equations

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

@[instance_reducible]

instance Algebraic.Aggregate.instFintypeRegister {J : Type} {State : J → Type} [(j : J) → Fintype (State j)] (op : Op State) : Fintype op.Register

Equations

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

def Algebraic.Aggregate.Op.slotContribution {J : Type} {State : J → Type} (op : Op State) : Fin ((signature State).Arity op) → Bool → op.Register

A slot's contribution; the unused register of a binary gate is trivial.

Equations

• (Algebraic.Aggregate.Op.binary function).slotContribution = fun (x : Fin ((Algebraic.Aggregate.signature State).Arity (Algebraic.Aggregate.Op.binary function))) (x_1 : Bool) => PUnit.unit
• (Algebraic.Aggregate.Op.special kind arity contribution readout).slotContribution = contribution

def Algebraic.Aggregate.Op.readout {J : Type} {State : J → Type} (op : Op State) : op.Register → Bool

The Boolean predicate applied to a special register; unused on binary operations.

Equations

• (Algebraic.Aggregate.Op.binary function).readout = fun (x : (Algebraic.Aggregate.Op.binary function).Register) => false
• (Algebraic.Aggregate.Op.special kind arity contribution readout).readout = readout

def Algebraic.Aggregate.interpretation {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] : Interpretation (signature State) Bool

Boolean evaluation of the mixed signature.

Equations

• Algebraic.Aggregate.interpretation (Algebraic.Aggregate.Op.binary f) arguments = f (arguments 0) (arguments 1)
• Algebraic.Aggregate.interpretation (Algebraic.Aggregate.Op.special kind arity contribution readout) arguments = readout (∏ slot : Fin arity, contribution slot (arguments slot))

inductive Algebraic.Aggregate.OrdinaryOp : Type

Operations of the ordinary circuit after guessing all special output bits.

• binary (function : Bool → Bool → Bool) : OrdinaryOp
• constant (value : Bool) : OrdinaryOp

@[reducible, inline]

abbrev Algebraic.Aggregate.ordinarySignature : Signature

Erased special gates have zero incoming wires.

Equations

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

def Algebraic.Aggregate.ordinaryInterpretation : Interpretation ordinarySignature Bool

Interpretation of binary operations and guessed constants.

Equations

• Algebraic.Aggregate.ordinaryInterpretation (Algebraic.Aggregate.OrdinaryOp.binary f) arguments = f (arguments 0) (arguments 1)
• Algebraic.Aggregate.ordinaryInterpretation (Algebraic.Aggregate.OrdinaryOp.constant value) x_2 = value

theorem Algebraic.Aggregate.ordinary_arity_le_two (op : OrdinaryOp) : ordinarySignature.Arity op ≤ 2

Each ordinary operation has at most two input slots.