[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] RE: categorial rep and per?

From: Bill Page
Subject: [Axiom-developer] RE: categorial rep and per?
Date: Sat, 12 May 2007 12:13:36 -0400

On May 12, 2007 5:35 AM Ralf Hemmecke wrote:
> On
> you write
> > I am especially interested in how the duality between rep
> > and per is involved in these constructions.
> My answer is: I don't know.

What I mean specifically is:

    project1(x:%):X == rep(x).a
    project2(x:%):Y == rep(x).b
    product(A:Type,f:A->X,g:A->Y):(A->%) ==
       (x:A):% +-> per [f(x),g(x)]


    inject1(x:X):% == per [a==x]
    inject2(y:Y):% == per [b==y]
    sum(A:Type,f:X->A,g:Y->A):(%->A) ==
       (x:%):A +->
         rep(x) case a => f(rep(x).a)
         rep(x) case b => g(rep(x).b)

Do you see how rep is used in the definition of 'project' but
per is used in the definition of 'inject'? And opposite in the
definitions of 'product' and 'sum'? I just thought that was a
little unexpected (to me) by-product of the duality.

> And I also don't know why you think that per and rep is
> something categorial.

Categorical in the sense of category theory - not necessarily
in the sense of category used in Axiom/Aldor. I guess I could
put it this way: I *want* to find a categorical definition of
rep and per because I do not fully understand why they appear
in Spad and Aldor but not in any other "object-oriented"
language with which I am familiar. I think (perhaps) that Spad
has made something explicit that is in fact implicit in these
other programming languages. Making this explicit is a good
thing, but I am not completely confident that the current
implementation - as a distinguished name 'Rep' and macros
'rep' and 'per'. I would like (perhaps) an appropriate
categorical semantics for rep and per and maybe some other
syntax in the Spad/Aldor language that properly distinguishes
this construct -- after all, this notion is central to the
implementation of abstract algebra in Axiom.

I tried to do something like this a while ago in

Perhaps it needs a little updating since I wrote it.

> Suppose I have a domain R with some exports CatR. And I 
> define for some other exports CatD a domain
> D: CatD == add {
>    Rep == R;
>    ...
> }
> rep and per relate R with D (basically saying that they
> are the same things as data structures with no features).
> But their exports have no relation at all.

Their exports are in fact related by the logic that is
implemented in ...

Exports are arrows.

> Mathematically seen, they are objects of different 
> categories. So rep and per would be functors (if
> anything). But how can such a construction be made
> functorial. I don't see that.

It is necessary to define more clearly I think what
*mathematical* category we are talking about. I was arguing
in RepAndPer that yes rep and per are adjoint functors in
a categorical sense. I still think that might be a fruitful
point of view.

Bill Page.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]