Some more implication visualizations

Stream: Equational

[Vlad Tsyrklevich]

The whole graph looks pretty similar to the last I produced one (here), but I just added some options to filter by number of variables and number of operations to see if the smaller graphs were interesting. For those that may be interested, here's some graphs in order of increasing complexity:
2 variables 2 operations
3 variables 2 operations
2 variables 3 operations
3 variables 3 operations

I'll finish cleaning up the script to submit tomorrow.

[Floris van Doorn]

How are these generated? Looking at the first graph, why is x = x not at the bottom? Why is it not in an equivalence class with x ∘ x = x ∘ x?

[Vlad Tsyrklevich]

Floris van Doorn said:

How are these generated? Looking at the first graph, why is x = x not at the bottom? Why is it not in an equivalence class with x ∘ x = x ∘ x?

Eq 1 is not included in the graph because it's not included in the output of lake exe extract_implications. Right we now we have proved Equation 1 is true, not that 1 implies Equation X (which is obviously true, but it's just not being picked up.) I could easily generate the individual theorems, but though it was unnecessary given theorem Equation1_true

[Joachim Breitner]

Vlad Tsyrklevich said:

not that 1 implies Equation X

The other direction, right?

[Vlad Tsyrklevich]

Err, yes.

[Floris van Doorn]

fyi: it is currently in the graph, just not in the right spot

[Floris van Doorn]

But I guess that holds for every node, since we could find/prove more implications between them.

[Vlad Tsyrklevich]

Floris van Doorn said:

fyi: it is currently in the graph, just not in the right spot

Ah, indeed. SimpleRewrites/theorems/Rewrite_yx.lean is the only one with a proof for Equation 1.

[Vlad Tsyrklevich]

I don't know if it makes sense for me to autogenerate proofs for it so it's included in the graph, or teach the tool about it. I don't suppose we'll have another such equation so maybe it's not such a loss to just generate the proofs

[Joachim Breitner]

Are you wondering whether it’s better to generate 4000 trivial Equation n => Equation1 theorems in lean, or teach the tool to understand the “Equation1 holds always” fact?

[Vlad Tsyrklevich]

yes, perhaps there is another obvious way to do it that I'm missing?

[Joachim Breitner]

I’m not following exactly what you are trying to do, and what’s your input. Is the input of your tool some JSON that includes the information “eqn1 holds always”? Then maybe either ignore that equation completely in your tool (as it is quite boring), or add edges to it from all other nodes.

[Vlad Tsyrklevich]

Right now lake exe extract_implications doesn't show X->1, should it? If so, should it know that because of special handling for theorem Equation1_true, or should we just generate the trivial proofs, or something else?

[Vlad Tsyrklevich]

graphviz generation tool PR here https://github.com/teorth/equational_theories/pull/160

[Joachim Breitner]

At least yesterday or so it included

  "unconditionals": [
    "Equation1"
  ],

in the output; not sure what has changed in the last 24h, things are moving too fast for me now that the weekend is over :-D

[Terence Tao]

These look great! I just created a list of visualizations in README.md (similar to the "recent progress", please add to it when submitting your PR to link these files. (I have lists both for single-shot visualizations generated at one point in time, and continuously updated visualizations.)

[Vlad Tsyrklevich]

ok now that Floris has pointed this out, I can't unsee Equation 1 in the graph. It also tripped me up somewhere else today, so I went ahead and created a PR to generate the explicit implications to Eq1, feel free to let me know if you disagree https://github.com/teorth/equational_theories/pull/211

[Joachim Breitner]

I still think it’s silly to create such a large file, unconditionals should just be understood by the data processing tools, just like they are supposed to understand that implication is transitive. But maybe it’s just easier this way, and gives more impressive “explict implications” stats.

[Vlad Tsyrklevich]

Yeah, my main thought is just that it then has to be special cased everywhere. I had to special case it today writing the EquationSearch tool because otherwise it was constantly generating them. Just made me think, why not just have the theorems. Alternatively, since we have a canonical extract implementations tool, we could implement it there instead? That also seems totally reasonable to me as an alternative.

[Terence Tao]

I'm fine with having the 4693 explicit implications X -> 1; it is true that this boosts the explicit implication count somewhat artificially, but one could try to prune it later and only generate the X->1 for which X is not known to imply any other equation.

Another option is simply to delete Equation1 from the graph; every law implies equation 1, and it is not difficult to show that equation 1, having no semantic content, cannot imply any other law, so adding it doesn't do anything interesting to the graph. (This is in contrast to Equation2, which is equivalent to a large number of other laws.) Perhaps once we have a fancy interactive graph visualization widget we would have an option to click that can add or remove Equation 1 as desired.

[Vlad Tsyrklevich]

I'll soon submit a PR to re-order the graph as per #Equational > Metatheory: meta-thread and just to experiment also added 2 separate options to remove Equation 1 and the Equation 2 equivalence class to see what it looks like without them:
graph_no_eq1_eq2.svg

I'll be updating the graph in the README too, but I'll keep Eqs 1+2 there.