ERat as Semiring

Stream: maths

[Martin Dvořák]

I want to define ERat (i.e., extended rational numbers) for my project (not for Mathlib).
Addition on EReal defined so that ⊥ + ⊤ = ⊤ + ⊥ = ⊥ in Mathlib.
What would go wrong if I defined addition on ERat so that ⊥ + ⊤ = ⊤ + ⊥ = 0 in my project?
I would like ERat to form a Semiring.
It cannot be a Ring because it is not even a CancelAddCommMonoid.
In my use case, I am not going to use [-∞, ∞], only (-∞, ∞].
However, the definition must be done for [-∞, ∞] because (-∞, ∞] would not even allow Mul.
So I am going to do [-∞, ∞] and define multiplication the same way EReal does.

protected def mul : ERat → ERat → ERat
  | ⊥, ⊥ => ⊤
  | ⊥, ⊤ => ⊥
  | ⊥, (y : ℚ) => if 0 < y then ⊥ else if y = 0 then 0 else ⊤
  | ⊤, ⊥ => ⊥
  | ⊤, ⊤ => ⊤
  | ⊤, (y : ℚ) => if 0 < y then ⊤ else if y = 0 then 0 else ⊥
  | (x : ℚ), ⊤ => if 0 < x then ⊤ else if x = 0 then 0 else ⊥
  | (x : ℚ), ⊥ => if 0 < x then ⊥ else if x = 0 then 0 else ⊤
  | (x : ℚ), (y : ℚ) => (x * y : ℚ)

My addition would also have to be defined manually, not using deriving.
I am not sure if something will go wrong.
Can you see a problem right away?
I will never define exponentiation&friends on my ERat.

TLDR:
I want to define ERat that forms a Semiring. Can it be done?
I think I should define ⊥ + ⊤ = ⊤ + ⊥ = 0. Is there a catch?

[Kevin Buzzard]

docs#Semiring

[Yaël Dillies]

Why do you want ERat?

[Yaël Dillies]

I can see a use for ENNRat, namely represent literals in ENNReal, but I can't see a use for ERat, just as I can't see a use for EReal.

[Martin Dvořák]

Yaël Dillies said:

Why do you want ERat?

In one point, I want to take a common denominator of all finite values in my Mutliset.

[Kevin Buzzard]

Apparently semirings are associative. I highly doubt that ⊥ + ⊤ = ⊤ + ⊥ = 0 can ever be made associative, because with your conventions (⊥ + ⊤) + 37 = 37 but no sensible convention could have ⊥ + (⊤ + 37) = 37. The philosophy that we have with EReal is that Top is "error" and Bot is "even worse error", and then associativity remains true because you can never go back from errors. If you want errors to add up to non-error answers then I suspect you're always going to have problems with associativity.

[Martin Dvořák]

Kevin Buzzard said:

Apparently semirings are associative. I highly doubt that ⊥ + ⊤ = ⊤ + ⊥ = 0 can ever be made associative, because with your conventions (⊥ + ⊤) + 37 = 37 but no sensible convention could have ⊥ + (⊤ + 37) = 37. The philosophy that we have with EReal is that Top is "error" and Bot is "even worse error", and then associativity remains true because you can never go back from errors. If you want errors to add up to non-error answers then I suspect you're always going to have problems with associativity.

Thank you for pointing out! I didn't notice!

[Yaël Dillies]

Martin Dvořák said:

Yaël Dillies said:

Why do you want ERat?

In one point, I want to take a common denominator of all finite values in my Mutliset.

How is that related to ERat? On what type is your multiset?

[Martin Dvořák]

Yaël Dillies said:

Martin Dvořák said:

Yaël Dillies said:

Why do you want ERat?

In one point, I want to take a common denominator of all finite values in my Mutliset.

How is that related to ERat? On what type is your multiset?

Ah, sorry for confusion. I was answering why I wanted ERat at opposed to EReal. You probably wondered why I was using ERat as opposed to ENNRat. In the pen-and-paper version, the values in my multisets are rational with some infinities (always positive infinity, but finite values can be negative).

[Yaël Dillies]

So what's the common denominator supposed to be?

[Yaël Dillies]

Isn't it valued in ℕ∞?

[Martin Dvořák]

Nope. Product of denominators of all finite values.

[Yaël Dillies]

Can you give an example where it's not ℕ∞-valued?

[Martin Dvořák]

I discussed the topic with my supervisor.
Here I write only a high-level summary of my use case...

We need to perform these operations:
A *ᵥ x aka $A \cdot x$
c ⬝ᵥ x aka $c^\top x$
We need to meet the following criteria:
The possible values inside $A$ have to include $\{ -1, 0, 1 \}$.
The possible values inside $c$ have to include $(-\infty, \infty]$.
The possible values inside $x$ have to include $[0, 1]$.
We need to enforce that $x$ contains rational values only.
Ordering has to be defined in the same sense as in textbook math.

Conclusion:

For simplicity,
$A$ will have values in $(-\infty, \infty)$,
$x$ will have values in $[0, \infty)$,
and so $A \cdot x$ will have values in $(-\infty, \infty)$.
The only option is that $c$ has values in $(-\infty, \infty]$,
therefore $c^\top x$ will have values in $(-\infty, \infty]$.

