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

[Ralf Hemmecke]

On 03/07/2006 08:52 PM, William Sit wrote:
> Ralf Hemmecke wrote:
> > 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;
> >    }
> > }
>
> Some typo above? should be '+: (%,%)->% == *' ?

Of course.

> I am not following your syntax
> for MyTimesPlus either (why use "where"?)  Parethesis not balanced also.

Hmm, I forgot the opening { after with. :-(
I've just "invented" this syntax for the purpose of renaming. Don't take 
it to serious.

> I thought you meant:
>  define MyTimesPlus: Category == MyMonoid with {
>   0: %;
>   +: (%,%);
>   ntimes: (%, Integer) -> %;
>   default {
>       0: % == 1;
>       +: (%, %) -> % == *;
>       ntimes: (%, Integer) -> % == power;
>   }
>  }
>
> which says a domain of category MyTimesPlus belongs to the category of MyMonoid
> but has three additional objects 0, + and ntimes, and here're the default
> implementations.

No. I definitely did not mean that. As your code looks to me, it should 
even be possible to compile that with the Aldor compiler. But in your 
code MyTimesPlus has only one monoid structure while in my code the 
"Monoid where {...}" would be the second monoid structure.
> Or do you really mean the defaults are compulsory?

Yes, it looks like a default, but it isn't. Or better, it was not
intended to be like 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).
> >
> > 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;
> >    ...
> > }
> >
> > 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);
> >    ...
> > }
> >
> > 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?

I don't need Integer in scope. And if Integer and MyInteger2 are in 
scope then clearly "0+1" is ambiguous. Even if you replace MyInteger2 by 
MyInteger1, "0+1" is ambiguous since 0 and 1 could be Integer or 
MyInteger1 and there would be both +: (Integer, Integer) -> Integer and 
+: (MyInteger1, MyInteger1) -> MyInteger1 in scope. That the compiler 
should reject it is clear with and without coerce functions to and from 
Integer. But if there is no coerce also the interpreter must reject that 
expression.

> > If both are in scope then nobody
> > can infer what "0 + 1" should return. In fact, constructing
> > implementations like that is also currently possible without renaming.
>
> No one can tell what "0+1" is unless the 0 and 1 are qualified as to which
> domain each belongs. You are creating an ambiguous situation deliberately, and
> so you have to make it unambiguous again by package call (which is in some sense
> the same as renaming). But what is your point?

Maybe I don't understand what the interpreter is doing. But if I just 
bring MyInteger2 into scope and NOT Integer (no idea how to do this in 
Axiom) then why wouldn't the interpreter be able to relate the 
characters (or literals) 0 and 1 as something of type MyInteger2 and the 
+ as the corresponding function from MyInteger2? The result of "0+1" is 
covered by

    (x: %) + (y: %): % == per (rep x * rep y);

so inside MyInteger2 the result is represented by the Integer 0 but 
should print (if I had implemented a output routine) as address@hidden

> You know, there is some mathematics behind these constructions, but that is bad
> mathematics:

I deliberately called it MyTimesPlus and not Ring!

> it may be fun to confuse students to switch the two monoid
> structures in Integer and even to interchange the notation for 0 and 1 and + and
> *. But no real mathematics is done that way, even if it is "allowed" AND
> correct! We don't say this is a bug in the mathematical system and we don't view
> it as a problem at all. So why should computer algebra systems be different? 

Of course, the MyInteger stuff above was some playing around, but you 
said that the interpreter could not figure out what is meant by "*" or 
"+" if Aldor would allow renaming. I still don't see the problem. It's a 
question of what one makes visible to the interpreter/compiler.

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) where explained better I think 
that would avoid lots of questions about that difference between 
mathematics and Axiom.

> > 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
>
> Do you mean you have to use the macro to ask:
>
>   MyInteger1 has MyTimesPlus
>
> while 'MyInteger1 has MyMonoid' works?

No.

For 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".

The expression

MyInteger1 has MyTimesPlus

should work perfectly and return true since MyInteger1 has been declared 
to be of that type.

Ralf