Arithmetic formulas for linear forms #
A linear form is an ordinary formula over the arithmetic signature. Coefficient symbols and
their interpretation are separate, and a selection map permits repeated or permuted inputs.
The formula includes one named zero, one constant and multiplication per coefficient, and one
addition per summand, including the initial addition to zero. Formula.toCircuit compiles it
with exactly the same arbitrary weighted cost.
Main definitions #
Cslib.Circuits.Formula.linearForm: a linear form in selected input variables.
Main results #
Cslib.Circuits.Formula.eval_linearForm: evaluation is the corresponding finite sum.Cslib.Circuits.Formula.cost_linearForm: exact cost including coefficient constants.
References #
- Adapted from LowerBound/Fusion/SumOfTerms/Waring/Translation.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib. This uses the generic formula compiler instead of a separate arithmetic expression language.
def Cslib.Circuits.Formula.linearForm {C : Type v} {n : ℕ} (zero : C) {k : ℕ} :
(Fin k → C) → (Fin k → Fin n) → Formula (arithSignature C) n
A linear form with coefficient symbols a, input selection select, and a named zero.
The selected inputs may repeat. The sum is accumulated from left to right, starting at zero.
Instances For
theorem Cslib.Circuits.Formula.eval_linearForm {C : Type v} {R : Type u} {n : ℕ} [Semiring R] (zero : C) (constant : C → R) (hzero : constant zero = 0) {k : ℕ} (a : Fin k → C) (select : Fin k → Fin n) (x : Fin n → R) :
(linearForm zero a select).eval (arithInterpretationWith C constant) x = ∑ i : Fin k, constant (a i) * x (select i)
Interpreting a linear form gives its finite sum of coefficient products.
theorem Cslib.Circuits.Formula.cost_linearForm {C : Type v} {n : ℕ} (zero : C) (weight : ArithOp C → ℕ) {k : ℕ} (a : Fin k → C) (select : Fin k → Fin n) :
cost weight (linearForm zero a select) = weight (ArithOp.const zero) + ∑ i : Fin k, (weight (ArithOp.const (a i)) + weight ArithOp.mul + weight ArithOp.add)
Exact weighted cost, charging the named zero and every coefficient constant.