Circuits adding dictionary terms

Nullary gates produce members of a prescribed dictionary, interpreted in any additive carrier. The standard dictionary cost charges those terms and makes binary addition and wiring free. Separate addition costs and arbitrary uniform weights are also provided.

Main definitions

• Cslib.Circuits.SumOfTerms.signature: additions and nullary dictionary terms.
• Cslib.Circuits.SumOfTerms.interpretation: interpret the dictionary in an additive carrier.
• Cslib.Circuits.SumOfTerms.dictionaryCost, Cslib.Circuits.SumOfTerms.termCost: term weights.
• Cslib.Circuits.SumOfTerms.addCost, Cslib.Circuits.SumOfTerms.weightedCost: addition counts and separate uniform weights for additions and terms.

Main results

• Cslib.Circuits.SumOfTerms.cost_weightedCost: separate the two gate counts.

References

• Adapted from Basis/SumOfTerms.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.

inductive Cslib.Circuits.SumOfTerms.Op (T : Type u) : Type u

Free binary addition and a nullary gate for each dictionary term.

• add {T : Type u} : Op T
• term {T : Type u} (value : T) : Op T

def Cslib.Circuits.SumOfTerms.instDecidableEqOp.decEq {T✝ : Type u_1} [DecidableEq T✝] (x✝ x✝¹ : Op T✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Circuits.SumOfTerms.instDecidableEqOp {T✝ : Type u_1} [DecidableEq T✝] : DecidableEq (Op T✝)

@[reducible, inline]

abbrev Cslib.Circuits.SumOfTerms.Op.arity {T : Type u_1} : Op T → ℕ

Addition reads two wires; dictionary terms read none.

@[reducible, inline]

abbrev Cslib.Circuits.SumOfTerms.signature (T : Type u) : Signature

The signature for sums of dictionary terms.

def Cslib.Circuits.SumOfTerms.interpretation {T : Type u_1} {V : Type u_2} [Add V] (value : T → V) : Interpretation (signature T) V

Interpret dictionary terms by their values and addition by carrier addition.

@[simp]

theorem Cslib.Circuits.SumOfTerms.interpretation_add {T : Type u_1} {V : Type u_2} [Add V] (value : T → V) (args : Fin 2 → V) : interpretation value Op.add args = args 0 + args 1

@[simp]

theorem Cslib.Circuits.SumOfTerms.interpretation_term {T : Type u_1} {V : Type u_2} [Add V] (value : T → V) (t : T) (args : Fin 0 → V) : interpretation value (Op.term t) args = value t

def Cslib.Circuits.SumOfTerms.dictionaryCost {T : Type u_1} (weight : T → ℕ) : Op T → ℕ

Charge each dictionary term its weight; addition is free.

@[simp]

theorem Cslib.Circuits.SumOfTerms.dictionaryCost_add {T : Type u_1} (weight : T → ℕ) : dictionaryCost weight Op.add = 0

@[simp]

theorem Cslib.Circuits.SumOfTerms.dictionaryCost_term {T : Type u_1} (weight : T → ℕ) (t : T) : dictionaryCost weight (Op.term t) = weight t

@[reducible, inline]

abbrev Cslib.Circuits.SumOfTerms.termCost {T : Type u_1} : Op T → ℕ

Count dictionary gates, with free addition.

def Cslib.Circuits.SumOfTerms.addCost {T : Type u_1} : Op T → ℕ

Count additions; dictionary gates are free.

def Cslib.Circuits.SumOfTerms.weightedCost {T : Type u_1} (addition term : ℕ) : Op T → ℕ

Assign one weight to additions and another to dictionary gates.

theorem Cslib.Circuits.SumOfTerms.cost_weightedCost {T : Type u_1} {n g : ℕ} (p : Program (signature T) n g) (addition term : ℕ) : p.cost (weightedCost addition term) = addition * p.cost addCost + term * p.cost termCost

Uniform weights separate into the addition and dictionary gate counts.