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.

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.