[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Curiosities with Axiom mathematical structures
From: |
Gabriel Dos Reis |
Subject: |
Re: [Axiom-developer] 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?) 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
Re: [Axiom-developer] Curiosities with Axiom mathematical structures, Andrey G. Grozin, 2006/02/26