This week I have been working both on fixing some existing code (including diagram layout) and on better understanding the code that I am going to write next. As far as the fixes are concerned, I have further polished the diagram layout code, including the addition of some pretty printing for DiagramGrid. I didn’t initially expect pretty printing to be useful for this class; however, it turned out that being able to quickly glance at the grid itself was very helpful in certain situations.
Something which makes me very content is that I have finally submitted a fix for the sort key problem for unordered collections. The essence of the problem is as follows. With hash randomisation enabled, the order of Basic.args changes on every run. On the other hand, Basic.sort_key traverses the arguments in the order in which they are stored; therefore, sort keys are dependent on the actual order of the arguments. This has given me trouble when working on laying out diagrams, specifically, in handling groups. The thing is that the group handling code relies on FiniteSet (this maybe isn’t the best idea, but that’s a different story, really ): groups are eventually converted to FiniteSet‘s of FiniteSet‘s. To assure stable output, the collection of FiniteSet‘s is sorted. However, due to the influence of hash randomisation on sort keys, this sorting would not actually produce the desired consequences. There was a similar problem in the same block of functionality which had to do with sorting Diagram‘s; the issue there was that a Diagram stores Dict‘s which, being unordered collections, were subject to the same sort key trouble. Pull request #1446 fixes all of these issues and, finally, the diagram drawing code almost always passes all of its tests.
It is worth mentioning that while the fix for the sort key problem was not included in the #1429, I was inclined to classify all problems as related to FiniteSet.sort_key. With the fix in the branch, it turned out that there were some other subtle sorting issues, which I am still fixing.
I have also sent pull request #1440 which fixes the pretty printing of morphisms and diagrams, introduced by myself in #1338. Initially, I would use short Unicode arrows for pretty printing morphisms, but Tom and I have arrived at the conclusion that these arrows look too condensed. I have then chosen to use long Unicode arrows; it turned out however that Unicode characters which span more than one symbol are not rendered consistently across different machines. On my computer, the longer arrow would overlap with the next character in line; on Tom’s, it would not. Aaron has suggested building up arrows out of em dashes and black right-pointing triangles, and this seems to work better, although it still looks ugly with some fonts (e.g., the default font in rxvt-unicode, as reported by Tom).
I have also promised to implement variable-length horizontal arrows. I have decided to postpone this for now, however, in order to better focus on my GSoC project. I will keep that task in mind, however, and will most probably return to it in a couple of days.
As for deciding the commutativity of diagrams, I have run into an unexpected conceptual problem, arising from the fundamental difference between diagrams with conclusions and without conclusions. Before explaining the problem, I will remind the description of these two types of constructions. A commutative diagram is a collection of morphisms (which usually form a connected directed graph) with the property that composing all morphisms along any two paths between any two objects produces the same composite morphism. While being quite general, in category theory it is customary to produce statements like “if there are such morphisms, there exist such morphisms, and the diagram is commutative”. This statement is clearly an implication. The class Diagram is a representation of the second type of statement and contains sets of premise morphisms and conclusion morphisms. Diagram is also conventionally capable of representing simple commutativity if no conclusions are specified.
While I was initially quite comfortable with using Diagram for both types of statements, I am really inclined to considering the creation of two separate classes now. Thus I plan to rename Diagram to Implication and add a different Diagram which will represent what I used to call “commutative diagram without conclusions”. That is, Diagram will hold only one collection of morphisms.
With this separation, it is immediately clear that, in the context of my model, the question “Is this diagram commutative?” actually incorporates two totally different questions:
- Is this Diagram commutative?
- Is this Implication true and commutative?
Fortunately for me ( ), this newly-discovered separation does not remove the possibility of answering both questions with almost the same algorithm. I will start with question (1) to further stress the difference between the semantics of diagrams and implications.
Consider a collection of Diagram‘s and Implication‘s known to be commutative. (By saying “an Implication is commutative” I will abuse the terminology and mean “an Implication is true and commutative.”) We need to decide whether the target Diagram is commutative. The algorithm I will describe is based on backward chaining and is therefore recursive. A recursive step consists of two stages: the commutativity stage and the inference stage. The goal of the commutativity stage is to decide whether the current version of the target Diagram is commutative; the goal of the inference stage is to see whether applying one of the Implication‘s will make the target Diagram commutative.
The commutativity stage starts with taking every morphism of the target Diagram and putting each of them into its own commutative subdiagram. Now, for each commutative subdiagram, the algorithm will pick a subset of morphisms and will then put the subsets together to form another subdiagram. This subdiagram will then be compared with each of the Diagram‘s known to be commutative. If a match is found, the subdiagram is added to the set of commutative subdiagrams. Then, all possible “absorptions” among the diagrams are performed (i.e., if subdiagram is a subdiagram of , the subdiagram is removed from the collection of subdiagrams (for obvious reasons)) and the iteration returns to its start, where it picks subsets of the new subdiagrams. Since the number of morphisms in the diagram is finite, this process is finite. If, in the end, the collection of commutative subdiagrams contains only the target diagram, it is deemed commutative.
Note that this alrogithm is very similar to one of the methods of finding all prime implicants of a boolean function (we called that Blake-Poretski algorithm at the university, but I cannot find any references on my Internet). I have considered the possibilities of directly converting the commutativity stage to a boolean function minimisation problem, but I haven’t found a sufficiently elegant way yet.
The inference stage exactly follows the idea of backward chaining. For each Implication an attempt is made to find the embedding of the premises into the target Diagram. If such an embedding is found, the corresponding conclusions are added to a copy of the target Diagram and a recursive examination of the modified Diagram is made. The found embedding of one of the Implication‘s plus the added conclusions are propagated down the recursion tree as commutative subdiagrams. The commutative stages of the following recursive calls will take their commutativity for granted.
If one of these recursive calls returns a positive result, this positive result is propagated up the call stack. If neither of the recursive calls returned a positive result, or if no embedding of an Implication has been found in a certain recursive call, a negative result is returned from this recursive call.
Note that it actually was the inference stage that I described in my original GSoC proposal.
Before showing how to answer question (2), I would like to analyse the algorithm idea I have just presented a little bit. One can see that the commutativity and inference stages are very different; so different, in fact, that they are almost independent. Therefore, these two bits of functionality will live in separate pieces of code, and will be later combined to function together. I will start by defining two internal classes, _CommutativityStage and _InferenceStage which will host the corresponding functions. The code that will actually combine the two will either be a global function or a class; this will be clearer later and is not important at the moment.
Question (2) now: “Is the given Implication true (and commutative)?”. In this case, one should start from the premises of the given Implication and apply the same strategy as in answering question (1). Here, however, the terminal criterion is that the target Diagram (obtained from the premises of the original Implication) is commutative and contains the conclusions of the original Implication.
A remark about comparing diagrams is due here: this is nothing but the subgraph isomorphism problem. I have already found this paper (haven’t read it yet), but I’m open to other paper suggestions in this regard
EDIT: I have decided to not follow this article and instead focus on a more basic solution. Should the need occur, I will implement this (apparently) more efficient version.
It is necessary to keep in mind that, besides finding the subgraph isomporphism proper, the code will have to pay attention to morphism properties as well.
Now, the most attentive readers might have already remarked that semantically splitting the class Diagram into two will impact diagram drawing. Yet, the impact will be rather modest, since the drawing code already knows how to deal with something similar to Implication; adding explicit support for new Diagram is going to require minimal effort.
In this blog post, I recognize that my initial class model was flawed in yet another place. I try to see this is as a sign of personal progress, though