Computability and finsupp and finite

Stream: general

[Wrenna Robson]

I'm sure this has been raised in a thread somewhere, but I can't find it.

Is there a good reason we can't consider redefining finsupp like so?

structure finsupp (α : Type*) (M : Type*) [has_zero M] :=
(to_fun : α → M)
(finite_support' : to_fun.support.finite)

Some experimentation with using it suggests that it's perfectly workable. https://gist.github.com/linesthatinterlace/6d3fcc10df7ea2716a82a2a260a47c9f

But I don't see why you require the current construction where it is a finset and a function along with a proof that the finset is the support of that function. It seems like that instantly makes computable definitions of operations on it a headache.

Obviously the set.finite predicate is relatively new. But this feels so obvious that I'm sure there's some good reason why it hasn't happened. But is that reason "it is not technically desirable" or "it would be a lot of work" or something else? Currently I'm always a little wary of using finsupp, precisely because it's this big noncomputable theory and so anything you build from it is also noncomputable.

[Eric Wieser]

The change you're suggesting makes summing over the support noncomputable

[Eric Wieser]

Right now that's computable, but addition isn't (for silly reasons not related to the definition of finsupp)

[Eric Wieser]

Pretty much all the "finsupp operations are not computable" cases are actually "finsupp chose to use classical.decidable instead of taking the necessary instance as an argument", which was done to make some things less painful

[Wrenna Robson]

Does it make it noncomputable even when you sum over a set with decidable mem (such as a coerced finset)?

[Wrenna Robson]

Like if you have a way of constructing finsupps from finsets.

[Eric Wieser]

There's no way to write docs#finsupp.sum in a computable way under your proposal, because you're removing the data it needs

[Wrenna Robson]

Right right

[Wrenna Robson]

That does make sense - and I can see why we want that to be computable. It just feels so weird that there's no way to make both of them so.

[Scott Morrison]

It's not that "there's no way". It's just that keeping things computable requires additional plumbing, getting decidability instances to the correct places (and uniformly, i.e. so we don't have defeq problems with instances preventing lemma firing). And since mathlib is classical, we decided not to do this plumbing.

[Wrenna Robson]

Right, so there's no theoretical barrier.

[Wrenna Robson]

I understand that - I do think it makes it a bit hard to build certain things which feel like they ought to be computable, and to a degree I don't then see why it's then something you bother caring about at all (if it is intended to be a classical library).

[Eric Wieser]

My understanding is that the decision is stronger than "we didn't want to do the plumbing"; it's "we didn't want mathematicians to have to think about connecting to the plumbing"

[Eric Wieser]

Having worked with concrete polynomials a bit I now believe this was the wrong decision, and being able to evaluate coeffs/degrees by refl would be more useful.

[Scott Morrison]

A big problem here is that there are many different reasonable representations of "computable polynomials", and different representations are better for different purposes. Our plan has been to do all the theory with classical polynomials, but without this necessarily obstructing (much) narrower developments of computational representations for particular purposes.

It's tempting to imagine we might have in parallel a development of computable polynomials with all the (highly infectious?) plumbing that requires, and also a development of classical polynomials with all that plumbing removed. But we can't realistically redevelop everything for all the different relevant representations; it wouldn't be one parallel development but many.

[Wrenna Robson]

I may as well make plain where I was thinking about this - I've been reading some of Brett Jacob's probability work as a result of this thread. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/elementary.20probability.20advice and I was thinking that if we wanted to build a formalization of his "structured probablistic reasoning" one would probably end up doing it off of finsupp, but then you lose much of the nice computability that should otherwise be inherent in the theory.

[Wrenna Robson]

It seems this tension might exist in multiple places, really - between computable representations and classical ones, where the latter are much easier/better for developing abstract theory on.

[Wrenna Robson]

@Eric Wieser does that imply that you'd also like to see some form of computable finsupp, or rather implement polynomials in a different way?

[Kyle Miller]

I think this also depends on what we mean by "compute."

• There's Lean-computable, which means rfl might work (well-founded recursion or different eq.recs can inhibit this though)
• There's the same Lean-computable, which means the VM compiler ought to work (modulo bugs), but this is for writing programs and the results are not formally verified.
• There's computable in the symbolic sense, where for example norm_num or simp can take a symbolic expression and put it into (ideally) a normal form.

For the third, there's no need for the backing type to have any nice computability properties.

When it comes to polynomials and computation, don't we mostly mean "take this symbolic expression and put it into a normal form"? One could write "data structures" that are special constructors for polynomials (for example dense representations, or sparse representations) and have tactics that efficiently operate on these constructors.

[Kyle Miller]

I wrote some implementations of computable polynomials over Int in Lean 4, but that was because I was just using it as a programming language to get some large unverified computations done. I'm not sure how useful these implementations would be for computing inside proofs.

[Wrenna Robson]

I suppose for something like finsupp, what I mean is that if I have f and g finsupps, I should be able to evaluate (f + g) at any point. Perhaps that's already possible, but then I don't understand what noncomputable actually means, perhaps.

[Wrenna Robson]

and indeed, I suppose, find (f + g).support, though I appreciate that is harder/the sticking point.

[Kyle Miller]

I guess a pertinent question is what you specifically mean by having f and g finsupps and what output you'd want from evaluating (f + g).

[Mario Carneiro]

Do you think that finsupp.sum should be computable? Folds over a finsupp are important to a lot of applications that use them, for example you take the sum of a finsupp to calculate the degree of a monomial

[Mario Carneiro]

and that means that finsupp.support needs to be data, not just an assertion of finiteness

[Wrenna Robson]

I definitely agree - as Eric pointed out to me above - that it is more important that finsupp.sum is computable for exactly the reason you say.

[Wrenna Robson]

And I hadn't appreciated that that would of course need the support to be data.

[Mario Carneiro]

Evaluating (f + g) at a point is already possible using the function part

[Mario Carneiro]

but calculating the support requires decidable equality of the codomain so that you can remove all the zeroes

[Wrenna Robson]

Right.

[Mario Carneiro]

Alternatively, you could relax that by saying that the provided list doesn't have to be the real support but only some superset of it, and then take a quotient

[Wrenna Robson]

Yes, superset is I think the obvious "next idea". But that surely runs into other issues.

[Mario Carneiro]

I think it comes back to "what do you actually want from the type"

[Wrenna Robson]

Yeah. And that might be quite different depending on the type.

[Mario Carneiro]

for computational purposes a closure + a linked list is really not a good representation at all

[Wrenna Robson]

(Or rather, on the thing you are building from the type.)

[Bolton Bailey]

I think something that I might want is for the following to output "3"

def a : polynomial ℕ := polynomial.C 1
def b : polynomial ℕ := polynomial.C 2
def c := a + b

#eval c.eval 17

Does the quotient way of doing this allow both for this as well as keeping finsupp.sum computable?

[Kyle Miller]

To check, when you say you want to #eval this, is it because you just want the number and you are OK with it being unproved?

[Johan Commelin]

Would you also be happy with #simp c.eval 17 returning 3?

[Kyle Miller]

or #norm_num c.eval 17

[Bolton Bailey]

Hmm, let me think

[Bolton Bailey]

I was trying to produce a simple example of what I wanted but in actuality I might want to be doing more complicated operations than just adding two known polynomials. The cryptographic algorithm is a bit complicated but what it does is to take as input a polynomial like a + b X + c X^3 + d X^4 and "split" it into two polynomials a + c X and b + d X, make a linear combination those two polynomials (a + cX) + k(b + dX), and then evaluate that and return an output.

[Wrenna Robson]

I suppose what the "noncomputable finsupp.sum" would look like under my original proposal is "shockingly and suspiciously similar to the already-existing finsum".

[Eric Wieser]

Mario Carneiro said:

Alternatively, you could relax that by saying that the provided list doesn't have to be the real support but only some superset of it, and then take a quotient

Wrenna Robson said:

Yes, superset is I think the obvious "next idea". But that surely runs into other issues.

Note this approach to computability already exists in mathlib, it's docs#dfinsupp

[Wrenna Robson]

"finsupp takes an altogether different approach here; it uses classical.decidable and declares finsupp.has_add as noncomputable. This design difference is independent of the fact that dfinsupp is dependently-typed and finsupp is not; in future, we may want to align these two definitions, or introduce two more definitions for the other combinations of decisions."

[Wrenna Robson]

Well that's uh.

[Wrenna Robson]

I did not realise this. So finsupp and dfinsupp are different in ways other than the fact that one is dependent. I didn't realise this (you would not know it from the name).

[Eric Wieser]

I have a branch somewhere that redefined finsupp as a special case of dfinsupp

[Wrenna Robson]

I mean it looks like the approach of dfinsupp is very clever and nice.

[Wrenna Robson]

So - right. Yes, that sounds good.

[Wrenna Robson]

Like, call me silly but that's what I'd do.

[Wrenna Robson]

That does mean I can increment my "number of ways to do finite sums in mathlib" counter by one.

[Wrenna Robson]

Because it sounds like dfinsupp.sum, finsupp.sum, finsum, finset.sum and tsum are all different.

[Wrenna Robson]

slaps \Sigma this bad boy can contain so many different notions of summation

[Eric Wieser]

See also docs#dfinsupp.sum_add_hom which removes the decidability requirement in exchange for a proof that it's not needed

[Wrenna Robson]

Oh true, I should count that too ;P

[Wrenna Robson]

That is really nice, honestly.

[Wrenna Robson]

Was there any particular issue with replacing finsupp with a special case of dfinsupp?

[Eric Wieser]

Refactors are hard

[Wrenna Robson]

looks sadly at my floor_order refactor yes