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, W
http://portal.axiom-developer.org/refs/articles/brown-free-c-g.pdf/file_view
from
http://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.uni-linz.ac.at/people/hemmecke/AldorCombinat/combinatsu14.html#x27-320008.1
I 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
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer