Dear Martin, > category theory is a subject that one could spend a lifetime on
Indeed ;-) and some people actually do so.... I don't buy your attitude to keep clear from it, as especially in computer science categories are invaluable. That may be different in computer algebra though... > I was thinking about how to convert a finite state machine into a instance of > Lambda, then I realised this is just about implementing stateful code in a > pure > functional language and Haskell has already solved that problem - use monads > .... Yes, Haskel is great, but it does not really have CAS abilities ;-). To have Aldor available would make AXIOM much more prone to use such techniques too. > Given the above issues, perhaps what I am looking for is some subset > of category theory that is simple enough to be implementable but > complex enough to provide the sort of framework I'm looking for. I didn't wanted to discourage you. I just wanted to understand what your objectives are. Also I know quite a bit of math on the categorical level, but have till now no idea how to implement them in a CAS. Any tool which might help doing so, or even give ideas how to approach my problems would be appreciated. > starting with the simplest concrete category where functors are mappings > between > finite sets and then building up Indeed a set itself can be seen as a category, as also a poset (with greater effect), functors are then just mappings. This point of view unites some constructions. The main problem I see, is how a CAS would `reason' about categorical statements. A commutative diagram is just an equation of some (strict) arrows, but you want to use properties of arrows, like monic, epic, or being a kernel or an equalizer (in general limits and colimits, unique arrows such as terminal and initial arros etc.) > 1) Programs like Haskell provides some category-theory-like > Typeclasses, using higher order functions and features of the language > like partial function application and currying. Haskel is not itself `categorical' but functional. Also types are actually best seen a functors. As AXIOM has an underlying lisp layer, it has some functional aspects, as untyped lambda calculus. However in a CAS one needs to reason about 'programs' and that is done by using the Curry-Howard isomorphism (proofs as programs). Its funny that recent developments in physics employ the same principle. But once more it is not evident (to me) how to actually code this... > 2) Attempts to more fully model category theory such as Charity > program I haven't looked into Charity. Just go ahead and see what you can do. Code rules. Cheers BF. -- % PD Dr Bertfried Fauser % Research Fellow, School of Computer Science, Univ. of Birmingham % Honorary Associate, University of Tasmania % Privat Docent: University of Konstanz, Physics Dept <http://www.uni-konstanz.de> % contact |-> URL : http://www.cs.bham.ac.uk/~fauserb/ % Phone : +44-121-41-42795 -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To post to this group, send email to fricas-devel@googlegroups.com. To unsubscribe from this group, send email to fricas-devel+unsubscr...@googlegroups.com. For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en.