Everything will be expressed using (extended/restricted) rationals.
For A *ᵥ x we will upgrade x to be over ℚ instead of over NNRat, so we can reuse the existing *ᵥ definition.
For c ⬝ᵥ x we will have to write new definitions:
First we need a custom multiplication of type WithTop ℚ → NNRat → WithTop ℚ.
Then we define a custom dot product that uses the custom multiplication together with standard + on WithTop ℚ.
Then we rebuild API for our dot product.

If you see any flaw in the plan above, please, point it out. I will be very thankful for it!

[Martin Dvořák]

The other option is to define everything over ERat and separately prove that c ⬝ᵥ x will never be ⊥ in the settings above.
Unfortunately, I still need to rebuild a lot of API myself because ERat cannot even form NonUnitalNonAssocSemiring.

[Michael Stoll]

Yaël Dillies said:

I can see a use for ENNRat, namely represent literals in ENNReal, but I can't see a use for ERat, just as I can't see a use for EReal.

You need EReal when you want to take infima or suprema of arbitrary sets of real numbers (e.g., docs#LSeries.abscissaOfAbsConv is naturally an EReal).

[Martin Dvořák]

Martin Dvořák said:

I think I should define ⊥ + ⊤ = ⊤ + ⊥ = 0.

It doesn't help at all!
We get 0 = ⊥ + ⊤ = 2*⊥ + (-1)*⊥ ≠ (2 - 1) * ⊥ = 1 * ⊥ = ⊥ hence distributivity is dead.

[Martin Dvořák]

Kevin Buzzard said:

Top is "error" and Bot is "even worse error"

What you described is the semantics of Option that (2x) underlies the type EReal (I know that you know, but I still wanted to point it out).
However, the semantics of EReal is different because multiplication by -1 gets you from one "error" to the other; therefore, I'd say there are two distinct special values rather than "errors".
I think EReal captures more of the concept of infinity and less of the concept of "error".

[Jireh Loreaux]

I think the point of addition on EReal is that it is defined precisely so that the natural exponential map from EReal to ENNReal is an additive-to-multiplicative isomorphism of monoids.

[Martin Dvořák]

Is there a good reason why docs#Matrix.mulVec requires [NonUnitalNonAssocSemiring α] despite docs#Matrix.dotProduct requiring [Mul α] [AddCommMonoid α] only?

[Josha Dekker]

Martin Dvořák said:

Is there a good reason why docs#Matrix.mulVec requires [NonUnitalNonAssocSemiring α] despite docs#Matrix.dotProduct requiring [Mul α] [AddCommMonoid α] only?

Have you tried replacing the assumption and using Aesop/apply wherever the proof breaks? Writing something that actually systematically replaces every assumption by weaker assumptions and checking if the proof still holds up is on my to-do list, once I’ve worked through the meta-programming book.

[Martin Dvořák]

What I've been doing this morning is to copy those definitions into my project, change it to [Mul α] [AddCommMonoid α] and reprove lemmas about "matrix times vector" on demand. It seems to work right now. However, if it is desirable to have the weaker assumptions in Mathlib, I can try to change it in place and PR the change to Mathlib.

[Yaël Dillies]

Martin Dvořák said:

We need to meet the following criteria:
The possible values inside $A$ have to include $\{ -1, 0, 1 \}$.
The possible values inside $c$ have to include $(-\infty, \infty]$.
The possible values inside $x$ have to include $[0, 1]$.

Okay, but why do you need this?

[Martin Dvořák]

There is a framework for constraint satisfaction&optimization called General-Valued Constraint Satisfaction Problems that works with this setting:
image.png
image.png
Essentially, infinity is a hard constraint and rational values are soft constraints that we want to minimize.

[Yaël Dillies]

Okay but do you actually need algebra on extended rationals?

[Martin Dvořák]

Lean version: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/Optimization/ValuedCSP.html#ValuedCSP

[Martin Dvořák]

Yaël Dillies said:

Okay but do you actually need algebra on extended rationals?

To simplify things. I want to say "minimize this sum" instead of "make sure none of these values is infinity, then coerce them to rationals under the assumption, then minimize the sum".

[Yaël Dillies]

I strongly suspect you will find the latter approach less painful

[Yaël Dillies]

Your current approach involves redoing most of mathlib's algebra library in the case you have some infinities lying around. The other approach only involves redefining what it means to minimise a goal.

[Martin Dvořák]

Yaël Dillies said:

Your current approach involves redoing most of mathlib's algebra library in the case you have some infinities lying around. The other approach only involves redefining what it means to minimise a goal.

IMO "minimize this sum" is a nice abstraction that works on paper. I would like to make it work in Lean as well. Note that in VCSP theory there is never negative infinity and there is never a multiplication between a negative number and infinity. In theory I have an ill-defined structure because $(-\infty, \infty]$ isn't closed under multiplication and $[-\infty, \infty]$ isn't distributive, but in practice it works as if it was a semiring because the "dangerous" operations are never performed. However, can it be formalized?

[Yaël Dillies]

So you have values and you have weights, right?

[Yaël Dillies]

Then can you try simply not having values and weights be in the same type?

[Martin Dvořák]

Yaël Dillies said:

Martin Dvořák said:

We need to meet the following criteria:
The possible values inside $A$ have to include $\{ -1, 0, 1 \}$.
The possible values inside $c$ have to include $(-\infty, \infty]$.
The possible values inside $x$ have to include $[0, 1]$.

Okay, but why do you need this?

I want to define a pseudoLP as an abstraction that is faithfully translated to LP. I have non-negative variables and my objective function can have some infinities (but no negative infinities). It can be straightforwardly translated to LP (restrict variables that come with infinity coefficient to be zero and kick out the term out of the sum), but I want to perform all algebra over pseudoLP.

[Martin Dvořák]

Yaël Dillies said:

Then can you try simply not having values and weights be in the same type?

This is what I've been considering here. For example (A x : Rat) and (c : ERat) could work but then c ⬝ᵥ x needs to be over ERat as well.

[Martin Dvořák]

I want to reuse existing definitions of A *ᵥ x and c ⬝ᵥ x which kinda forces me to do everything over the same type and separately prove that negative infinities will never arise and so on.

[Yaël Dillies]

Wait, I thought you didn't want to multiply infinities by negative values? So you can't possibly allow (w : Rat) • (v : ERat)

[Yaël Dillies]

(w : NNRat) • (v : ERat) would be fine

[Martin Dvořák]

Yaël Dillies said:

Wait, I thought you didn't want to multiply infinities by negative values? So you can't possibly allow (w : Rat) • (v : ERat)

Yeah, I got it wrong. As per my older post, if I went in the heterogeneous direction, I'd probably declare (x : NNRat) and (A : Matrix _ _ Rat) and (c : ERat).

[Martin Dvořák]

Yaël Dillies said:

(w : NNRat) • (v : ERat) would be fine

The problem is that the existing definition docs#Matrix.dotProduct doesn't allow mixing types, hence I consider doing it all over ERat and separately proving that A *ᵥ x is finite and that c ⬝ᵥ x is nonnegative (or at least does not contain negative infinity).

[Yaël Dillies]

Okay but docs#Matrix.dotProduct is a stupid wrapper for something more general, right? Why forcing you to use it?

[Martin Dvořák]

Yaël Dillies said:

Okay but docs#Matrix.dotProduct is a stupid wrapper for something more general, right? Why forcing you to use it?

Because there is a lot of API in terms of docs#Matrix.dotProduct and so on.

[Martin Dvořák]

And because my pseudoLP is nicely readable despite of being ill-defined.

[Yaël Dillies]

Again, non-problems

[Yaël Dillies]

The "lot of API in terms of Matrix.dotProduct" is just a bunch of wrappers around docs#Finset.sum lemmas

[Yaël Dillies]

∑ i, w i • v i is all around in mathlib

[Martin Dvořák]

Martin Dvořák said:

However, if it is desirable to have the weaker assumptions in Mathlib, I can try to change it in place and PR the change to Mathlib.

Should I take your @Yaël Dillies opinion as "no" regarding the potential refactor of docs#Matric.mulVec from [NonUnitalNonAssocSemiring α] to [Mul α] [AddCommMonoid α] as I was considering above?

[Yaël Dillies]

That' s a "no" indeed, since what you seem to really want is not even that but rather [SMul α β] [AddCommMonoid β]

[Martin Dvořák]

If we forget about my use case for a minute, what is best for Mathlib?

[Yaël Dillies]

Not have Matric.mulVec as a def

[Martin Dvořák]

Note that docs#Matrix.dotProduct uses [Mul α] [AddCommMonoid α] which is like halfway towards the general version.

[Martin Dvořák]

Yaël Dillies said:

Not have Matric.mulVec as a def

Would Matric.mulVec and Matrix.dotProduct be better as abbrev? Or not present in Mathlib at all?

[Yaël Dillies]

As notation, I would say

[Antoine Chambert-Loir]

Also, if you only use multiplication in particular cases , it may mean you require a module structure rather than a ring structure.

[Eric Wieser]

Martin Dvořák said:

Is there a good reason why docs#Matrix.mulVec requires [NonUnitalNonAssocSemiring α] despite docs#Matrix.dotProduct requiring [Mul α] [AddCommMonoid α] only?

I think it's just for conciseness; the second generality is pretty useless anyway, as the product isn't well-behaved at all

[Martin Dvořák]

Is the generality of [NonUnitalNonAssocSemiring α] as opposed to [Semiring α] useful?

In any case, I redefined Matrix.mulVec and Matrix.vecMul locally so that they require only [Mul α] [AddCommMonoid α] in the same manner as Matrix.dotProduct does.

[Jireh Loreaux]

Regarding non-unital semirings: sure. I'll want to consider matrices with entries in a (non-unital) C⋆-algebra acting on vectors of elements in that algebra. For example see: https://en.wikipedia.org/wiki/Hilbert_C*-module#C*-algebras (this doesn't mention the action of matrices, but you can imagine it's there).