Graphiti

Stream: Equational

[Vlad Tsyrklevich]

OK, Graphiti v1 is here: https://tsyrklevi.ch/graphiti/ (the old link redirects) Give it a test and see what forms of filtering or visualization you might find useful for a graph explorer like this. Right now, clicking on a node in the graph takes you to the equation explorer, if it's an equivalence class, the one with the lowest number. I'd like to make the links instead be on the (123) number, i just haven't managed to get that working yet

[Terence Tao]

Vlad Tsyrklevich said:

OK, Graphiti v1 is here: https://tsyrklevi.ch/graphiti/ (the old link redirects) Give it a test and see what forms of filtering or visualization you might find useful for a graph explorer like this. Right now, clicking on a node in the graph takes you to the equation explorer, if it's an equivalence class, the one with the lowest number. I'd like to make the links instead be on the (123) number, i just haven't managed to get that working yet

Nice! Do you plan to host it externally for the duration of the project, or do you want to have it an internal component of the repository? Either would be fine with me, and the README.md can be updated accordingly.

One suggestion: instead of having the example queries go directly to the graph, have the example queries auto-populate the text boxes so that, when the submit button is pressed, the correct graph is reached. This would serve as a sort of "tutorial" on how to use the text box options.

[Vlad Tsyrklevich]

Terence Tao said:

Vlad Tsyrklevich said:

OK, Graphiti v1 is here: https://tsyrklevi.ch/graphiti/ (the old link redirects) Give it a test and see what forms of filtering or visualization you might find useful for a graph explorer like this. Right now, clicking on a node in the graph takes you to the equation explorer, if it's an equivalence class, the one with the lowest number. I'd like to make the links instead be on the (123) number, i just haven't managed to get that working yet

Nice! Do you plan to host it externally for the duration of the project, or do you want to have it an internal component of the repository? Either would be fine with me, and the README.md can be updated accordingly.

One suggestion: instead of having the example queries go directly to the graph, have the example queries auto-populate the text boxes so that, when the submit button is pressed, the correct graph is reached. This would serve as a sort of "tutorial" on how to use the text box options.

I figured I would put it in the repo once it's ready, but for now there may be feedback and using my own hosting is faster turn-around for testing (+ figuring out CI and all that will also take a bit of work). Good idea on populating the fields.

[Vlad Tsyrklevich]

I figured eventually the equation viewer could also link back to it, or even embed it in an iframe or something like that. Ah and that reminds me, one immediate improvement is to make links open in a new tab instead of redirecting so that the graph doesn't go away

[Nicholas Carlini]

(I found it useful to do the same thing and host for a day or two to get comments and improve quickly and then push. Doing CI was less work than I thought. You can look at my PR which just added it for the equations list)

[Vlad Tsyrklevich]

Yup, I'm copying your approach, and haven't looked at CI yet, but was planning to crib your work there as well

[Vlad Tsyrklevich]

I looked briefly at it to see if I should use the same graph implementation but it looks like we had different enough uses/purposes for it not to make sense

[Nicholas Carlini]

I'm going to hopefully rewrite the equation one to just use the sparse graph of direct implications and remove anything that can be derived. In principle this should shrink things quite a lot and make the page more responsive

[Vlad Tsyrklevich]

That's what I do, I'm just using the closure of the condensed graph and not even doing fancy encoding, just JSON, and it's fast.

[Nicholas Carlini]

Yeah. Makes sense. Back in the "old" days when I started the page the graph wasn't complete enough where doing that saved much (maybe 2x?), now it makes a lot more sense

[Vlad Tsyrklevich]

One idea I haven't figured out, is what may be an interesting graph to show by default on the equation viewer page. The implies/implied_by may be too large to be practical, but maybe something like "Show implies/implied_by up to 2 steps in the transitive reduction"? I don't know if that's actually useful though

[Vlad Tsyrklevich]

OK I've implemented my remaining TODO items and v2 is up: https://tsyrklevi.ch/graphiti/?1 Note that I did not figure out an easy way to make the (XYZ) equation numbers links, I'm going to leave vertex links the way they are. I didn't get any feedback on new features, so assuming there's no further feedback I'll get started on upstreaming it.

Note that the last example query is something I actually used yesterday to verify my lowest common ancestor implementation, so that's nice to have found an immediate use for the tool.

[Vlad Tsyrklevich]

I suppose one idea is that right now combining different fields is an implicit AND. If you wanted to see everything EqX implies or is implied_by, you'd want an OR query instead, but I'm not sure if anyone actually cares to make that particular query, so better to see if anyone can think of specific uses they want

[Vlad Tsyrklevich]

https://github.com/teorth/equational_theories/pull/401

[Vlad Tsyrklevich]

@Nicholas Carlini https://github.com/teorth/equational_theories/pull/404 Let me know if you have any feedback, and if you're happy with it I'll take it out of draft

[Vlad Tsyrklevich]

equational#440 implements the capability discussed in https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Equation.2065.20-.3E.20left.20cancellability/near/475352370 to graph unknowns+conjectures from the equation explorer, modulo collapsing unknowns+conjectures because that was the easiest data for me to read (plus, this probably makes the interface a bit simpler without much loss in information.)

