RE: [Axiom-developer] Re: BINGO, Curiosities with Axiom mathematical structures

[Bill Page]

On March 10, 2006 7:30 AM Ralf Hemmecke wrote:
> ...
> extend MyInteger: MyMonoid(MyInteger, *$MyInteger) == add;
> ...
>    stdout << "1: " << (Z has MyMonoid(Z, *$Z)) << newline;
>    stdout << "2: " << (Z has MyMonoid(Z, +$Z)) << newline;
>    stdout << "3: " << (M has MyMonoid(M, *$M)) << newline;
>    stdout << "4: " << (M has MyMonoid(M, +$M)) << newline;
> ... 
> and try to explain the output.
> 
> 1: T
> 2: T
> 3: T
> 4: T
> 
> ---------------------------------------------------
> 
> OK, and now the explanation. One would like the output
> (T, F, T, F), rigth?
> 
> Now look at MyInteger. It has type
> 
> with {
>    ArithmeticType; -- includes +, *, 0, 1
>    MyMonoid(MyInteger, *$MyInteger);
> }
> 
> Well, but MyMonoid is a **function**. So the type is (nearly)
> with {
>    ArithmeticType;
>    square: MyInteger -> MyInteger;
>    default {square(t: MyInteger): T == (*$MyInteger)(t, t)}
> }
> 
> You see, the * is hidden behind the == sign. The actual exports
> are that of ArithmeticType together with "square". It should be
> clear that then 2 and 4 from above also return true.
> 

Your explanation looks good but then I thought: What about those
categories in Axiom that take a member of some domain as a parameter.
If this parameter does not appear in any export of the category
then surely this same "error" would occur right?

Consider for example 'DirectProductCategory'

http://wiki.axiom-developer.org/axiom--test--1/src/algebra/VectorSpad/tangle
?submit=tangle&chunk=category+DIRPCAT+DirectProductCategory

It's paramters are:

  DirectProductCategory(dim:NonNegativeInteger, R:Type)

but 'dim' does not appear in the signatures of the list of exports
as one can verify with:

  ')sh DIRPCAT

In fact 'dim' only to the right of the == some default functions
such as 'dimension' and 'size'.

One might predict using your analysis above that 'DIRPCAT(2,INT)'
and 'DIRPCAT(3,INT)' would be treated identically. But try this:

(1) -> DIRPROD(2,INT) has DIRPCAT(2,INT)

   (1)  true
   Type: Boolean

(2) -> DIRPROD(2,INT) has DIRPCAT(3,INT)

   (2)  false
   Type: Boolean

-------

How does Axiom know that (2) is false?

Could this have something to do with the way SPAD compiles categories
compared to Aldor?

Regards,
Bill Page.