AInterval

[Ralf Hemmecke]

Hi Waldek,

I've just created a pull request factoring out some interval arithmetic
that is not necessarily bound to floating point operatioons.

https://github.com/fricas/fricas/pull/200

If you accept, I will reformat to fit the FriCAS style, i.e. using

foo : Type

instead of

foo: Type

Ralf

[Waldek Hebisch]

Looks good. But I have some doubt about 'error?'. Namely,
various q-functions allow doing things without checking,
so 'qinterval' in principle may create an interval where
lower bound is bigger than the upper bound. But usual
convention is that it is responsibility of user of
q-functions to ensure that arguments are valid. And other
functions just assume that they deal with valid things.
Do you intend/need to create invalid intervals? If not,
then 'error?' looks redundant.

--
Waldek Hebisch

[Waldek Hebisch]

On Fri, Jun 20, 2025 at 10:55:32PM +0200, 'Ralf Hemmecke' via FriCAS - computer algebra system wrote:

BTW, did you think about making it a bit more general? IIUC
addition works the same for OrderedAbelianSemiGroup, subtraction
probably needs OrderedAbelianGroup, multiplicative operations
should work for Join(OrderedAbelianSemiGroup, SemiRng).

Also, AFAICS when you have Ring as an argument, then the result
is valid SemiRing.

This just a suggestion, if you do not want to generalize, then
it is fine.

--
Waldek Hebisch

[Ralf Hemmecke]

While looking into the generalization of AInterval, I realized that abs
is defined in OrderedRing.

https://fricas.github.io/api/OrderedRing.html#index-1

Technically, it would be OK to define it already in OrderedAbelianGroup.

Basically the definition is

abs(x) == if x>0 then x else -x

so why is there need to have a multiplication in the structure?

Ralf

[Waldek Hebisch]

Right, current location of abs is a historical artifact.

--
Waldek Hebisch

[Ralf Hemmecke]

Ooops. In OrderedRing I find

positive? x == x>0
negative? x == x<0
sign x ==
positive? x => 1
negative? x => -1
zero? x => 0
error "x satisfies neither positive?, negative? or zero?"
abs x ==
positive? x => x
negative? x => -x
zero? x => 0
error "x satisfies neither positive?, negative? or zero?"

If a ring is equipped with a total order, how can this error case ever
occur? It would mean there are elements that are neither 0 nor smaller
nor bigger than 0. What kind of total order is this?

Or is it taking care of the Float domain? But Float is only a fake ring
for convenience. In the long run I would like to take away the Ring
property from Float.

Anyway, if I now provide a patch in moving the above functions to
OrderedAbelianGroup, I would like to remove this error case. But I fear
that this might change something in other places of FriCAS.

Suggestions?

Ralf

[Waldek Hebisch]

On Sat, Jun 21, 2025 at 01:40:15PM +0200, 'Ralf Hemmecke' via FriCAS - computer algebra system wrote:
> Ooops. In OrderedRing I find
>
> positive? x == x>0
> negative? x == x<0
> sign x ==
> positive? x => 1
> negative? x => -1
> zero? x => 0
> error "x satisfies neither positive?, negative? or zero?"
> abs x ==
> positive? x => x
> negative? x => -x
> zero? x => 0
> error "x satisfies neither positive?, negative? or zero?"
>
> If a ring is equipped with a total order, how can this error case ever
> occur? It would mean there are elements that are neither 0 nor smaller nor
> bigger than 0. What kind of total order is this?
>
> Or is it taking care of the Float domain? But Float is only a fake ring for
> convenience. In the long run I would like to take away the Ring property
> from Float.

AFAICS Float has honest linear order. That could be for DoubleFloat
where due to IEEE thing hardware will return stupid results. But I
suspect that this is just "defensive" coding.

BTW: DoubleFloat should use hardware or system abs and sign, so our
definitions above should not matter for it.

> Anyway, if I now provide a patch in moving the above functions to
> OrderedAbelianGroup, I would like to remove this error case. But I fear that
> this might change something in other places of FriCAS.

I would probably write:

abs(x) ==
x < 0 => -x
x

and similar for sign. But error case does not bother me too much.
If there are bugs in say comparison routine, than getting error
is slightly better than propagating further wrong result.

Your current patch is reasonable. But it is also reasonable to
eliminate error cases.

BTW: You can find a few 'error "impossible"' instructions that
I wrote. Assuming that there are no errors in coding and
reasoning they will be never executed. But practice is
imperfect, and some of those actually produced error message.

--
Waldek Hebisch

[Ralf Hemmecke]

I just realized that

%%% (155) -> OrderedRing has OrderedSemiGroup

(155) false

Isn´t that something we should correct?

See attached patch.

Ralf

[Ralf Hemmecke]

We have a view places where the introduction of OrderedField would make
sense?

Opinions?

Ralf

