nonconstructive polynomials

Stream: maths

[Kevin Buzzard]

Does anyone remember why polynomials went from constructive to nonconstructive many years ago? I remember that constructivism was causing problems but I don't remember what the problems were. I think the change happened in around 2019?

[Ruben Van de Velde]

That would be in #1391?

[Kevin Buzzard]

Oh nice -- thanks!

[Eric Wieser]

In my opinion, while polynomial maybe should be heavily classical, I don't see any reason finsupp should be.

[Kevin Buzzard]

It might be one of those situations like finset vs set.finite -- sometimes one works better than the other and there's no best option

[David Wärn]

This has been discussed many times before, but I'd like to repeat the constructivist point of view on this affair. What's really important about the polynomial ring $R[X]$ is its universal property -- it's the free $R$-algebra on one generator. In mathlib, we define $R[X]$ as the monoid algebra $R[M]$ where $M = \N$ -- again $R[M]$ should also have a universal property, and it's easy to show that $R[X]$ and $R[\N]$ have the same universal property. Then we define $R[M]$ using docs#finsupp as $M \to_0 R$. In general, $I \to_0 R$ should have the universal property of a coproduct of $I$-many copies of $R$ in the category of add_comm_monoids, and it's again easy to derive the universal property of $R[M]$ from that of $M \to_0 R$.

The bad news is that in order to prove the universal property of (mathlib's version of) $I \to_0 R$, we need decidable equality for both $I$ and $R$. (If one used the dependent version docs#dfinsupp instead, then we would only need decidable equality for $I$, but let's not worry about this.) This causes problems to do with decidable_eq not being definitionally proof irrelevant, so in #1391 the definitions were refactored so as to always use the classical proof of decidable equality. Hence 'polynomials are non-constructive in mathlib'.

The good news is that there's a perfectly sensible constructive definition of $I \to_0 R$ which does not need any decidable equality. For example you can take the abelianization of (an additive version of) docs#free_product. This way one represents polynomials as 'formal linear combinations of monomials' (quotiented appropriately) instead of representing them as functions. The universal property is somewhat tautological with this definition.

So, what would happen if we refactored mathlib to use the above constructive definition in place of finsupp / dfinsupp? Would this keep both constructive and classical users happy? I don't know. Certainly it would require a lot of effort. Either way I think it would be good to put more emphasis on the universal property of $I \to_0 R$. The current definition encourages users to look evaluate terms of $I \to_0 R$ at points $i : I$, which is sort of an API leak from my point of view and usually not the right thing to do.

[Mario Carneiro]

It's worth mentioning that #1391 points to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/timeout.20when.20working.20with.20ideal.20of.20polynomial.20ring as the discussion that lead to the decision

[Mario Carneiro]

FYI, Kenny had a prototype of the constructive free_product style polynomial ring at the time. IIRC people weren't happy with the fact that this made the definition less natural / obvious to work with

[Eric Wieser]

Is there any reason we should be treating $I \to_0 R$ and $R[X]$ in the same way, @David Wärn? I'd argue that evaluation of $I \to_0 R$ at $i : I$ is exactly what finsupp is for, as a finitely supported function is just a function with some extra properties; it's just not necessarily what polynomialshould be built around.

[Yaël Dillies]

Let me also say that "polynomials are noncomputable" really means "Lean's inbuilt computation fails on polynomials" because we very much can (and should) write our computation system. I'm of the opinion that decidable instances are just a bad way of handling computability (see Kyle's compute for a possible alternative) and that we shouldn't bother making stuff computable with respect to that standard.

[David Wärn]

Eric Wieser said:

Is there any reason we should be treating $I \to_0 R$ and $R[X]$ in the same way, David Wärn? I'd argue that evaluation of $I \to_0 R$ at $i : I$ is exactly what finsupp is for, as a finitely supported function is just a function with some extra properties; it's just not necessarily what polynomialshould be built around.

Yes I agree. It's not that finsupp is inherently problematic, it's just that most of the time when we use it in mathlib (to implement polynomial, mv_polynomial, monoid_algebra, or direct sums of vector spaces), there is an alternative which works better constructively.

[Bolton Bailey]

David Wärn said:

The good news is that there's a perfectly sensible constructive definition of $I \to_0 R$ which does not need any decidable equality. For example you can take the abelianization of (an additive version of) docs#free_product. This way one represents polynomials as 'formal linear combinations of monomials' (quotiented appropriately) instead of representing them as functions. The universal property is somewhat tautological with this definition.

I'm a bit nervous about this. Wouldn't this mean that if I tried to do ((1 + X)^40).eval 3, it would take time exponential in 40?

[Bolton Bailey]

Additionally, wasn't there some discussion of changing docs#to_poly to make it convert any vector into a polynomial? I'm wanting to have computable polynomials for my own work and I was thinking that just operating on vectors of coefficients instead could be a good way of sidestepping the issue.

[Junyan Xu]

David Wärn said:

The bad news is that in order to prove the universal property of (mathlib's version of) $I \to_0 R$, we need decidable equality for both $I$ and $R$. (If one used the dependent version docs#dfinsupp instead, then we would only need decidable equality for $I$, but let's not worry about this.)

For polynomials, I = ℕ, which has constructive decidable_eq, so indeed we needn't worry about this. My estimation is that bringing finsupp closer to dfinsupp will make polynomials much more amenable to computation.

[Junyan Xu]

By the way I evaluated (or rather, thought-experimented with) several approaches of redefining polynomial/finsupp a while ago, including close relatives of docs#free_product that uses multiset instead of list (which underlies docs#free_monoid) (Edit: not quite close; I use multiset of pairs of coefficient and degree, which is a key difference). As long as you use decidable_eq to combine like terms, you don't get exponential blowup when computing (1 + X)^40.

[David Wärn]

Bolton Bailey said:

I'm a bit nervous about this. Wouldn't this mean that if I tried to do ((1 + X)^40).eval 3, it would take time exponential in 40?

Yes, but it's no worse than the current situation where the computation is stuck. And you could still compute it using lemmas or tactics

[David Wärn]

There are at least three ways to define the 'coproduct of a family of add_comm_monoids':

• start from multiset (the free commutative monoid) and quotient by a homomorphism condition
• start from free_product and quotient by a commutativity condition (i.e. take the abelianization)
• start from list (the free monoid) and simultaneously quotient by homomorphism condition and a commutativity condition.

I would say all of these are really equivalent. What I like about this construction is that it seems to have all the advantages of the current classical definitions in mathlib (e.g. it's very general and doesn't rely on decidable_eq) without using any classical axioms. I would also argue that it's conceptually more natural

[David Wärn]

Basing polynomial on dfinsupp with a constructive proof of decidable_eq nat might also work, but I think this wouldn't work as well for mv_polynomial or other places where we currently use finsupp.

[Eric Wieser]

My impression is that the decidable_eq burden of finsupp lies with decidable equality of the codomain (which is needed to determine the support), rather than decidable_eq of the domain (which is usually either the naturals, or the set of variables for the polynomial)

[Yakov Pechersky]

@David Wärn is #15476 helpful?