Affine, polynomial and arithmetic bases

Three ways of computing over a commutative semiring F:

• the affine basis (Cslib.Circuits.affineSignature), whose operations of arity k are the affine maps x ↦ a₀ x₀ + ... + a_{k-1} x_{k-1} + b;
• polynomial interpretations (Cslib.Circuits.Interpretation.IsPolynomial), in which every operation of a signature is a polynomial in its arguments, with any coefficients and of any degree;
• the arithmetic basis (Cslib.Circuits.arithSignature): addition and multiplication of arity two, and a constant gate of arity zero for each element of F.

The affine and arithmetic bases are polynomial. Over a finite field every operation is a polynomial, so the distinction matters only over infinite fields, where it is essential: an infinite field admits injections F × F → F, through which a single wire can carry any amount of information.

In an arithmetic circuit the constants are leaves, and Cslib.Circuits.Circuit.innerSize counts exactly the additions and multiplications.

Main definitions

• Cslib.Circuits.affineSignature, Cslib.Circuits.affineInterpretation: the affine basis.
• Cslib.Circuits.arithSignature, Cslib.Circuits.arithInterpretation: the arithmetic basis.
• Cslib.Circuits.arithInterpretationWith: interpret the constant symbols in another carrier.
• Cslib.Circuits.ArithOp.mulCost: count multiplications, including scalar multiplications.
• Cslib.Circuits.ArithOp.addCost: count additions.
• Cslib.Circuits.Interpretation.IsPolynomial: every operation is a polynomial.

Main results

• Cslib.Circuits.isPolynomial_affineInterpretation, Cslib.Circuits.isPolynomial_arithInterpretation: both bases are polynomial.
• Cslib.Circuits.Circuit.fanInAtMost_two_arith: arithmetic circuits have fan-in two.

References

• P. Bürgisser, M. Clausen, M. A. Shokrollahi, Algebraic Complexity Theory, Chapter 4

@[reducible, inline]

abbrev Cslib.Circuits.affineSignature (F : Type u) : Signature

The affine basis over F: an operation of arity k is a vector of k coefficients and a constant.

def Cslib.Circuits.affineInterpretation (F : Type u) [Semiring F] : Interpretation (affineSignature F) F

An affine operation with coefficients a and constant b computes x ↦ ∑ i, a i * x i + b.

@[simp]

theorem Cslib.Circuits.affineInterpretation_apply (F : Type u) [Semiring F] (k : ℕ) (a : Fin k → F) (b : F) (x : Fin k → F) : affineInterpretation F ⟨k, (a, b)⟩ x = ∑ i : Fin k, a i * x i + b

An affine operation with arity k, coefficients a and constant b.

inductive Cslib.Circuits.ArithOp (F : Type u) : Type u

The operations of the arithmetic basis.

• add {F : Type u} : ArithOp F

  Addition.

• mul {F : Type u} : ArithOp F

  Multiplication.

• const {F : Type u} (c : F) : ArithOp F

  A constant.

@[reducible, inline]

abbrev Cslib.Circuits.ArithOp.arity (F : Type u) : ArithOp F → ℕ

The arity of an arithmetic operation: two for addition and multiplication, zero for a constant.

@[reducible, inline]

abbrev Cslib.Circuits.arithSignature (F : Type u) : Signature

The arithmetic basis: addition and multiplication of arity two, and constants of arity zero.

def Cslib.Circuits.arithInterpretationWith (F : Type u) {R : Type u_1} [Add R] [Mul R] (constant : F → R) : Interpretation (arithSignature F) R

Addition and multiplication in R, with constant symbols interpreted by constant. For example, MvPolynomial.C interprets field constants as constant polynomials.

def Cslib.Circuits.arithInterpretation (F : Type u) [Semiring F] : Interpretation (arithSignature F) F

Addition, multiplication and constants.

@[simp]

theorem Cslib.Circuits.arithInterpretationWith_add {F : Type u} {R : Type u_1} [Add R] [Mul R] (constant : F → R) (x : Fin 2 → R) : arithInterpretationWith F constant ArithOp.add x = x 0 + x 1

@[simp]

theorem Cslib.Circuits.arithInterpretationWith_mul {F : Type u} {R : Type u_1} [Add R] [Mul R] (constant : F → R) (x : Fin 2 → R) : arithInterpretationWith F constant ArithOp.mul x = x 0 * x 1

@[simp]

theorem Cslib.Circuits.arithInterpretationWith_const {F : Type u} {R : Type u_1} [Add R] [Mul R] (constant : F → R) (c : F) (x : Fin 0 → R) : arithInterpretationWith F constant (ArithOp.const c) x = constant c

def Cslib.Circuits.ArithOp.mulCost {F : Type u} : ArithOp F → ℕ

Multiplications cost one; additions and constants are free. Multiplication by a scalar still costs one.

def Cslib.Circuits.ArithOp.addCost {F : Type u} : ArithOp F → ℕ

Additions cost one; multiplications and constants are free.

theorem Cslib.Circuits.Circuit.eval_arithInterpretationWith_mvPolynomial {F : Type u} {R : Type u_1} [CommSemiring R] {n m : ℕ} (c : Circuit (arithSignature F) n m) (constant : F → R) (x : Fin n → R) (j : Fin m) : (MvPolynomial.eval x) (c.eval (arithInterpretationWith F (⇑MvPolynomial.C ∘ constant)) MvPolynomial.X j) = c.eval (arithInterpretationWith F constant) x j

Evaluating the formal polynomial computed by a circuit agrees with evaluating the circuit in the coefficient semiring. The converse need not hold over a finite field.

def Cslib.Circuits.Interpretation.IsPolynomial {F : Type u} [CommSemiring F] {σ : Signature} (I : Interpretation σ F) : Prop

An interpretation is polynomial when every operation is given by a polynomial in its arguments.

theorem Cslib.Circuits.isPolynomial_affineInterpretation {F : Type u} [CommSemiring F] : (affineInterpretation F).IsPolynomial

The affine basis is polynomial.

theorem Cslib.Circuits.isPolynomial_arithInterpretation {F : Type u} [CommSemiring F] : (arithInterpretation F).IsPolynomial

The arithmetic basis is polynomial.

theorem Cslib.Circuits.Circuit.fanInAtMost_two_arith {F : Type u} {n m : ℕ} (c : Circuit (arithSignature F) n m) : c.FanInAtMost 2

Arithmetic circuits have fan-in at most two.