[Axiom-math] Type equivalence of domains in Axiom and Aldor

[Bill Page]

Dear Friends of Axiom and Aldor,

As a result of the recent message thread about "iterators and
cartesian product" in the Axiom library I have been thinking again
about type equivalence. For example consider the following domains in
Axiom:

(1) -> P:=Product(Stream Integer,Stream Integer)

(1) Product(Stream Integer,Stream Integer)
Type: Domain
(2) -> Q:=Stream Product(Integer,Integer)

(2) Stream Product(Integer,Integer)
Type: Domain

On reflection (pun intended) it seems that 'Stream' is a "sum-like"
domain constructor so that we might reasonably expect algebraically
that a 'Product' distributes over a 'Stream' and therefore wish to
design the Axiom library so that this is satisfied.

Thus we should have

P = Q

Side Note: Perhaps with an extension of the domain 'Domain' that Gaby
recently introduced in OpenAxiom it would actually be possible to
write and evaluate this expression in Axiom.

I understand that neither Spad nor Aldor actually evaluate type
expressions like P and Q above so it does not make sense to ask for
"value" equality of these two domains. But perhaps EQUAL in the Lisp
sense (ref: http://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node74.html)
could appliy?

Therefore I would propose the following definition of type-equivalence
of domains:

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.

It seems that in principle it should be possible to give an efficient
decision procedure for this test if it is not already implemented
somewhere in the Spad and Aldor compilers. I would like to understand
this better from the point of view of the compiler and iterpreter
design.

Obviously it makes sense to require that two equivalent domains must
provide the same set of exported operations (the same interface)
having the same names and same signatures. But as I understand the
intention of the semantics of categories in both Axiom and Aldor this
is not enough. We want categories to represent abstract concepts
usually with a well-defined mathematical meaning. That is the reason
for explicitly referring to satisfaction of categories in the
definition above. Further since domains can also explicitly include
exported operations in the 'with' clause (i.e. "anonymous categories"
as defined in the Aldor user's guide), if this mathematical meaning is
carried only by the named categories, such anonymous categories must
always be assumed to represent different categories in each domain in
which they occur.

With this definition it is easy to show that the current definitions
of 'Product' and 'Stream' do not satisfy the expected distributive
property. Right now both 'Stream' and 'Product' have explicit exports,
further the actual list of exported operations does not match at all:

(3) -> )sh P
Product(Stream Integer,Stream Integer) is a domain constructor.
Abbreviation for Product is PRODUCT
This constructor is not exposed in this frame.
Issue )edit /usr/local/lib/axiom/target/i686-suse-linux/../../src/algebra/PRODUCT.spad
to see algebra source code for PRODUCT

------------------------------- Operations --------------------------------

?*? : (Integer,%) -> % ?*? : (PositiveInteger,%) -> %
...

(3) -> )sh Q
Stream Product(Integer,Integer) is a domain constructor.
Abbreviation for Stream is STREAM
This constructor is exposed in this frame.
Issue )edit /usr/local/lib/axiom/target/i686-suse-linux/../../src/algebra/STREAM.spad
to see algebra source code for STREAM

------------------------------- Operations --------------------------------

#? : % -> NonNegativeInteger ?=? : (%,%) -> Boolean
...

As a mininum it would probably be necessary to introduce two new
cateogies: StreamCat(S) and ProductCat(X,Y). Then it would seem that
would be necessary add code along the lines of

Product(A: SetCategory,B: SetCategory): ProductCat(A,B) with
if A has StreamCat(S) and B has StreamCat(S) then
StreamCat(S)

And

Stream(S:Type): StreamCat(S) with
if S has ProductCat(A,B) then
ProductCat(A,B)

for some set of allowed domains A, B and S, including for example
'Integer'. Of course there is a problem here about specifying the
specific list of domains for A, B and C. It would be desirable I
think, if the compiler could produce generic code which would apply
whtn A, B and C are still unknowns. Is this possible?

Of course we also need the implementations of the associate operations.

With these changes we would be able to satisfy the definition of the
type-equivalence of P and Q above.

I would like to know if other developers think this more algebraic
approach to the design of the Axiom library domains makes sense.
Comments and criticisms are invited.

Regards,
Bill Page.

[Saul Youssef]

Hi Bill,

I unfortunately couldn't make it to the Aldor workshop and I
haven't touched the language in a few years, but I do have a comment.

Your questions have definite answers in category theory and
since Aldor is *almost* doing category theory, it's tempting to think
that the categorical answers to your questions are really what should
naturally fit into the language. I wrote up something trying this out
for the 2001 workshop

http://atlas.bu.edu/~youssef/papers/math/aldor/aldor.pdf

I still think that this is a good way to look for flaws in the
language - implement category theory and see what goes wrong.

Best regards,

Saul Youssef

Post by Bill Page
Dear Friends of Axiom and Aldor,
As a result of the recent message thread about "iterators and
cartesian product" in the Axiom library I have been thinking again
about type equivalence. For example consider the following domains in
(1) -> P:=Product(Stream Integer,Stream Integer)
(1) Product(Stream Integer,Stream Integer)
Type: Domain
(2) -> Q:=Stream Product(Integer,Integer)
(2) Stream Product(Integer,Integer)
Type: Domain
On reflection (pun intended) it seems that 'Stream' is a "sum-like"
domain constructor so that we might reasonably expect algebraically
that a 'Product' distributes over a 'Stream' and therefore wish to
design the Axiom library so that this is satisfied.
Thus we should have
P = Q
Side Note: Perhaps with an extension of the domain 'Domain' that Gaby
recently introduced in OpenAxiom it would actually be possible to
write and evaluate this expression in Axiom.
I understand that neither Spad nor Aldor actually evaluate type
expressions like P and Q above so it does not make sense to ask for
"value" equality of these two domains. But perhaps EQUAL in the Lisp
sense (ref: http://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node74.html)
could appliy?
Therefore I would propose the following definition of type-equivalence
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.
It seems that in principle it should be possible to give an efficient
decision procedure for this test if it is not already implemented
somewhere in the Spad and Aldor compilers. I would like to understand
this better from the point of view of the compiler and iterpreter
design.
Obviously it makes sense to require that two equivalent domains must
provide the same set of exported operations (the same interface)
having the same names and same signatures. But as I understand the
intention of the semantics of categories in both Axiom and Aldor this
is not enough. We want categories to represent abstract concepts
usually with a well-defined mathematical meaning. That is the reason
for explicitly referring to satisfaction of categories in the
definition above. Further since domains can also explicitly include
exported operations in the 'with' clause (i.e. "anonymous categories"
as defined in the Aldor user's guide), if this mathematical meaning is
carried only by the named categories, such anonymous categories must
always be assumed to represent different categories in each domain in
which they occur.
With this definition it is easy to show that the current definitions
of 'Product' and 'Stream' do not satisfy the expected distributive
property. Right now both 'Stream' and 'Product' have explicit exports,
(3) -> )sh P
Product(Stream Integer,Stream Integer) is a domain constructor.
Abbreviation for Product is PRODUCT
This constructor is not exposed in this frame.
Issue )edit /usr/local/lib/axiom/target/i686-suse-linux/../../src/algebra/PRODUCT.spad
to see algebra source code for PRODUCT
------------------------------- Operations --------------------------------
?*? : (Integer,%) -> % ?*? : (PositiveInteger,%) -> %
...
(3) -> )sh Q
Stream Product(Integer,Integer) is a domain constructor.
Abbreviation for Stream is STREAM
This constructor is exposed in this frame.
Issue )edit /usr/local/lib/axiom/target/i686-suse-linux/../../src/algebra/STREAM.spad
to see algebra source code for STREAM
------------------------------- Operations --------------------------------
#? : % -> NonNegativeInteger ?=? : (%,%) -> Boolean
...
As a mininum it would probably be necessary to introduce two new
cateogies: StreamCat(S) and ProductCat(X,Y). Then it would seem that
would be necessary add code along the lines of
Product(A: SetCategory,B: SetCategory): ProductCat(A,B) with
if A has StreamCat(S) and B has StreamCat(S) then
StreamCat(S)
And
Stream(S:Type): StreamCat(S) with
if S has ProductCat(A,B) then
ProductCat(A,B)
for some set of allowed domains A, B and S, including for example
'Integer'. Of course there is a problem here about specifying the
specific list of domains for A, B and C. It would be desirable I
think, if the compiler could produce generic code which would apply
whtn A, B and C are still unknowns. Is this possible?
Of course we also need the implementations of the associate operations.
With these changes we would be able to satisfy the definition of the
type-equivalence of P and Q above.
I would like to know if other developers think this more algebraic
approach to the design of the Axiom library domains makes sense.
Comments and criticisms are invited.
Regards,
Bill Page.
_______________________________________________
Aldor-l mailing list
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Ralf Hemmecke]

Dear Saul,

Post by Saul Youssef
Your questions have definite answers in category theory and
since Aldor is *almost* doing category theory, it's tempting to think
that the categorical answers to your questions are really what should
naturally fit into the language. I wrote up something trying this out
for the 2001 workshop
http://atlas.bu.edu/~youssef/papers/math/aldor/aldor.pdf
I still think that this is a good way to look for flaws in the
language - implement category theory and see what goes wrong.

I quite like what you wrote. But I somehow fear that the compiler does
not accept your code. Could you provide the compilable sources of this
paper?

Furthermore, you do quite a lot of high-level constructions. To me it
seems that they are OK to do category theory, but have you any comment
how these constructions could be used to reduce the amount of
programming work, i.e. code reuse?

Ralf

PS:
Mistakes...

Page 5:
Id(Obj:Category):Category == with
id: (A:Obj) -> (A->A)
default
id(A: Obj):(A->A) == (a:A):A +-> a --rhx: I changed this line.

Page 10:

homList(A:Categorify P,B:Categorify P):SingleInteger == add

should probably read

homList(A:Categorify P,B:Categorify P):List(A->B) ==

[Saul Youssef]

Hi Ralf,

Post by Ralf Hemmecke
I quite like what you wrote.

Thanks.

Post by Ralf Hemmecke
But I somehow fear that the compiler does
not accept your code. Could you provide the compilable sources of this
paper?

I'm attaching my code from the time (~3k lines) which includes the
bits in the paper. It all actually at least used to compile and work
in 2001.

Post by Ralf Hemmecke
Furthermore, you do quite a lot of high-level constructions. To me it
seems that they are OK to do category theory, but have you any comment
how these constructions could be used to reduce the amount of
programming work, i.e. code reuse?

Category theory is famous for seeming to be about nothing, but still
being one of the most important ideas from 20th century math anyway.
Possibly the best thing is to look at Groups.as to get a flavor of
something concrete happening. This implements the category of groups
(in the math sense) and is described a little bit in this talk as a
more concrete example

http://atlas.bu.edu/~youssef/homepage/talks/categories/categories.html

There's a whole field of "applications of category theory to computer
science" with ten years of conferences at least (which I know next to
nothing about), but still, as far as I know, there is no language
where one can conveniently create and manipulate categories, objects,
morphisms, adjoints, etc. Having this, I think, could suddenly make a

[Ralf Hemmecke]

Thank you Saul,

First, thank you very much for your code. Under which license is it?
Public domain, mBSD, GPL, ... ?

Unfortunately, the compiler has changed a bit.

woodpecker:~/scratch/Youssef/london>aldor Basics.as
woodpecker:~/scratch/Youssef/london>aldor Categories.as

#1 (Error) There are 2 meanings for the operator `+'.
Meaning 1: (Obj, Obj) -> Obj
Meaning 2: (A: Obj, B: Obj) -> (
Obj with
...
#2 (Error) There are 2 meanings for the operator `..'.
Meaning 1: (Obj, Integer) -> Obj
Meaning 2: (A: Obj, n: Integer) -> (
Obj with
...
#3 (Error) There are 2 meanings for the operator `*'.
Meaning 1: (Obj, Obj) -> Obj
Meaning 2: (A: Obj, B: Obj) -> (
Obj with
...
#4 (Error) There are 2 meanings for the operator `^'.
Meaning 1: (Obj, Integer) -> Obj
Meaning 2: (A: Obj, n: Integer) -> (
Obj with
...

In fact, I don't quite know how to resolve that problem.
Actually, I wonder why I don't see any line numbers here.

Post by Saul Youssef
I'm attaching my code from the time (~3k lines) which includes the
bits in the paper. It all actually at least used to compile and work
in 2001.

I guess the commands "ao" and "ai" that I find in "compile" and
"exercise" mean something like

alias ao=aldor -fao
alias ai=aldor -G interp

Or did you use other scripts?

Post by Saul Youssef
One of the things that encouraged me at the time was thinking
about the simplest Aldor category in the mathematical sense: objects
of the category are Aldor domains satisfying
Domain: Category == with # no signatures (my favorite base category
for a library)

I wonder why you called it "Domain" and not something else? In some way
you are right

A: Domain

then says that A is a domain. Sounds not too bad.

Ralf

[Saul Youssef]

Post by Ralf Hemmecke
Thank you Saul,
First, thank you very much for your code. Under which license is it?
Public domain, mBSD, GPL, ... ?

No problem. I offer it freely with no restrictions or claims.

Post by Ralf Hemmecke
Unfortunately, the compiler has changed a bit.

It might be useful for you just as a sample of odd code that should
work but is structurally different from what you're used to.

Post by Ralf Hemmecke
woodpecker:~/scratch/Youssef/london>aldor Basics.as
woodpecker:~/scratch/Youssef/london>aldor Categories.as
#1 (Error) There are 2 meanings for the operator `+'.
Meaning 1: (Obj, Obj) -> Obj
Meaning 2: (A: Obj, B: Obj) -> (
Obj with
...
#2 (Error) There are 2 meanings for the operator `..'.
Meaning 1: (Obj, Integer) -> Obj
Meaning 2: (A: Obj, n: Integer) -> (
Obj with
...
#3 (Error) There are 2 meanings for the operator `*'.
Meaning 1: (Obj, Obj) -> Obj
Meaning 2: (A: Obj, B: Obj) -> (
Obj with
...
#4 (Error) There are 2 meanings for the operator `^'.
Meaning 1: (Obj, Integer) -> Obj
Meaning 2: (A: Obj, n: Integer) -> (
Obj with
...
In fact, I don't quite know how to resolve that problem.
Actually, I wonder why I don't see any line numbers here.

I haven't a clue about this, but that's why I included the old foam
output in case it's a clue for you. This stuff was all compiled just
before the London Ontario meeting in 2001.

Post by Ralf Hemmecke
I guess the commands "ao" and "ai" that I find in "compile" and
"exercise" mean something like
alias ao=aldor -fao
alias ai=aldor -G interp
Or did you use other scripts?

I'm sure you're right, but I couldn't even tell you for sure at this point.

Post by Ralf Hemmecke

Post by Saul Youssef
One of the things that encouraged me at the time was thinking
about the simplest Aldor category in the mathematical sense: objects
of the category are Aldor domains satisfying
Domain: Category == with # no signatures (my favorite base category
for a library)

I wonder why you called it "Domain" and not something else? In some way
you are right
A: Domain
then says that A is a domain. Sounds not too bad.
Ralf

I do think that this is nicer than "DomainCategory", "SetCategory"
etc. In this style, you typically produce domains by applying domain
constructors (i.e. "functors") and quotients rather than implementing
them directly, so you might as well then keep the nice names for the
categories.

- Saul

[Bill Page]

Post by Saul Youssef

Post by Ralf Hemmecke
Thank you Saul,
First, thank you very much for your code. Under which license is it?
Public domain, mBSD, GPL, ... ?

No problem. I offer it freely with no restrictions or claims.

Post by Ralf Hemmecke
Unfortunately, the compiler has changed a bit.

It might be useful for you just as a sample of odd code that should
work but is structurally different from what you're used to.

Saul,

I have been spending some time trying to compile your code for
"computing with category theory" in the new open source release of
Aldor and working on a version that I hope will work inside Axiom. But
as Ralf noted it seems that either the compiler has changed in several
subtle ways or perhaps your code as based on a somewhat different
branch development of Aldor? In several places in your code you refer
to "bugs in 1.1.12p6" and your hope that these will be solved so to
enable to more complete implementation of your ideas. I am very
curious what to what the version number 1.1.12p6 refers.

[Saul Youssef]

Hi Bill,

Post by Bill Page
I have been spending some time trying to compile your code for
"computing with category theory" in the new open source release of
Aldor and working on a version that I hope will work inside Axiom. But
as Ralf noted it seems that either the compiler has changed in several
subtle ways or perhaps your code as based on a somewhat different
branch development of Aldor? In several places in your code you refer
to "bugs in 1.1.12p6" and your hope that these will be solved so to
enable to more complete implementation of your ideas. I am very
curious what to what the version number 1.1.12p6 refers.

[Bill Page]

Ralf,

I think the problem here is that the new version of the Aldor compiler
needs a little more help just be reassured that you really are writing
a function that returns a domain. The empty 'with {}' clause seems to
do the trick.

Here is a patch to 'Categories.as' that allows it to compile... but I
have not yet compiled the rest so I am not 100% sure that the end
result will be ok. (Also attached as a file.):

***@sage:~/aldor-src/aldor/install/aldor# aldor Categories.as
***@sage:~/aldor-src/aldor/install/aldor# diff -au Categoris.as_orig
Categories.as
diff: Categoris.as_orig: No such file or directory
***@sage:~/aldor-src/aldor/install/aldor# diff -au Categories.as_orig
Categories.as
--- Categories.as_orig 2007-11-08 10:09:11.000000000 -0800
+++ Categories.as 2007-11-08 10:11:54.000000000 -0800
@@ -64,14 +64,14 @@
define Product(Obj:Category):Category == with
Product: (A:Obj,B:Obj) -> ( AB:Obj, AB->A, AB->B,
(X:Obj)->(X->A,X->B)->(X->AB) )
Product: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) ->
(AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2))
- *:(Obj,Obj)->Obj
+ *:(Obj,Obj)->Obj with {}
default
Product(A1:Obj,B1:Obj,A2:Obj,B2:Obj):(AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2))
==
(ab1:Obj,pa1:ab1->A1,pb1:ab1->B1, product1: (X:Obj) ->
(X->A1,X->B1) -> (X->ab1)) == Product(A1,B1)
(ab2:Obj,pa2:ab2->A2,pb2:ab2->B2, product2: (X:Obj) ->
(X->A2,X->B2) -> (X->ab2)) == Product(A2,B2)
(f:A1->A2)*(g:B1->B2):(ab1->ab2) == product2 ( ab1 )(
(x:ab1):A2 +-> f pa1 x, (x:ab1):B2 +-> g pb1 x )
(ab1,ab2,*)
- (A:Obj)*(B:Obj):Obj ==
+ (A:Obj)*(B:Obj):Obj with {} ==
(AB:Obj,pa:AB->A,pb:AB->B,product:(X:Obj)->(X->A,X->B)->(X->AB))
== Product(A,B)
AB add

@@ -81,14 +81,14 @@
define CoProduct(Obj:Category):Category == with
CoProduct: (A:Obj,B:Obj) -> ( AB:Obj, A->AB, B->AB,
(X:Obj)->(A->X,B->X)->(AB->X) )
CoProduct: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) ->
(AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1))
- +:(Obj,Obj)->Obj
+ +:(Obj,Obj)->Obj with {}
default
CoProduct(A1:Obj,B1:Obj,A2:Obj,B2:Obj):(AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1))
==
(ab1:Obj,ia1:A1->ab1,ib1:B1->ab1, sum1: (X:Obj) ->
(A1->X,B1->X) -> (ab1->X)) == CoProduct(A1,B1)
(ab2:Obj,ia2:A2->ab2,ib2:B2->ab2, sum2: (X:Obj) ->
(A2->X,B2->X) -> (ab2->X)) == CoProduct(A2,B2)
(f:A2->A1)+(g:B2->B1):(ab2->ab1) == sum2 ( ab1 ) (
(x:A2):ab1 +-> ia1 f x, (x:B2):ab1 +-> ib1 g x )
(ab1,ab2,+)
- (A:Obj)+(B:Obj):Obj ==
+ (A:Obj)+(B:Obj):Obj with {} ==
(AB:Obj,ia:A->AB,ib:B->AB,product:(X:Obj)->(A->X,B->X)->(AB->X))
== CoProduct(A,B)
AB add

