Noncomputable polynomials

Stream: new members

[Daan van Gent]

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]

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

[Daan van Gent]

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]

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

[Mario Carneiro]

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]

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]

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]

Because we tried computable polynomials and it was HELL.

[Pim Spelier]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

it's good for constructive math but not computation

[Reid Barton]

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

[Pim Spelier]

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]

They're equal but not definitionally equal

[Reid Barton]

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

[Mario Carneiro]

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

[Scott Morrison]

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?