Re: [Axiom-developer] categorical design

[Bertfried Fauser]

Dear Bill,

        I judge myself not an expert in category theory (though I heavily
use it) and I am certainly not aware of the complexity of AXIOMs type
system (yet). But perhaps the following may help:

a) There is not "category theory" per se. Many people do quite different
(and sometimes contradicting) things with categories. Hence with "category
theory" there has to come meta information to make sure its used the
_polictical correct_ way. I had some problems with other mathematicians
whene I used categories not that way ;-)
-- Set Based category theory, ie the older version. This is still based on
   the idea (Bourbaki by the way) that all of mathematics should be based
   on set theory (in my eyes a contradictinmg paradigm to quantum mechanics).
   Nevertheless, this treatment came up with homological algebra and went
   into categories which are *not* af type set at all....
-- Function based category theory (still a new branch of mathematics,
   started by William Lawvere and others, using *constructivistic* ideas
   of Brouwer [hence a generic computational approch, one should think]).
   The idea is to define functions as elementary objects and then compute
   from scratch what kind of (sometimes awkward!) objects may be
   manipulated by these functions (domains and codomains may be categories
   itself). It does not make a choice of a _basic category_ but leaves
   this open.
        Regarding AXIOM, a valuable choice would be a topos. Topi (Lawvere
   calls them toposes, which is linguistical barbaric ;-) Constitute a
   sort of category which is very close to Set, but slightly larges, just
   axiomatizing the basic structures of Set. Its a general experience,
   that if you axiomatize mathematical structures in a categorial way
   then you get more general structures due to isomorphism invariance of
   these _objects_.

b) From matroid theory (which encodes very basic facts about linear and
general dependance of objects) one learns that there is something like a
cryptomorphism spoiling the idea that mathematics is a well ordrere (or
even partially ordered) lattice. Indeed you find complicate isomorphisms
from one axiom system into another which maps basic structures to very
complicated ones and vice versa (Tim's 'shere', by the way a very
complicated topological problem to detect on which (hyper)surface a graph
may live).
        Hence I guess that there will be no generic or cannonical choice
for an starting point in the type lattice, but it should be a matter of
taste and adjusted to the problems you want to attack.

c) Isomorphisms problem.
        It is a general *problem* (dealt with under the name of
_categorification_ to 'categorify' a mathematical structure, say the
natural numbers. Since this is a generalization it is neither canonical
nor unique and needs meta input (experience or even information from
physics ie experiments) if the math shall be related to soemthing
reasonable. A current problem is to categorify the theory of categories (a
typical mathematical thinking <grin>) which leads to n-category theory,
which I am try to employ in quantum physics. This is unsolved mathematical
reasearch, ....

d) Isomorphisms implementation problem.
        From my own experiments with CAS (eg Maple) there is anothe
rproblem for actual computations. Having defined a mathematical category,
you have set up an abstract structure of relations between functions.
However, if you want to implement this, you need _elements_ on which such
functions can act. That is you need a modell for your category, such
modells may be *tremendously* different and it might be a practical
impossible task to construct an isomorphsims (type conversion) between
such elements *even if you can mathematically prove they are of the same
kin*!
        Moreover, you find *non representable* categories, which cannot be
represented over the category Set, which are quite awkward object. I do
not yet see how to impelemt such categories is a CAS.
        A further example is that patological objects migcome into play.
Zbigniew Oziewicz and I do search for years now a categorial description
of Clifford algebras. But reasonable axioms *include* some further
algebras with quite obscure behaviour which you would not like to address
by this name. If you introduce base (ie elements represnting the algebra)
this diaspears, but I do not yet know why..... Such problems will arise if
a strickt mathematical type system would be implemented.

Hence the AXIOM types may still have a need to be based on some
representations, which is a second layer of non abstractnes (after the
choice of a starting 'north pole' in the type graph. I see currently no
way around this (but I am not an expert in type-ing ;-) )

hope this is informative for you, otherwise I apologize
cheers
BF.

% |   | PD Dr Bertfried Fauser    Fachbereich Physik    Fach M 678  |
%  \ /  Universit"at Konstanz     78457 Konstanz        Germany     |
% (mul) Phone : +49 7531 883786   FAX : +49 7531 88-4864 or 4266 (comul)
%   |   E-mail: address@hidden                   / \
%   |   URL   : http://clifford.physik.uni-konstanz.de/~fauser    |   |

>> A prophet does not count in his country -- a patriot nowhere else <<