Polynomial gates over commutative algebras: definitions

A program whose gates are polynomials with coefficients in a commutative ring K can be run over every commutative K-algebra A: each operation substitutes its arguments into its gate polynomial. This file fixes the notation for that formal semantics.

• algebraInterpretation P A: the interpretation over A in which the operation op substitutes its arguments into the polynomial P op.
• wirePolynomial P p w: the polynomial in the inputs carried by the wire w, the value of w over the polynomial ring K[X₀, …, X_{n-1}] at the variables.
• FormallyComputes P c f: every output wire of c carries the polynomial f o. This is the usual notion of an arithmetic circuit computing a polynomial; over an infinite field it agrees with computing the polynomial function.
• arithmeticPolynomial constant: the gate polynomials X₀ + X₁, X₀ X₁ and the constants of arithmetic circuits (Arithmetic.signature).
• jacobian f a and hessian g a: the matrices of first partial derivatives of a family of polynomials and of second partial derivatives of one polynomial, evaluated at a point a of a K-algebra L.

The gate polynomials may be arbitrary: any degree, any coefficients, any arity.

noncomputable def Algebraic.Cutwidth.MultiOutput.Taylor.algebraInterpretation {K : Type u_1} [CommSemiring K] {σ : Signature} (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) (A : Type u_2) [CommSemiring A] [Algebra K A] : Interpretation σ A

The interpretation over a commutative K-algebra A in which each operation op substitutes its arguments into its gate polynomial P op.

Equations

• Algebraic.Cutwidth.MultiOutput.Taylor.algebraInterpretation P A op x = (MvPolynomial.aeval x) (P op)

noncomputable def Algebraic.Cutwidth.MultiOutput.Taylor.wirePolynomial {K : Type u_1} [CommSemiring K] {σ : Signature} {n s : ℕ} (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) (p : Program σ n s) : Wire n s → MvPolynomial (Fin n) K

The polynomial carried by each input or gate wire: its value over the polynomial ring at the variables.

Equations

• Algebraic.Cutwidth.MultiOutput.Taylor.wirePolynomial P p = p.trace (Algebraic.Cutwidth.MultiOutput.Taylor.algebraInterpretation P (MvPolynomial (Fin n) K)) MvPolynomial.X

def Algebraic.Cutwidth.MultiOutput.Taylor.FormallyComputes {K : Type u_1} [CommSemiring K] {σ : Signature} {n m : ℕ} (P : (op : σ.Op) → MvPolynomial (Fin (σ.Arity op)) K) (c : Circuit σ n m) (f : Fin m → MvPolynomial (Fin n) K) : Prop

A circuit with gate polynomials P formally computes the polynomials f when its output o carries the polynomial f o.

Equations

• Algebraic.Cutwidth.MultiOutput.Taylor.FormallyComputes P c f = ∀ (o : Fin m), Algebraic.Cutwidth.MultiOutput.Taylor.wirePolynomial P c.program (c.outputs o) = f o

noncomputable def Algebraic.Cutwidth.MultiOutput.Taylor.arithmeticPolynomial {K : Type u_1} [CommSemiring K] {Kc : Type u_2} (constant : Kc → K) (op : (Arithmetic.signature Kc).Op) : MvPolynomial (Fin ((Arithmetic.signature Kc).Arity op)) K

The gate polynomials of arithmetic circuits: addition is X₀ + X₁, multiplication is X₀ X₁, and a constant symbol is the constant polynomial of its value.

Equations

• Algebraic.Cutwidth.MultiOutput.Taylor.arithmeticPolynomial constant Algebraic.Arithmetic.Op.add = MvPolynomial.X 0 + MvPolynomial.X 1
• Algebraic.Cutwidth.MultiOutput.Taylor.arithmeticPolynomial constant Algebraic.Arithmetic.Op.mul = MvPolynomial.X 0 * MvPolynomial.X 1
• Algebraic.Cutwidth.MultiOutput.Taylor.arithmeticPolynomial constant (Algebraic.Arithmetic.Op.constant c) = MvPolynomial.C (constant c)

noncomputable def Algebraic.Cutwidth.MultiOutput.Taylor.jacobian {K : Type u_1} [CommSemiring K] {n : ℕ} {ι : Type u_2} {L : Type u_3} [CommSemiring L] [Algebra K L] (f : ι → MvPolynomial (Fin n) K) (a : Fin n → L) : Matrix ι (Fin n) L

The Jacobian matrix of a family of polynomials at a point a: the entry in row o and column j is ∂ f o / ∂ X j evaluated at a.

Equations

• Algebraic.Cutwidth.MultiOutput.Taylor.jacobian f a = Matrix.of fun (o : ι) (j : Fin n) => (MvPolynomial.aeval a) ((MvPolynomial.pderiv j) (f o))

noncomputable def Algebraic.Cutwidth.MultiOutput.Taylor.hessian {K : Type u_1} [CommSemiring K] {n : ℕ} {L : Type u_2} [CommSemiring L] [Algebra K L] (g : MvPolynomial (Fin n) K) (a : Fin n → L) : Matrix (Fin n) (Fin n) L

The Hessian matrix of a polynomial at a point a: the entry in row i and column j is ∂² g / ∂ X i ∂ X j evaluated at a.

Equations

• Algebraic.Cutwidth.MultiOutput.Taylor.hessian g a = Matrix.of fun (i j : Fin n) => (MvPolynomial.aeval a) ((MvPolynomial.pderiv i) ((MvPolynomial.pderiv j) g))