Re: [Axiom-developer] Curiosities with Axiom mathematical structures

[Gabriel Dos Reis]

Ralf Hemmecke <address@hidden> writes:

| On 02/26/2006 05:42 PM, Gabriel Dos Reis wrote:
| > Hello Willian,
| > thanks for the quick reply.
| > William Sit <address@hidden> writes:
| > | Gabriel Dos Reis wrote:
| > | >   In the impressive diagram titled "Basic Agebra Hierarchy" displayed
| > | > in the Axiom Book (I only have a copy of the edition copyrighted 1992,
| > | > NAG), AbelianSemiGroup is not "derived" from SemiGroup, and similarly
| > | > AbelianMonoid is not "derived" from Monoid.  I find that curious as it
| > | > goes counter the mathematical fact that an AbelianMonoid *is* a
| > | > Monoid, with an additional algebraic law (commutation).
| > | > | >   Does anyone know the reason of those curiosities?
| > | | One probable reason may be the convention in mathematics to use +
| > | instead of * when a semigroup, monoid, or group is abelian.
| > I find that argument very unconvincing for several reasons:
| >    1.  "+" or "*" are *syntax*, not algebraic properties.  Whether a
| >        monoid is Abelian or not does stop it from being a monoid.  The
| >        mathematical definition of an Abelian monoid is that it is a
| >        monoid, whose operation *additionally* is commutative.
| >        2.  The set of natural numbers, NN, has *many* Abelian
| > structures on it,
| >        for examples:
| >           a. (NN, +, 0) -- the usual addition
| >           b. (NN, *, 1) -- the usual multiplication, commutative!
| >           c. (NN, max, 0) -- "max" is the usual maximum function
| >         Such a counterexample can be multiplied.
| 
| One reason for having Monoid and AbelianMoniod (one with "*" and the
| other with "+") is that neither SPAD nor Aldor allows to rename
| functions during inheritance.

yes, that is true for many (all?) object-oriented languages.  I can
understand the language limitation, but that is hardly an excuse for
chosing in advance that "+" is for Abelian monoid and "*" for
non-Abelian ones.

| Note that one would have to say something like
| 
| define Monoid(
|    *: (%, %) -> %;
|    1: %
| ): Category == ...
| 
| define Group(
|    *: (%, %) -> %,
|    inv: % -> %,
|    1: %
| ): Category == ...
| 
| define Ring(.....): Category == with {
|    Monoid(*, 1);
|    Group(+, -, 0);
| }

Ring should be both Monoid and Group, whether they shoud be categories,
I don't really know.

| 
| OK, that is not well thought of...
| 
| Anyway, there is not way to do this in Aldor, yet. At least nobody has
| told me so far.
| 
| If such renaming could be implemented into the Aldor language that
| would make it even better suited for mathematics. However, then there
| is need that someone implements these ideas into the compiler. Who?

I'm not sure renaming is a good solution, at least if I was going to
solve this issue I would not go there.  However, I do believe that
expressing mathematical structures in a way that reflect mathematical
properties and understanding is essential.

I believe this is something solvable -- at least, that can be
approximated to a good extent -- in a type system based on predicate
system directly available at the programming level.  We've been
developing such an idea to build a type system for C++ template
arguments, see

   http://public.research.att.com/~bs/popl06.pdf

presented at POPL this year.

Notice that the "post facto extenstion" of Aldor is a starting point,
but it still does not help solving that issue..

The make the approach practical for large libraries in Axiom/Aldor I
believe some form of deduction of category/domain argument deduction
would needed.  However, Axiom/Aldor types being dependent, that be
challenging.   Anyway, I have searched the literature for the
descirption of Axiom/Adlor type system as implemented, I have found
nothing that could assist me.

-- Gaby