@@ -97,9 +97,9 @@
+++
define MultiProduct(Obj:Category):Category == with
Product:(A:Obj,n:Integer) ->
(Prod:Obj,Integer->(Prod->A),(X:Obj)->(Tuple (X->A))->(X->Prod))
- ^:(Obj,Integer) -> Obj
+ ^:(Obj,Integer) -> Obj with {}
default
- (A:Obj)^(n:Integer):Obj ==
+ (A:Obj)^(n:Integer):Obj with {} ==
(Prod:Obj,project:Integer->(Prod->A),product:(X:Obj)->(Tuple
(X->A))->(X->Prod)) == Product(A,n)
Prod add

@@ -108,9 +108,9 @@
+++
define CoMultiProduct(Obj:Category):Category == with
CoProduct:(A:Obj,n:Integer) -> (
Sum:Obj,Integer->(A->Sum),(X:Obj)->(Tuple (A->X))->(Sum->X))
- ..:(Obj,Integer) -> Obj
+ ..:(Obj,Integer) -> Obj with {}
default
- (A:Obj)..(n:Integer):Obj ==
+ (A:Obj)..(n:Integer):Obj with {} ==
(Sum:Obj,insert:Integer->(A->Sum),sum:(X:Obj)->(Tuple
(A->X))->(Sum->X)) == CoProduct(A,n)
Sum add

***@sage:~/aldor-src/aldor/install/aldor#

--------

Regards,
Bill Page.

