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

[William Sit]

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;
    }
 }

This effectively passes the structure maps for the second MyMonoid as parameters
(see SandBoxMonoid where Bill Page implemented similar code and where I made
some comments).

The "natural" thing for the change in code is, mathematically, "where" always
explains the notation. Here the second 'MyMonoid' demands the meaning of 1, *
and power.  However, as commented on SandBoxMonoid, this does not solve the
notation issue.

 
> >> 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).
> >>
> >> 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, and will not give 'MyInteger1' the second 'MyMonoid' structure
with '(+,0,ntimes)'.

> >> MyInteger2: MyTimesPlus == add {
> >>    Rep == Integer;
> >>    0: % == per 1;
> >>    1: % == per 0;
> >>    (x: %) + (y: %): % == per (rep x * rep y);
> >>    (x: %) * (y: %): % == per (rep x + rep y);
> >>    ...
> >> }

Here also, the definitions for '(+, 0)' override the defaults or contradicts it.
The way it was in your version, you must somehow be able to tell the compiler
the definitions for '(*, 1, power)' for the second 'MyMonoid' structure. Without
two different identifiers for the two instances of 'MyMonid', you cannot even
package qualify the two '*', two '1' and the two 'power' maps in 'MyInteger2'.

> >> Now, clearly, it can easily be figured out what 0, 1, +, etc. mean if
> >> MyInteger1 or MyInteger2 is in scope.
> >
> > Depends. Most likely, MyInteger1 and MyInteger2 would have coercion to and 
> > from
> > Integer (to enable input).  Unless you type qualify the constants, it is not
> > clear what an interpreter would do.
> 
> No? Without coerce functions and without Integer in scope what would be
> the problem if the interpreter only sees MyInteger2?

The problems that I see appear way before 'MyInteger2' can be "in scope" because
of the overriding problems and 'MyInteger2' should not have compiled, in
principle. On the other hand, 'MyInteger2' may well compile by replacing
'MyTimesPlus' by 'MyTimesPlus2'. However, then we lost the notation, and the two
"*" and "1" must be package called, which unfortunately, is impossible because
there is no distinction between the two substructures (both are 'MyMonoid'
without parameters).

[premature discussions on scope snipped]
 
> I deliberately called it MyTimesPlus and not Ring!

Ok, problem at issue is not the Ring structure, but the dual monoid structures.
 
> 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. 

> >> But let's continue with MyInteger1/2.
> >> If I now ask
> >>
> >> MyInteger1 has MyMonoid
> >>
> >> then that refers to the multiplicative structure. I have, however, to say
> >>
> >> macro MyAdditiveMonoidMacro == {
> >>    MyMonoid where {
> >>      0: % == 1;
> >>      +: (%, %) -> % == +;
> >>      ntimes: (%, Integer) -> % == power;
> >>    }
> >> }
> >> MyInteger1 has MyAdditiveMonoidMacro

> The syntax with the "where" is NOT Aldor. This is just an ad hoc syntax
> introduced by me. But without the macro one would have to use
> parentheses around the category (including the "where") since "has"
> binds higher than "where".

OK, I see you are attempting to use the macro to isolate the second 'MyMonoid'
structure from 'MyTimesPlus'.  This macro is in some sense the equivalent or
replacement for 'AbelianMonoid'. So there is not much advantage over the present
implementation, except that, if it works, we could have defined either as:

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

or

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

in which cases, 'MyAbelianMonoid[2] has Monoid' would work, but the notation
still does not. In fact, even in the first case, the Interpreter will have to
parse + as in MyAbelianMonoid, then translates it to * of MyMonoid, where this *
is implemented in MyAdditiveInteger as a mangled +. All these overhead, for
what? Would this have been simpler the way it currently is?

The real problem is how to ask 'MyInteger2 has MyMonoid(+,0,ntimes)' and without
the parameters and get an affirmative answer. That problem still has not been
solved (except as currently in Axiom).

William