Search space for (EqX ∧ EqY) → EqZ

Stream: Equational

[Vlad Tsyrklevich]

I had the thought that if we were to redo this project with what we know now, we would know that the search space is much smaller than it might have initially seemed--instead of 4694^2≈22m combinations, the actual search space is closer to ~1420^2≈2m after collapsing equivalence classes and another halving after considering duals. I began to wonder if there would be a similarly large reduction in searching for the implications of the conjunction of any two of the original 4,694 equations to the same set based on knowledge of the EqX → EqZ case and decided to calculate it on a whim.

Naively, the space is 4694^3≈103b but after collapsing equivalence classes it is 1420^3≈2.8b. We can do better by a simple algorithm: Fix X<Y. If EqX is a descendant of EqY or vice versa, the problem is already solved (it's simply the implications of the ancestor.) Otherwise, we find EqX and EqY's lowest common ancestors, compute their closures, and subtract the closures of the LCAs from that of EqX and EqY. We must search all of those implications. I conjectured that the reduction would be rather large, but it only reduced the space to ~785m, with a further 2x reduction by duals [unless I'm mistaken, is it sure that if (EqX ∧ EqY) → EqZ that (dual(EqX) ∧ dual(EqY)) → dual(EqZ)?]

This is perhaps a poor method of estimating the problem size, since in the conjunction case it may be much harder to apply the same tools to refute implications and there won't be any equivalence classes to reduce the search space. I just thought to share in case anyone found it as interesting as I did to consider.

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

As an initial test, one could gather the existing finite counterexample magmas and see how many such implications they refute.

[Terence Tao]

Thanks for this. So naively it could be two or three orders of magnitude more complex to get the triple intersections. Once one fixes X, and just looks at Y->Z relative to X, one is back to an implication graph problem and so in particular we get to use transitivity again. I imagine the finite magmas and also the newer linear magmas will also eliminate a lot of cases. It's also possible that by performing transitivity on the graph on 4694^2 classes (one for each pair X,Y) rather than 4694 classes, one can get a lot more mileage out of transitivity. This begins to get quite CPU-intensive though.

I feel like we need more input from the universal algebraists as to what kind of data sets might actually be useful for their work beyond this proof of concept.

[Vlad Tsyrklevich]

I had not considered that by fixing X, you get back to the same problem as what we have now. That does actually change how difficult it seems. Now you get the same tools and speed-ups as we have now, but just on ~1420 problems, each individually smaller on average, 785m/~1420≈550k instead of ~2m. I imagine the average case may collapse into a few huge equivalence classes, and that implications becomes easier while refutation becomes harder.

[Will Sawin]

Transitivity for the X-fixed problem can be stated as (X and Y) implies Z together with (X and Z) implies W gives (X and Y) implies W. Stated this way it's clear you can chain together in multiple ways, like if Y and W implies something you can use that as well. So there are advantages to considering the different problems together.