grep '\<Field\>' *.spad | grep '\<OrderedRing\>'
crfp.spad: -- R : Join(Field, OrderedRing, CharacteristicZero)
crfp.spad: R : Join(Field, OrderedRing)
numeigen.spad: Par : Join(Field, OrderedRing) -- it will be NF or RN
numeigen.spad: Par : Join(Field, OrderedRing) -- Float or
RationalNumber
numeigen.spad: Par : Join(Field, OrderedRing) -- Float or
RationalNumber
numsolve.spad: Par : Join(Field, OrderedRing) -- will be Float or RN
numsolve.spad: Par : Join(Field, OrderedRing ) -- it will be NF or RN
numsolve.spad: Par : Join(OrderedRing, Field) -- RN or NewFloat
numsolve.spad: Par : Join(Field, OrderedRing)
reclos.spad: TheField : Join(OrderedRing, Field)
reclos.spad: TheField : Join(OrderedRing, Field)
reclos.spad: TheField : Join(OrderedRing, Field, RealConstant)
sf.spad: Join(Field, OrderedRing, RealConstant, RetractableTo Integer,
sf.spad:++ it is defined to be a join of a Field and OrderedRing, some of

[Waldek Hebisch]

On Sun, Jun 22, 2025 at 12:43:21PM +0200, 'Ralf Hemmecke' via FriCAS - computer algebra system wrote:
> We have a view places where the introduction of OrderedField would make
> sense?
>
> Opinions?

I tried to avoid having too many categories. Mathematically
OrderedField does not say more than Join(Field, OrderedRing).
But Spad compiler distinguishes the two, if you require
OrderedField for an argument, then Join(Field, OrderedRing)
is not enough. So requiring OrderedField we need to assert
it explicitely. Note that it does not work well with conditional
exports, we would need extra conditional rules for OrderedField
while currently rules for OrderedRing and Field are enough.

This probably does not make much difference for ordered fields,
but as a general rule due to propagation of conditions longish
Join-s in domain conditions are preferable to "shortcuts" like
OrderedField.

--
Waldek Hebisch

[Waldek Hebisch]

Yes. Please commit.

--
Waldek Hebisch

[Ralf Hemmecke]

On 6/21/25 00:02, Waldek Hebisch wrote:
> BTW, did you think about making it a bit more general?....

> Also, AFAICS when you have Ring as an argument, then the result
> is valid SemiRing.

I've just tried to make AIntervalCategory more general.

I hope I got the conditions and export categories correct.
Would be nice if someone could re-check.

https://github.com/fricas/fricas/pull/200

Ralf

[Waldek Hebisch]

ATM I did not look at conditions and categories. However,
I have noticed a different issue. Namely, Interval is
supposed to be an implementation of interval artithmetic.
Which means that interval obtained as result of
interval arithmetic is supposed to contain interval
computed using infinitely precise artithmtic. Since
operations in Float are approximate it means that
results of arithmetic operations on intervals need to be
enlarged to compensate for effect of rounding. This
is done by use of roundUp and roundDown in qinterval.

I did not check if roundUp and roundDown _always_ lead
to correct result, but without them results are clearly
incorrect.

So, most of operations in Interval should stay the same.

--
Waldek Hebisch

[Waldek Hebisch]

On Mon, Jun 23, 2025 at 12:29:20AM +0200, 'Ralf Hemmecke' via FriCAS - computer algebra system wrote:
> On 6/21/25 00:02, Waldek Hebisch wrote:
> > BTW, did you think about making it a bit more general?....
> > Also, AFAICS when you have Ring as an argument, then the result
> > is valid SemiRing.
>
> I've just tried to make AIntervalCategory more general.
>
> I hope I got the conditions and export categories correct.
> Would be nice if someone could re-check.

I think that instead of

if R has OrderedSemiGroup then
SemiRng
....

you need

if R has OrderedSemiGroup and R has SemiRng then
SemiRng
...

That is SemiGroup and AbelianSemiGroup do not imply distributivity,
so SemiRng assert more than this.

Similarly for OrderedMonoid.

Also, do you really mean Field without ordering restrictions for
unit?, inv and '/'? AFAICS on any field one can introduce
structure of OrderedAbelianGroup by using a well-ordered basis
over rational numbers and lexicograpic order on corresonding
vectors. But a lot of fields do not have order consitent
with field operations.

--
Waldek Hebisch

[Ralf Hemmecke]

On 6/23/25 02:00, Waldek Hebisch wrote:
> I think that instead of
>
> if R has OrderedSemiGroup then
> SemiRng
> ....
>
> you need
>
> if R has OrderedSemiGroup and R has SemiRng then
> SemiRng
> ...
>
> That is SemiGroup and AbelianSemiGroup do not imply distributivity,
> so SemiRng assert more than this.

Ah, right. I was paying too much attention on minimality and missed
that. Thanks.

> Also, do you really mean Field without ordering restrictions for
> unit?

I also corrected this. There are two commits, because I pushed too early
without realizing that there was still an error after the first patch. :-(

Ralf

[Ralf Hemmecke]

On 6/23/25 01:22, Waldek Hebisch wrote:
> ATM I did not look at conditions and categories. However,
> I have noticed a different issue. Namely, Interval is
> supposed to be an implementation of interval artithmetic.
> Which means that interval obtained as result of
> interval arithmetic is supposed to contain interval
> computed using infinitely precise artithmtic. Since
> operations in Float are approximate it means that
> results of arithmetic operations on intervals need to be
> enlarged to compensate for effect of rounding. This
> is done by use of roundUp and roundDown in qinterval.

Right. That is why qInterval has no default implementation. And Interval
does not inherit anything from AInterval only from AIntervalCategory.
AInterval is for the exact case, Interval for Floating point intervals.

> I did not check if roundUp and roundDown _always_ lead
> to correct result, but without them results are clearly
> incorrect.

Yes. But roundUp and roundDown are implemented / used in Interval and
there is no default package for IntervalCategory.

> So, most of operations in Interval should stay the same.

Yes, when I first designed AIntervalCategory, I had in mind that the
semantics of Interval should not change. Of course, I could have made a
mistake, but then it would have been unintentional.

Maybe I should come up with a number of tests?

Ralf

[Waldek Hebisch]

On Mon, Jun 23, 2025 at 08:12:06AM +0200, 'Ralf Hemmecke' via FriCAS - computer algebra system wrote:
> On 6/23/25 01:22, Waldek Hebisch wrote:
> > ATM I did not look at conditions and categories. However,
> > I have noticed a different issue. Namely, Interval is
> > supposed to be an implementation of interval artithmetic.
> > Which means that interval obtained as result of
> > interval arithmetic is supposed to contain interval
> > computed using infinitely precise artithmtic. Since
> > operations in Float are approximate it means that
> > results of arithmetic operations on intervals need to be
> > enlarged to compensate for effect of rounding. This
> > is done by use of roundUp and roundDown in qinterval.
>
> Right. That is why qInterval has no default implementation. And Interval
> does not inherit anything from AInterval only from AIntervalCategory.
> AInterval is for the exact case, Interval for Floating point intervals.

OK, your patch removes implementations of '+', '-', '*' but
defaults in AIntervalCategory call qinterval from Interval.

> > I did not check if roundUp and roundDown _always_ lead
> > to correct result, but without them results are clearly
> > incorrect.
>
> Yes. But roundUp and roundDown are implemented / used in Interval and there
> is no default package for IntervalCategory.
>
> > So, most of operations in Interval should stay the same.
>
> Yes, when I first designed AIntervalCategory, I had in mind that the
> semantics of Interval should not change. Of course, I could have made a
> mistake, but then it would have been unintentional.
>
> Maybe I should come up with a number of tests?

That is actually tricky. In case on Interval what matters are
tiny 1 bit differences which occur in special cases.

--
Waldek Hebisch

[Waldek Hebisch]

Looks OK now.

--
Waldek Hebisch

[Qian Yun]

Well, I think OrderedRing should not have OrderedMonoid.

(The quoted email says OrderedSemiGroup, but the attached patch
in quoted email and commit 7564b5d2 says OrderedMonoid.)

Because OrderedMonoid says if x < y, then for all z we have z*x < z*y.
But for OrderedRing, if x < y, then z*x < z*y only if z > 0.

The attached patch provides a fix.

But the conditions in AIntervalCategory are too complicated,
maybe there are still room to improve or simplify.

- Qian

[Ralf Hemmecke]

On 7/3/26 15:41, Qian Yun wrote:
> Well, I think OrderedRing should not have OrderedMonoid.

> (The quoted email says OrderedSemiGroup, but the attached patch
> in quoted email and commit 7564b5d2 says OrderedMonoid.)
>
> Because OrderedMonoid says if x < y, then for all z we have z*x < z*y.
> But for OrderedRing, if x < y, then z*x < z*y only if z > 0.

Gosh... you are completely right. Good catch.

The order should respect the + operation. OrderedMonoid or
OrderedSemiGroup alone is certainly wrong.
Maybe this was just a "typo" on my side and I actually mean
OrderedAbelianSemiGroup. I must check more carefully.

> The attached patch provides a fix.

I must think about this more.

> But the conditions in AIntervalCategory are too complicated,
> maybe there are still room to improve or simplify.

True. I guess, I have to add a few more OrderedAbelian... conditions in
ainterval.spad. Give me some time.

Ralf

[Waldek Hebisch]

On Fri, Jul 03, 2026 at 09:41:00PM +0800, Qian Yun wrote:
> Well, I think OrderedRing should not have OrderedMonoid.
>
> (The quoted email says OrderedSemiGroup, but the attached patch
> in quoted email and commit 7564b5d2 says OrderedMonoid.)
>
> Because OrderedMonoid says if x < y, then for all z we have z*x < z*y.
> But for OrderedRing, if x < y, then z*x < z*y only if z > 0.

Clearly there is a contradiction. But it is not clear to me
how we should resolve it. One possibility is to change axioms
of OrderedMonoid. Another possibility is to have two different
categories. Another possibility is to replace OrderedMonoid
by OrderedRing in many conditions.

Currently 8 categories inherit OrderedMonoid and they do this
via OrderedRing. 26 domains have OrderedMonoid, most of those
are rings. FreeMonoid is not a Ring, but it does not have zero.
InfiniteCyclicGroup also is not a Ring. Since it uses multiplicative
notation formally it does not have zero.

So is we change axiom so that current axioms only apply when
there is no zero and in presence of zero we have ring-like
axiom, then it seems that all current domains will satisfy
changed axioms. Of course, there is a question if code
is compatible with changed axioms.

BTW: Element z of a semigroup S is called zero if for all
x in S we have z*x = z and x*z = z. It is easy to check
that zero, if exists is unique. And clearly no semigroup
with zero can satisfy original axioms of OrderedMonoid.

--
Waldek Hebisch

[Ralf Hemmecke]

On 7/3/26 16:59, Waldek Hebisch wrote:
> Clearly there is a contradiction. But it is not clear to me how we
> should resolve it. One possibility is to change axioms of
> OrderedMonoid. Another possibility is to have two different
> categories. Another possibility is to replace OrderedMonoid by

> OrderedRing in many condition.

Oh, I did not think in this direction.

> BTW: Element z of a semigroup S is called zero if for all x in S we
> have z*x = z and x*z = z.

> And clearly no semigroup with zero can satisfy original axioms of
> OrderedMonoid.

True. So a multiplicative ordered structure can only exist if there is
no zero. In other words declaring some structure to export
OrderedSemiGroup, automatically claims that there is no zero in the
structure, i.e. a structure Join(OrderedSemiGroup, AbelianGroup) does
not exist.

Ralf

[Waldek Hebisch]

Not so bad. We have problem only when addition and multiplication
are related is a special way. But for expample integers where
both '+' and '*' means addition is OK.

BTW: In the past I used the following domain:

)abbrev domain REVINT ReverseOrderInteger
-- Integers with reverse order. Since order is reverse it fails to be
-- an ordered ring
ReverseOrderInteger : Join(IntegralDomain, OrderedSet, ConvertibleTo Integer,
RetractableTo Integer) == Integer add
(x : %) < (y : %) == (y pretend Integer) < (x pretend Integer)
(x : %) > (y : %) == (x pretend Integer) < (y pretend Integer)
(x : %) <= (y : %) == (y pretend Integer) <= (x pretend Integer)
(x : %) >= (y : %) == (x pretend Integer) <= (y pretend Integer)


Later I obtained desired effect in a different way, but domains
like this could be useful to test soundness of our type system.

--
Waldek Hebisch

[Ralf Hemmecke]

On 7/3/26 19:55, Waldek Hebisch wrote:
> Not so bad. We have problem only when addition and multiplication
> are related is a special way. But for expample integers where
> both '+' and '*' means addition is OK.

Well, but if * also means addition, wouldn't that then also be
commutative and I had to use OrderedAbelian(Semi)Group (important:
"Abelian" in the name)?

Otherwise, true. If there is no distributive law, then ...
But let's restrict to rings.

> BTW: In the past I used the following domain:
>
> )abbrev domain REVINT ReverseOrderInteger
> -- Integers with reverse order. Since order is reverse it fails to be
> -- an ordered ring
> ReverseOrderInteger : Join(IntegralDomain, OrderedSet, ConvertibleTo Integer,
> RetractableTo Integer) == Integer add
> (x : %) < (y : %) == (y pretend Integer) < (x pretend Integer)
> (x : %) > (y : %) == (x pretend Integer) < (y pretend Integer)
> (x : %) <= (y : %) == (y pretend Integer) <= (x pretend Integer)
> (x : %) >= (y : %) == (x pretend Integer) <= (y pretend Integer)
>
>
> Later I obtained desired effect in a different way, but domains
> like this could be useful to test soundness of our type system.

Hmmm, maybe our axiom for OrderedRing is just one of the definitions.

https://en.wiktionary.org/wiki/ordered_ring

We have

=========================
++ Axiom:
++ \spad{0 < a and b < c => ab < ac}

OrderedRing() : Category == Join(OrderedAbelianGroup, Ring,
CharacteristicZero)
=========================
and OrderedAbelianGroup inherits from
=========================
++ \spad{ x < y => x+z < y+z}
OrderedAbelianSemiGroup() : Category == Join(OrderedSet, AbelianSemiGroup)
=========================

The the definition here:

https://en.wikipedia.org/wiki/Ordered_ring

just says x>=0 and y>=0 implies x*y>=0.

If we defined the axioms for OrderedRing like on wikipedia, your
ReverseOrderInteger would also not fit.
In fact, ReverseOrderInteger just uses a different symbol for <, namely
">", so it is just renaming, right.

This is something we cannot model in SPAD. It's a bit like the problem
that we must have Group and AbelianGroup to distinguish between additive
and multiplicative structures. I haven't yet heard of any programming
language that can capture true mathmatical structures.

Ralf

[Waldek Hebisch]

On Fri, Jul 03, 2026 at 11:31:08PM +0200, 'Ralf Hemmecke' via FriCAS - computer algebra system wrote:
> On 7/3/26 19:55, Waldek Hebisch wrote:
> > Not so bad. We have problem only when addition and multiplication
> > are related is a special way. But for expample integers where
> > both '+' and '*' means addition is OK.
>
> Well, but if * also means addition, wouldn't that then also be commutative
> and I had to use OrderedAbelian(Semi)Group (important: "Abelian" in the
> name)?

Of course in such case '*' is commutative. But nothing forbids such
use, see InfiniteCyclicGroup.

> Otherwise, true. If there is no distributive law, then ...

Exactly.

AFAICS both definitions are equivalent. Our is just more explicit.

> In fact, ReverseOrderInteger just uses a different symbol for <, namely ">",
> so it is just renaming, right.

Yes. But various interfaces, like Heap, hardcode names of operations.
To use them you may need renaming (or something more complicated).

> This is something we cannot model in SPAD. It's a bit like the problem that
> we must have Group and AbelianGroup to distinguish between additive and
> multiplicative structures. I haven't yet heard of any programming language
> that can capture true mathmatical structures.

Here we go into dangerous direction. On one hand, in math renaming
is considered to be trivial. OTOH in practice mathematicians
assume usual names of operations. Semigroup people study zero(es)
(two sided zero is unique, but there can be multiple say left zeros),
but usually do not use additive notation for such semigroups,
even if they are commutative.

Traditional math notation is highly context sensitive, to model
that we would have so carry context everywhere. But how context
affects things is very ad-hoc, so I would prefer to _not_ go
in such direction. More precisely, for some computations it
make sense to formulate them as conditional rewrites, it makes
sense to have context here carrying common conditions. But in
general implicit context like in human math is IMHO not
appropriate in computerised system.

