Detail of the KAN Project

2.6.1 Survey: There is much we can learn from other computer algebra packages and consequently we will make contact with the creators of these packages. We shall also seek to enlarge our client list so as to increase the stock and variety of concrete problems which will complement the theoretical perspective in driving the development of Kan.

2.6.2 Categorical Research: The prototype of Kan calculates certain quotients by modelling them as Kan extensions over 1#1. The kernel of Kan will be written to enable it to model finitely presented Kan extensions. This will involve research in the following areas:

• Kan Presentations: The classic colimit formula expresses Kan extensions as (pointwise) colimits and hence provides a basic data structure and rewrite rules which are valid for all Kan extensions. In addition to this, specific (possibly infinite) algebraic structures are modelled by finite presentations whose associated free functor constructs a free algebra from its finite presentation. This free algebra enriches the basic data structure to form one specific for the problem at hand. In the prototype of Kan, two such free functors were used i) The free monoid functor constructs strings from data in the presentation and hence leads to computation based upon string rewriting and ii) the free ring functor constructs polynomial rings and hence leads to computation based upon Gröbner basis techniques.

  In these examples, the domain of the free functor is 1#1 but the theory of lfp-categories [1] gives conditions under which the one structure can be presented in terms of another structure rather than just 1#1. This opens the way to a form of divide and conquer approach using presentations over presentations. Consequently, we will look for new forms of Kan presentations at both this theoretical level and, more concretely, by investigating specific problems.

• The Algebra of Kan Extensions: There are a number of situations where the efficiency of Kan could be improved by expressing a quotient in terms of a simpler quotient. For example, if a group defined by a presentation has a convergent rewrite system, one would use this convergent rewrite system to compute the cosets generated by a subgroup, rather than computing the cosets from scratch. The correctness of such optimisations involve theorems relating the rewrite relations involved and, since these rewrite relations are defined to compute Kan extensions, this amounts to theorems about Kan extensions. Thus researching the algebraic laws of Kan extensions, e.g. the effect of functoriality, change of base theorems and enrichment [13,29], will provide the theoretical basis for a variety of optimisations (see section 2.6.4).

2.6.3 Rewriting Research: Research will provide a general notion of rewriting for the kernel and optimisations to ensure the efficiency of Kan.

• Categorical Rewriting: Since Kan is not to be limited to specific problem domains, rewriting in Kan will have to be parameterised by the data forming the Kan extension. This parameterisation will be based upon Dr Ghani's monadic models of rewriting which are the first models to contain an underlying model of the objects being rewritten. By varying the base category of the monad one derives different notions of rewriting while enriching the monad, over say 2#2, models the rewriting. Consequently rewriting for a particular Kan extension will be derived by instantiating these abstract models of rewriting with the data of the specific Kan extension to obtain a more concrete notion of rewriting.
• New Knuth-Bendix Procedures: Knuth-Bendix completion [2] provides a general procedure for converting rewrite systems into convergent rewrite systems which generate the same theory and hence decide the quotient. As we develop new notions of rewriting we shall have to generalise existing forms of Knuth-Bendix completion. In addition, Knuth-Bendix completion is parameterised by a termination order and the prototype of Kan only uses a specific termination order. Kan will use different termination orders to obtain the best completion procedure for each specific problem.
• Logged Rewriting: Typically in rewriting one is only interested in the existence of a rewrite between two terms. However, logged rewriting [21,23] seeks to retain information about the structure of the rewrite so as to provide a checkable record of the computation. Different possibilities exist as to the structure of these logs with the algebra of 2-categories being the best known. Categorical rewriting suggests these labels should not be considered separately but rather as arising from a different enrichment, e.g. Cat rather than Pre. We shall therefore study logged rewriting from this theoretical perspective as well as the more concrete perspectives occurring in the literature.
• Modular Rewriting: Modular rewriting [31,44] seeks criteria under which rewrite systems inherit properties from their smaller (and hence easier to reason about) subsystems. In particular, modularity would allow us to obtain a convergent rewrite system more efficiently from convergent subsystems than from a brute force method. Dr Ghani has worked on categorical and non-categorical approaches to modular rewriting (see track record) and will guide research here.
• Automata: The normal forms of a convergent rewrite relation generated by a Kan extension over 1#1 form a regular language and hence can be recognised by an automata. This gives a representation of the quotient structure as with the enumerative algorithms, but without the limitation to finite structures. We shall investigate how general this situation is with Prof R. Thomas who is an expert on automatic structures [7].

2.6.4 Software Development: Four main deficiencies of the prototype program can be identified: i) the different components are not yet fully integrated; ii) the user interface is not tailored for end-users; iii) the system has as yet no optimisations; iv) the prototype cannot be interfaced with other systems. We will address these deficiencies as follows:

• Software Structure: Integration of the components of the package Kan will be achieved by implementing categorical structures defined in consultation with the Computational Category Theory Group for international standards, ensuring the compatibility of Kan with other packages.
• User Interface: The input/output interfaces will be worked out in consultation with our clients. There will be different `tailored' modes so that different users can interact with Kan in a manner most suitable for their needs.
• Optimisations: There are three lines of optimisation which will increase the efficiency of Kan: i) choosing between different coefficient fields and orderings for both the terms and rewrite rules, ii) calling specialised rewriting algorithms when appropriate, e.g. in finite, commutative and difference binomial situations; iii) by using modularity as mentioned in section 2.6.2.
• Integration and Communication: Developments in technology (eg OpenMath) for presenting and interlinking mathematical software widen the immediate benefits of computer algebra packages such as KBMAG [24], Vector Enumerator [34] and our proposed Kan, which interface to a popular system (such as 3#3 [16]). In the longer term, the improved communications should make it possible to link to fast Gröbner basis programs (such as SINGULAR, OPAL [30] or Bergman) for greater efficiency.

2.6.5 Testing and Applications: The software will be tested with the help of clients who wish to solve problems to which Kan can be applied.