Sum-of-terms circuit basis

This basis represents restricted arithmetic circuits whose charged gates produce members of a prescribed dictionary and whose free gates add already constructed values. By choosing the term type appropriately, it models diagonal depth-three circuits (sums of powers), sums of products, tensor-rank decompositions, and related representation problems.

Coefficients can be included in the term parameter itself. This keeps the syntax independent of any scalar action on the semantic carrier.

inductive Algebraic.SumOfTerms.Op (T : Type u) : Type u

Binary addition and a family of nullary dictionary terms.

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

@[instance_reducible]

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

Equations

• Algebraic.SumOfTerms.instDecidableEqOp = Algebraic.SumOfTerms.instDecidableEqOp.decEq

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

Equations

• Algebraic.SumOfTerms.instDecidableEqOp.decEq Algebraic.SumOfTerms.Op.add Algebraic.SumOfTerms.Op.add = isTrue ⋯
• Algebraic.SumOfTerms.instDecidableEqOp.decEq Algebraic.SumOfTerms.Op.add (Algebraic.SumOfTerms.Op.term value) = isFalse ⋯
• Algebraic.SumOfTerms.instDecidableEqOp.decEq (Algebraic.SumOfTerms.Op.term value) Algebraic.SumOfTerms.Op.add = isFalse ⋯
• Algebraic.SumOfTerms.instDecidableEqOp.decEq (Algebraic.SumOfTerms.Op.term a) (Algebraic.SumOfTerms.Op.term b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Algebraic.SumOfTerms.arity {T : Type u_1} : Op T → ℕ

Arity of sum-of-terms operations.

Equations

• Algebraic.SumOfTerms.arity Algebraic.SumOfTerms.Op.add = 2
• Algebraic.SumOfTerms.arity (Algebraic.SumOfTerms.Op.term value) = 0

@[simp]

theorem Algebraic.SumOfTerms.arity_add {T : Type u_1} : arity Op.add = 2

@[simp]

theorem Algebraic.SumOfTerms.arity_term {T : Type u_1} (term : T) : arity (Op.term term) = 0

@[reducible, inline]

abbrev Algebraic.SumOfTerms.signature (T : Type u) : Signature

Signature for free addition of charged dictionary terms.

Equations

• Algebraic.SumOfTerms.signature T = { Op := Algebraic.SumOfTerms.Op T, Arity := Algebraic.SumOfTerms.arity }

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

Interpret a term by its dictionary value and addition by carrier addition.

Equations

• Algebraic.SumOfTerms.interpretation termValue Algebraic.SumOfTerms.Op.add input = input 0 + input 1
• Algebraic.SumOfTerms.interpretation termValue (Algebraic.SumOfTerms.Op.term term) x_2 = termValue term

def Algebraic.SumOfTerms.weightedCost {T : Type u_1} (addition term : ℕ) : OperationCost (signature T)

Charge source additions and dictionary terms independently.

Equations

• Algebraic.SumOfTerms.weightedCost addition term Algebraic.SumOfTerms.Op.add = addition
• Algebraic.SumOfTerms.weightedCost addition term (Algebraic.SumOfTerms.Op.term value) = term

def Algebraic.SumOfTerms.termCost {T : Type u_1} : OperationCost (signature T)

Charge one for each dictionary term and make addition free.

Equations

• Algebraic.SumOfTerms.termCost = Algebraic.SumOfTerms.weightedCost 0 1

def Algebraic.SumOfTerms.dictionaryCost {T : Type u_1} (weight : T → ℕ) : OperationCost (signature T)

Charge each dictionary term by a term-dependent natural weight and make addition free.

Equations

• Algebraic.SumOfTerms.dictionaryCost weight Algebraic.SumOfTerms.Op.add = 0
• Algebraic.SumOfTerms.dictionaryCost weight (Algebraic.SumOfTerms.Op.term value) = weight value

def Algebraic.SumOfTerms.additionCost {T : Type u_1} : OperationCost (signature T)

Charge source additions and make dictionary terms free.

Equations

• Algebraic.SumOfTerms.additionCost = Algebraic.SumOfTerms.weightedCost 1 0

def Algebraic.SumOfTerms.gateCost {T : Type u_1} : OperationCost (signature T)

Charge every source operation once.

Equations

• Algebraic.SumOfTerms.gateCost = Algebraic.SumOfTerms.weightedCost 1 1

@[simp]

theorem Algebraic.SumOfTerms.weightedCost_add {T : Type u_1} (addition term : ℕ) : weightedCost addition term Op.add = addition

@[simp]

theorem Algebraic.SumOfTerms.weightedCost_term {T : Type u_1} (addition term : ℕ) (value : T) : weightedCost addition term (Op.term value) = term

@[simp]

theorem Algebraic.SumOfTerms.termCost_add {T : Type u_1} : termCost Op.add = 0

@[simp]

theorem Algebraic.SumOfTerms.termCost_term {T : Type u_1} (term : T) : termCost (Op.term term) = 1

@[simp]

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

@[simp]

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

@[simp]

theorem Algebraic.SumOfTerms.additionCost_add {T : Type u_1} : additionCost Op.add = 1

@[simp]

theorem Algebraic.SumOfTerms.additionCost_term {T : Type u_1} (term : T) : additionCost (Op.term term) = 0

@[simp]

theorem Algebraic.SumOfTerms.gateCost_add {T : Type u_1} : gateCost Op.add = 1

@[simp]

theorem Algebraic.SumOfTerms.gateCost_term {T : Type u_1} (term : T) : gateCost (Op.term term) = 1

theorem Algebraic.SumOfTerms.program_cost_weightedCost {T : Type u_1} {n g : ℕ} (program : Program (signature T) n g) (addition term : ℕ) : Program.cost (weightedCost addition term) program = addition * Program.cost additionCost program + term * Program.cost termCost program

Weighted source cost decomposes exactly into addition count and dictionary term count.

theorem Algebraic.SumOfTerms.circuit_cost_weightedCost {T : Type u_1} {n m : ℕ} (circuit : Circuit (signature T) n m) (addition term : ℕ) : circuit.cost (weightedCost addition term) = addition * circuit.cost additionCost + term * circuit.cost termCost

Circuit form of exact weighted source-cost decomposition.