--
Waldek Hebisch

[Waldek Hebisch]

On Fri, Jul 03, 2026 at 04:59:01PM +0200, Waldek Hebisch wrote:
> On Fri, Jul 03, 2026 at 09:41:00PM +0800, Qian Yun wrote:
> > Well, I think OrderedRing should not have OrderedMonoid.
> >
> > (The quoted email says OrderedSemiGroup, but the attached patch
> > in quoted email and commit 7564b5d2 says OrderedMonoid.)
> >
> > Because OrderedMonoid says if x < y, then for all z we have z*x < z*y.
> > But for OrderedRing, if x < y, then z*x < z*y only if z > 0.
>
> Clearly there is a contradiction. But it is not clear to me
> how we should resolve it. One possibility is to change axioms
> of OrderedMonoid.

Attaches is a patch with new axioms. If nobody finds problem
with then I am going to commit it.

--
Waldek Hebisch

[Qian Yun]

I don't like it. It loses the "for all" property.
What does OrderedSemiGroup have 0 (addition identity) mean?

Counter example found by LLM:

=======
Consider the set of real numbers \mathbb{R} under a modified
associative operation \star:
x \star y = x \cdot y if y > 0
x \star y = 0 if y \le 0
This operation \star is associative and compatible with the standard
total order of \mathbb{R}.
The element 0 is indeed a semigroup zero since:
0 \star x = 0 (for both x > 0 and x \le 0)
x \star 0 = 0 (for all x in \mathbb{R})
Now, let x = 1, y = 2 (so x < y). Let the multiplier be z = -1 < 0.
According to the proposed axioms, we should have:
x \star z > y \star z => 1 \star (-1) > 2 \star (-1)
But since z \le 0, by our operation definition:
1 \star (-1) = 0 and 2 \star (-1) = 0
Thus, we would require 0 > 0, which is FALSE.
========


My view is that: multiplication comes from two places:
one is Group, another one is Ring.

I think we should simply remove OrderedMonoid from OrderedRing,
and keep current axioms.

- Qian

[Waldek Hebisch]

On Sun, Jul 05, 2026 at 07:51:32AM +0800, Qian Yun wrote:
> On 7/4/26 11:08 PM, Waldek Hebisch wrote:
> > On Fri, Jul 03, 2026 at 04:59:01PM +0200, Waldek Hebisch wrote:
> >> On Fri, Jul 03, 2026 at 09:41:00PM +0800, Qian Yun wrote:
> >>> Well, I think OrderedRing should not have OrderedMonoid.
> >>>
> >>> (The quoted email says OrderedSemiGroup, but the attached patch
> >>> in quoted email and commit 7564b5d2 says OrderedMonoid.)
> >>>
> >>> Because OrderedMonoid says if x < y, then for all z we have z*x < z*y.
> >>> But for OrderedRing, if x < y, then z*x < z*y only if z > 0.
> >>
> >> Clearly there is a contradiction. But it is not clear to me
> >> how we should resolve it. One possibility is to change axioms
> >> of OrderedMonoid.
> >
> > Attaches is a patch with new axioms. If nobody finds problem
> > with then I am going to commit it.
> >
>
> I don't like it. It loses the "for all" property.

Well, we have "for all" propety. Simply it is split into
3 cases that cover everything.

> What does OrderedSemiGroup have 0 (addition identity) mean?

As explained in the patch 0 here means semigroup zero (no
assumption about existence of addition):

+++ we say that a semigroup has zero if there exists element z
+++ such that for all x we have z*x = x*z = z. Below we will
+++ write 0 instead of z.

>
> Counter example found by LLM:
>
> =======
> Consider the set of real numbers \mathbb{R} under a modified
> associative operation \star:
> x \star y = x \cdot y if y > 0
> x \star y = 0 if y \le 0
> This operation \star is associative and compatible with the standard
> total order of \mathbb{R}.
> The element 0 is indeed a semigroup zero since:
> 0 \star x = 0 (for both x > 0 and x \le 0)
> x \star 0 = 0 (for all x in \mathbb{R})
> Now, let x = 1, y = 2 (so x < y). Let the multiplier be z = -1 < 0.
> According to the proposed axioms, we should have:
> x \star z > y \star z => 1 \star (-1) > 2 \star (-1)
> But since z \le 0, by our operation definition:
> 1 \star (-1) = 0 and 2 \star (-1) = 0
> Thus, we would require 0 > 0, which is FALSE.
> ========

Note that \star fails our current axioms for the same reason:
our axioms require strict inequality (in fact, as I wrote _any_
semigroup with zero fails our axioms). And we want strict
inequality because it holds in popular structures and has
strong consequences.

You may also look at max + semiring. That is nonegative real
numbers with two operations. One, playing the role of additions
is x \oplus y = max(x, y), second, playing role of multiplication
is x \otimes y = x + y. This is a semiring, that is both
\oplus and \otimes are associative, and distributive law holds.
There is no zero and it is OrderedSemigroup according to our
axioms. OTOH it is not OrderedAbelianSemigroup, because
inequality is not strict.

If you want to handle semigroups as above, you need different
axioms. We could have condition like WeakMonotonicityOfAddition,
StrongMonotonicityOfMultiplication or SignedMonotonicityOfMultiplication.
The first two hopefully are clear, the last one means the
axiom I gave. But I am not eager to use such names.

Part of the problem is that our categories are named
and there is limited supply of good names. Unfortunately,
in mathematical practice names are reused and made to carry
different meanings in different areas (and sometimes within
a single area).

> My view is that: multiplication comes from two places:
> one is Group, another one is Ring.

Well, "typical" homogeneous '*' comes from Magma. There is a
bunch if inhomogeneous ones due to module-like structures.
And some in domains that do not fit well into our category
structure. Now, strict inequality for all elements implies
cancelation property, so if you have semigroup you can
embed it into a group. Semigrup with zero can not be embedded
into a group. Since the example above fails our axioms,
it can not be embedded into an ordered ring. So in view of
the example do you want to keep your view?

> I think we should simply remove OrderedMonoid from OrderedRing,
> and keep current axioms.

If you remove OrderedMonoid from OrderedRing, then build fails. So
you need to adjust conditions. ATM it seems that definition I gave
is the simplest possible adjustment.

--
Waldek Hebisch

[Qian Yun]

On 7/5/26 9:23 AM, Waldek Hebisch wrote:
>
>> I think we should simply remove OrderedMonoid from OrderedRing,
>> and keep current axioms.
>
> If you remove OrderedMonoid from OrderedRing, then build fails. So
> you need to adjust conditions. ATM it seems that definition I gave
> is the simplest possible adjustment.
>

If we remove OrderedMonoid from OrderedRing, then build only fails
at AIntervalCategory, and is easily fixed.

I kind of understand your reasoning, but it still bothers me
that in common literature, the axiom for ordered semigroup
is if x<y then for all z, x*z<y*z.

In your patch, '\' is missing in front of 'spad{z < 0}'.
And typo 'than -> then'.
Also it's better to use a,b,c instead of x,y,z, and leave
symbol z for 0.

- Qian

[Ralf Hemmecke]

On 7/5/26 10:51, Qian Yun wrote:
>>> I think we should simply remove OrderedMonoid from OrderedRing,
>>> and keep current axioms.

I also tend(ed) to remove OrderedMonoid from OrderedRing. (I cannot decide.)

However, Waldek's proposal is certainly an improvement. It explicitly
states the axioms.
Actually, we currently only say
'Semigroups with compatible ordering.'

I support Waldek's patch.
I'm not a native English speaker, but insted of
Ordered semigroups which are also a monoid.
I would write
Ordered semigroups which are also monoids.
(i.e. plural in both cases).

On 7/5/26 17:04, Waldek Hebisch wrote:
> Yes, OrderedMonoid does not add new axioms. We should replace
> it by Join(OrderedSemiGroup, Monoid)

Personally, I liked having names for known structure/categories and
didn't like when Waldek introduced something like

Join(SemiRng, AbelianMonoid)

instead of using a separately named category. But I now see, that
because of the rule "a domain belongs to a category by assertion", named
categories are somewhat inflexible in 'has' expressions. Aldor
introduced the concept of post-facto-extensions
https://www.aldor.org/docs/HTML/chap10.html which is (unfortunately) not
present in SPAD.

I currently think that introducing a named category that does not
introduce explicit new axioms is unnecessary. So OrderedMonoid could, in
fact, just be a macro.

>> If you remove OrderedMonoid from OrderedRing, then build fails. So
>> you need to adjust conditions. ATM it seems that definition I gave
>> is the simplest possible adjustment.

> If we remove OrderedMonoid from OrderedRing, then build only fails
> at AIntervalCategory, and is easily fixed.

I will propose something for AIntervalCategory soon. I'll try not to use
OrderedMonoid.

> I kind of understand your reasoning, but it still bothers me
> that in common literature, the axiom for ordered semigroup
> is if x<y then for all z, x*z<y*z.

Well, if the structure has no zero, there is no difference.
If there is, then you wouldn't call it a "ordered semigroup".
If I look at https://en.wikipedia.org/wiki/Ordered_semigroup, then it
says that only a partial order is assumed, i.e. some elements can be
incomparable. Our category anyhow claims a total order, i.e.
OrderedSemiGroup does not actually capture partially ordered sets with a
semigroup structure. That is also unfortunate, but changing that would
probably need a lot of checks in the library.

> In your patch, '\' is missing in front of 'spad{z < 0}'.
> And typo 'than -> then'.

Yes.

> Also it's better to use a,b,c instead of x,y,z, and leave
> symbol z for 0.

It is mathematically irrelevant, but not using z in the last two
paragraphs would avoid possible confusion, so I somehow support Qian's
argument.

Ralf

[Qian Yun]

On 7/5/26 9:23 AM, Waldek Hebisch wrote:
>

> If you want to handle semigroups as above, you need different
> axioms. We could have condition like WeakMonotonicityOfAddition,
> StrongMonotonicityOfMultiplication or SignedMonotonicityOfMultiplication.
> The first two hopefully are clear, the last one means the
> axiom I gave. But I am not eager to use such names.

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/GroupWithZero/Defs.html

Seems lean/mathlib4 have something like that.

But currently we don't have a need for those fine distinctions?

- Qian

[Ralf Hemmecke]

On 7/5/26 23:12, 'Ralf Hemmecke' via FriCAS - computer algebra system wrote:
> I will propose something for AIntervalCategory soon. I'll try not to use
> OrderedMonoid.

Well, I must take it back. With the proposed patch (introducing axioms
in OrderedSemiGroup), there is actually no need to change anything in
AIntervalCategory.

For a while I was thinking that I should remove the order condition on
the multiplicative part. However, that would be wrong, since with

