Redundant categories

[Waldek Hebisch]

Several categories are redundant, that is logically thay say the
same thing as appropriate Join (but due to Spad semantics introduce
unneeded differences). For example

OrderedAbelianMonoid() : Category ==
Join(OrderedAbelianSemiGroup, AbelianMonoid)

OrderedCancellationAbelianMonoid() : Category ==
Join(OrderedAbelianMonoid, CancellationAbelianMonoid)

OrderedFinite() : Category == Join(OrderedSet, Finite)

OrderedIntegralDomain() : Category ==
Join(IntegralDomain, OrderedRing)

OrderedMonoid() : Category == Join(OrderedSemiGroup, Monoid)


Some cases are bordeline, like:

OrderedRing() : Category == Join(OrderedAbelianGroup, OrderedMonoid, Ring,
CharacteristicZero)

Namely, Join(OrderedAbelianGroup, OrderedMonoid, Ring) implies
CharacteristicZero, but CharacteristicZero has to be asserted in
some place.

In some cases categories introduce extra signatures, this is the
case with OrderedAbelianGroup. In this case we could conditionaly
introduce signatures in OrderedAbelianSemiGroup.

I am thinking about removing redundant definitions above. Or maybe
use definitions like:

OrderedAbelianMonoid() == Join(OrderedAbelianSemiGroup, AbelianMonoid)

and teach Spad compiler to handle them correctly (that is essentially
as a global macro which on use expands to appropriate Join).

BTW: I am looking at a problem with RealClosure and the first thing that
I have noticed is that RealClosure does not export OrderedIntegralDomain.
So I checked deeper and it turned out that OrderedIntegralDomain is
essentially unused. AFAICS the only domains that assert
OrderedIntegralDomain are Integer and Fraction(Integer). The point
here is that correctly maintaing such redundant categories takes
effort and they may lead to false conjectures during debugging,
so there is non-negligable cost of keeping them.

--
Waldek Hebisch

[Ralf Hemmecke]

Hi Waldek, (hi Peter)

I must say that initially I was against removing those categories that
you listed. There is some convenience having just one category instead
of a Join.

However, in the cases you listed, there is indeed no new information in
the additional category.

That is different in

CharacteristicZero() : Category == Ring

Maybe, the guiding principle for a separate category should be that it
introduces additional axioms that cannot concluded from the axioms that
the arguments of the Join impose.
It would be supercool if there were a formal way to specify those axioms
(even if they are not (yet) used by the compiler). We should be able to
formally specify them in (an extended) SPAD and even to ask a domain for
its axioms. Actually, the axioms coverning each category should already
be present at least in the ++ docstrings.

That said, I think I am fine with removal of those categories.

Well, complete removal might be tricky, since there is certainly
external code around (my QEta package is one of them) that uses
OrderedAbelianMonoid.

As for

> OrderedAbelianMonoid() == Join(OrderedAbelianSemiGroup, AbelianMonoid)

... already during my Aldor times I saw such statements and was (and I
still) am unsure, what the meaning of == here actually is.

I have the impression that the above is a little different from

OrderedAbelianMonoid(): Category == Join(OrderedAbelianSemiGroup,
AbelianMonoid)

but I have no idea in which way. And hopefully there is no additional
difference in meaning between Aldor and SPAD.

Peter, can you say something about "==" with and without the ":Category"
specification on the left-hand side?

Ralf

[Tim Daly]

Based on my experience I would suggest that just adding the 

axioms to the docstrings isn't useful. Nobody maintains

docstrings and nobody bothers to create them. At best every

docstring should have ++URL pointers to papers related to the code.

The point of the SANE version of Axiom is to merge LEAN axioms

and definitions with Axiom. They are strongly typed already.

My chosen path is to add another tower in parallel with the Category

and Domain towers, e.g. a Grounding Tower. The Ring category would 

have a RingProof "Grounding" which contains all of the Ring definitions 

and axioms. These are available to the compiler to prove code in 

anything that uses Ring.

Axiom types would have parallel expression in the Proof tower

(e.g. containing "RingProof") so they can be accumulated as you 

ascend the towers.

Adding axioms in this way has the advantage that the current code

doesn't need to be changed immediately. It allows the compiler to

gather all of the axioms applicable to a Domain. These axioms

and the SPAD code can be sent to the LEAN compiler to prove

the algorithms in the Domain correct.

In this way you can prove that GCD gets used correctly and

will deliver proven results. Once proven, GCD could be used

everywhere in further proofs.

Groebner code has already been proven. Why isn't the proof

part of Axiom?

