Polynomial interpretations and their formal wire values

An interpretation is polynomial when each gate operation agrees everywhere with a multivariate polynomial in its argument slots. The signature may contain arbitrarily many operations and constants, with no degree bound. Formal substitution assigns a polynomial to every original circuit wire. Its degree-one coefficient vector will provide a local linear realization without changing the program graph.

def Algebraic.Cutwidth.MultiOutput.Polynomial.IsPolynomial {F : Type u_1} [CommSemiring F] {σ : Signature} (I : Interpretation σ F) : Prop

Every operation is represented by a polynomial in its argument slots.

Equations

• Algebraic.Cutwidth.MultiOutput.Polynomial.IsPolynomial I = ∀ (op : σ.Op), ∃ (q : MvPolynomial (Fin (σ.Arity op)) F), ∀ (x : Fin (σ.Arity op) → F), I op x = (MvPolynomial.eval x) q

def Algebraic.Cutwidth.MultiOutput.Polynomial.signature (F : Type u_2) [CommSemiring F] : Signature

The signature containing every finite-arity polynomial over the coefficient field.

Equations

• Algebraic.Cutwidth.MultiOutput.Polynomial.signature F = { Op := (arity : ℕ) × MvPolynomial (Fin arity) F, Arity := Sigma.fst }

noncomputable def Algebraic.Cutwidth.MultiOutput.Polynomial.interpretation (F : Type u_2) [CommSemiring F] : Interpretation (signature F) F

A polynomial operation evaluates its displayed polynomial.

Equations

• Algebraic.Cutwidth.MultiOutput.Polynomial.interpretation F op x = (MvPolynomial.eval x) op.snd

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.isPolynomial_interpretation {F : Type u_1} [CommSemiring F] : IsPolynomial (interpretation F)

The full polynomial signature has a polynomial interpretation.

noncomputable def Algebraic.Cutwidth.MultiOutput.Polynomial.IsPolynomial.gatePolynomial {F : Type u_1} [CommSemiring F] {σ : Signature} {I : Interpretation σ F} (hI : IsPolynomial I) (op : σ.Op) : MvPolynomial (Fin (σ.Arity op)) F

A chosen polynomial representing one operation.

Equations

• hI.gatePolynomial op = ⋯.choose

noncomputable def Algebraic.Cutwidth.MultiOutput.Polynomial.IsPolynomial.formalInterpretation {F : Type u_1} [CommSemiring F] {σ : Signature} {I : Interpretation σ F} (hI : IsPolynomial I) (n : ℕ) : Interpretation σ (MvPolynomial (Fin n) F)

Formal substitution of wire polynomials into each gate polynomial.

Equations

• hI.formalInterpretation n op args = (MvPolynomial.aeval args) (hI.gatePolynomial op)

noncomputable def Algebraic.Cutwidth.MultiOutput.Polynomial.IsPolynomial.wirePolynomial {F : Type u_1} [CommSemiring F] {σ : Signature} {n s : ℕ} {I : Interpretation σ F} (hI : IsPolynomial I) (p : Program σ n s) : Wire n s → MvPolynomial (Fin n) F

The polynomial carried by each original input or gate wire.

Equations

• hI.wirePolynomial p = p.trace (hI.formalInterpretation n) MvPolynomial.X

noncomputable def Algebraic.Cutwidth.MultiOutput.Polynomial.linearPart {n : ℕ} {F : Type u_2} [CommRing F] (q : MvPolynomial (Fin n) F) : Fin n → F

The linear coefficient vector, computed by formal differentiation at zero.

Equations

• Algebraic.Cutwidth.MultiOutput.Polynomial.linearPart q i = (MvPolynomial.eval fun (x : Fin n) => 0) ((MvPolynomial.pderiv i) q)

noncomputable def Algebraic.Cutwidth.MultiOutput.Polynomial.linearPolynomial {F : Type u_1} [CommSemiring F] {n : ℕ} (row : Fin n → F) : MvPolynomial (Fin n) F

The formal linear polynomial with the given coefficient row.

Equations

• Algebraic.Cutwidth.MultiOutput.Polynomial.linearPolynomial row = ∑ i : Fin n, MvPolynomial.C (row i) * MvPolynomial.X i