x in [a, b]

we want

r*x in r * [a, b] = [inf(r*a, r*b), sup(r*a, r*b)]

which certainly requires compatibility with the multiplicative structure.

As I see it now, I don't have to change anything in ainterval.spad.

Ralf

[Qian Yun]

So, a summary:

Zero can't be in a Group, because it has no inverse.

But zero can be in a SemiGroup.

SemiGroup with zero has new axiom.

Ordered SemiGroup with zero has another new axiom.

I guess Waldek wants to merged this new axiom into OrderedSemiGroup
because currently we don't have a need for this separate
OrderedSemiGroupWithZero.

So there is a gap between OrderedSemiGroup and OrderedRing.
But currently in fricas, there's no domain that satisfies
OrderedSemiGroupWithZero but fails to satisfy OrderedRing.

I guess we can leave it alone until the need rises?

- Qian

[Waldek Hebisch]

On Tue, Jul 07, 2026 at 07:32:10AM +0800, Qian Yun wrote:
> So, a summary:
>
> Zero can't be in a Group, because it has no inverse.
>
> But zero can be in a SemiGroup.
>
> SemiGroup with zero has new axiom.
>
> Ordered SemiGroup with zero has another new axiom.
>
> I guess Waldek wants to merged this new axiom into OrderedSemiGroup
> because currently we don't have a need for this separate
> OrderedSemiGroupWithZero.
>
> So there is a gap between OrderedSemiGroup and OrderedRing.
> But currently in fricas, there's no domain that satisfies
> OrderedSemiGroupWithZero but fails to satisfy OrderedRing.

Well, there is. NonNegativeInteger is only a semiring, not a ring.
Its multiplicative semigroup has zero and satisfies new axiom
(but not the old one). Currently we have

(6) -> NNI has OrderedSemiGroup

(6) false
Type: Boolean
(7) -> NNI has OrderedMonoid

(7) false
Type: Boolean
which agrees with old definition.

> I guess we can leave it alone until the need rises?

There is no pressing need to better express ordering properties of
NonNegativeInteger. We also have SmallOrdinal. With "natural"
operations it is a semiring that also statisfies new axiom. With
"ordered" operations things get more complex, namely "ordered"
operations are monotonic, but not strictly monotonic.

--
Waldek Hebisch

[Qian Yun]

(I clicked "Reply" instead of "Reply to mailing list", resending.)

If you want to use the new axioms, then code in mring.spad
will need to be changed:

if M has OrderedMonoid then
-- we use that multiplying an ordered list of monoid elements
-- by a single element respects the ordering
if R has noZeroDivisors then
a : % * b : % ==
+/[[[ta.Mn*tb.Mn, ta.Cf*tb.Cf]$Term
for tb in b ] for ta in reverse a]

(The "+" assumes argument don't contains duplicated "k:M",
if one of them is 0, then a list of 0 will be at the end
of result.)

And how to test if M has 0, by "if M has 0 : () -> M"?

So if you want to add the new axioms, it's better to give
it a new name, instead of putting axioms under conditions
in OrderedSemiGroup. Otherwise the user still have to
differentiate the two cases.


Also, it seems that in fricas, to make the axioms useful for
algorithms (have more nice properties), we are preferring
total order over partial order, and strictly monotonic
over monotonic.

- Qian

[Waldek Hebisch]

On Tue, Jul 07, 2026 at 05:30:23PM +0800, Qian Yun wrote:
> (I clicked "Reply" instead of "Reply to mailing list", resending.)
>
> If you want to use the new axioms, then code in mring.spad
> will need to be changed:
>
> if M has OrderedMonoid then
> -- we use that multiplying an ordered list of monoid elements
> -- by a single element respects the ordering
> if R has noZeroDivisors then
> a : % * b : % ==
> +/[[[ta.Mn*tb.Mn, ta.Cf*tb.Cf]$Term
> for tb in b ] for ta in reverse a]
>
> (The "+" assumes argument don't contains duplicated "k:M",
> if one of them is 0, then a list of 0 will be at the end
> of result.)
>
> And how to test if M has 0, by "if M has 0 : () -> M"?
>
> So if you want to add the new axioms, it's better to give
> it a new name, instead of putting axioms under conditions
> in OrderedSemiGroup. Otherwise the user still have to
> differentiate the two cases.
>
>
> Also, it seems that in fricas, to make the axioms useful for
> algorithms (have more nice properties), we are preferring
> total order over partial order, and strictly monotonic
> over monotonic.

Yes, there is trouble in mring.spad and possibly in other
places. To see what is best I think we should simplify
current conditions. AFAICS currently we have two base
conditions, that is OrderedAbelianSemiGroup and
OrderedSemiGroup. OrderedAbelianMonoid, OrderedAbelianGroup
and OrderedCancellationAbelianMonoid are redunant, that is
can be replaced by appropriate Join-s. Similary,
OrderedMonoid is redundant. Condition in OrderedRing is
different than condition needed in mring, so we need
third base condition. As first step I would try to get
rid of redundant categories, that is OrderedAbelianMonoid,
OrderedAbelianGroup, OrderedCancellationAbelianMonoid
and OrderedMonoid. Actually, removing OrderedAbelianGroup,
OrderedCancellationAbelianMonoid and OrderedMonoid looks easy
(I have a working patch). OrderedAbelianMonoid is used in
about 30 places, removing it should not be hard but look a
bit tedious.