[Terence Tao]

It seems that some of the implication arrows are still downward, e.g., https://teorth.github.io/equational_theories/graphiti/?render=true&implies=73,99,125,203,229,255,4380,4435&highlight_red=73&highlight_blue=99,125,203,229,255,4380,4435&show_unknowns_conjectures=on is oriented somewhat weirdly (125 implies 73 and 229).

[Vlad Tsyrklevich]

Hmm, yes it's the 'unknown' edges changing the final layout decisions. Taking a look locally to see if there is an easy way to force graphviz to do what I want (essentially lay it out without any input from the unknown edges)

[Vlad Tsyrklevich]

I can do it, though it makes it harder to interpret anyway in this case (note I've added back arrowheads for implication edges)
graph.png

[Vlad Tsyrklevich]

Supressing arrowheads for implication edges makes it a little visually clearer what is what
graph.png

[Vlad Tsyrklevich]

equational#508

[Vlad Tsyrklevich]

Ran into something annoying today, I realized in simple graphs that should be highly symmetric due to duality (e.g. this example of equations of just 1 variable) graphiti would lay out them quite poorly, red is self-dual and blue is one of the set of duals.
graph.png

[Vlad Tsyrklevich]

I could force them into being more dual-symmetric, but it makes the graph hard to interpret (and also violates Hasse convention to boot)
graph (1).png

[Vlad Tsyrklevich]

The best I got was something like this
graph (2).png
Overall fairly disappointing for showing something so highly symmetric

[Vlad Tsyrklevich]

equational#637 has the changes to marginally improve dual symmetry and also adds a checkbox to collapse duals into equivalence classes--something i was playing around with when trying to look at large graphs.

[Daniel Weber]

How hard would it be to add an option to highlight "terminal" laws, laws which aren't implied by anything? (the other direction could also be interesting, laws which don't imply anything)

[Alex Meiburg]

Do you mean, anything except equations 1 and 2? Those are the unique initial and terminal objects here. (Is there a word for this object in posets/categories, like "maximally non-terminal" or similar?)

[Daniel Weber]

You can limit the equations rendered, and then it can be different from 1 and 2

[Daniel Weber]

I believe those are called atoms and coatoms, if I understood you correctly

[Vlad Tsyrklevich]

It should definitely be doable, I usually "manually" do this by providing the target equation as a highlighted point from the equation explorer links--I assume you're manually generating these graphs, right? Perhaps instead of manually doing it I should have two colors that specifically mean no-forward-implications/no-backwards-implications and always highlight those.

[Vlad Tsyrklevich]

Ah I see from the PRs that you are generating links from FME, and these lists may be quite large and it's hard to see the terminals there.

[Vlad Tsyrklevich]

equational#776 adds seeing 'neighborhoods' of a given law, e.g. you can specify a given number of edges to look in both implies/implied by direction.

[Vlad Tsyrklevich]

cc @Harald Husum this should address https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Equation.20Explorer.20Enhancements/near/478017126

[Vlad Tsyrklevich]

Examples:
1 edge away from 43
2 edges away from 43
all reachable from 43

[Amir Livne Bar-on]

Very nice!

Another feature request (or more of a question since I don't know if it would be useful): how do you feel about a mode where each node is a small box? With a single number, or even an empty circle. And the equations data would show on a popup when hovering

[Vlad Tsyrklevich]

To understand: Is the use case just to make it easier to see the graph shape without the equivalence class/equations cluttering the graph? Or is there something else that also gives?

[Amir Livne Bar-on]

Only that more of it would fit on the screen, and maybe it will also make it easier for graphviz to figure out a nice layout

[Vlad Tsyrklevich]

Example run here. Doesn't look bad! The symmetry above 43 is much better represented.

[Amir Livne Bar-on]

I just checked locally and graphviz connects the exact same vertices in the exact same way. But it's still less cluttered as edges have more space to spread around.

[Vlad Tsyrklevich]

I can also manually compress the graph visually a bit. It's busier but maybe nice if you have lots vertices. Looking at the entire graph is still a mess though.

[Amir Livne Bar-on]

We have large anti-chains so it must be a lot wider than it is tall. And unless by some miracle it's close to being planar, there won't be a nice way to render.

[Amir Livne Bar-on]

Another feature idea from a friend - make nodes wider if it helps the layout, especially terminal nodes. This will allow edges to be vertical and much less messy. I don't know if it's possible to do without implementing a layout engine from scratch though.

[Vlad Tsyrklevich]

Ah, I hadn't thought of that! That's a really cool idea-- I'll give a think if that's implementable somehow within how Graphiti works.

[Harald Husum]

Great work, @Vlad Tsyrklevich ! I will definitely make use of this feature. Really appreciate you implementing it. :thank_you:

[Michael Bucko]

Harald Husum schrieb:

Great work, Vlad Tsyrklevich ! I will definitely make use of this feature. Really appreciate you implementing it. :thank_you:

Love it too!