GSoC 2012 Application Sergiu Ivanov: Category Theory Module

About Me

Basic Information

Name: Sergiu Ivanov

Enrollment: University of the Academy of Science of Moldova, http://www.edu.asm.md/en (partly in Romanian)

Melange link_id: unlimitedscolobb

Contacts: E-mail: unlimitedscolobb at gmail dot com or sivanov at math dot md, IRC: scolobb, GitHub username: scolobb.

Background

My initial focus was on computer science; in the years 2004-2007, I have successfully taken part in a number of school Olympiads in programming and algorithms. At the university (2007-2011), I have studied formal languages, operating systems, networking, databases, object-oriented programming and Prolog. In my spare time I have got acquainted with a number of programming languages and frameworks, among which are C/C++, Java, Python, .NET/Mono, Smalltalk, Common Lisp, Haskell. At the university, I have also taken courses in calculus, probability, discrete mathematics, numerical methods, and optimisation.

In tried to be a part of GSoC 2008 with GNU/Hurd, with the project "Namespace-based Translator Selection". I was not accepted because of my low activity during the proposal ranking period; however, I worked on the idea voluntarily; one can find the short report of what has been done here. I was accepted to GSoC 2009 to the same organisation (GNU/Hurd), with the project "VFS-based Unionmount". The documentation of the tool I have developed (by extending another one) can be found here.

In my last year of bachelor studies I have implemented a remoting framework in Haskell. The code is here. My diploma project was a simulator of P systems written in Java, Jython, C, and Haskell. The code is here. In my diploma project I made use of OpenCL/CUDA.

I am currently pursuing MSc in "Mathematics and Informatics". I have had courses in parsing, theory of algorithms, measure theory. I have had (or am having) quite a bit of algebra-related courses: modules (and a bit of rings), lattices, quasigroups, Gröbner bases. I am doing part-time research in computability theory with focus on unconventional computing models. In my spare time I am learning category theory, functional programming, and lambda calculus.

My Environment and Coding Skills

I'm running the latest 64-bit Gentoo Linux. I have Python 2.7.2 installed. I prefer to code in Emacs.

I have been using Python every now and then for about 4 years now. I wrote simple to moderately complex university assignments in Python, including a wxPython-based application for creating and editing simple graphs and for running basic graph algorithms (minimal spanning trees and shortest paths mainly) with a custom widget for visually editing graphs. My knowledge of Python remains somewhat patchy, though.

Although I have had encounters with other version control systems, I am most comfortable with Git. I have been actively using Git since 2009, including for management of my university coding and documentation projects.

Patch Requirement

I have submitted a fix for for Issue 3106; the corresponding pull request has been merged into master.

I have also worked on Issue 2142; the corresponding pull request has not yet been merged, but will hopefully be soon.

The Project

Abstract

Category theory is a relatively new domain of mathematics which arose in an attempt to generalise existing algebraic structures. Because of the novelty of the approaches used in this domain, the number of people applying it is only increasing slowly. On the other hand, there is no way yet to represent category theoretic reasoning in modern CAS. The goal of this project is making SymPy capable of both representing category theoretic reasoning and carrying out a part of category theoretic reasoning automatically, with main focus on deciding the commutativity of diagrams.

Introduction

Diagrams

One of the most important tools in category theoretical reasoning is the commutative diagram. A diagram in a category A is a subclass of objects and some of the morphisms between the objects. For example, the objects A,B,C\in A and the morphisms f:A->B, g:B->C form a diagram. A popular way to represent such diagrams is by actually drawing the objects as dots and the corresponding morphisms as arrows between them. For example, [3] is a graphical representation of a diagram. When drawing diagrams, it is common to omit the arrows which are compositions of other arrows already present in the diagram and which do not bear any special significance for the diagram itself.

For further examples of (larger) commutative diagram, check out [8].

Consider a diagram in a category A and two objects A,B\in A which are connected by a path from A to B in the diagram. When one follows the path, one constructs the composition of the morphisms represented by the corresponding arrows, in the order of traversal. Thus, by following the path from A to B in the diagram A-(f)->C-(g)->B, one constructs the morphism gf. A commutative diagram is a diagram in which the following holds: for a pair (A,B) of objects in this diagram, every path from A to B yields the same morphism f.

