## Stream: new members

### Topic: Noncomputable polynomials

#### 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?

#### Kenny Lau (Aug 30 2020 at 15:28):

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

#### 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.

#### Mario Carneiro (Aug 30 2020 at 22:30):

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

#### 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

#### 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.

#### 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.

#### Patrick Massot (Sep 01 2020 at 20:40):

Because we tried computable polynomials and it was HELL.

#### 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?

#### 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.

#### 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.

#### 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

#### Mario Carneiro (Sep 01 2020 at 20:45):

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

#### Mario Carneiro (Sep 01 2020 at 20:45):

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

#### 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.

#### 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

#### Mario Carneiro (Sep 01 2020 at 20:49):

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

#### Mario Carneiro (Sep 01 2020 at 20:50):

it's good for constructive math but not computation

#### 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

#### 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?

#### Reid Barton (Sep 01 2020 at 20:53):

They're equal but not definitionally equal

#### Reid Barton (Sep 01 2020 at 20:56):

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

#### 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

#### 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