Computable degree-bound polynomials

Stream: mathlib4

[Bolton Bailey]

I am approaching a point in my project where I would like to have my polynomials be computable, so I am thinking again about how we can make that happen. People have suggested that we introduce a new type, which is an idea I have resisted because I don't want to reprove the entire Polynomial API, and it feels like bifurcation.

It occurred to me, though, that the polynomials I am working with all always have an explicit upper bound on their degree. I thought maybe this could be a new type I could introduce, with the following benefits:

• I'm pretty sure that the definition would just be def degreeBound_polynomial {R} (n : nat) := Fin (n+1) -> R. I think this avoids the computability issue, which was previously mainly about not knowing whether certain terms cancelled out (because we needed to make a Finset of the nonzero terms). Now, these zero terms are just carried around.
• Now that we are in Lean 4, heterogeneous operators are, I understand, much easier. So it should be fine to define HMul (db_polynomial R a) (db_polynomial R b) (db_polynomial R (a+b))
• For the applications that I in particular am working on, it would be fine, I think, since the degree-bound exists for all the polynomials I use anyway.
• Thinking in terms of security for cryptography, this makes it more likely that code written using this type is constant time, thus making timing-based side-channel attacks less likely (though side-channel attacks are a complicated area and there's much I don't understand about them).
• Perhaps we can someday make a computable polynomial out of equivalence classes of these?

Potential Cons

• Issues with db_polynomial R (a+b) not having the same type as db_polynomial R (b+a).
• For polynomials whose actual degree is much less than the bound, equality comparisons are more expensive than they have to be.

Any thoughts on this?

[Chris Hughes]

Representing arrays as functions Fin n -> R can be extremely slow depending on what sort of computation you want to do. The coefficients won't actually be stored, the only thing stored will be the function that computes them, which could become extremely complicated quite quickly. I think I once tried matrices in a similar way, and it's super slow because if for example you try to invert a matrix, then each time you access an element of this matrix it will recompute the inverse. You should probably use Array or Vector or List instead.

[Kevin Buzzard]

Could this be the cause of the slowness in lean4#2564 ? Some not-that-slow thing being done millions of times?

[Mario Carneiro]

I suspect that it is possible to normalize Fin n -> R functions in some way such that all the values are precomputed and the function is just fun i => array.get i on an array thunk

[Mario Carneiro]

@Kevin Buzzard Kernel computation automatically memoizes everything, so I don't think this is sufficient to explain the situation there

[Mario Carneiro]

It's just #eval computation that suffers from the issue Chris is highlighting

[Bolton Bailey]

Chris Hughes said:

You should probably use Array or Vector or List instead.

Vector would be the appropriate one, since it comes with a built-in length. Does Vector have an Add instance though?

[Eric Wieser]

Why do you want the length in the type?

[Bolton Bailey]

Isn't that what we're discussing here?

[Bolton Bailey]

I guess you're proposing a degree bound polynomial type that is equivalent to List? I suppose that could work. The downside I see is that if I want to write something like P is true of all polynomials with degree bound 10, it's written like forall (p : DBpolynomial R), p.degree_bound < 10 -> P p rather than forall (p : DBPolynomial R 10), P p

[Bolton Bailey]

It also feels confusing for [1, 0] to be of the same type as [1], since they are not equal, but they correspond to the same polynomial.

[Bolton Bailey]

I think one of the previous proposals for computable polynomials was through setoids on lists, I guess this is another way to fix all this. I had a PR !3#16160 building to this.

[Eric Wieser]

Bolton Bailey said:

I guess you're proposing a degree bound polynomial type that is equivalent to List?

I'm not going as far as proposing it; simply asking why you're proposing something different

[Mario Carneiro]

Q: What kind of computation are you doing with these polynomials? Does norm_num / ring computation suffice? (in which case you might just be able to use regular polynomials)

[Bolton Bailey]

I guess to elaborate more, you can look at this comment. Note that I've written it one way in Lean, but if you look at the reference, everything is written using a special notation for the set of polynomials with degree below a certain value. So it feels like there should be a def of some kind for this concept.

[Mario Carneiro]

Isn't there already a definition for bounded degree polynomials?

[Mario Carneiro]

degreeLE or something

[Bolton Bailey]

Mario Carneiro said:

Q: What kind of computation are you doing with these polynomials? Does norm_num / ring computation suffice? (in which case you might just be able to use regular polynomials)

I'd like to be able to write code that manipulates the polynomials and then returns other polynomials/evaluations of polynomials, I don't want to just prove things.

[Mario Carneiro]

can you be more specific?

[Mario Carneiro]

any concrete code manipulating polynomial-like objects almost certainly will need to invent its own data structures for the polynomials

[Mario Carneiro]