It turns out that the property of a diagram to be commutative is sufficiently eloquent to express almost any category theoretic statements; this makes commutative diagrams one of the fundamentally important instruments in category theory. A lot of proofs are done by (or can be reduced to) checking whether a certain diagram is (or certain diagrams are) commutative.

In certain concrete categories, checking the commutativity of a diagram can be done directly, by choosing an arbitrary element of the object A and computing to what element it is mapped in B by every path from A to B in the diagram. If the mappings are the same for any such pair of objects A and B, then diagram is commutative. This approach obviously depends heavily on knowing the internal structure of objects and the exact effect of every morphism in the diagram. Thus, this approach will not obviously work for abstract categories; in fact, it will not work for all concrete categories even, in the cases when the structure of objects is insufficiently detailed.

The most general approach to checking the commutativity of diagrams is based on the fact that a lot of category theoretical statements can be expressed as the property of a diagram to be commutative. Consider a category A with a set of properties expressed as a set of commutative diagrams D. Then a diagram in category A will be commutative if it is a "composite" of some diagrams in D. Slightly more formally, a diagram will be commutative if one can find embeddings of diagrams from D which are sufficiently "well-placed".

Current Situation

No software implementation of anything closely related to category theory currently shows up in searches. While tools for manipulating concrete algebraic structures abound, it seems that it is impossible to even represent category theoretical reasoning in any of the modern CAS. While not being a formally concrete source, [4] illustrates the situation rather vividly.

There have been some indications that people are working on having such things implemented, namely that a group of people on the sage-combinat mailing list are creating a class structure similar to what I suggest. I will contact them to compare the scopes of our projects and see how we could do each other benefit.

Goal

This Google Summer of Code 2012 project has two major goals:

make it possible to represent category theoretical reasoning in SymPy by creating and manipulating categories and diagrams, and
make it possible to decide the commutativity of diagrams.

Relevance and Benefits for SymPy

While I believe that it is absolutely clear which benefits this project will bring to the end users working with category theory, the number of such users is still apparently very low. Therefore, I feel it necessary to explicitly elucidate the benefits SymPy herself will gain from having a category theory module. There are three fundamental points to this matter, as I see it:

