Background for KAN

Scientific 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 meta-language 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 2-categorical 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.