Tropically degree-bound polynomials

Stream: maths

[Bolton Bailey]

I previously brought up degree-bound polynomials in the context of computability. It has occurred to me since then that if you consider the type of polynomials with a "degree bound" tacked on, this is actually still a semiring, because the degree bound has the structure of a tropical semiring.

Is there a name for this concept? The first thing that came to mind was "Tropical Polynomial" but per this discussion, I think this just means "polynomial over a tropical ring".

[Alex J. Best]

What is the tropical ring? Tropicals are a semiring normally.

[Bolton Bailey]

Good point, I guess I mean semiring, will edit.

[Damiano Testa]

Could you explain a little more what you mean by "degree bound"? Specifically, how do you define multiplication.

Say the bound is 1, so that X should be allowed. Shouldn't X * X not be allowed?

[Bolton Bailey]

The type is

def TropicallyBoundPolynomials (R) [Semiring R] : Type :=
{ p : (Polynomial R × Tropical (OrderDual ℕ)) // p.1.natDegree ≤ p.2.untrop }

[Bolton Bailey]

Multiplication is defined as (p1, b1) * (p2, b2) = (p1 * p2, b1 + b2)

[Bolton Bailey]

So (X, 1) * (X, 1) = (X^2, 2)

[Bolton Bailey]

And addition is (p1, b1) + (p2, b2) = (p1 + p2, max b1 b2)

[Damiano Testa]

So each polynomial appears a lot of times as the first coordinate, right?

[Bolton Bailey]

Yes

[Bolton Bailey]

Hmm, is it really a Semiring?

[Damiano Testa]

And even if you start with a CommRing, what you obtain is not even cancellative.

[Bolton Bailey]

Good point. Do we have a typeclass for whatever this is?

[Damiano Testa]

It might be a Semiring, but it is certainly not much more than a Semiring, even if R is a Field.

[Bolton Bailey]

I'm trying to figure out whether 0 is (0, 0) or if I should add infinity to the set of bounds and let the zero be (0, infinity)

[Damiano Testa]

Btw, the compute_degree tactic exploits this and basically operates under the assumption that the actual degree of what you feed it is the least nat satisfying all the constraints.

[Damiano Testa]

(0, 0) is not zero, since (X,1) * (0,0) = (0,1) and not (0,0).

[Damiano Testa]

So you should maybe use degree rather than natDegree.

[Bolton Bailey]

Well, that's adding a bottom in the wrong direction, right?

[Bolton Bailey]

Even if I'm using degree, (X,1) * (0,bot) = (0,1)

[Bolton Bailey]

What I need, I think, is to take the order dual of (Nat with Top)

[Bolton Bailey]

Hmm, I think that doesn't work either

[Damiano Testa]

Yes, it seems that (0, top) is not a zero for addition, right?

[Damiano Testa]

Because it absorbs all degrees to top.

[Damiano Testa]

So, (0,top) + (X,1) = (X,top), but if (0,top) were 0, then the answer would have to be (X,1).

[Bolton Bailey]

Yes, I think there's a problem either way
if the zero is (0,0) then (x, 1) * (0, 0) = (0, 1), so mul_zero fails
if the zero is (0,top) then (x, 1) + (0, top) = (x, top), so add_zero fails

[Bolton Bailey]

Shucks

[Bolton Bailey]

I'm still a bit confused where I went wrong. Wikipedia says there is such a thing as a "max tropical semiring"

[Bolton Bailey]

def Foo (R) [CommSemiring R] : Type := Polynomial R × Tropical (OrderDual (WithBot ℕ))

instance [CommSemiring R] : CommSemiring (Foo R) := by
  unfold Foo
  apply @Prod.instCommSemiring _ _ --failed to synthesize CommSemiring (Tropical (WithBot ℕ)ᵒᵈ)

How do I get it to not compain about failed to synthesize and let me try to synthesize this myself?

[Bolton Bailey]

I want to apply docs#Tropical.instCommSemiringTropical

[Bolton Bailey]

I guess the problem is that while Nat is a monoid, (WithBot Nat) is not?

[Andrew Yang]

Something like apply (config := { allowSynthFailures := true }) ...

[Junyan Xu]

(deleted)

[Bolton Bailey]

Ok last ditch effort. If I artificially redefine the type as Option { p : (Polynomial R × Tropical (OrderDual ℕ)) // p.1.natDegree ≤ p.2.untrop } and define none as the zero and give it the behavior to satisfy add_zero, mul_zero, is it a Semiring then?

[Junyan Xu]

This actually works:

import Mathlib.Algebra.Tropical.Basic
import Mathlib.Data.Polynomial.Degree.Definitions

instance : LinearOrderedAddCommMonoidWithTop (OrderDual (WithBot ℕ)) where
  __ : LinearOrderedAddCommMonoid (OrderDual (WithBot ℕ)) := inferInstance
  __ : Top (OrderDual (WithBot ℕ)) := inferInstance
  le_top _ := bot_le (α := WithBot ℕ)
  top_add' x := WithBot.bot_add x

noncomputable example (R) [Semiring R] :
    Semiring (Polynomial R × Tropical (OrderDual (WithBot ℕ))) := inferInstance

[Bolton Bailey]

Wait what? What is the zero of this instance and what is (X, 1) * 0?

[Junyan Xu]

The zero in Polynomial R × Tropical (OrderDual (WithBot ℕ)) is surely (0, 0), and the zero in OrderDual (WithBot ℕ) should be toDual ↑0. (sorry, forgot about Tropical)
(X, 1) * 0 has to be 0 for it to be a semiring.

[Bolton Bailey]

I am excited but confused. What is the definition of the multiplication operation then?

[Junyan Xu]

The zero in Tropical (OrderDual (WithBot ℕ)) is defined by
Tropical.instZeroTropical = { zero := Tropical.trop ⊤ }, so trop (toDual ⊥) in this case.
And multiplication is addition on WithBot ℕ:

Tropical.instMulTropical = { mul := fun x y => Tropical.trop (Tropical.untrop x + Tropical.untrop y) }

[Bolton Bailey]

Ah ok, maybe I was wrong about Damiano's comment being wrong about needing to do degree rather than natDegree

[Junyan Xu]

Yeah with degree I think the carrier should be {p | p.1.degree ≤ OrderDual.ofDual (p.2.untrop)}

[Damiano Testa]

I suspect that what is going on is that the product of semirings is a semiring (pretty clear), but then I at least got confused on whether we were supposed to take max or min on the tropical component.

[Bolton Bailey]

Needing to use OrderDual is unhelpful for clarity on that front.

[Damiano Testa]

Also, both conventions max and min are used in informal maths for tropical semirings.

[Bolton Bailey]

I think I can definitively say that what we are interested in is what wikipedia calls the "max tropical semiring".

[Damiano Testa]

So the conclusion is that the identity on the tropical side is bot, since the operation is max, right?

[Bolton Bailey]

multiplication is addition on WithBot ℕ

So I guess the point is that the bot absorbs everything, so the zero can be (0, bot) and when I multiply this by anything and get (0, bot)

[Damiano Testa]

My mental image of trop is "min-plus algebras", so I will get confused about this frequently.

[Damiano Testa]

Bolton Bailey said:

multiplication is addition on WithBot ℕ

So I guess the point is that the bot absorbs everything, so the zero can be (0, bot) and when I multiply this by anything and get (0, bot)

I think so: what you are calling "multiplication" is the operation on the product that is multiplication on polynomials. That operation converts to addition on the tropical component: when you add anything to bot you get bot.

[Junyan Xu]

Anyway this is what you originally want

import Mathlib.Algebra.Tropical.Basic
import Mathlib.Data.Polynomial.Degree.Definitions

instance : LinearOrderedAddCommMonoidWithTop (OrderDual (WithBot ℕ)) where
  __ : LinearOrderedAddCommMonoid (OrderDual (WithBot ℕ)) := inferInstance
  __ : Top (OrderDual (WithBot ℕ)) := inferInstance
  le_top _ := bot_le (α := WithBot ℕ)
  top_add' x := WithBot.bot_add x

variable (R) [Semiring R]

noncomputable example : Semiring (Polynomial R × Tropical (OrderDual (WithBot ℕ))) := inferInstance

example : Subsemiring (Polynomial R × Tropical (OrderDual (WithBot ℕ))) where
  carrier := {p | p.1.degree ≤ OrderDual.ofDual p.2.untrop}
  mul_mem' {p q} hp hq := (p.1.degree_mul_le q.1).trans (add_le_add hp hq)
  one_mem' := Polynomial.degree_one_le
  add_mem' {p q} hp hq := (p.1.degree_add_le q.1).trans (max_le_max hp hq)
  zero_mem' := Polynomial.degree_zero.le

[Yaël Dillies]

Do I see that you need to dualise what you need to input in docs#Tropical ? @Yakov Pechersky and I concluded a while back that it was probably better to define addition on Tropical using max, not min.

[Antoine Chambert-Loir]

To handle these two classical normalizations, what's the best move? Reformulate everything in terms of a well chosen one? ‘max‘, ‘*‘ would also be natural in certain contexts. Unfortunately, I have no axiomatic characterization to offer.