Organisation of algebraic structures. Efforts are beginning to have SymPy deal with algebraic structures like groups, modules, rings. This makes the problem of having common fundamental infrastructure relevant. The category theory module will offer a number of classes which will serve as a checklist when implementing a new algebraic structure (homomorphism, zero object, kernel, etc.) and will contribute to uniform implementations of such structures.
Stating facts about algebraic structures. My implementation of diagrams will make it possible to state some facts about certain constructions (see, for example, Aaron's question about expressing isomorphisms between two groups [6]) and then effectively apply these statements by deciding commutativity of some other diagrams. Moreover, some category theoretic notions (functors [5]) will eventually make it possible to state more general facts involving heterogeneous algebraic structures (like the fact that a module has the underlying abelian group).
Priority. SymPy may become the first widely available general purpose CAS offering category theoretic tools.
Automatic drawing of commutative diagrams. People will be able to have diagrams typeset for them automatically, which is going to be very useful for authors of articles on category theory.

Please note that, while dealing with commutative diagrams involves working with graphs, commutative diagrams are a very special kind of graphs and, as I describe my vision of the implementation, it will be easy to notice that the whole thing includes much more details pertaining to mathematical logic and artificial intelligence (like backward chaining) than to graph theory.

Implementation Idea

I am going to split the implementation of this project into three mandatory phases, as well as an extra phase which is concerned with further improvement and extension of what will be implemented during the first three phases. Note that, due to the complexity of the things I will have to implement, I expect to only have the basics of the category theory module done by the end of the summer of code.

Class Hierarchy

In this phase I will implement the foundation classes for representing the mathematical notions I have introduced earlier in the proposal.

I will start with defining the class Class, which will represent a class in set theoretic sense. Since the existing class Set in sympy.core is defined sufficiently loosely, I will leave Class empty and essentially a synonym of Set. This is done in the waiting for the future implementation of set theory with distinction between classes and sets.

I will then define Object which will represent an object in a category and Morphism, which will represent a morphism. In this very basic form, Object will only store a string name. Morphism will store a name as well, but also a reference to the domain and codomain objects. Morphism will also store a list components of instances of Morphism, which will initially be equal to [self]. Morphism will have a method compose() which will take a Morphism as an argument and will return the morphism resulting from the composition of self and the argument, in this order, if the two morphisms are composabable (self has the domain equal to the codomain of the argument). This new morphism will store references to the morphisms it was obtained from in components. This functionality will be generalised for morphisms which are already composites of other morphisms. Morphism will also have a method flatten() which will discard the information about compositions and will store [self] in components.

Next I will define Category to contain an instance of Class which will represent the class of objects in the category. Category will have a method morphisms() which will return the set of morphisms between two objects belonging to the category. I will also define the method all_morphisms() which should return the class of all morphisms of this category and will initially have it throw a NotImplementedError. Note that it should not be required to actually generate all morphisms of a category to construct the class of all morphisms; I intend to only have a number of criteria which will allow checking whether a morphism belongs to a Category or not. Category will also have a string field holding a name.

The next class is Diagram, which will contain a collection of objects of a category and the corresponding morphisms. In practise, diagrams are often used to represent implications of the type "If there are morphisms with such properties, then there also exist morphisms with such properties and the diagram is commutative". To cope with this, I will split the collection of morphisms in Diagram into two parts: one representing condition of the implication and the second part representing the result of the implication. Morphisms will be stored together with their attributes, which will be represented as strings ("unique", "exists", "isomorphism", etc.).

I will enable Category to store a collection of diagrams which are known to be commutative in this certain category and thus represent the properties of this category. For convenience, the user will be able to add a diagram to this collection by invoking the method Category.assert_commutative().

At the end of this phase I expect to have a basic, yet sufficient collection of utilities to represent a wide gamma of category theoretic reasoning limited to a single category.

Drawing Diagrams

In this phase I will focus on graphically representing diagrams. The reason for doing this so early is that visually apprehending a diagram is much easier than understanding the corresponding morphism equalities.

While a diagram can be perceived as a graph, there are a number of specific requirements to their graphical representation (take a look at [3]):

objects are represented as object names rather than points;
diagrams are most often represented in a grid-like layout;
morphisms which are compositions of other morphisms in the diagram are often omitted if they do not carry any useful properties.

I will start by adding the method simplify() to the diagram. This method will omit the morphisms which are compositions of other morphisms shown in the diagram and which do not have any attributes.

I will then add the class DiagramDrawer which will have the methods draw_as_text() and draw_as_image() which will both take a Diagram as an argument. The first one should produce a textual representation of the diagram, while the second one should produce an actual image. Both methods will throw a NotImplementedError in DiagramDrawer. I will then define the class TikZDrawer, which define the draw_as_text() method to produce the TikZ code of the image of the diagram. TikZ is a LaTeX package for creating graphics programmatically [7].

Producing TikZ output offers a number of advantages, among which is that the resulting figure will be easy to include in LaTeX source and scale to the necessary size. Moreover, TikZ output will keep SymPy independent of any external library, while also allowing proper formatting of mathematical text using LaTeX expressions.

Eventually, the class DiagramDrawer may be extended by a different class which will be able to produce a graphical representation of a diagram in a separate window, just like Plot does currently. In the meantime, it should be possible to achieve a similar effect by wrapping the TikZ code from TikZDrawer into a valid LaTeX skeleton code, render it to PDF and show the result.

I will now present the idea of how to draw a commutative diagram. As I have already remarked, due to the specificity of the task, general algorithms are not applicable (at least not that readily). Remember that, in the end, we would like to see the diagram drawn in a grid-like layout. Another important remark is that we assume that the diagram is commutative.

Quite naturally, the process of representing a commutative diagram graphically splits into two stages: the analysis stage, at which the structure of the diagram is analysed and general decisions are taken, and the drawing stage, which consists in actually producing text and arrows. The analysis stage will be implemented as a set of methods in the class DiagramAnalyzer. This class will include the method draw() which will perform analysis of the supplied diagram and will use an instance of a class derived from DiagramDrawingBackend to actually do the drawing. DiagramDrawingBackend will deal with the technicalities of drawing and will expose a number of high-level specialised methods, among which should be draw_morphism() and draw_morphism_curved(), which will draw arced morphism to account for the cases when the morphisms A-(f)->B-(g)->C will get arranged in a line and the a morphism A-(gf)->C will also need to be represented. Note that it will be the responsibility of draw_morphism() to also draw the names of the objects and morphism labels. Classes derived from DiagramDrawingBackend will deal with concrete back-ends; in this project I plan to implement TikZBackend.

Drawing starts with the simplified version of the diagram, as returned by Diagram.simplify(). Then one step of constructing the transitive closure of the underlying directed graph of the diagram is performed. Note that, during the actual drawing phase, the morphisms obtained at this stage will not be represented. After this operation the diagram will consist of two types of structures:

triangles, consisting of triples of objects A, B, C with the corresponding morphisms f:A->B, g:B->C, and gf:A->C;
pairs of objects A and B and the corresponding morphism f:A->B.

The next stage is computing the "length" of morphisms included in the diagram. Consider a morphism f:A->B. If there are morphisms g:A->C and k:C->B, then the length of f is the length of g plus the length of k.

The actual drawing starts with choosing a minimal triangle (with minimal sum of lengths of its sides). This triangle will be drawn as a right-angled triangle. Then, for each side of the triangle, among the list of all triangles which also include this side, choose the minimal and draw it. This process will continue recursively while there are no more undrawn objects which belong to a triangle. When this happens, the remaining pairs of objects A and B will be drawn. For the cases when an object in this pair belongs to an "outer rim" in the already drawn structure (i.e., in at least one of the four directions "up", "left", "down", "right" nothing is yet drawn), the morphism is drawn in one of the free directions. For the remaining pairs, the objects which are yet to be drawn will be arranged in a circle around the already drawn structure.

For each of the yet undrawn morphisms, check if this morphism goes horizontally, vertically, or diagonally (k*pi/4 relatively to the horizon). If so, draw the morphism in an arc; if not, draw it in a straight line.

Note that, except for the last stage of placing objects, when they are arranged in a circle, all objects get placed in a grid. Besides being in agreement with the initial requirement, this will also allow the drawing algorithm to remember where the objects are placed by storing a rectangular array of flags. This array is how the algorithm will know whether an object is on the "outer rim".

At the moment, the behaviour of the drawing algorithm for a wrongly constructed diagram with more than one connected component is undefined. It is easy to check for this problem, however, if this eventually proves necessary.

While the algorithm exposed in this section is definitely unfit for representing general graphs, I expect that, due to the specificity of the underlying graphs of commutative diagrams, it will work well. Note again that a normal size for a commutative diagram is under 20 objects, which will also allow deducing heuristics to further improve the drawing algorithm.

Deciding the Commutativity of Diagrams

In this phase I am going to implement the procedure for deciding whether a diagram is commutative, provided that a certain set of diagrams is commutative. Remember that Category.assert_commutative() is used to explicitly state whether a diagram is commutative in a certain category.

Checking the commutativity of a diagram will be initiated by a call to Diagram.is_commutative() which will take as argument a list of diagrams which are known to be commutative or a Category in which the check should be performed. In the following paragraph I will describe the actual functionality without going into detail as far as splitting the code into functions or methods is concerned. The reason for not doing this is that I consider that how this separation is going to happen is rather obvious.

I will start the presentation of the procedure by remarking the similarity between deciding the commutativity of a diagram and an inference problem in artificial intelligence [9]. Indeed, we start from a number of facts (diagrams known to be commutative) and we need to arrive at a certain goal (whether a certain diagram is commutative). One of the most widely used approaches to practically solving such inference problems (especially for non-zero-order logic) is backward chaining [10]. I will show how backward chaining can be directly adapted to decide the commutativity of a diagram.

Backward chaining is a recursive procedure which starts from a given goal and tries to unify [11] the goal with one of the available predicates. A recursive step can be viewed as consisting of two stages: the pattern matching [12] stage, at which the predicate to unify the goal with is chosen, and the unification stage, at which the unification itself is performed. For every matching predicate and the result of unifying the goal with it, the procedure is repeated (recursively). A parallel can be informally built with the commutativity problem. Take the target diagram as goal and the diagrams commutative known to be commutative, as known predicates (facts, actually). The pattern matching stage consists in finding the diagrams which "fit" into the target diagram. The unification stage consists in adding the "necessary" (see definition of Diagram) morphisms to the target diagram and in marking the resulting "subdiagram" as commutative. The procedure is recursively restarted for any such match and goes on until a branch of recursion "proves" that the whole target diagram is commutative or until all branches end up with a negative result.

I will now give a technically detailed description of the algorithm, structured in blocks, according to the overview in the previous paragraph.

The algorithm starts by constructing the reflexive and transitive closure of the target diagram. On the other hand, it will simplify() each of the diagrams known to be commutative. This will be done with the hope to improve performance.

Recall that a Diagram includes two sets of morphisms, one of which corresponds to the premises of an implication, while the other one represents the result of the implication. The pattern matching stage consists in finding an embedding of the underlying directed graph of the premises of a diagram D_1 known to be commutative into the underlying directed graph of the target diagram. Note that morphisms in a Diagram possess attributes, which will be considered when looking for an embedding. Thus, an embedding of D_1 will only be chosen for unification if all the morphisms in the embedding have exactly the same sets of attributes as the corresponding morphisms in D_1.

The unification stage will consist in adding the morphisms of D_1 which represent the result of the implication to the target diagram and in marking the obtained subdiagram (essentially, a subgraph of the underlying graph of the target diagram) as commutative by annotating each morphism in the subdiagram with the same commutative component ID (number). If the new commutative component has common edges (morphisms) with another commutative component, then these components are merged into one by annotating their edges with the same component ID.

After unification, the procedure continues recursively. If no embeddings were found, a negative result is returned. If at least some of the recursive calls returns a positive result, this result is immediately propagated up the recursion tree. Note that, since unification may add new morphisms, at each new recursive call, one must examine all diagrams known to be commutative anew, regardless of whether either of this diagrams has already been unified with.

Positive result is obtained when the whole diagram is proved to be a single commutative component. This can be verified by checking whether all morphisms have been marked with the same connected component ID. This check will happen at the beginning of each recursive call, right before pattern matching.

Further Benchmarking, Optimisations and Extensions

As I have said in the introductory paragraph, this phase is optional and I will only manage to enter it if I complete the previous stages sufficiently soon. I would like to note, however, that I will continue working on the items enumerated in this section after the end of the Google Summer of Code program.

The following represents a list of things which will receive special attention during this phase (in no particular order):

Benchmarking and optimisation. The algorithms I have described in the previous sections will need to perform rather demanding computations. I expect that performance will be acceptable due to the relatively small sizes of practical commutative diagrams, but this has to be thoroughly verified. While doing the benchmarking, I also expect to collect sufficient understanding of how performance depends on input data in order to develop better heuristics and optimise further optimise the algorithms.
Showing resulting embeddings. I suppose that it will be useful to actually see the embeddings which led to deciding that a diagram is commutative. This should be rather easy to implement.
Rendering the diagrams. This will be implemented by wrapping the TikZ output from TikZDrawer into skeleton LaTeX code, rendering the code and popping a PDF viewer window with the rendered diagram.
Integration with implementations of group theory. In this summer I expect to see group theory implemented in SymPy. It would be very illustrative to actually integrate this implementation with the classes described in section Class Hierarchy. Moreover, it may provide some very useful practical insight which may contribute to certain modifications of the class hierarchy I plan to implement initially.
Non-technical documentation. While I absolutely will write rather detailed docstrings for anything I will implement, separate user-friendly and non-technical documentation with a proper outline is always better, and this is what I am going to provide.

Deliverables

The following list summarises the results I plan on obtaining by the end of summer:

a basic class hierarchy for representing category theoretical reasoning within a single category,
functionality to graphically represent commutative diagrams, and
functionality to automatically check for commutativity of a diagram starting from a set of diagrams known to be commutative.

Why I Fit

I have been rather intensively studying category theory for about 6 months already (with a slight interruption in the latest month). I have olympiad experience with solving problems on graphs and I have read [13]. I do have what I consider solid (but not exhaustive) experience with Prolog and I have coauthored a paper on doing forward and backward chaining with P systems (a biologically-inspired computational device) [14]. I believe this makes me well-equipped for solving the problems I have posed in this proposal.

Time Distribution

Before the start of the coding period, I will have to spend quite a lot of time on university matters, which leaves about 2-3 hours per day for SymPy. In this time I plan to rebase https://github.com/sympy/sympy/pull/563 , as well as to work on http://code.google.com/p/sympy/issues/detail?id=2528 I will also continue studying [2]. Further, I will throw a look at how different graph packages draw graphs (for example, I will scan the code of the functions listed in [15]).

The schedule of the summer exam session has not yet been firmly established at my university; it is absolutely certain, however, that I will have finished all my exams by June 1st. While I expect to have finished earlier than that, I will plan my activities starting with this date.

During the period before mid-term evaluations, I plan to be fully dedicated to the project, which amounts to not less than 7 hours on average, every day (including the weekend). After the mid-term evaluations, closer to the end of July, I may leave for a week of vacation. Aside from that, I am going to spend the same amount of time (7 hours every day) working on the project.

The following is an approximate timeline of my activities at week scale:

June 1 - June 3: start creating the class hierarchy, write some basic test suites;
June 4 - June 10: finalise the classes started the previous week and extend the test suites;
June 11 - June 17: implement Diagram.simplify() and create the skeletons of classes pertaining to drawing the diagrams; write the test suites;
June 18 - June 24: implement TikZDrawingBackend;
June 25 - July 1: implement the core of the drawing functionality;
July 2 - July 8: finalise the drawing functionality; improve the heuristics;
July 9 - July 15: write the tests for the procedure of deciding the commutativity of a diagram; implement the pattern matching stage; start working on unification;
July 16 - July 22: implement unification;
July 23 - July 29: polish and finalise the code; start doing benchmarks and improving the heuristics;
July 30 - August 5: write non-technical documentation; implement showing the embeddings which resulted in deciding that a certain diagram is commutative;
July 6 - August 12: integrate the (already done) implementation of group theory with the category theoretic classes;
August 13 - August 19: sort out the remaining issues; start working on a direction enumerated in the next section.

Note that, while I do not explicitly remark this in the timeline, I expect to be pushing the changes upstream as soon as I have bits of functionality which I am confident in. This will hopefully keep the burden of reviewing the changes low.

After the end of GSoC-2012 I plan to finish the tasks listed in the fourth stage of the implementation, but also work on other problems listed in the following section.

Perspectives

While the amount of work I plan for in this project is rather big, it will only lay the foundations of a proper implementation of category theory in SymPy. Among the things which should eventually be implemented are the following (in no particular order):

Functors [5]. Category theory is said to have three notions at its foundation: category, functor, and natural transformation (functor morphism). Implementation of only one of these three notions is planned in this project. Implementing the other two will make the category theory module considerably more suited for much a larger class of practical problems.
Better diagram drawing. I do not expect to arrive at absolutely flawless drawing functionality at the end this summer. There is yet a lot of experience to be gathered by solving practical drawing problems and understanding the specificity of the underlying graphs of commutative diagrams which influence the ways of representing them graphically.
Complex attributes in diagrams. It may turn out that simple string attributes for morphisms in commutative diagrams will not suffice for some particular cases. This will require introducing more complex attributes which will certainly influence the course of deciding the commutativity of a diagrams.
Direct verification of commutativity. Should the user have a concrete category with sufficiently detailed information about the structure of objects, it should be useful to be able to check the commutativity of the diagram directly, by symbolically computing the mappings of elements along paths in the diagram.
Diagram chasing. Directly verifying the commutativity of a diagram as described in the previous item is only possible when all the morphisms in the diagram are exactly known. This only covers a rather small subset of situations, which is why it would be very useful to eventually implement diagram chasing. [16] may be helpful in achieving this goal.