Re: [fricas-devel] Re: [Axiom-math] Type equivalence of domains in Axiom and Aldor

[Bill Page]

On 10/27/07, Ralf Hemmecke wrote:
>
> >   Def: Two domains P and Q are equivalent if and only if both domains 
> > satisfy
> >   exactly the same set of categories: (P has x) = (Q has x) for all Category
> >   expressions x *and* neither P nor Q has any explicit exports that are not
> >   provided by some named category.
>
> Let's see...
>
> Cat: Category == with {
>    coerce: Integer -> %;
>    coerce: % -> Integer;
>    bar: (%, %) ->  %;
> }
> P: Cat == add {
>    Rep == Integer; import from Rep
>    coerce(x: Integer): % == per x;
>    coerce(x: %): Integer == rep x;
>    bar(x: %, y: %): % == per(rep x + rep y);
> }
> ----------------------------------^
>
> Q: Cat == add {
>    Rep == Integer; import from Rep
>    coerce(x: Integer): % == per x;
>    coerce(x: %): Integer == rep x;
>    bar(x: %, y: %): % == per(rep x - rep y);
> }
> ----------------------------------^
>
> You are saying that P and Q are equivalent.
>

No. I should have explicitly written "type-equivalent" as I did
elsewhere in that message. I would only want to say that their types
are equivalent - that they necessarily represent the same kind of
things. Something like: "they are both monoids".

I would also say that without giving more information about the use of
the category 'Cat' you are at risk of abusing the intention of
defining a category - at least in the context of the design of a
library such as Axiom library. What is the "meaning" of 'Cat' if it
makes sense to give two rather different definitions of 'bar'? I
started my discussion by saying that I assumed that the intention of
defining a category was to represent some specific aspect or common
mathematical property of a as set of mathematical object(s). I do not
want to think of a category as a mere syntactical convenience for
example like a macro.

Regards,
Bill Page.