In the long term SPAD code should migrate to LEAN code

to produce proven mathematics that can interact and compute.

This is a much better path than Aldor. Heck, even "real mathematicians"

might concede that it "could be useful" :-)

Tim

SANE synonyms:  rational, coherent, judicious, sound

[Tim Daly]

By the way, you're already behind the curve. The day is coming

(next month?) where the algorithms are proven by Claude?

https://youtu.be/JKk77rzOL34

Tim

--
You received this message because you are subscribed to a topic in the Google Groups "FriCAS - computer algebra system" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/fricas-devel/OFrwS22IefU/unsubscribe.
To unsubscribe from this group and all its topics, send an email to fricas-devel...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/fricas-devel/c3531b84-35c3-42e9-9ff3-f3e814428f5dn%40googlegroups.com.

[Grégory Vanuxem]

Hello Tim, *,

Le mer. 25 févr. 2026 à 09:21, Tim Daly <axio...@gmail.com> a écrit :
>
> Based on my experience I would suggest that just adding the
> axioms to the docstrings isn't useful. Nobody maintains
> docstrings and nobody bothers to create them. At best every
> docstring should have ++URL pointers to papers related to the code.

Just about this. I also do not see a point to add axioms in
docstrings, particularly for categories evoked in this discussion. An
undergraduate course in Algebra gives this easily. Concerning, ++URL,
I think it would be very good to have a \link{name}{URL} or something
like that. This isn't handled yet, and I'd often like to provide links
to the Julia modules I interface with (for example, the Nemo
documentation[1] parts). In fact for the categories discussed here I
wonder which link you would give. A book? Personally I love Algebra
of Serge Lang though it is not very accessible to a beginner, an URL,
Wikipedia? Hmm hmm that's difficult to choose. For a book or an URL.

Concerning maintaining usual docstrings (operations), almost 20% of my
docstrings are AI generated and after check/fix that suits my needs. I
would also say that now the majority of my .input 'make check's are
also done by AI, I use AI principally for unappealing things to me. So
"nobody maintains docstrings and nobody bothers to create them" is
(can be) wrong I think.

After, for the rest, LEAN, proving algorithms, and all that stuff is
beyond my knowledge, I leave this for others, like you for example. I
have almost no knowledge about this in computer logic/mathematics.

Greg

[1] https://nemocas.github.io/Nemo.jl/latest/

[Tim Daly]

I have added code to make URLs "live" so you can click on a link.

Of course, Axiom source cods is in book form using LaTex so it is 

easy to add live links in books.

In the ideal case each algorithm would have a URL available describing the

algorithm with an analysis. The current system supports ++ comments on each

function which have an additional character such as ++E, which gives an example

showing how to call the function. The comments show up when you )display the function.

Extending this with ++U would make it possible to show a URL for each function 

linking a paper that explains the theory. The simple extention of ++ comments makes 

the function documentation from )display much more useful.

These days the real fun would be adding a Grok (++G) call to explain the function.

I've been using Grok to understand Trager's thesis and it really helps a lot.

As for a Serge Lang link, I have been unable to read his books though I have them. :-)

Proving Axiom algorithms correct was one of the initial goals announced when

I released Axiom to the world. I tried with many different proof systems. I had

several discussions with J Strother Moore at UTexas about their work. I also looked

at OCAML, HOL, Mizar, TLA+, and COQ.

LEAN is the first system that "really got it right", introducing a programming language

that reduces to proofs. In the fullness of time it would make sense to rewrite

the whole system in LEAN code. Proven algorithms provide trusted answers.

It seems obvious to me that mathematics, including algorithms, requires proof.

This is mathematics, after all. As a (failed) mathematician I still feel that a

computer algebra system should reach for that standard.

Rumor has it not everyone agrees :-)

Tim

--
You received this message because you are subscribed to a topic in the Google Groups "FriCAS - computer algebra system" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/fricas-devel/OFrwS22IefU/unsubscribe.
To unsubscribe from this group and all its topics, send an email to fricas-devel...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/fricas-devel/CAHnU2dYf_NNGTnW-f7Z3-Bty5SLYOAwzkQdkC4zRpNfXafGwcg%40mail.gmail.com.

[Grégory Vanuxem]

I am on a smartphone, a pain. He is concise, this is what I like.

Not found how to select the text. 

Greg

BTW thanks for your response 

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/CAJn5L%3D%2Bv8Ont%3Dpfyzef3bKXpSNnjUEaF%2BdjGZ1VKNGJdrhvLPw%40mail.gmail.com.

[Grégory Vanuxem]

Some family things. Sorry. Very sorry