axiom-developer
[Top][All Lists]

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

 From: Ralf Hemmecke Subject: Re: [Axiom-developer] Re: BINGO,Curiosities with Axiom mathematical structures Date: Tue, 14 Mar 2006 12:24:48 +0100 User-agent: Thunderbird 1.5 (X11/20051201)

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

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();

```