Zulip Chat Archive

Stream: maths

Topic: constructive polynomials

Reid Barton (Oct 12 2019 at 17:59):

I know polynomials were changed to use classical logic, and that's fine, but it occurred to me that there is a constructively correct notion of $R[X]$ , and it isn't the one we were using (unless $R$ has decidable equality).

Johan Commelin (Oct 12 2019 at 18:06):

Which is...

Reid Barton (Oct 12 2019 at 18:07):

Namely, you can either take some free construction, or you can work with list R modulo the relation of adding 0s to the end of the list, and I think these are constructively equivalent. Moreover, all the polynomial operations can be implemented without using equality on R aside from decidable equality of polynomials (obviously) and degree (slightly less obviously, but also clearly correctly, since deg (1 + (a - b) * X) is 0 iff a = b).

Reid Barton (Oct 12 2019 at 18:09):

The second one is also a lot more reasonable for computation than the current representation, since addition is linear and not quadratic for example

Reid Barton (Oct 12 2019 at 18:09):

I'm not sure whether there is a compelling reason to switch at this point though

Johan Commelin (Oct 12 2019 at 18:12):

This doesn't easily generalize to mv_poly right?

Johan Commelin (Oct 12 2019 at 18:13):

If anything, I would like to redefine polynomial R as mv_polynomial unit R, and make the two API play more in sync. There is lots of stuff that has to be done twice, and isn't done in exactly the same way, etc...

Reid Barton (Oct 12 2019 at 18:14):

The big free construction still works for mv_polynomial, and I think you can also do something more similar to the current implementation but constructively correct, but it won't be as nice as lists

Reid Barton (Oct 12 2019 at 18:19):

free_comm_ring is almost the "big free construction", except it needs to be free_algebra, and also use free_comm_monoid in place of multiset

Reid Barton (Oct 12 2019 at 18:19):

Or you can build it directly from the syntax of algebras

Patrick Massot (Oct 12 2019 at 18:24):

Reid, are you still checking your topology PR? It doesn't sound like it...

Reid Barton (Oct 12 2019 at 18:29):

I discovered that there were a sizable number of irrelevant universe parameter order changes, so I "fixed" them and rebuilt

Reid Barton (Oct 12 2019 at 18:32):

Oh sorry, I misremembered how multiset is implemented. It is actually the correct thing already.

Patrick Massot (Oct 12 2019 at 18:32):

So, do you think we can merge?

Kenny Lau (Oct 13 2019 at 00:44):

@Reid Barton the constructive polynomials on R is R (x)_Z Z[x]

Yury G. Kudryashov (Oct 18 2019 at 01:22):

@Johan Commelin One-variable polynomials can be evaluated on non-commutative rings (e.g., matrices or bounded linear operators; not sure if this is implemented in mathlib), and it can't work with mv_polynomial.

Johan Commelin (Oct 18 2019 at 05:10):

Hmm, fair enough

Johan Commelin (Oct 18 2019 at 05:11):

So you are saying that polynomial should be defined as mv_noncomm_polynomial unit?

Yury G. Kudryashov (Oct 19 2019 at 14:24):

AFAIK, we don't have mv_noncomm_polynomial (yet).

Yury G. Kudryashov (Oct 19 2019 at 14:28):

Probably I'd prefer to have a few monoids of monomials, and let *_polynomial be monoid_algebra monomials_type.

Yury G. Kudryashov (Oct 19 2019 at 14:28):

Where monoid_algebra is https://en.wikipedia.org/wiki/Group_ring for monoids instead of groups (I'm not sure what is the right word for this).

Kevin Buzzard (Oct 19 2019 at 15:41):

I've heard it being called "monoid ring" before

Mario Carneiro (Oct 19 2019 at 16:22):

I recall Kenny having a formalization of polynomials using quotients of ring expressions that is pretty constructive

Johan Commelin (Oct 19 2019 at 16:39):

@Yury G. Kudryashov I think finsupp already allows you to do monoid rings

Johan Commelin (Oct 19 2019 at 16:40):

It's been a while that I read that part of the source though

Last updated: Dec 20 2023 at 11:08 UTC