Post by Ralf Hemmecke
Thank you Saul,
First, thank you very much for your code. Under which license is it?
Public domain, mBSD, GPL, ... ?
Unfortunately, the compiler has changed a bit.
woodpecker:~/scratch/Youssef/london>aldor Basics.as
woodpecker:~/scratch/Youssef/london>aldor Categories.as
#1 (Error) There are 2 meanings for the operator `+'.
Meaning 1: (Obj, Obj) -> Obj
Meaning 2: (A: Obj, B: Obj) -> (
Obj with
...
#2 (Error) There are 2 meanings for the operator `..'.
Meaning 1: (Obj, Integer) -> Obj
Meaning 2: (A: Obj, n: Integer) -> (
Obj with
...
#3 (Error) There are 2 meanings for the operator `*'.
Meaning 1: (Obj, Obj) -> Obj
Meaning 2: (A: Obj, B: Obj) -> (
Obj with
...
#4 (Error) There are 2 meanings for the operator `^'.
Meaning 1: (Obj, Integer) -> Obj
Meaning 2: (A: Obj, n: Integer) -> (
Obj with
...
In fact, I don't quite know how to resolve that problem.
Actually, I wonder why I don't see any line numbers here.

Post by Saul Youssef
I'm attaching my code from the time (~3k lines) which includes the
bits in the paper. It all actually at least used to compile and work
in 2001.

I guess the commands "ao" and "ai" that I find in "compile" and
"exercise" mean something like
alias ao=aldor -fao
alias ai=aldor -G interp
Or did you use other scripts?

Post by Saul Youssef
One of the things that encouraged me at the time was thinking
about the simplest Aldor category in the mathematical sense: objects
of the category are Aldor domains satisfying
Domain: Category == with # no signatures (my favorite base category
for a library)

I wonder why you called it "Domain" and not something else? In some way
you are right
A: Domain
then says that A is a domain. Sounds not too bad.
Ralf
_______________________________________________
Aldor-l mailing list
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Bill Page]

Ralf,

Here is another version that is slightly more friendly to the #pile
syntax (-: no {} required :-). I presume that the compiler generates
the same code...

--- Categories.as_orig 2007-11-08 10:09:11.000000000 -0800
+++ Categories.as 2007-11-08 10:45:51.000000000 -0800
@@ -66,3 +66,3 @@
Product: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) ->
(AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2))
- *:(Obj,Obj)->Obj
+ *:(Obj,Obj)-> with Obj
default
@@ -73,3 +73,3 @@
(ab1,ab2,*)
- (A:Obj)*(B:Obj):Obj ==
+ (A:Obj)*(B:Obj): with Obj ==
(AB:Obj,pa:AB->A,pb:AB->B,product:(X:Obj)->(X->A,X->B)->(X->AB))
== Product(A,B)
@@ -83,3 +83,3 @@
CoProduct: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) ->
(AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1))
- +:(Obj,Obj)->Obj
+ +:(Obj,Obj)-> with Obj
default
@@ -90,3 +90,3 @@
(ab1,ab2,+)
- (A:Obj)+(B:Obj):Obj ==
+ (A:Obj)+(B:Obj): with Obj ==
(AB:Obj,ia:A->AB,ib:B->AB,product:(X:Obj)->(A->X,B->X)->(AB->X))
== CoProduct(A,B)
@@ -99,5 +99,5 @@
Product:(A:Obj,n:Integer) ->
(Prod:Obj,Integer->(Prod->A),(X:Obj)->(Tuple (X->A))->(X->Prod))
- ^:(Obj,Integer) -> Obj
+ ^:(Obj,Integer) -> with Obj
default
- (A:Obj)^(n:Integer):Obj ==
+ (A:Obj)^(n:Integer): with Obj ==
(Prod:Obj,project:Integer->(Prod->A),product:(X:Obj)->(Tuple
(X->A))->(X->Prod)) == Product(A,n)
@@ -110,5 +110,5 @@
CoProduct:(A:Obj,n:Integer) -> (
Sum:Obj,Integer->(A->Sum),(X:Obj)->(Tuple (A->X))->(Sum->X))
- ..:(Obj,Integer) -> Obj
+ ..:(Obj,Integer) -> with Obj
default
- (A:Obj)..(n:Integer):Obj ==
+ (A:Obj)..(n:Integer): with Obj ==
(Sum:Obj,insert:Integer->(A->Sum),sum:(X:Obj)->(Tuple
(A->X))->(Sum->X)) == CoProduct(A,n)
***@sage:~/aldor-src/aldor/install/aldor#

----

Regards,
Bill Page.

Post by Bill Page
Ralf,
I think the problem here is that the new version of the Aldor compiler
needs a little more help just be reassured that you really are writing
a function that returns a domain. The empty 'with {}' clause seems to
do the trick.
Here is a patch to 'Categories.as' that allows it to compile... but I
have not yet compiled the rest so I am not 100% sure that the end

[Ralf Hemmecke]

Hello Bill,

I think, I don't like your suggestion.
I'd rather change it into

define Product(Obj:Category):Category == with {
...
-- *:(Obj,Obj)->Obj;
default {
local mult(A:Obj, B:Obj):Obj == {
(
AB:Obj,
pa:AB->A,
pb:AB->B,
product:(X:Obj)->(X->A,X->B)->(X->AB)
) == Product(A,B);
AB add;
}
*: (Obj,Obj)->Obj == mult;
}
}

The "default" is like defining an anonymous "add" body which exports
anything on the left of == that is not declared local. So

*: (Obj,Obj)->Obj

will get exported by Product(Obj) even if you put a "--" as I did above.

Ralf

Post by Bill Page
Ralf,
Here is another version that is slightly more friendly to the #pile
syntax (-: no {} required :-). I presume that the compiler generates
the same code...
--- Categories.as_orig 2007-11-08 10:09:11.000000000 -0800
+++ Categories.as 2007-11-08 10:45:51.000000000 -0800
@@ -66,3 +66,3 @@
Product: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) ->
(AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2))
- *:(Obj,Obj)->Obj
+ *:(Obj,Obj)-> with Obj
default
@@ -73,3 +73,3 @@
(ab1,ab2,*)
- (A:Obj)*(B:Obj):Obj ==
+ (A:Obj)*(B:Obj): with Obj ==
(AB:Obj,pa:AB->A,pb:AB->B,product:(X:Obj)->(X->A,X->B)->(X->AB))
== Product(A,B)
@@ -83,3 +83,3 @@
CoProduct: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) ->
(AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1))
- +:(Obj,Obj)->Obj
+ +:(Obj,Obj)-> with Obj
default
@@ -90,3 +90,3 @@
(ab1,ab2,+)
- (A:Obj)+(B:Obj):Obj ==
+ (A:Obj)+(B:Obj): with Obj ==
(AB:Obj,ia:A->AB,ib:B->AB,product:(X:Obj)->(A->X,B->X)->(AB->X))
== CoProduct(A,B)
@@ -99,5 +99,5 @@
Product:(A:Obj,n:Integer) ->
(Prod:Obj,Integer->(Prod->A),(X:Obj)->(Tuple (X->A))->(X->Prod))
- ^:(Obj,Integer) -> Obj
+ ^:(Obj,Integer) -> with Obj
default
- (A:Obj)^(n:Integer):Obj ==
+ (A:Obj)^(n:Integer): with Obj ==
(Prod:Obj,project:Integer->(Prod->A),product:(X:Obj)->(Tuple
(X->A))->(X->Prod)) == Product(A,n)
@@ -110,5 +110,5 @@
CoProduct:(A:Obj,n:Integer) -> (
Sum:Obj,Integer->(A->Sum),(X:Obj)->(Tuple (A->X))->(Sum->X))
- ..:(Obj,Integer) -> Obj
+ ..:(Obj,Integer) -> with Obj
default
- (A:Obj)..(n:Integer):Obj ==
+ (A:Obj)..(n:Integer): with Obj ==
(Sum:Obj,insert:Integer->(A->Sum),sum:(X:Obj)->(Tuple
(A->X))->(Sum->X)) == CoProduct(A,n)
----
Regards,
Bill Page.

