Implication Statistics

Stream: Equational

[Harald Husum]

I was curious about the distributions of the implication counts, both incoming and outgoing from our equivalence classes, so I made some plots:

implications_log.png

Interactive versions, which I find more useful:
implications_linear.html
implications_log.html

Not sure there is that much to learn from these, but I noticed that we have some outliers. The Equivalence classes for Equations 3, 23, 40, 375 and 3715 have more implications than one would expect from the number of classes that implies them. If that pattern holds when considering more operations I guess that is an interesting property. Maybe one could think of them as "central" in the implication graph somehow.

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

It would be interesting to use different colors depending on the number of variables that occur in each equation. We already have some heuristics telling us what Implies/ImpliedBy counts we should expect based on that number.

[Harald Husum]

I could do that, but the equation expressions aren't in outcomes.json which I relied on for this plot. I would have to source them from elsewhere. Suggestions?

[Terence Tao]

https://github.com/teorth/equational_theories/blob/main/data/equations.txt has the list of 4694 equations

[Harald Husum]

Terence Tao said:

https://github.com/teorth/equational_theories/blob/main/data/equations.txt has the list of 4694 equations

Thanks! In hindsight I could probably have found that with a search of the repo.

Here's the plot colored by the (minimum) number of variables needed to express the equivalence classes:

newplot.png

Does it match your intuition, @Zoltan A. Kocsis (Z.A.K.) ?

[Harald Husum]

Here's the interactive version, since it's helpful to see which equation a point represents by hovering.

stats_with_color.html

[Terence Tao]

That's a really nice plot. Would you mind if we added it to our (very sparse) images directory? It does seem to largely align with the intuition that the implication graph tends to flow from many-variable equations to few-variable equations. It seems that the two-variable and three-variable equations dominate the bulk of the graph, which I guess also matches with our experience as these are the equations we are almost always dealing with in the human-generated arguments.

[Amir Livne Bar-on]

Maybe we can also add the twisting monoid to the plot somehow? (If this data is even available)
It should be highly correlated to the number of variables but interesting to see if we can pinpoint what feature of many variables causes a law to be strong

[Terence Tao]

There's a lot of statistics one could consider adding to the plot - size of smallest finite magma example also comes to mind - so maybe one could PR the script as well as the image so that others can add more features over time?

[Harald Husum]

I'm open to make a PR out of both the script and the plot. The script needs some cleanup first, though, and I'm not sure how much time I have in the next few days, so expect some delay. In the meantime I'm open to suggestions, like yours @Amir Livne Bar-on. As long as I can source the data from somewhere I can hopefully cobble together something.

[Harald Husum]

I found some time to work on this after all; the script and image are incoming in #792.

I haven't looked at adding the twisting monoid or size of the smallest finite magma yet, but that should be doable as followup work to this PR.

[Harald Husum]

stats.html
stats_smallest_magma.png

It turns out that equivalence classes with smallest nontrivial magma size > 2 tend to be at the "periphery" of the Hasse diagram. The larger the smallest nontrivial magma size the more isolated the equivalence class. Maybe not a huge surprise.

[Terence Tao]

There are some equations for which no non-trivial finite magma is currently known (we only checked all magmas of order up to 4, and some up to 5). Are those equations listed in the plot currently?

[Harald Husum]

They are, with gray color. See e.g. equation 2 in the bottom right. I can't immediately spot any others, but there's definitely some over-plotting going on here though, so some points might be hiding underneath others.

[Harald Husum]

Ah, in addition to equation 2 it looks like there's only 1286 and its dual 2301 that lack a smallest nontrivial magma.

Perhaps a future direction of the project could be to identify a smallest nontrivial magma for the two latter? I'm not in a position to judge whether that is feasible or not, but if I've understood it correctly, no law of less than 5 operations can be Austin, correct?

[Terence Tao]

Interesting! We had obtained a linear model of order 7 for 1286, as noted in the commentary on equation explorer, but we had not ruled out the possibility of a model of order 5 or 6. This looks like it could be done via ATPs though, if anyone has some spare CPU cycles to devote to finishing this off, then we can complete the "smallest finite magma" table.

[Harald Husum]

Sounds like a good idea! I hope someone picks up that idea.

I'm noting, by the way, that also 1286/2301 lies on the periphery. I'm conjecturing that as one expands the number of operations under consideration, the cardinality of the smallest non-trivial magma will continue to negatively correlate with "centrality", where a measure for the latter property can be defined as log(n_implications * n_implied_by).

[Harald Husum]

Amir Livne Bar-on said:

Maybe we can also add the twisting monoid to the plot somehow? (If this data is even available)
It should be highly correlated to the number of variables but interesting to see if we can pinpoint what feature of many variables causes a law to be strong

Can't seem to find data on the twisting monoid anywhere. Let me know if you can produce any.

[Amir Livne Bar-on]

Checked with Mace4, equation 1286 doesn't have models with sizes 2-6, the smallest non-trivial model is of order 7

[Terence Tao]

OK, in equational#795 I have manually updated the smallest_magma.txt and smallest_magma_examples.txt files to include these examples, hopefully this doesn't break anything.

[Terence Tao]

@Matthew Bolan produced twisting monoid statistics at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/1485/near/480756118

[Amir Livne Bar-on]

Terence Tao said:

OK, in equational#795 I have manually updated the smallest_magma.txt and smallest_magma_examples.txt files to include these examples, hopefully this doesn't break anything.

The text in Equation1286.md refers to (p,a,b) = (11,1,7) as a proof of non-implication of equation 3. The example you added is idempotent, and is in fact a renaming of the linear model (p,a,b) = (7,6,2). The isomorphic version that's properly linear is

[0, 6, 5, 4, 3, 2, 1], [2, 1, 0, 6, 5, 4, 3], [4, 3, 2, 1, 0, 6, 5], [6, 5, 4, 3, 2, 1, 0], [1, 0, 6, 5, 4, 3, 2], [3, 2, 1, 0, 6, 5, 4], [5, 4, 3, 2, 1, 0, 6]

[Jose Brox]

Amir Livne Bar-on ha dicho:

Checked with Mace4, equation 1286 doesn't have models with sizes 2-6, the smallest non-trivial model is of order 7

Double checked!