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

[Gabriel Dos Reis]

Ralf Hemmecke <address@hidden> writes:

| On 03/02/2006 08:23 PM, Gabriel Dos Reis wrote:
| > "Bill Page" <address@hidden> writes:
| > | On February 27, 2006 11:08 AM Gabriel Dos Reis wrote:
| > | > Ralf Hemmecke <address@hidden> writes:
| > | > | 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.
| 
| > The reason I previously said I did not see why Monoid should be a
| > category is that the operation is already passed in as a parameter, so
| > there would nothing to implement "inside" in the Monoid.
| 
| I had to read your statement several times until I got the point. I

Sorry about that.

| must admit that I probably have not thought clearly enough before I
| wrote down the code. But it's clear that als a (multisorted) universal
| algebra
| 
| define Monoid: Category == with {
|    1: %;
|    *: (%, %) -> %
| }
| 
| can mathematically be seen as
| 
|    a Monoid is a tuple (%, (f_1, f_2)) where % is the underlying set,
|    f_1 is the unit element and f_2 is multiplication.

Yes.

Furthermore, the monoid operation uniquely identifies the neutral
element; consequently  I think the syntax can be minimized to

   define Monoid(T: type, m: T x T -> T) : Category with {
          neutral : T;
   }

Here, I don't expect neutral to be exported to the "global scope".
Rather it should be visible only through the member access operator,
e.g. 

| (Unfortunately, nothing in the Aldor code above says anything about
| relations between 1 and *.)

I understand that, but I'm all for stepwise refinement.  First, get
rid of the syntax that stands in the way, then more on "semantics",
e.g. more interesting stuff :-)

| But although the operations are called 1 and * that should not
| matter. They should be just place holders for the actual name of the
| operation in the concrete monoid.

Exactly.  And they should not be exported to the "global scope".

[...]

| > Indeed, there would be a redundancy in the system.  The underlying type
| > and the operation suffice to uniquely define the structure.  So that
| > means, the other parameters are somehow "function" of the essential
| > parameters. That implies that indeed Monoid will be a category which
| > domains will implement by supplying the value for the neutral element.
| > Same reasoning for Group where the type and the operation suffice to
| > define the inverse and the neutral element.
| 
| Yes. The domain provides the value for the neutral element. And who
| provides the name for the neutral element? You know the domain Integer
| is both a Monoid with respect to addition and multiplication. You have
| just the identifier "1" in the category Monoid. How would I
| specify/name the additive unit element in Integer?

That problem is a non-problem if you observe the following.  The
neutral element is a function of the monoid operation.  Furthermore,
each *instance* of monoid structure gives rise a unique neutral
element (for example, accessible  through member access).  So there is
no conflict between the neutral element of Monoid(N, +) and that of
Monoid(N, *).  They are all (a priori) different.  They matter only
when using generic function, but then by the time such functions are
called the particular monoid instance is already sealed so there is no
possible confusion.


| 
|  > | However, there is no way in Axiom to express that a Ring is a Monoid
|  > | (SemiGroup if you like) "with respect to multiplication" and a Group
|  > | (which is also a Monoid) "with respect to addition".
|  >
|  > I understand there is no way.  My issue is *why*? E.g. is it
|  > fundamental or just implementation details that shrine into the
|  > interface?  My suspected answer is that it is an artifact of the
|  > used object-oriented technology.
| 
| I cannot belief that this issue is fundamental, but I am not an expert
| in this field. I you could help to come up with a nice syntax that
| would allow a compiler to translate
| 
|    [*] a Ring is a SemiGroup "with respect to multiplication"
|        and a Group (which is also a Monoid) "with respect to addition"
| 
| into reasonable binaries, I would highly appreciate it, since it would
| make Aldor even more "mathematical".

   define Magma(T: Type, m: T x T -> T) : Category;

   define SemiGroup(T: Type, m: T x T -> T) : Join(Magma(T, m)) with {
       Associative(T, m);
   }

   define Monoid(T: Type, m: T x T -> T) : Join(SemiGroup(T, m)) with {
        neutral : T;
   }

   define Group(T: Type, m: T x T -> T) : Join(Monoid(T, m)) with {
        inverse : T -> T;
   }

   define AbelianGroup(T: Type, m: T x T -> T) : Join(Group(T, m)) with {
        Commutative(T, m);
   }

   define Ring(T: Type, a : T x T -> T, m : T x T -> T) :
             Join(AbelianGroup(T, a), SemiGroup(T, m)) with {
       Distributive(T, a, m);
   }

the syntax is not right but I guess you get the idea.

-- Gaby