Post by Bill Page
Ralf,
I think the problem here is that the new version of the Aldor compiler
needs a little more help just be reassured that you really are writing
a function that returns a domain. The empty 'with {}' clause seems to
do the trick.
Here is a patch to 'Categories.as' that allows it to compile... but I
have not yet compiled the rest so I am not 100% sure that the end

[Bill Page]

Thanks, Ralf. I like your version better than mine. It makes more
sense than the apparently redundant syntactic change I proposed ...
although I wonder why we should define a local function rather than
just write it inline. Would you agree however that that fact that
Saul's original variant does not compile should be considered a
regression bug in the Aldor compiler?

Regards,
Bill Page.

Post by Ralf Hemmecke
Hello Bill,
I think, I don't like your suggestion.
I'd rather change it into
define Product(Obj:Category):Category == with {
...
-- *:(Obj,Obj)->Obj;
default {
local mult(A:Obj, B:Obj):Obj == {
(
AB:Obj,
pa:AB->A,
pb:AB->B,
product:(X:Obj)->(X->A,X->B)->(X->AB)
) == Product(A,B);
AB add;
}
*: (Obj,Obj)->Obj == mult;
}
}
The "default" is like defining an anonymous "add" body which exports
anything on the left of == that is not declared local. So
*: (Obj,Obj)->Obj
will get exported by Product(Obj) even if you put a "--" as I did above.
Ralf

Post by Bill Page
Ralf,
Here is another version that is slightly more friendly to the #pile
syntax (-: no {} required :-). I presume that the compiler generates
the same code...
--- Categories.as_orig 2007-11-08 10:09:11.000000000 -0800
+++ Categories.as 2007-11-08 10:45:51.000000000 -0800
@@ -66,3 +66,3 @@
Product: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) ->
(AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2))
- *:(Obj,Obj)->Obj
+ *:(Obj,Obj)-> with Obj
default
@@ -73,3 +73,3 @@
(ab1,ab2,*)
- (A:Obj)*(B:Obj):Obj ==
+ (A:Obj)*(B:Obj): with Obj ==
(AB:Obj,pa:AB->A,pb:AB->B,product:(X:Obj)->(X->A,X->B)->(X->AB))
== Product(A,B)
@@ -83,3 +83,3 @@
CoProduct: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) ->
(AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1))
- +:(Obj,Obj)->Obj
+ +:(Obj,Obj)-> with Obj
default
@@ -90,3 +90,3 @@
(ab1,ab2,+)
- (A:Obj)+(B:Obj):Obj ==
+ (A:Obj)+(B:Obj): with Obj ==
(AB:Obj,ia:A->AB,ib:B->AB,product:(X:Obj)->(A->X,B->X)->(AB->X))
== CoProduct(A,B)
@@ -99,5 +99,5 @@
Product:(A:Obj,n:Integer) ->
(Prod:Obj,Integer->(Prod->A),(X:Obj)->(Tuple (X->A))->(X->Prod))
- ^:(Obj,Integer) -> Obj
+ ^:(Obj,Integer) -> with Obj
default
- (A:Obj)^(n:Integer):Obj ==
+ (A:Obj)^(n:Integer): with Obj ==
(Prod:Obj,project:Integer->(Prod->A),product:(X:Obj)->(Tuple
(X->A))->(X->Prod)) == Product(A,n)
@@ -110,5 +110,5 @@
CoProduct:(A:Obj,n:Integer) -> (
Sum:Obj,Integer->(A->Sum),(X:Obj)->(Tuple (A->X))->(Sum->X))
- ..:(Obj,Integer) -> Obj
+ ..:(Obj,Integer) -> with Obj
default
- (A:Obj)..(n:Integer):Obj ==
+ (A:Obj)..(n:Integer): with Obj ==
(Sum:Obj,insert:Integer->(A->Sum),sum:(X:Obj)->(Tuple
(A->X))->(Sum->X)) == CoProduct(A,n)
----
Regards,
Bill Page.

Post by Bill Page
Ralf,
I think the problem here is that the new version of the Aldor compiler
needs a little more help just be reassured that you really are writing
a function that returns a domain. The empty 'with {}' clause seems to
do the trick.
Here is a patch to 'Categories.as' that allows it to compile... but I
have not yet compiled the rest so I am not 100% sure that the end

--~--~---------~--~----~------------~-------~--~----~
You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group.
For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en
-~----------~----~----~----~------~----~------~--~---

[Ralf Hemmecke]

Post by Bill Page
Thanks, Ralf. I like your version better than mine. It makes more
sense than the apparently redundant syntactic change I proposed ...
although I wonder why we should define a local function rather than
just write it inline. Would you agree however that that fact that
Saul's original variant does not compile should be considered a
regression bug in the Aldor compiler?

Yes and no.

Suppose you want to declare

---BEGIN aaa.as
#include "aldor"
define Cat: Category == with {
foo: String -> Integer;
foo: (s: String) -> Integer;
}
---END aaa.as

The types of both foos are different. The question now is, would you
like Cat to export 2 or only 1 function?

Now there is a very special case...

Would you like X and Y

X: Record(x: A);
Y: Record(y: A);

be of the same type?

So I cannot really say yes or no to your question and would rather be
happy to hear more information from the people who changed the compiler
behaviour.

What is the background? And (more importantly) what is the semantics of
"Cat" according to the language definition. I cannot say whether it
exports one or two functions.

Ralf

