Affine, polynomial, and arithmetic bases

Three ways of computing over a field F:

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

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

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

@[reducible, inline]

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

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

Equations

• Complexity.Frontier.affineSignature F = { Op := (k : ℕ) × (Fin k → F) × F, Arity := fun (o : (k : ℕ) × (Fin k → F) × F) => o.fst }

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

An affine operation computes x ↦ ∑ i, a i * x i + b.

Equations

• Complexity.Frontier.affineInterpretation F o x = ∑ i : Fin o.fst, o.snd.1 i * x i + o.snd.2

inductive Complexity.Frontier.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 Complexity.Frontier.ArithOp.arity (F : Type u) : ArithOp F → ℕ

The arity of an arithmetic operation.

Equations

• Complexity.Frontier.ArithOp.arity F Complexity.Frontier.ArithOp.add = 2
• Complexity.Frontier.ArithOp.arity F Complexity.Frontier.ArithOp.mul = 2
• Complexity.Frontier.ArithOp.arity F (Complexity.Frontier.ArithOp.const c) = 0

@[reducible, inline]

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

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

Equations

• Complexity.Frontier.arithSignature F = { Op := Complexity.Frontier.ArithOp F, Arity := Complexity.Frontier.ArithOp.arity F }

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

Addition, multiplication, and constants.

Equations

• Complexity.Frontier.arithInterpretation F Complexity.Frontier.ArithOp.add x_2 = x_2 0 + x_2 1
• Complexity.Frontier.arithInterpretation F Complexity.Frontier.ArithOp.mul x_2 = x_2 0 * x_2 1
• Complexity.Frontier.arithInterpretation F (Complexity.Frontier.ArithOp.const c) x_2 = c

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

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

Equations

• Complexity.Frontier.IsPolynomial I = ∀ (o : σ.Op), ∃ (P : MvPolynomial (Fin (σ.Arity o)) F), ∀ (x : Fin (σ.Arity o) → F), I o x = (MvPolynomial.eval x) P

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

Arithmetic circuits are polynomial.

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

The affine basis is polynomial.