To fix OrderedRing we probably should add OrderedSemigroupWithZero
having new axiom and exporting 0. Then we can define

OrderedRing() : Category == Join(OrderedAbelianSemiGriup,
OrderedSemiGroupWithZero, Ring, CharacteristicZero)


--
Waldek Hebisch

[Qian Yun]

Agreed with the two-step approach.

I can also accept with addition of OrderedSemiGroupWithZero.

Just saying, after the changes, only OrderedRing will have
this new property, (maybe NNI as well), right?

- Qian

[Waldek Hebisch]

On Fri, Jul 10, 2026 at 11:01:23AM +0800, Qian Yun wrote:
> Agreed with the two-step approach.
>
> I can also accept with addition of OrderedSemiGroupWithZero.
>
> Just saying, after the changes, only OrderedRing will have
> this new property, (maybe NNI as well), right?

We have NonNegativeRational and SmallOrdinal which are only
semirings. And we could propagate this property to polynomials
over semirings (and possibly fractions). There are general
constructions: given an ordered semigroup we can add zero to
it (getting semigroup where all elements are nonnegative) or
we can add zero and mirror copy of the semigroup (getting
a semigroup with negative elements). So potentially there
is a collention of domais which will have this poperty, but
are not rings.

> On 7/10/26 10:53 AM, Waldek Hebisch wrote:
> >
> > Yes, there is trouble in mring.spad and possibly in other
> > places. To see what is best I think we should simplify
> > current conditions. AFAICS currently we have two base
> > conditions, that is OrderedAbelianSemiGroup and
> > OrderedSemiGroup. OrderedAbelianMonoid, OrderedAbelianGroup
> > and OrderedCancellationAbelianMonoid are redunant, that is
> > can be replaced by appropriate Join-s. Similary,
> > OrderedMonoid is redundant. Condition in OrderedRing is
> > different than condition needed in mring, so we need
> > third base condition. As first step I would try to get
> > rid of redundant categories, that is OrderedAbelianMonoid,
> > OrderedAbelianGroup, OrderedCancellationAbelianMonoid
> > and OrderedMonoid. Actually, removing OrderedAbelianGroup,
> > OrderedCancellationAbelianMonoid and OrderedMonoid looks easy
> > (I have a working patch). OrderedAbelianMonoid is used in
> > about 30 places, removing it should not be hard but look a
> > bit tedious.
> >
> > To fix OrderedRing we probably should add OrderedSemigroupWithZero
> > having new axiom and exporting 0. Then we can define
> >
> > OrderedRing() : Category == Join(OrderedAbelianSemiGriup,
> > OrderedSemiGroupWithZero, Ring, CharacteristicZero)
> >
> >
>

> --
> You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to fricas-devel...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/fricas-devel/9a1db48d-7adb-42ae-ac35-fa76aa47c7a0%40gmail.com.

--
Waldek Hebisch

[Waldek Hebisch]

On Fri, Jul 10, 2026 at 11:01:23AM +0800, Qian Yun wrote:

> Agreed with the two-step approach.
>
> I can also accept with addition of OrderedSemiGroupWithZero.
>
> Just saying, after the changes, only OrderedRing will have
> this new property, (maybe NNI as well), right?

Attached is a prelimnary patch. Main thing is new category
SetWithZero and OrderedSemiGroupWithZero. But to properly
propagate conditions and avoid dumplicate signature I had
reorganize several other categories and domains. I also
did part of proposed simplification and some that I did not
mention earlier (removal of OrderedFinite and OrderedIntegralDomain).
ATM I keep OrderedAbelianMonoid, as removing it would make patch
bigger. I also removed unsoud propagation of OrderedSet from
QFCAT.

> On 7/10/26 10:53 AM, Waldek Hebisch wrote:
> >
> > Yes, there is trouble in mring.spad and possibly in other
> > places. To see what is best I think we should simplify
> > current conditions. AFAICS currently we have two base
> > conditions, that is OrderedAbelianSemiGroup and
> > OrderedSemiGroup. OrderedAbelianMonoid, OrderedAbelianGroup
> > and OrderedCancellationAbelianMonoid are redunant, that is
> > can be replaced by appropriate Join-s. Similary,
> > OrderedMonoid is redundant. Condition in OrderedRing is
> > different than condition needed in mring, so we need
> > third base condition. As first step I would try to get
> > rid of redundant categories, that is OrderedAbelianMonoid,
> > OrderedAbelianGroup, OrderedCancellationAbelianMonoid
> > and OrderedMonoid. Actually, removing OrderedAbelianGroup,
> > OrderedCancellationAbelianMonoid and OrderedMonoid looks easy
> > (I have a working patch). OrderedAbelianMonoid is used in
> > about 30 places, removing it should not be hard but look a
> > bit tedious.
> >
> > To fix OrderedRing we probably should add OrderedSemigroupWithZero
> > having new axiom and exporting 0. Then we can define
> >
> > OrderedRing() : Category == Join(OrderedAbelianSemiGriup,
> > OrderedSemiGroupWithZero, Ring, CharacteristicZero)
> >

--
Waldek Hebisch

[Qian Yun]

1. src/algebra/exposed.lsp is not updated accordingly.

2. The axioms for OrderedMonoid should be copied to
OrderedSemiGroup.

3. For AIntervalCategory, use the following?

if R has SetWithZero then SetWithZero

and the exports and implementation involving "^" seems
to be complicated and can be simplified.

- Qian