[draft] Polynomial

[samparkky]

This draft pull request introduces a new way to represent a polynomial over commutative ring -- as a vector over the commutative ring -- and a proof that polynomials themselves make up a commutative ring.

[jamesmckinna]

Zeroth thoughts:

• thanks for the contribution!
• It's complicated, though, given that we already have at least one such representation (in the RingSolver architecture, based on an optimised Horner normal form, IIRC), and committing the namespace to have Algebra.Polynomial be the home for this presentation of the dense representation, while natural, seems ... premature without further discussion. I might tentatively suggest Algebra.Polynomial.Dense.* as a better root path for these additions?
• if it is indeed 'draft', then it would be helpful to avoid any premature detailed review by marking it as such.

First thoughts:

• there is no need to base this on CommutativeRing: the only place that I can see where *-comm is used is in the shift lemmas for multiplication, where one of the arguments is 0#, and 0# commutes with everything multiplicatively (as does 1#...); the use of Consequences to streamline proofs in the presence of commutativity is a short-cut, but not actually necessary, IIUC
• so: suggest at least that the PR be refactored to base on Ring, with additional properties when multiplication is Commutative

Second thought:

• no need for subtraction/unary negation either! So please consider doing this for Semiring instead? Indeed, the stdlib style might be to try to identify the minimal axiomatisation for which Polynomial makes sense, and build up from there. This PR makes a lot of commitments (esp. to naming) which might prove costly to refactor if we wanted to generalise later?

Third thought:

• (but this could be added downstream) any version of Polynomial ought at least to have (some version of) its characteristic universal property, or even simply eval given an element of the underlying Carrier?

Fourth thoughts:

• ergonomics: which version of Vec works best? the 'structural' account (Vec as you have it), or the 'functional' account (as in Data.Vec.Functional); or even a bounded version for normalising away leading zeroes? It's possible that each of these would require cast in order to state, and prove, basic properties, but should be investigated further...
• some of your cast lemmas, as well as some of the actual suc/pred arithmetic, may already be present in the library, and it might be sensible to refactor to lift any missing others out as Data.Vec.Properties and Data.Nat.Properties?

[Taneb]

I've been working on a slightly different implementation of this. Let me find what I've done and compare - notably, I used lists rather than vectors, and didn't have a notion of degree

[Taneb]

@jamesmckinna

there is no need to base this on CommutativeRing: the only place that I can see where *-comm is used is in the shift lemmas for multiplication, where one of the arguments is 0#, and 0# commutes with everything multiplicatively (as does 1#...); the use of Consequences to streamline proofs in the presence of commutativity is a short-cut, but not actually necessary, IIUC

I think you need commutativity of multiplication to show that polynomial evaluation preserves multiplication

[jamesmckinna]

@Taneb

there is no need to base this on CommutativeRing: the only place that I can see where *-comm is used is in the shift lemmas for multiplication, where one of the arguments is 0#, and 0# commutes with everything multiplicatively (as does 1#...); the use of Consequences to streamline proofs in the presence of commutativity is a short-cut, but not actually necessary, IIUC

I think you need commutativity of multiplication to show that polynomial evaluation preserves multiplication

Hmmm. https://math.stackexchange.com/questions/806119/do-polynomials-make-sense-over-non-commutative-rings

Otherwise could we even speak about polynomials over rings such as square matrices (for the Cayley-Hamilton theorem, for example, even if that's usually only considered for matrices over commutative rings, such matrices don't enjoy commutative multiplication... while for any polynomial and its values, it is the case that powers of an element do commute...)?

I think the real issue is making sure that multiplication is defined correctly... see also https://en.wikipedia.org/wiki/Monoid_ring

[JacquesCarette]

Non-commutative polynomial rings certainly do make sense and are useful. See for examples the skew polynomials that arise when modeling various kinds of operators.

Axiom does allow polynomials over coefficients rings like square matrices.

[Taneb]

For reference, here's my implementation of polynomials: https://gist.github.com/Taneb/3257f47436ec6b11de403d839d7c413b

[samparkky]

Thank you for the detailed feedback and the comments and I apologize for the delayed response. Although it will take some time, I will try implement the changes using the semiring instead of the commutative ring and eventually prove the universal property of polynomial rings. Since this is only a draft which I should have made it clear, any further comments or suggestions are welcome.

[gallais]

Given that we have very few (scaling & shifting) degree-respecting operations, that our notions of addition or equality are heterogeneous, do we really need to have an index-enforcing representation? Especially if it forces us to have a bunch of cast all over the place?

How about defining degree as a function (maybe even one that disregards irrelevant 0#s for semiring where that's decidable) and proving its properties separately?