Background for KANScientific and Technological Relevance
Computer Algebra: There are a number of successful
computer algebra packages for group theory, for example GAP [16],
Quotpic [25], KBMAG [24] and MRC
[39]. Kan is not expected to compete with these packages,
but to solve problems outside group theory where there are currently
few tools. The closest package to Kan is Carmody and Walters'
enumerative program [8] for computing Kan extensions over
Sets. However, i) Kan will compute Kan extensions over more
categories than
Sets and therefore quotients in other problem domains;
ii) Kan will not be enumerative and hence not limited to finite
structures; iii) Kan will be optimised to meet the
specific requirements of different users.
Category Theory: Since its inception, category theory has
been applied to an ever wider range of problems and is now ubiquitous
in many areas of mathematics and computer science. The use of category
theory as a metalanguage for algebra can be traced back to Linton
[33] and Lawvere [32] and the study of algebra has since
remained central to the development of category theory [3].
Kan extensions were originally developed 40 years ago [28] and
have since become a fundamental construction in category theory
[13,36]. Nevertheless, the use of Kan extensions as a
semantic framework for general computer algebra
packages is a new contribution of our own.
Rewriting and Gröbner Bases: Rewrite
systems [4,2] are of importance in a number of different
areas of mathematics and computer science. For example, string
rewriting plays a fundamental role in computational group theory
[14,42], while term and graph rewriting underlie
theorem provers [19] and functional programming [27].
Gröbner basis theory [11] can be seen as rewriting for
polynomials [37,20]. Originally developed to solve the ideal
membership problem, it has since been successfully applied in theorem
proving, robotics, integer programming,
differential equations etc.[6].
Categorical Rewriting: Categorical Rewriting provides a semantics for rewriting at an intermediate level of abstraction between the syntax and the relational model. Originally, research focused on 2categorical structures [41,40,26]. More recently, Dr Ghani has developed monadic models of rewriting [17] which are novel in containing an underlying model of the objects being rewritten. This opens the way for rewrite relations parameterised by the the objects being rewritten, which is precisely what will be required by Kan.

Author: Anne Heyworth
Last updated: 11th May 2001
MCS Web Maintainer
Any opinions expressed on this page are those of the author.
© University of Leicester.