Zulip Chat Archive

Stream: maths

Topic: constructive polynomials


view this post on Zulip 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]R[X], and it isn't the one we were using (unless RR has decidable equality).

view this post on Zulip Johan Commelin (Oct 12 2019 at 18:06):

Which is...

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 12 2019 at 18:09):

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

view this post on Zulip Johan Commelin (Oct 12 2019 at 18:12):

This doesn't easily generalize to mv_poly right?

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 12 2019 at 18:19):

Or you can build it directly from the syntax of algebras

view this post on Zulip Patrick Massot (Oct 12 2019 at 18:24):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 12 2019 at 18:32):

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

view this post on Zulip Patrick Massot (Oct 12 2019 at 18:32):

So, do you think we can merge?

view this post on Zulip Kenny Lau (Oct 13 2019 at 00:44):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 18 2019 at 05:10):

Hmm, fair enough

view this post on Zulip Johan Commelin (Oct 18 2019 at 05:11):

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

view this post on Zulip Yury G. Kudryashov (Oct 19 2019 at 14:24):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Oct 19 2019 at 15:41):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 19 2019 at 16:39):

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

view this post on Zulip Johan Commelin (Oct 19 2019 at 16:40):

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


Last updated: May 18 2021 at 06:15 UTC