DASHBOARD: equivalence classes in implication matrix image

[harahu]

Is your feature request related to a problem? Please describe.
Looking at the red and blue colored image on the dashboard page, I see a lot of repeating patterns that I think are the result of the members of large equivalence classes being spread out row and column wise. While satisfying to look at, I fear that this tartan-like pattern is hiding more interesting and fundamental details.

Describe the solution you'd like
Perhaps subtler details of greater value will emerge if the image rows and columns are sorted by equivalence class, such that an equivalence class will make up a single continuous block in the image. Or, to lend less weight to large equivalence classes, one could grant only one row/col to any known equivalence class.

[vlad902]

Assuming equivalence classes are collapsed, what should the left-right/top-down sorting be? Should it still just be the numeric identifier of the equation? Is there some other 'more natural' sorting? That seems like it may contribute to whether you can 'see' a pattern or not, but perhaps it would stand out regardless.

[harahu]

Good question. There might not be a single correct group ordering. Different orderings might yield different insights. That said, I have some ideas. I think it could make sense to order the groups by the number of implications by each group. One would then have some similarity with the Grahiti graphs, having the Equation 2 equivalence group at the bottom and the Equation 1 group at the top.

If there are other ideas for ordering, I think the best way to determine what gets to occupy the dashboard is to just generate images for all of them and compare them.

[harahu]

I went ahead and wrote some shitty code along the lines described above. Below are my results:

First, for clarity, this is what I had in mind, sans the collapsing of equivalence classes:

The big blue block at the bottom of the picture shows the Equation 2 equivalence class, implying all other equations. The row at the top of the image are the implications of Equation 1, so only itself. In between the equations are ordered first by equivalence class, then by number of implications of the group.

Now, collapsing the equivalence classes, we get:

I realize that I like that the first one informs you on how big the classes are.

[teorth]

I like the first plot, it contains several visible features that one can then point to and annotate, such as the one you mentioned that "The equation2 equivalence class implies everything". Ultimately the choice of what image to use should be guided by aesthetic and pedagogical considerations rather than mathematical ones - one wants an image that actually conveys information to a human viewer (in contrast to images such as QR codes which are designed to convey information to machine viewers).

[harahu]

[...] one wants an image that actually conveys information to a human viewer (in contrast to images such as QR codes which are designed to convey information to machine viewers).

Fully onboard with this. It's just a question about which information one wants to convey. I can see these kinds of pictures being useful for two distinct purposes:

• Conveying the progress of the project.
• Conveying some form of mathematical intuition about the equation and implication set.

My hunch at the moment is that the first proposal is better suited for both, but I'm not a mathematician, so I won't pretend I'm the best judge of this. So, do let me know whether there's variations on grouping and ordering of equations you think could be useful: I could try to render them.

Some other observations of mine from the first picture:

• The rectangles stringed along the diagonal represent the mutual implications internal to the various equivalence classes, with the side length representing the size of the class.
• It seems like the only times we get blue color on the upper right side of the diagonal is as part of these rectangles on the diagonal. Hence, the few open problems beyond the diagonal could represent (relatively) low hanging fruit.
• There's still a handful of open questions touching the diagonal. I think settling these problems would finalize the equivalence classes.

These are probably trivial observations, but I found them interesting.