Computable Polynomials

Stream: CSLib

[Bolton Bailey]

I have been working on implementation of Turing machines with composition in CSLib#269. I noticed that I was asked to make some of my definitions noncomputable due to the underlying noncomputability of Mathlib's Polynomial type, which has been discussed on this zulip many times before. I'm also aware that some libraries of noncomputable polynomials have been implemented, for example this one. Perhaps computability will be more important to a computer science library than a math library. Should CSLib attempt to use a computable polynomial implementation in view of this?

[Shreyas Srinivas]

Where do polynomials enter the picture in TM composition? Also are you extending Mathlib defs of Turing Machines?

[Ching-Tsun Chou]

Why does it matter if some of your definitions are noncomputable?

[Bolton Bailey]

Where do polynomials enter the picture in TM composition?

They don't enter into Turing machine composition itself (I guess I should have been more clear about this) but the PR also includes a proof that compositions of polynomial time Turing machines are polynomial time, and that is the point at which Polynomial enters.

Also are you extending Mathlib defs of Turing Machines?

In this case, I have not been extending the Mathlib defs of Turing machines because in various ways, I have found them hard to work with / I have a view to generalizing them in a finer-grained ways that seem incompatible with using a lot of the data structures as written.

Why does it matter if some of your definitions are noncomputable?

Well, I guess I am asking if it does. Mathlib has gotten a long way without being very concerned about code generation, but it strikes me that a computer science library might have more reason to be concerned about this for the reason that it is perhaps more integrated with uses of computers that produce runnable code. Given that CSLib is still relatively new, I am wondering if it is a good idea to try to keep code computable as much as possible in anticipation of this, or if the people interested in CSLib feel it would be best to not worry about it.

[Ching-Tsun Chou]

Unless you are generating code from the polynomials themselves, I really don't see why you should care about whether the polynomials are "computable". Even if you are generating code from the Turing machines, I don't see why any complexity results about the TMs proved using "noncomputable" polynomials would be any less valid simple because the polynomials are "noncomputable".

[Snir Broshi]

Bolton Bailey said:

it strikes me that a computer science library might have more reason to be concerned about this for the reason that it is perhaps more integrated with uses of computers that produce runnable code.

I'm generally in favor of computable polynomials (specifically MvPolynomial), but this reminds me of a famous quote:

Computer science is no more about computers than astronomy is about telescopes. ~ Edsger Dijkstra

[Snir Broshi]

Also I think Mathlib would be more intersted in computable polynomials than CSLib; they're great for algorithms in symbolic maths, e.g. finding a minimal polynomial of an expression using a Gröbner basis.

[Shreyas Srinivas]

I don’t think mathlib cares about computing with computable polynomials. Why reinvent CAS in lean for practical use, when existing CAS tools already do the job better

[Shreyas Srinivas]

They might want computable polynomials if there are mathematical use cases for them

[Snir Broshi]

I disagree that CAS tools are fine as-is. I believe Mathlib should subsume CAS.
But whether you agree doesn't change the claim that Mathlib is more suited to want them, precisely because of this. I'm not the only one that wants CAS; #Computer algebra

[Derek Sorensen]

We are working on computable polynomials in Lean! :slight_smile: https://github.com/Verified-zkEVM/CompPoly our use case is for zkVMs but feel free to reach out, the idea is to have a computable version of the mathlib polynomials. this is a successor to the repo you pointed to @Bolton Bailey

[Shreyas Srinivas]

Verifying CAS is definitely interesting. But there is the gap between algorithms that are easy to verify and algorithms which are efficient

[Derek Sorensen]

Our medium-term goal has been to propose an upstream to CSLib once this is in good shape

[Derek Sorensen]

we have basic definitions of uni- and multivariate polynomials rn but still have some way to go to get the typeclasses right, ring isomorphisms, and some efficient implementations of e.g. interpolation, FFT/NTT, etc etc

[Derek Sorensen]

contributions are welcome!!

[Derek Sorensen]

(by "our" I mean the Ethereum Foundation btw)

[Shreyas Srinivas]

Oh hi Derek nice to meet you here after all these years. What representation do you use?

[Alexander Hicks]

Re: mathlib, I believe if one digs through the zulip archives there have been past discussions about computable polynomials and why we shouldn't expect them to show up in mathlib (unless something changes...), which I think is fine, but I definitely think CSLib should aim to be computable wherever possible, if only by introducing lemmas showing equivalence between a noncomputable object with a computable one (as was done in CompPoly to related computable polynomials to the those of mathlib and their associated theory).

[Shreyas Srinivas]

Large parts of CS don't care about computability either (See Leo's talk at last year's CAV keynote)

[Derek Sorensen]

Likewise @Shreyas Srinivas ! :slight_smile: It's been a while! For univariate polynomials it's a dense coefficient array; for multivariate, a sparse map from monomials to coefficients

[Derek Sorensen]

certainly for our use case (formal verification of production cryptographic protocols) computability is a huge win

[Alexander Hicks]

Shreyas Srinivas said:

Large parts of CS don't care about computability either (See Leo's talk at last year's CAV keynote)

Which is why I think it's fine for a theory to be developed around noncomputable definitions and to then have translation lemmas to a computable representation. The fact that computability is not striclty necessary for some people should not be a blocker to the library being useful to the subset of people for whom it is, or an agreement needs to be made about having another general purpose computable library so that we avoid having many people maintaining thigns with limited time; I believe there are already several other computable polynomial libraries, for example, but don't know what their exact status is.

