Zulip Chat Archive

Stream: new members

Topic: Noncomputable polynomials


view this post on Zulip Daan van Gent (Aug 30 2020 at 15:22):

I am trying to define polynomial runtime of Turing machines and I encountered the following error
definition 'p' is noncomputable, it depends on 'polynomial.semiring'.
A minimal working example is
def p : polynomial ℕ := 1.
How do I avoid this error without making computability theory non-computable?

view this post on Zulip Kenny Lau (Aug 30 2020 at 15:28):

what's wrong with making computability theory non-computable?

view this post on Zulip Daan van Gent (Aug 30 2020 at 15:31):

I don't know what the boon of computability is in lean, but I figured it would be better. Either way, it seems a bit silly that polynomial evaluation is non-computable.

view this post on Zulip Mario Carneiro (Aug 30 2020 at 22:30):

The thing that is computable is the TM, not the bound

view this post on Zulip Mario Carneiro (Aug 30 2020 at 22:33):

Polynomials used to be computable, but for multivariate polynomials specifically, you need decidable equality on the type to be able to tell monomials apart, and these assumptions caused problems for regular proofs. If you want a special computable type for univariate polynomials on nat, define it yourself and prove equivalence to the usual one

view this post on Zulip Pim Spelier (Sep 01 2020 at 20:40):

I've been looking at this a bit, and I'm having a hard time finding out the underlying reason why polynomial/basic.lean starts with noncomputable theory. Apparently add_monoid_algebra's are noncomputable, because add_comm_monoid's are noncomputable, but then I can't find why those are noncomputable.

view this post on Zulip Pim Spelier (Sep 01 2020 at 20:40):

I'm asking, because I don't think it's a good idea to just copy the files I need, replace R by nat everywhere, and remove the noncomputable theory.

view this post on Zulip Patrick Massot (Sep 01 2020 at 20:40):

Because we tried computable polynomials and it was HELL.

view this post on Zulip Pim Spelier (Sep 01 2020 at 20:41):

I was wondering (but I don't know how this would work) if it's possible to only make the theory noncomputable if the semiring is noncomputable?

view this post on Zulip Reid Barton (Sep 01 2020 at 20:42):

This is exactly how you get into trouble. Because then the definition of operations (like addition or whatever) depends on how you compute things (mainly equality to zero) in the semiring.

view this post on Zulip Reid Barton (Sep 01 2020 at 20:43):

And then someone who says "I don't care about this computability stuff, just use classical to decide everything" gets a different notion of addition.

view this post on Zulip Reid Barton (Sep 01 2020 at 20:44):

It's also possible to evaluate some operations (like the ring operations, and evaluation) without needing any decidable equality, but it requires a different representation than the one mathlib currently uses

view this post on Zulip Mario Carneiro (Sep 01 2020 at 20:45):

Also, even back in the days of computable polynomials, the actual computation method is pretty terrible

view this post on Zulip Mario Carneiro (Sep 01 2020 at 20:45):

For univariate polynomials over nat you can do a lot better with the obvious algorithm

view this post on Zulip Reid Barton (Sep 01 2020 at 20:47):

Actually we might even have the correct constructive definition (the free R-algebra on the set of variables as generators) somewhere in mathlib.

view this post on Zulip Mario Carneiro (Sep 01 2020 at 20:49):

I would actually suggest the list_blank representation (which is already being used for TMs) instead of finitely supported functions

view this post on Zulip Mario Carneiro (Sep 01 2020 at 20:49):

The free R-algebra has the problem that things never get reduced

view this post on Zulip Mario Carneiro (Sep 01 2020 at 20:50):

it's good for constructive math but not computation

view this post on Zulip Reid Barton (Sep 01 2020 at 20:50):

right, that one also works I think for single variable polynomials--I'm pretty sure using a quotient somewhere is essential

view this post on Zulip Pim Spelier (Sep 01 2020 at 20:51):

Reid Barton said:

This is exactly how you get into trouble. Because then the definition of operations (like addition or whatever) depends on how you compute things (mainly equality to zero) in the semiring.

Not sure I understand it. Any two terms of decidable x=0 are equal right? Whether you get them through choice or through decidable_eq on the semiring. So how does the definition of operations depend on how you compute these kinds of terms?

view this post on Zulip Reid Barton (Sep 01 2020 at 20:53):

They're equal but not definitionally equal

view this post on Zulip Reid Barton (Sep 01 2020 at 20:56):

So the effect is that rfl stops working for no apparent reason.

view this post on Zulip Mario Carneiro (Sep 01 2020 at 20:56):

IIRC the main problem was not lack of defeq but rather really slow typeclass inference for everything depending on polynomials

view this post on Zulip Scott Morrison (Sep 01 2020 at 22:01):

On the other hand, the tweaks we made to typeclass inference that halved the compilation time of mathlib were made after we made polynomials classical. Who knows if those problems would have gone away?


Last updated: May 16 2021 at 20:13 UTC