finset semiring

Stream: Is there code for X?

[Damiano Testa]

Dear All,

I may have asked this already, but is there a version of docs#set.set_semiring which is based on finsets? I tried various replacements s/set/finset/ in set.set_semiring, but nothing worked...

Thanks!

[Yaël Dillies]

No, we don't have that. What do you need it for?

[Yaël Dillies]

(also I'm editing heavily data.finset.pointwise so please request my review on all PRs that touch it)

[Damiano Testa]

Ok, thanks! I am currently playing around with defining a map from (laurent_)polynomials to set.set_semiring associating to a polynomial its support. I am hoping that several lemmas about the support can then be proved using what is already available from the semiring instance on set_semiring. Since in my case the support is a finset, I would like to exploit this.

[Damiano Testa]

In particular, I do not need it yet, but I will want to relate the computations in set.set_semiring to the max/min of the support and then it would be good to have the finsets being carried around by the semiring structure.

[Damiano Testa]

(so, for the moment, I am simply trying it out, to see if I can avoid duplicating a large part of the support/degree/nat_degree/... API for Laurent polynomials, using set.set_semiring. If this works, then it might make sense to do this already for add_monoid_algebra.

[Damiano Testa]

(effectively, this amounts to working with add_monoid_algebra where the add monoid is 0,1 with absorbing addition, I think.)

[Yaël Dillies]

Oh nice! In what sense do the set_semiring operations correspond to support operations?

[Damiano Testa]

My last comment may have been a little cryptic. What I meant is that I think that finset.finset_semiring(or whatever it should be called) is also add_monoid_algebra (with_zero (trivial ring))... maybe?

[Damiano Testa]

the correspondence is that support of sums are contained in sums of supports and supports of product are contained in products of supports

[Damiano Testa]

This is exactly what you need to get many statements about degrees (sub)adding under products, additions...

[Yaël Dillies]

I think they should be called set_semiring and finset_semiring (without the namespaces) and put in a new file, because they have little to do the rest of the pointwise API now

[Damiano Testa]

(so, essentially, you pretend that there is no cancellation in your additions/multiplications and you obtain the "right" "generic" statement, which is always greater than or equal than the correct statement.)

[Damiano Testa]

Ok, anyway, my idea was to exploit something that is already available, to avoid writing a lot of API myself. If the API that I am hoping for is missing somewhere else, I might just as well write it for exactly what I want! :wink:

[Yaël Dillies]

... by which I mean, if I were to add everything that's as related to the rest of data.set.pointwise as set_semiring is, I would blow the size of the file to several thousand lines.

[Damiano Testa]

Ok, maybe my idea does not make much sense, given the state of affairs. I am just trying to avoid having to write a lot of almost identical APIs for degree, int_degree, trailing_degree, trailing_int_degree, leading_coeff, trailing_coeff for Laurent polynomials...

[Yaël Dillies]

No I think you're onto something, but I will have to think about it more.

[Damiano Testa]

Ok, basically, anything that would prove "quickly" statements like degree (f * g) ≤ degree f * degree g would be very welcome! If it is as polymorphic as possible on the notion of degree, that would be even better!

[Damiano Testa]

(I would like to leverage the fact that, from the point of view of supports, that statement is simply a statement about the support of addition.)

[Damiano Testa]

Most of the results about various forms degree are simply statements about adding finite subsets of a linear order and gathering trivialities about them.

[Damiano Testa]

I view cancellation and disappearance from support of some terms as an unfortunate coincidence. The API should include all the results about degrees that are compatible with "opaque cancellation" and then deal more precisely with cancellation, as the need arises.

[Damiano Testa]

Anyway, I have to take care of some "real-world" problems. :upside_down: