[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Ralf Hemmecke
Subject: Re: [Axiom-developer] Curiosities with Axiom mathematical structures
Date: Wed, 08 Mar 2006 17:54:25 +0100
User-agent: Thunderbird 1.5 (X11/20051201)

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

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

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

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?


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.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]