Equation Explorer Enhancements

Stream: Equational

[Joe McCann]

Opened PR: https://github.com/teorth/equational_theories/pull/625 to perform the following enhancements to the equation explorer

1. Allow you to search by equation number
2. Download the explorer table as a CSV

If there are any other code / infra improvements I'd love to take them on, as I feel thats where I will be able to add the most value

[Joe McCann]

Feel free to discuss this / any other enhancements

[Terence Tao]

Thanks! I see you also suggested being able to download the entire implication graph as a CSV. That's like a 50MB file or something, but if that's doable I think it's a good idea. I've opened equational#626 for this.

[Joe McCann]

Yerrrrrrr, I'll see if I can get that working

[Terence Tao]

By the way the jump to equation number doesn't seem to work in the live version, any number gets sent to https://teorth.github.io/equational_theories/implications/?0

[Joe McCann]

thanks for the find, Ill see if I can diagnose

[Joe McCann]

I was able to determine the bug. Will push a fix when I address, for now it at least has not impacted any prior functionality, so I will try to push with the download implication graph as a CSV

[Zoltan A. Kocsis (Z.A.K.)]

This is a sweet QoL enhancement!

In the long run, I'd like to see:

1. the Filter feature from Finite Magma Explorer ported to the Equation Explorer. It really helps with exploration, and since externals are starting to analyze the data, now feels like the right moment. Too bad I don't have the time to work on it :(
2. a background worker to speed up the initial loading times and not freeze the whole page while it loads.

So if you're looking for further dev work to do shortly @Joe McCann I think implementing any of these would be really useful.

filter-by-number.png
filter-by-pattern.png

[Amir Livne Bar-on]

About page load time - I looked at the profiler, and it looks like the time is spent in mapThroughLUT, isImplies and isAntiImplies. Probably if we didn't convert back from IDs to strings it would go faster. We can index into an array to get at the properties of each ID. (or define the IDs to have the properties we want as bit-fields if we want to be fancy about it)

[Joe McCann]

Raised PR: https://github.com/teorth/equational_theories/pull/628 so now we can download the full raw implication table from the equation explorer. This includes a download popup so that we can have the psychological effect of distractions making it feel shorter lmao

I also provided a bugfix for the searching by int which should work. @Zoltan A. Kocsis (Z.A.K.) I can work on adding the filter feature in. Do you think filtering in the search bar would be the best way to integrate the two?

Also hopefully theres no more bugs cause it is sleep time on the east coast haha, see y'all in the morn :sweat_smile:

[Vlad Tsyrklevich]

The biggest speed improvement we can make is not using the output of lake exe extract_implications outcomes and instead using the condensed graph representation that graphiti does. It's only ~20k edges for implications (for the closure), and probably not too much more for the non-implications. This means we lose the ability to differentiate explicit/implicit but no one uses that anyway (or so I think).

[Vlad Tsyrklevich]

Slightly more simply, I think a huge portion of time is spent in calculateStats due to it doing the 4694**2 loop to calculate the stats. Optimizing that shouldn't be too hard (e.g. compute by equivalence class, pre-compute it, etc.)

[Vlad Tsyrklevich]

I haven't had time to think about it due to being busy, but I think there's very low hanging fruit there.

[Vlad Tsyrklevich]

(Deleted)

[Zoltan A. Kocsis (Z.A.K.)]

Do you think filtering in the search bar would be the best way to integrate the two?

Yeah, I think this would be the best way to do it (you can load up the FME with multiplication table 0 to see how it works there).

[Zoltan A. Kocsis (Z.A.K.)]

Optimizing that shouldn't be too hard (e.g. compute by equivalence class, pre-compute it, etc.)

Is there any reason not to have CI pre-compute at least the main equation table? A CI that takes 5 seconds longer, in exchange for 5 seconds less each time somebody visits the Equation Explorer, seems totally worth it.

[Vlad Tsyrklevich]

There are forms of filtering that can change those numbers (e.g. does conjecture count as unknown?) hence why it's computed online now I think. But no, there is no reason not to precompute it given the lag. I just haven't had the time to implement the better solution of using condensed representations that would simplify the problem and not require the caching.

[Vlad Tsyrklevich]

Basically we could make that loop 10 or 40 [(4694/1450)^2 or (4694/725)^2] times faster depending on how we process the graph, but perfect shouldn't be the enemy of good.

[Eric Taucher]

Joe McCann said:

If there are any other code / infra improvements I'd love to take them on

While static displays such as with GraphViz are nice, I find Cytoscape.js offers more features to deal with large graphs, interaction with the graph, making selections, etc.
Note: Cytoscape and Cytoscape.js are different code bases, they are similar tools but search engines often don't make the distinction with results.

A downside is that if one wants to store the data in a JSON file then a web server is needed to avoid CORS errors when retrieving. I do find that using AI such as ChatGPT to help write the JavaScript, HTML, CSS, and JSON for such a project is often helpful, but not always accurate the first time but quite often able to get to working code correctly with some error messages given to the AI.

I have also been working on this myself but the large data, 50 M, or more with possible multiple files is something I have not done with Cytoscape.js which is pushing me to learn more about the technology and if it can be effectively done.

If you are curious and have questions, please ask.

[Vlad Tsyrklevich]

@Eric Taucher You shouldn't need 50mb of data, check out the data graphiti exports. It's pretty tiny, and I use an even smaller portion of it (I export the closure of the condensed graph, but in graphiti itself I compute the reduction due to reasons of how graphiti works.)

[Vlad Tsyrklevich]