[Shreyas Srinivas]

speaking of cryptographic protocols, has anyone worked on embedding Tamarin into lean? I had a chat with Cas a while ago and he mentioned that there's an intermediate tool whose translation would take a lot of effort but might not get done in academia for "academia" reasons

[Alexander Hicks]

Not afaik, maybe this will come up at HACS later this year as I believe he'll attend, but I don't know who would be interested in working on this.

[Shreyas Srinivas]

Cas is clear that he is not willing to get someone working on this. It doesn't produce work that can be published in a meaningful timeframe (especially since it would be re-implementing some existing haskell code in lean)

[Shreyas Srinivas]

It will have to come from the industry, if I understand his reasoning correctly.

[Chris Henson]

My interpretation of the philosophy of CSLib is that we try to reuse Mathlib infrastructure as much as possible, but are open to well motivated deviations. At least one of these cases is already made for computability reasons. The idea of computable polynomials has emerged several times and seems to already have a concrete use case here, so I would personally be open to upstreaming as @Derek Sorensen suggests.

[Eric Wieser]

Alexander Hicks said:

Re: mathlib, I believe if one digs through the zulip archives there have been past discussions about computable polynomials and why we shouldn't expect them to show up in mathlib (unless something changes...),

@Yaël Dillies is making progress on an independently useful refactor that will unblock further work to make polynomial computable; but that likely doesn't mean 'computable with the performance characteristics you want"

[Wrenna Robson]

Yes I agree with Eric that it is worth distinguishing between "computable polynomials" and "performant polynomials".

[Wrenna Robson]

Though the work that @Derek Sorensen mentions is certainly great stuff.

[Wrenna Robson]

That said - @Derek Sorensen, may I ask, why did you decide to have CPolynomial be a wrapper around Array, rather than, say, using a sigma type or a dependent structure (or even a quotient if you want to get fancy) to ensure it was a minimal such polynomial?

[Wrenna Robson]

Ah I see this is CPolynomialC, essentially.

[Derek Sorensen]

yeah there is discussion internally on what should be the "canonical" polynomial representation - either raw arrays or these canonical arrays (a subtype). ultimately, the motivation for this library is to make performant specs. so, our priority has been to use data structures that map fairly straightforward onto how one might find them in the wild, in code to be verified

[Wrenna Robson]

That makes sense. I personally favour the latter - I have in a personal repository an implementation of finite permutations where there's a similar sort of problem.

[Derek Sorensen]

right, that's good to know! it's a soft TODO to make that change. depending on the ergonomics of using CompPoly as specs for production code we will adapt, but you're adding to the argument of making the canonical polynomials the trimmed/subtype

[Wrenna Robson]

Actually what I do there is start with PermOf n, the permutation of size n (which might fix n, so really you can view is as permutations that permute up to n points - analogous to polynomials of up to n degrees). It is convenient to have this, and then you can define some function which calculates the minimum size of a permutation (what is the largest non-fixed point) and the permutation of type PermOf (a.minSize). And then that is a natural thing to build into a little structure.

[Derek Sorensen]

do you have a link you'd be willing to share? :slight_smile: would be interested in having a look

[Derek Sorensen]

I'm trying to find the right balance between "computable" (and beautiful, theoretically), and "performant." I'm guessing that will result in multiple implementations with ring isomorphisms between them (that's the plan, at least)

[Wrenna Robson]

https://github.com/linesthatinterlace/controlbits/tree/master/CBConcrete/CBConcrete/PermOf

[Wrenna Robson]

Here we go

[Wrenna Robson]

MonoidHom.lean is the file where I construct the finite thingy.

[Wrenna Robson]

You have obviously a set of injections upwards (for polynomials of degree <= n and permutations of n elements respectively) and essentially the goal is to take the direct limit.

[Wrenna Robson]

I believe that is what it is called - Mathlib does have an implementation of the direct limit but it certainly isn't performant.

[Wrenna Robson]

Derek Sorensen said:

I'm trying to find the right balance between "computable" (and beautiful, theoretically), and "performant." I'm guessing that will result in multiple implementations with ring isomorphisms between them (that's the plan, at least)

Yes, indeed it may be the case that you end up with multiple ones along this path.

[Wrenna Robson]

Obviously Equiv.Perm (Fin n) exists but you know it's nice to think we could get better performance using arrays (also it is sort of hard to computably construct finite permutations that way...)

[Wrenna Robson]

Anyway I am trying to pay attention to your work with interest.

[Wrenna Robson]

Was good to chat to Alex and Bolton about it last year at HACS.

[Derek Sorensen]

yeah, this is great feedback :slight_smile: aiming to have CompPoly in a reasonably good state before HACS this year, will report as we get more mature on the project!

[Alexander Hicks]

I guess one thing to add regarding computable polynomials and computable v efficient is that, at least for our use cases, we'll happily rely on domain specific compilers that have many optimisations built-in (e.g. https://github.com/fractalyze/prime-ir) which let's us focus on implementing a simpler theory of computable polynomials (and associated algorithms) whilst leaving the performance engineering to the compiler and, if required, verifying the compiler via Lean-MLIR or rewriting it in Lean. Then the question becomes what do we want to have in the high level source code, what are we leaving to the compiler, and how to co-develop both effectively.