[Saul Youssef]

Hi Bill, Ralf,

To put things in perspective, I tried two alternative definitions
of Product and coProduct besides the ones in Categories.as. One is as
the right adjoint of the diagonal functor (Ideal.as) and the other is
as a special case of general limits and colimits (Limits.as). The
last two seemed like that should work in the language, but didn't due
to compiler problems. The one in Categories.as got used only because
it's the only one of the three that worked at the time.

- Saul

Post by Ralf Hemmecke
Hello Bill,
I think, I don't like your suggestion.
I'd rather change it into
define Product(Obj:Category):Category == with {
...
-- *:(Obj,Obj)->Obj;
default {
local mult(A:Obj, B:Obj):Obj == {
(
AB:Obj,
pa:AB->A,
pb:AB->B,
product:(X:Obj)->(X->A,X->B)->(X->AB)
) == Product(A,B);
AB add;
}
*: (Obj,Obj)->Obj == mult;
}
}
The "default" is like defining an anonymous "add" body which exports
anything on the left of == that is not declared local. So
*: (Obj,Obj)->Obj
will get exported by Product(Obj) even if you put a "--" as I did above.
Ralf

Post by Bill Page
Ralf,
Here is another version that is slightly more friendly to the #pile
syntax (-: no {} required :-). I presume that the compiler generates
the same code...
--- Categories.as_orig 2007-11-08 10:09:11.000000000 -0800
+++ Categories.as 2007-11-08 10:45:51.000000000 -0800
@@ -66,3 +66,3 @@
Product: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) ->
(AB1:Obj,AB2:Obj,(A1->A2,B1->B2)->(AB1->AB2))
- *:(Obj,Obj)->Obj
+ *:(Obj,Obj)-> with Obj
default
@@ -73,3 +73,3 @@
(ab1,ab2,*)
- (A:Obj)*(B:Obj):Obj ==
+ (A:Obj)*(B:Obj): with Obj ==
(AB:Obj,pa:AB->A,pb:AB->B,product:(X:Obj)->(X->A,X->B)->(X->AB))
== Product(A,B)
@@ -83,3 +83,3 @@
CoProduct: (A1:Obj,B1:Obj, A2:Obj,B2:Obj) ->
(AB1:Obj,AB2:Obj,(A2->A1,B2->B1)->(AB2->AB1))
- +:(Obj,Obj)->Obj
+ +:(Obj,Obj)-> with Obj
default
@@ -90,3 +90,3 @@
(ab1,ab2,+)
- (A:Obj)+(B:Obj):Obj ==
+ (A:Obj)+(B:Obj): with Obj ==
(AB:Obj,ia:A->AB,ib:B->AB,product:(X:Obj)->(A->X,B->X)->(AB->X))
== CoProduct(A,B)
@@ -99,5 +99,5 @@
Product:(A:Obj,n:Integer) ->
(Prod:Obj,Integer->(Prod->A),(X:Obj)->(Tuple (X->A))->(X->Prod))
- ^:(Obj,Integer) -> Obj
+ ^:(Obj,Integer) -> with Obj
default
- (A:Obj)^(n:Integer):Obj ==
+ (A:Obj)^(n:Integer): with Obj ==
(Prod:Obj,project:Integer->(Prod->A),product:(X:Obj)->(Tuple
(X->A))->(X->Prod)) == Product(A,n)
@@ -110,5 +110,5 @@
CoProduct:(A:Obj,n:Integer) -> (
Sum:Obj,Integer->(A->Sum),(X:Obj)->(Tuple (A->X))->(Sum->X))
- ..:(Obj,Integer) -> Obj
+ ..:(Obj,Integer) -> with Obj
default
- (A:Obj)..(n:Integer):Obj ==
+ (A:Obj)..(n:Integer): with Obj ==
(Sum:Obj,insert:Integer->(A->Sum),sum:(X:Obj)->(Tuple
(A->X))->(Sum->X)) == CoProduct(A,n)
----
Regards,
Bill Page.

Post by Bill Page
Ralf,
I think the problem here is that the new version of the Aldor compiler
needs a little more help just be reassured that you really are writing
a function that returns a domain. The empty 'with {}' clause seems to
do the trick.
Here is a patch to 'Categories.as' that allows it to compile... but I
have not yet compiled the rest so I am not 100% sure that the end

[Francois Maltey]

Thanks Bill,

Post by Bill Page
Dear Friends of Axiom and Aldor,
I have been thinking again about type equivalence.
(1) -> P:=Product(Stream Integer,Stream Integer)
(2) -> Q:=Stream Product(Integer,Integer)
Type: Domain

