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

[Ralf Hemmecke]

Hi Bill,

> Hmmm... surely this must have been considered in the design of
> Aldor. Are there no Aldor categories like DIRPCAT that take a
> member of a domain as a parameter?

All categories in libaldor either take no parameter or just domain 
parameters.

In libalgebra, I could only find

define ResidueClassRing(R: CommutativeRing, p: R): Category
define DirectProductCategory(dim: MachineInteger, T: ExpressionType):

So it the same problem occurs.

> This seems like a natural mathematical construction to me.

I somehow agree, but unfortunately, we have no clear statement from the 
original designers about how Aldor's "Category" relates to mathematical 
categories or order-sorted algebras. There is only the PhD thesis of 
Doye. Maybe we should try to contact and ask people that appear in the 
original Axiom book personally about it. A bit of history would 
certainly be of value for Axiom.

> > If you look at DirProdCat as a function then clearly
> >   DirProdCat(2,Z) = DirProd(3,Z) = with{first:%->Z}
> > so why would one want another output?
> >
> > ----------- dirprod.as
> > #include "aldor"
> > #include "aldorio"
> >
> > define DirProdCat(n: Integer, R: Type): Category == with {
> >    first: % -> R;
> > }
>
> Well, clearly the application of the category 'DIRPCAT(2,INT'
> makes good sense in Axiom, don't you think?

Well, since (I think) the category of pairs of rings makes sense, it 
should also make sense in Axiom.

> How else would you propose to define this category?

I have no idea, how to define this category in Axiom in another way.
But obviously, there is a problem if one wants to check whether a domain 
satisfies that category.


> How could we do without it  in defining the domain 'DIRPROD(2,INT)'?

Hmm, I guess you would not like

  define DirectProductCategory(T: Ring): Category == ...

since that bears less information.

> To me this is the
> reason why we want another output from your example Aldor
> program. I would conclude that in fact internally (as you
> already said above):
>
>   DirProdCat(2,Z) ~= with{first:%->Z}
>
> There must be something additional on the right-hand side
> that is not reflected in the syntax of the category constant
> 'with' clause.

Well, you are in some sense right. As defined in the Aldor User Guide 
Section 7.5 if you define

define CatA: Category == with {foo: % -> %}
DomA: with {foo: % -> %} == add {foo(x:%): % == x}

then "DomA has CatA" returns false, because DomA is not explicityly 
declared to be of type CatA. There is this invisible symbol %% for each 
category from which a domain inherits. So in that sense

  CatA ~= with{foo: %->%}

Ralf

PS: Enjoy the output

aldor -grun -laldor cattest.as
A has CatA        : F
A has CatA 3      : F
A has CatA 3      : F
A has CatA Integer: T
A has CatA Boolean: F
-----------------
B has CatA        : F
B has CatA 2      : T
B has CatA 3      : T
B has CatA Integer: F
B has CatA Boolean: F

of the following program... ;-)

It seems that domains as parameters are treated differently than 
elements. Look especially at

define CatA(R: Type): Category == with {bar: () -> ()}

the "with" does not involve R in any way.

---- cattest.as ------------------
#include "aldor"
#include "aldorio"

define CatA: Category == with {foo: %->%}
define CatA(R: Type): Category == with {bar: () -> ()}
define CatA(n: Integer): Category == with {baz: () -> ()}

DomA(R: Type): CatA(R) == add { 
  bar(): () == {}
}

DomA(n: Integer): CatA(n) == add {      
  baz(): () == {}
}

main(): () == {
  macro A == DomA Integer;
  macro B == DomA 2;
  import from Integer;
  stdout << "A has CatA        : " << (A has CatA) << newline;
  stdout << "A has CatA 3      : " << (A has CatA 2) << newline;
  stdout << "A has CatA 3      : " << (A has CatA 3) << newline;
  stdout << "A has CatA Integer: " << (A has CatA(Integer)) << newline;
  stdout << "A has CatA Boolean: " << (A has CatA(Boolean)) << newline;
  stdout << "-----------------" << newline;
  stdout << "B has CatA        : " << (B has CatA) << newline;
  stdout << "B has CatA 2      : " << (B has CatA 2) << newline;
  stdout << "B has CatA 3      : " << (B has CatA 3) << newline;
  stdout << "B has CatA Integer: " << (B has CatA(Integer)) << newline;
  stdout << "B has CatA Boolean: " << (B has CatA(Boolean)) << newline;
}

main();