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

[Ralf Hemmecke]

On 03/09/2006 06:17 PM, William Sit wrote:
> Hi Ralf:
>
> Earlier, Ralf Hemmecke wrote (typo corrected):
> > > > If we have
> > > >
> > > > define MyMonoid: Category == with {
> > > >    1: %;
> > > >    *: (%, %) -> %;
> > > >    power: (%, Integer) -> %;
> > > > }
> > > >
> > > > -- and (now fancy notation with renaming)
> > > >
> > > > define MyTimesPlus: Category == with {
> > > >    MyMonoid;
> > > >    MyMonoid where {
> > > >      0: % == 1;
> > > >      +: (%, %) -> % == *;
> > > >      ntimes: (%, Integer) -> % == power;
> > > >    }
> > > > }
> You clarified:
> > I've just "invented" this syntax for the purpose of renaming. Don't take
> > it to serious.
> >
> > [snipped] ... in my code the
> > "MyMonoid where {...}" would be the second monoid structure.
>   [snipped] 
> > Yes, it looks like a default, but it isn't. Or better, it was not
> > intended to be like default.

> Ok, thanks for the clarrification. I see you are really defining an algebraic
> structure with two monoid substructure, one using (*, 1, power) and the other
> (+, 0, ntimes) and you are making a renaming of the second to conform to the
> single rigid MyMonoid declarations. The key is the new use of "where" which
> instructs the compiler to perform, hopefully, the isomorphism mechanism I
> described previously. But I think your construction probably would not work. In
> particular, the domain constructor for an MyTimesPlus object would have to
> specify the '(*, 1, power)' of the second 'MyMonoid': the forced definition for
> '(+,0, ntimes)' can only make sense AFTER '(*, 1, power)' is defined for the
> second 'MyMonoid' structure, since that is only a notational substitution
> device.

> The alternative, as suggested along the lines by Martin would be:
>
>  define MyTimesPlus2: Category == with {
>     MyMonoid;
>     0: %
>     +: (%,%)->%
>     ntimes: (%, Integer) -> %
>     MyMonoid where {
>       1 == 0;
>       *: (%, %) -> % == +;
>       power: (%, Integer) -> % == ntimes;
>     }
>  }

Well, it seems that my "where" invention was not explained clearly 
enough. What I meant by

  MyMonoid where {
    0: % == 1;
    +: (%, %) -> % == *;
    ntimes: (%, Integer) -> % == power;
  }

was that this construct actually defines a category that exports
    0: %;
    +: (%, %) -> %;
    ntimes: (%, Integer) -> %;
and at the same time declares those functions to be just other names for
1, *, and power in the structure MyMonoid. It all boils down to 
declaring a category

  with {
    0: %;
    +: (%, %) -> %;
    ntimes: (%, Integer) -> %;
  }

but somehow with the name MyMonoid attached to it. Or saying it in 
another way. It is like defining MultiplicativeMonoid and AdditiveMonoid 
 and giving them the same name MyMonoid. I don't anymore think that 
such "renaming" has much advantage. (However, I was not so convinced 
before the discussion started.)

BTW, in my "where" syntax I though quite a bit whether I should write

  + == *

or

  * == +

Unfortunately, my choice led you to think it is a category default.

> > > > Then MyTimesPlus has 6 different signatures.
> > > > If one removes the line "ntimes" then it would be only 5 and "power"
> > > > would correspond to the multiplication (or (more correctly) to the
> > > > actual implementation of it in a corresponding domain).

Hmm, I thought that explanation would have been enough to explain my 
"funny syntax". Sorry for all the confusion.

> > > > So, operator symbols and operator names agree as long as they are not
> > > > renamed.
> > > >
> > > > And one could also build
> > > >
> > > > MyInteger1: MyTimesPlus == add {
> > > >    Rep == Integer;
> > > >    0: % == per 0;
> > > >    1: % == per 1;
> > > >    ...
> > > > }
>
> Here the definition of 0:% either overrides that given in 'MyTimesPlus' or
> contradicts it,

Neither of them, since there is NO category default in MyTimesPlus, 
MyInteger1 **must** implement all 6 signatures.

> > The whole discussion came about since people (including me) wonder why
> > an AbelianMonoid does not inherit from Monoid. If that design (and the
> > reasons why it must be that way in Axiom) were explained better I think
> > that would avoid lots of questions about that difference between
> > mathematics and Axiom.
>
> Agreed. I suppose it is left to us, through these discussions, to recover what
> might have been in the minds of the original designers. 

Oh, now I am a bit puzzled. Didn't I read the name "William Sit" on one 
the first pages of the original Axiom book (by Jenks&Sutor)? I always 
thought you are one of the designers. No?

Ralf