especially if everything is bounded degree, that's a specialized situation where you can do much better by using custom data structures

[Bolton Bailey]

Mario Carneiro said:

any concrete code manipulating polynomial-like objects almost certainly will need to invent its own data structures for the polynomials

Right, because mathlib's polynomials aren't computable, so I am looking for a good way to make a new data structure that can go in mathlib which I can manipulate.

[Mario Carneiro]

what's the actual application? Can you give an example?

[Mario Carneiro]

the design of a data structure for computational purposes is very tightly coupled to the algorithm in which it is being used

[Bolton Bailey]

You're not the first person to suggest this to me. But if a paper describes an algorithm using polynomials, I'd like to be able to use mathlib's Polynomial type to implement it.

[Bolton Bailey]

I am working on a verified implementation of this paper

[Bolton Bailey]

An example of a polynomial operation that I need to be able to do: I am given three polynomials a b c over a finite field such that a * b - c = 0 on some subgroup of the field. I want to be able to compute the polynomial (a * b - c)/V, where V is the monic polynomial whose roots are the subgroup.

[Bolton Bailey]

(I'm actually noticing now that the degree-bound won't work for this, since V = X^|H| - 1 is asymptotically slower to divide by if it's represented as a huge vector.)

[Mario Carneiro]

are these in the quotient ring R[X]/V?

[Mario Carneiro]

yeah, if you actually want to get the asymptotic order right for a complicated paper like that you will have to implement all the tricks

[Bolton Bailey]

Well a,b,c are all Lagrange interpolants of arbitrary functions from the subgroup H to the field, so a * b has degree larger than |H|.

[Yuyang Zhao]

I may need R[X]/(X^n-1) for my FFT.

[Mario Carneiro]

saying that an algorithm "uses polynomials" is to me a bit analogous to "using graphs". It's a conceptual language for describing the program, but it is only tenuously related to the actual implementation and a naive implementation will be completely impractical

[Mario Carneiro]

We can certainly have a type for doing naive calculations with polynomials, but most applications will want something better

[Eric Wieser]

Mario Carneiro said:

We can certainly have a type for doing naive calculations with polynomials

Is there any reason not to make Polynomial be that type?

[Mario Carneiro]

It was, once upon a time

[Mario Carneiro]

but people didn't like the decidability assumptions

[Eric Wieser]

(related wiki page)

[Eric Wieser]

I assume the "once upon a time" is the first column of that table

[Mario Carneiro]

I believe so

[Mario Carneiro]

(we have a new entry for the list of zulip conversations)

[Kevin Buzzard]

Mathlib already has an algorithm for dividing a polynomial by its roots, you just do division with remainder and prove there's no remainder.

[Bolton Bailey]

I am ok with implementing the tricks, but I'd like to implement them in a type that I can put in mathlib when I'm done.

Mario Carneiro said:

but people didn't like the decidability assumptions

This is sort of the point of this whole suggestion. It can be another type that doesn't interfere with Polynomial, but which the people who want computability can use.

[Bolton Bailey]

I guess that fact that the type actually already does exist in mathlib hampers this.

[Mario Carneiro]

are they univariate polynomials? This also simplifies things a lot

[Bolton Bailey]

Mario Carneiro said:

are they univariate polynomials? This also simplifies things a lot

Erf, it's complicated. There are lots of "sparse" bivariate polynomials, but I guess they're all ultimately represented in the concrete algorithms as univariate polynomials, yes.

[Bolton Bailey]

Yuyang Zhao said:

I may need R[X]/(X^n-1) for my FFT.

Also, it's worth noting that the "tricks" we are talking about are essentially always discrete Fourier transforms, so I'm always interested to know more about FFT work for this reason. Do you have a PR?

[Mario Carneiro]

I would just do unbounded-degree univariate polynomials over a DecidableEq ring by using Array and keeping the tail trimmed

[Mario Carneiro]

and then you can implement bounded-degree multiplication in the quotient ring by polynomial division with that underlying representation

[Mario Carneiro]

that seems like a reasonable compromise between flexibility and performance that could fit as a mathlib type

[Bolton Bailey]

I guess the best way for me to start on that then is maybe to revive my setoid list PR, possibly with more decidability assumptions.

[Yuyang Zhao]

Bolton Bailey said:

Yuyang Zhao said:

I may need R[X]/(X^n-1) for my FFT.

Also, it's worth noting that the "tricks" we are talking about are essentially always discrete Fourier transforms, so I'm always interested to know more about FFT work for this reason. Do you have a PR?

No, it's still on my todo list. I'm still thinking about how to make it easier to prove the correctness of an (not naturally functional) algorithm with as little loss of efficiency and generality as possible. Maybe I'm too perfectionistic. :smiling_face_with_tear: