Non-commutative linear implications

Stream: Equational

[Matthew Bolan]

I recently learned that Singular's LETTERPLACE has great support for non-commutative groebner bases over the integers, so I was finally able to more or less entirely compute the implication graph for magmas $(G, \diamond)$ where $G$ is some subgroup of the additive group of a ring $R$ and $x \diamond y = a x + b y + c$ with $a,b,c \in R$.

These 3 files:
comm_linear_ouput.txt
non_comm_linear_ouput.txt
infinite_gb.txt
together should cover every single law not equivalent to the singleton law.

In each file for each law I list two rewrite systems, one for when $a,b,c$ commute, a more general one without this assumption, as well as implications these each give counterexamples to (so this contains the data of both the commutative linear and the general linear implication graph). They are the rewrite systems you get if you expand out the law in terms of $a,b,c$ and assume the constant term and the coefficients of $x,y$ vanish. Counterexamples to implications are given polynomial rings over $\mathbb Z [a,b,c] / \sim$ and $\mathbb Z \langle a,b,c \rangle / \sim$ respectively.

The file comm_linear_ouput.txt contains all laws where passing to non-commutative linear models from commutative gains nothing (for the equations under the purview of this project). Here I only computed enough relations in the non-commutative case to show that no new implications are falsified by passing to the non-commutative case, so the rewrite systems I list in that file are possibly incomplete.

The file non_comm_linear_ouput.txt contains laws where some extra implications were falsified by non-commutative linear models as compared to commutative ones. The non-commutative rewrite systems here are complete and finite, provided Conjecture 15 in this paper by the authors of the library I used is true. Perhaps someone here knows an unconditional test I can do.

For the 6 equations in infinite_gb.txt, [1113, 1682, 1885, 2534, 4380, 4470], I could not find a finite non-commutative Groebner basis over $\mathbb Z$ (the ones listed in the file seem to continue infinitely with the obvious patterns), but the computation suggested that certain implications would become false when passing to the non-commutative case. Luckily most of the questionable implications are already dealt with by transitivity (for example 1113 -> 2441 is false for linear magmas, because 1117 -> 2441 is false for linear magmas and 1117 implies 1113). The only problematic ones are 1682 -> 1832, 1885 and their duals, but for these I managed to find a 5-dimensional linear model mod 2 falsifying them.

Finally, unfortunately I do think Singular's code for non-commutative Groebner bases has a rare bug in it, where it seems to sometimes drop relations it should not. I think I managed to avoid this for almost all listed equations (I checked if the final bases still generated the original polynomials), but 1463 and its dual were affected no matter what I tried, so I had to add in the (true) identity $a^2 - 1 = 0$ manually for it. Luckily none of the equations where the non-commutative linear models can falsify anything new seem affected.

[Matthew Bolan]

For completeness, the model for 1682 is

$$x \diamond y = \left(\begin{array}{rrrrr} 0 & 0 & 0 & 1 & 1 \\ 1 & 0 & 0 & 0 & 1 \\ 0 & 0 & 0 & 1 & 0 \\ 0 & 0 & 1 & 0 & 0 \\ 0 & 1 & 0 & 1 & 1 \end{array}\right)x + \left(\begin{array}{rrrrr} 0 & 1 & 0 & 0 & 1 \\ 0 & 1 & 0 & 0 & 0 \\ 1 & 1 & 0 & 1 & 1 \\ 0 & 0 & 0 & 1 & 0 \\ 0 & 0 & 1 & 1 & 1 \end{array}\right)y.$$

Here it is on FME. I found it by doing the same groebner basis computation but mod 2 and with an assumption c = 0.

[Terence Tao]

Interesting. So, just to clarify, you have completely determined the relation "Law X implies Law Y for noncommutative linear magmas", without the need to trust Singular? If so, it might be worth adding this data to the github and updating the paper to make a reference to it. It sounds like it would take significant effort to formalize it in Lean but we can leave it as a supplemental, unformalized data set which may be of some interest to future researchers.

[Matthew Bolan]

I am trusting Singular that the elements of the Groebner basis it computes actually belong to the relevant ideal, and that it reduces polynomials modulo the Groebner basis correctly. I am not trusting that the Groebner basis actually generates the original ideal, since this is easy to check and seems to not always be true due to some bug.

[Matthew Bolan]

I think the effort of formalizing the anti-implications amounts to proving in lean some condition for a rewrite system to be complete, and then confirming this for the systems I list. It also is probably possible for many of the laws to produce finite linear witnesses to the anti-implication automatically . The implications seem harder since one needs to essentially do a Groebner basis computation to confirm the original polynomials generate the rewrite rules I list, but perhaps I can record expressions for the rewrite rules in terms of the original generators somehow. If possible that would also remove some trust of Singular.

[Matthew Bolan]

But otherwise yes, I've hopefully completely determined the relation.

[Matthew Bolan]

Here by the way is the bug report to Singular I made https://github.com/Singular/Singular/issues/1263 . The issue seems quite rare so I wouldn't be surprised if I'm the first to notice it.

[Matthew Bolan]

Ugh, there might be some other bug in sage/singular's Groebner basis code that affects this - equation 2696 specifically has incorrect looking output for the commutative calculation (but the non-commutative basis singular computes seems correct at first glance).

R.<a,b,c> = PolynomialRing(ZZ, 3)
I = R.ideal((-1)+(a*a*b)+(a*b*a)+(a*b*b)+(b),a*a*a)
print(a*a*a in I)

prints false in sage 9.3, and printing a Groebner basis of I prints

[a*b^2 - 2*a*b + 2*a + b - 1, a^2 + a*b0*b^2 - a]

where I have no idea what the b0 in the final element is supposed to be.

Luckily the bug seems patched in sage 10.5, so I can rerun everything in that version. As far as I can tell only it only affected 2696 Edit: actually the effects seem worse than I thought. I guess it was naive of me to sanity check the non-commutative calculations but not the commutative ones.

[Matthew Bolan]

In the meantime, assuming the correctness of my non-commutative calculation, the following are the only implications which:
a) Hold for finite magmas.
b) Are falsified by a linear magma

1117 2530
1117 2534
1117 2441
1117 2538
1117 2444
2538 1109
2538 1113
2538 1020
2538 1117
2538 1023
1113 2441
1113 2534
2534 1113
2534 1020

Somewhat disappointingly, I think by transitivity/duality they all come from the anti-implication $1117 \not \to 2441$, which we already knew had this property.

[Matthew Bolan]

The effects of this bug might be worse than I thought, so I'll hold off on talking about the graph in the commutative case until I rerun everything together with a few more sanity checks.

[Matthew Bolan]

Well, I unfortunately should stop work on this for a while, but poking around the documentation reveals that it should be possible to remove any trust of singular when I eventually revisit this - in principle I can get singular to print out expressions of the Groebner basis in terms of the original basis and vice versa, which then could be verified externally.

[Terence Tao]

Perhaps in the future it will become standard practice to have computer algebra packages have the option to provide proof certificates of their output in a language such as Lean. Given the somewhat unsettled nature of this story, I think for now I will just make a mention of it in the next log entry, and also add a link to this discussion in the blueprint, rather than putting it in the draft paper.

[Matthew Bolan]

I think that's fair for now. I do think a more trustable version of this story is realistically achievable though, so hopefully I (or someone else) can manage that before the end of the project.

[Andrés Goens]

Terence Tao said:

Perhaps in the future it will become standard practice to have computer algebra packages have the option to provide proof certificates of their output in a language such as Lean. Given the somewhat unsettled nature of this story, I think for now I will just make a mention of it in the next log entry, and also add a link to this discussion in the blueprint, rather than putting it in the draft paper.

wouldn't that be worth a mention in the draft paper? as a cautionary tale of (unverified) computer algebra code or, with a more positive spin, ta call to arms to have more CAS' output proof certificates?

[Matthew Bolan]

CAS outputting proof certificates sounds amazing, does anyone know if any already output proof certificates for some computations? It would be one potential solution to the question of how we can ever trust the output of closed-source software.

[Matthew Bolan]

I would be somewhat crushed if this wound up in the paper as an example of what not to do. I still think I can work around these bugs though.

[Terence Tao]

We do have an extremely rudimentary ``conclusions and future directions'' section of the paper currently. I will add a note to the outline of that section to also possibly discuss developing the linear magma implication using verified CAS as a future direction.

[Pace Nielsen]

@Matthew Bolan I know that in Mathematica you can ask for a proof certificate for prime factorizations. (It is especially important there, because the main prime factorization routine uses only a probabilistic primality test.)

[Kevin M]

I'm not entirely following the calculations done here (I've only worked with commutative ideals), so it is likely the following observations are trivial or not applicable. But in case a computational tooling perspective is useful, I'd like to point out that in many ways Groebner basis calculations are very close to already having a "proof certificate". Especially if the desired statement is of the form "This system of polynomials p_i has no solution", more specifically, when the Groebner basis collapses to just 1. Then a "proof certificate" is just a list of polynomials f_i such that sum f_i p_i = 1. As relating ideal membership questions back to the original basis is a common desired calculation, most computer algebra systems already provide the ability to do this. (Usually called a "lift"; or "basis transformation" if they force you to do it for the entire basis at once.)

In previous uses of Singular I've noticed there is some kind of issue with "lift" in that it runs way longer than necessary (I think internally it continues until a full Groebner basis is calculated even when that is overkill). But in this case it sounds like the problem size is small enough to allow running many basis calculations quickly, so maybe that would not be an issue here. Anyway in singular, I think what you want is called "liftstd". It gives the Groebner basis, and a matrix of polynomials showing how the new basis is related to the original generators. This can then be verified by a simpler tool that only needs to know how to multiply and sum polynomials to allow verifying ideal membership (and I guess the other tool would also need to be able to verify a basis is a Groebner basis if you want to prove solutions exist, instead of just prove ideal membership).

I've done something like this before to verify some (albeit much simpler) Singular calculations showing ideal membership with Mathematica. (I'm not familiar with lean) if a routine could be programmed in Lean to do this polynomial multiplication and sum, an external tool could generate lists of polynomials as proof certificates.

[Matthew Bolan]

Yes, I've already rewritten the old code to use liftstd, and am hopeful we can gain trust in the implications like this. Unfortunately around 1/4th of the laws give a surprising error message that I am unsure how to avoid (Non-commutative groebner bases are in general infinite, so singular requires you to only compute them up to a degree bound. Bases which were computed just fine before now complain that liftstd is doing multiplications above the bound set for the ring, and this does not change no matter how large I set the degree bound it seems), and I had a few unfortunate crashes which cut things short.

[Matthew Bolan]

I'm fairly hopeful that for the anti-implications I can just dodge the question of verifying whether something is a Groebner basis just by producing explicit, hopefully finite, linear models for those anti-implications - indeed this seems to already be possible automatically for most of the bases I've already computed. Implications can then be confirmed by an ideal membership test doing only polynomial multiplications in the way you suggest, provided I can get liftstd to cooperate.

[Kevin M]

I think I understand the basics of the liftstd issue you are hitting.

I believe under the hood Singular does liftstd by essentially doing the following (I think it actually changes Ring to have multiple coefficients instead of adding variables, but similar idea):

• if there are N generators, introduce N new variables, and choose monomial order so these are 'last' to show up in leading monomials
• define a new ideal where each generator_i is changed to generator_i + newvar_i
• run a Groebner basis computation (possibly cutting off computations where new_vars end up in leading terms?)

The Groebner basis is the resulting basis with newvars set to zero, and the transformation from the original generators can be read off by looking at the terms with newvars in each basis.

So I could see why trying to "tame" the usual liftstd by limiting degree could be problematic, as new terms are showing up internally. Even worse, its default stopping condition when the Groebner basis itself may not be finite, may not work well here.

While annoying, we could use this trick "by hand" to calculate individual lifts if necessary:
Change ring to have N new variables for the generator tracking, and also a new var X for the lift tracking.
Define an ideal with old_generator_i + newvar_i, and poly_to_lift - X. With order that old vars would be leading before X, and X before newvar_i.
Do a bounded degree Groebner calculation (increase degree until X shows up as a leading monomial).
Then you have your "lift" as X + new_var(0) some_poly + new_var(1) some_other_poly + ...

Hmm... alternatively I guess you could use the coefficient idea, and only define X as a new variable? Similar idea, just allows different options when defining the monomial order. I don't know which would work nicer with Singular internals.

Its annoying that such a routine would have to be written explicitly, but it may be the only way to "tame" the lifting in non-commutative ideals.

[Matthew Bolan]

I don't mind putting in the work to fix things like this (In fact I was already toying with just writing my own version of liftstd since we're verifying the calculation anyway and it would be a good learning experience), it just wouldn't be responsible of me to do so this week.