Can I understand that as the relationship between
Complex Fraction Integer and Fraction Complex Integer ?
[I don't find any surprising effect done by this coerce.]

Post by Bill Page
It seems that 'Stream' is a "sum-like" domain constructor so
that we might reasonably expect algebraically that a 'Product'
distributes over a 'Stream' and therefore wish to
design the Axiom library so that this is satisfied.

I know that cartesian product of set is the set of brace
E x F = {(x,y) | x in E and y in F}.
Product (Set XX, Set YY) is Set Product (XX, YY)

Post by Bill Page
Thus we should have P = Q.

Do you identify Set and Stream ?
but a stream can repeat its elements [1,2,3,1,2,3,1,...
Perhaps I mismatch the Domain << Stream Integer >> and the use of one Stream.

Post by Bill Page
I understand that neither Spad nor Aldor actually evaluate type
expressions like P and Q.

1.. x 1.. may be [(1,1), (1,2),(2,1), (1,3),(2,2),(3,1), ...

Post by Bill Page
But perhaps EQUAL in the Lisp sense could apply?

A semi-decidable equal ?
The answer is false when view tests shows that the results are differents.
The answer is true when the inner built are equal.
The answer is unknown in the other cases.

It's not a problem :
1 - 2*sin^2 x and 2*cos^2 x - 1 are differents for most (or all) systems.

Post by Bill Page
Therefore I would propose the following definition of type-equivalence
Def: Two domains P and Q are equivalent if and only if
(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.

I don't understand this last case.

Post by Bill Page
But as I understand the
intention of the semantics of categories in both Axiom and Aldor this
is not enough. We want categories to represent abstract concepts
usually with a well-defined mathematical meaning.

Product in for-loop isn't exactly the product of 2 sets.

In a for-loop [a,b,a] x [1,2] gives [a,1],[b,1],[a,1],[a,2],[b,2],[a,2].
types can be differents. A for-loop might also works for [a,b] x [1..].

Does your product can be understand
for cartesian products of set and for for-loop ?

Post by Bill Page
I would like to know if other developers think this more algebraic
approach to the design of the Axiom library domains makes sense.

Martin almost convinces me that the algebraic
[f (u,v) for (u,v) in [a,b,c] X [1,2,3]]
is better than [f (u,v) for u in [a,b,c] repeat for v in [1,2,3]]

but I expect a syntax suggar and automatic coerce.

The * isn't the better operator because this locks
{1,2,3} * {1,2,3} = {1,2,3,4,6,9}
and {1,2,3} + {1,2,3} = {2,3,4,5,6}

I hope I don't appear too stupid !

F.

[Martin Rubey]

Post by Francois Maltey
Martin almost convinces me that the algebraic
[f (u,v) for (u,v) in [a,b,c] X [1,2,3]]
is better than [f (u,v) for u in [a,b,c] repeat for v in [1,2,3]]
but I expect a syntax suggar and automatic coerce.

It occurred to me that the following might make it even clearer:

what does a looping construct have to do with a Cartesian product? Except that
one may (but doesn't have to) use it to *implement* a function that returns all
elements of a Cartesian product.

Post by Francois Maltey
The * isn't the better operator because this locks
{1,2,3} * {1,2,3} = {1,2,3,4,6,9}
and {1,2,3} + {1,2,3} = {2,3,4,5,6}

I actually wondered already once, why "+" is not union$Set, "-" not
difference$Set. I didn't think of the possibility above, although I doubt that
it would be too useful. After all, you can even define it only if the elements
understand "+" and "*".

Martin

[Francois Maltey]

Dear Martin,

Post by Martin Rubey
what does a looping construct have to do with a Cartesian product?

The construct arround reduce/concat isn't so usual in order to
built several overlapped loops.
cartesian product and repeat keyword are two possibilities.

Post by Martin Rubey

Post by Francois Maltey
The * isn't the better operator because this locks
{1,2,3} * {1,2,3} = {1,2,3,4,6,9}
and {1,2,3} + {1,2,3} = {2,3,4,5,6}

I actually wondered already once, why "+" is not union$Set, "-" not
difference$Set.

I think that operator for sets are missing.
union (union (E, F), G) is less clever than E union F union G.

But why do you want a +. It might be possible to have more operators

Post by Martin Rubey
I didn't think of the possibility above, although I doubt that
it would be too useful.

For finite set it's not useful,
but very useful for intervals ; and intervals and set are close.

I like to use it for chaotic systems, with numerical instability.
or in order to separate root of a function.

newton methods can forget some mutiple roots.
interval methods, with operations over intervals, can add false roots.

Post by Martin Rubey
After all, you can even define it only if the elements
understand "+" and "*".

I meet this needs for functions.
axiom doesn't understand that sin+cos is the fuction x +-> (sin x + cos x)

François

[Martin Rubey]

Post by Francois Maltey
Dear Martin,

Post by Martin Rubey
what does a looping construct have to do with a Cartesian product?

The construct arround reduce/concat isn't so usual in order to
built several overlapped loops.
cartesian product and repeat keyword are two possibilities.

Post by Martin Rubey

Post by Francois Maltey
The * isn't the better operator because this locks
{1,2,3} * {1,2,3} = {1,2,3,4,6,9}
and {1,2,3} + {1,2,3} = {2,3,4,5,6}

I actually wondered already once, why "+" is not union$Set, "-" not
difference$Set.

I was thinking of Boolean algebra. Now, I looked a little closer to find the
Category "Logic", which exports /\ and \/, which would in fact be a lot better
than + and *.

Post by Francois Maltey
I think that operator for sets are missing.
union (union (E, F), G) is less clever than E union F union G.

(1) -> \/(a: Set INT, b: Set INT): Set INT == union(a, b)
Function declaration ?\/? : (Set Integer,Set Integer) -> Set Integer
has been added to workspace.

(2) -> set [1,2,3] \/ set [2,3,4]
Compiling function \/ with type (Set Integer,Set Integer) -> Set
Integer

(2) {1,2,3,4}
Type: Set Integer

Post by Francois Maltey
But why do you want a +. It might be possible to have more operators

yes, but I want to be use the "right" operators. As we know already (see
Monoid / AbelianMonoid discussion), currently this is not always possible in
Aldor or Axiom. But when it is, we should use them.

Just to make sure, I did not say that your definition of * and + for sets is
bad per se. I only found it unusual. And I do not want "unusual" things in
the axiom library. The user should make this definitions himself.
Unfortunately, there is a bug in the interpreter:

(1) -> _*(A: Set INT, B: Set INT): Set INT == set concat [[(a*b)$Integer for a in members A] for b in members B]
Function declaration ?*? : (Set Integer,Set Integer) -> Set Integer
has been added to workspace.
Type: Void
(2) -> 2*3
Compiling function * with type (Set Integer,Set Integer) -> Set
Integer
Conversion failed in the compiled user function * .

Cannot convert from type Integer to Set Integer for value
2

Post by Francois Maltey
axiom doesn't understand that sin+cos is the function x +-> (sin x + cos x)

I do not see the connection to the topic above. But still, you can quite
easily build a domain that has, for example, univariate functions as objects.
That might indeed be useful.


Martin

[Ralf Hemmecke]

Post by Bill Page
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.

Ralf

[Bill Page]

Post by Ralf Hemmecke

Post by Bill Page
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.