The KAN Project

An Overview of Kan: Many important mathematical and computer science problems can be phrased in terms of describing the quotient of an algebraic structure. The simplest example is that of equivalence classes which are formed by quotienting a set by an equivalence relation. A number of examples arise in group theory: finitely presented groups are quotients of free groups; cosets are quotients of groups by subgroups; quotient groups are formed by quotienting a group with a normal subgroup and orbits are quotients of a set by a group action. These group theoretic examples have analogues in the theory of rings and modules.

Kan Extensions: The common structure of these problems is evident and suggests they should not be studied in isolation but rather as specific instances of the more general problem of deciding equality in a quotient structure. Kan will achieve this by using a specification language based upon category theory whose algebraic nature fits well with the problems to be solved. At first sight, it would seem natural to model quotients as coequalizers but this is too restrictive as all objects would be forced to belong to the same category. For example, cosets are quotients of a group by a subgroup but form a set and not a group. One of our key contributions is the observation that Kan extensions are a sufficiently general structure to model all the above quotients in a computationally effective manner.

Computation: The representation of a problem as a Kan extension provides a data structure which represents the algebraic structure to be quotiented and rules defining the quotient. Computing the Kan extension amounts to providing an algorithm for deciding when two elements of the data structure represent the same element in the Kan extension. Rewriting offers the following methodology to achieve this -- orient the rules in order to form a rewrite relation and then obtain a convergent rewrite relation generating the same theory. Two elements will be identified in the quotient if and only if they have the same normal form in the convergent rewrite relation.

The most appealing feature of Kan is that it will not be limited to specific problem domains or to finite structures. Our key innovation is to achieve this not by simply collecting together a series of disparate algorithms from specific problem domains, but rather by unifying these problem domains at the specification level using category theory and at the computational level using rewriting.

Deliverables: This project will provide the following deliverables.

• More powerful package: We will broaden the range of problems which can be solved using Kan. This involves understanding how other problems can be specified using Kan extensions.
• More powerful computation: We will use categorical rewriting to implement new and more powerful forms of rewriting which are capable of computing these Kan extensions.
• Software development: We will ensure the software package meets the requirements of its users by enhancing both the kernel's functionality and efficiency.
• Benchmarking, Evaluation and Testing: We will test the package with a variety of state-of-the-art problems posed by our clients. This will ensure that Kan is of relevance to the wider mathematical community and provide the benchmarks by which the project should be judged.