
From:  Ralf Hemmecke 
Subject:  Re: [Axiomdeveloper] Re: Combinat 
Date:  Sat, 30 Jun 2007 22:42:51 +0200 
Useragent:  Thunderbird 2.0.0.4 (X11/20070604) 
if we are here dealing already with a sort of pointers (or function arrays) is there already in Aldor/Axiom a 'functor' domain?
Not that I know.
I think of a Functor domain in the following sense, it should implement a 'categoy' (in the mathematical sense) of morphisms which opperate on another (pair of) categor(y/ies). The functionality of such a category would be to implement naturality of maps, coherence, composability of morphisms, etc.
You might be interested in this paper that deals at least in part with these issues Domains of data and domains of terms in AXIOM by BROWN, R. & DRECKMANN, Whttp://portal.axiomdeveloper.org/refs/articles/brownfreecg.pdf/file_viewfromhttp://www.informatics.bangor.ac.uk/public/math/research/preprints/95/algtop95.html
I am quite disappointed from that paper. It is totally uninteresting from my species project point of view. Maybe the other way round, that species can be used to construct the directed graphs data structure. But that sounds a bit odd if I use functors (species) in order to implement categories.
In fact, it isn't. Axiom/Aldor cannot deal with categories and the keyword "Category" is a big misnomer. Aldor is better at describing universal algebras (or rather the multisorted case). And this is exactly what the above paper does. It describes a category by its algebraic properties. Unfortunately, all the categories from that paper have only finitely many objects. To me that is nothing really useful. For the species project I need the category of finite sets and bijections. Clearly, that category has infinitely many objects. It even has more than uncountably many objects. Take r any real. Then {r} is an object in that category.
I must say, I really doubt that any good implementation of a category is ever possible. Collecting all the arrows of a category explicitly, makes no sense for me. Same with the objects. If you want to compute in a category you probably have to do this, but then you are restricted to "finitely many".
As you can see in the ToDo of http://www.risc.unilinz.ac.at/people/hemmecke/AldorCombinat/combinatsu14.html#x27320008.1I did not yet take the time to work out the details of how the implementation of a species (i.e. a functor of a special kind) can be seen categorially. Note that I have a LabelType. That is a restriction that is imposed by the programming language Aldor. I cannot have a List of everything but only a List over objects of the same type. Same for a species. The labels must all be of the same type. Of course I could form unions, but again all objects/labels have to be of the same type.
There is no equivalent in the species theory. A species is a functor F that takes a finite set U and returns a finite set F[U]. There is no type attached.
IFF such a thing would work, species would be an instance, as also lambda rings and symmetric functions ;)
Yes, yes, but don't forget, we have to deal with infinite things. I will not even be able to get the full category of natural numbers on my computer... ;)
I think that is very interesting.
Oh yes, I agree. But that would call for a workshop similar to the one we had on symmetric functions. Since I don't work so much with categories, it would be interesting to hear what people would like to do when the want categories/functors/natural transformations being implemented on a computer. To me that sounds much more complicated than the symmetric function business. Actually, categories are so simple as algebraic structures. But that is not everything.
Ralf
[Prev in Thread]  Current Thread  [Next in Thread] 