Technically d3-graphviz also allows interactivity, I just didn't implement it due to limited time and at least for drawing the full graph it was already pushing the limits of what it can handle. I do believe though that other technologies might be useful. In particular I looked at maybe using cytoscape's dagre layout but it couldn't handle the full (condensed-reduced) graph

[Vlad Tsyrklevich]

(Also for the CORS errors, one can just use e.g. python -m http.server 8000 --directory home_page/graphiti to launch a web server and get around them but perhaps you have already figured that out)

[Eric Taucher]

Vlad Tsyrklevich said:

(Also for the CORS errors, one can just use e.g. python -m http.server 8000 --directory home_page/graphiti to launch a web server and get around them but perhaps you have already figured that out)

Yes, thanks.

Cytoscape.js can be used in a single HTML page without a server if all the data is included within it. This requires generating a static HTML page containing the HTML, CSS, JSON, and JavaScript whenever an update to the graph data is detected.

The reason for exploring the use of external JSON files was to allow the pages to update automatically based on graph data being generated and stored in a repository as the project progresses.

I typically use Cytoscape.js with Prolog and run a server using SWI-Prolog (reference). As you noted, I have also used other simple servers to host such pages dynamically.

The final goal is to include a single HTML page in the GitHub repository so that a user who wants to experiment with the graph would not need to understand how to set up a web server or install additional software, and thus this would not require the maintenance of a web server after the project is done. :blush:

[Vlad Tsyrklevich]

just an FYI if you weren't aware: there is a github workflow action that re-generates data on commits, so if you were to integrate your tool upstream you'd get this for free, e.g. graphiti/equation explorer do this for the data they consume. And GitHub also provides free hosting, e.g. the dashboard/equation explorer/graphiti all run for free

[Eric Taucher]

Vlad Tsyrklevich said:

there is a github workflow action that re-generates data on commits

Thank you.

I did not know this and will definitely take a look.

[Vlad Tsyrklevich]

.github/workflows/blueprint.yml

[Terence Tao]

By the way, even if the implicit/explicit distinction is not currently utilized in Equation Explorer, I think it could potentially do so in the future, e.g., through equational#343.

[Vlad Tsyrklevich]

I think that tool probably makes more sense outside of equation explorer (though I'm not particularly qualified to comment on what such a tool requires)

[Jose Brox]

It would also be nice to be able to:
1) Search by equation name: Astérix, Obélix, Dupont, Dupond, Ramanujan, Hardy, Littlewood...
2) Filter by properties, like Austin law, or properties with respect to the implication graph.

[Terence Tao]

I guess a text search of the commentary files could be triggered if the search box input does not parse as a number or an equation. Also a minor thing: pressing “enter” in the search box does not currently trigger search.

[Harald Husum]

As an amateur trying to grasp the landscape of equational laws, one question that I often end up pondering is: What could a law that is slightly weaker or slightly stronger than some other law look like? This questions is essentially a generalization of the MathOverflow question question that provided some of the background for the project.

I'd love to somehow use Equation Explorer to identify equations that "as directly as possible" implies, or are implied by, an equation. By "directly" I mean that there are no (as of yet identified) equivalence classes between the equations in the implication graph. I realize that this "directness" is an artifact of the set of laws the project considers. If we were to expand the set to e.g. laws using five operations, we'd get different results. Still, I feel like this way of navigating the graph is interesting and useful in an orthogonal way to what can be done in EE today.

Perhaps better suited in another thread, but I realize this goes for Graphiti as well. Being able to filter the visualized graph by only drawing laws that are within a certain number of implication steps away from some origin would be nice.

[Daniel Weber]

As the proofs are transitively reduced, a good approximation of this is using the "Show only explicit proofs" option

[Vlad Tsyrklevich]

Harald Husum said:

Perhaps better suited in another thread, but I realize this goes for Graphiti as well. Being able to filter the visualized graph by only drawing laws that are within a certain number of implication steps away from some origin would be nice.

Yeah I've thought about this, it shouldn't be too hard to only display vertices a given depth away from some vertex, it just starts to get hard sometimes to make different search options compose well with these more complicated query forms. Not to say that they shouldn't be implemented though, that's just what's stopped me from doing it so far.

[Vlad Tsyrklevich]

Daniel Weber said:

As the proofs are transitively reduced, a good approximation of this is using the "Show only explicit proofs" option

I would be curious how that feature works with the duality support in the closure code actually. (Also while implications are mostly reduced, there are still some theorems outside of the reduction in the repo.)

[Vlad Tsyrklevich]

But this question fundamentally seems to be asking a question you could answer by visualizing one forward/backward edge away in graphiti, so perhaps that's the right tool for the job instead of adding yet another mode to EE.

[Harald Husum]

As you point out, Graphiti is also well suited to cater to this need. Perhaps better suited. As long as I have a tool to reach for, I don't particularly mind which one it is.

[Vlad Tsyrklevich]

Vlad Tsyrklevich said:

Basically we could make that loop 10 or 40 [(4694/1450)^2 or (4694/725)^2] times faster depending on how we process the graph, but perfect shouldn't be the enemy of good.

still slow, but better https://github.com/teorth/equational_theories/pull/705 Caching would help, but now loading the raw data is starting to be ~half the load time so there's less benefit

[Vlad Tsyrklevich]

Deleting the 'Try this' links improves equation page load times another ~360ms. I don't think they're worth noticeable delay, but I'll let others decide. It's also possible that there's a better way of rendering them, but I don't know much about web optimization

[Terence Tao]

Maybe we could disable "try this" by default, and then load them if a relevant checkbox is enabled?