[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures
From: 
Gabriel Dos Reis 
Subject: 
Re: [Axiomdeveloper] Curiosities with Axiom mathematical structures 
Date: 
27 Feb 2006 17:08:27 +0100 
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?) objectoriented languages. I can
understand the language limitation, but that is hardly an excuse for
chosing in advance that "+" is for Abelian monoid and "*" for
nonAbelian 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