Wrong ordering of equations

Stream: Equational

[Bruno Le Floch]

There are two issues with the various places where we described and implemented the equation ordering, so I am worried there might be more. Extra eyes would be welcome. I take the lists of 4694 equations of size ≤4 in the Equations directory as ground truth because it is Lean code used in our formal proofs. (By "size" I mean what we usually call "order", but this word would lead to confusion here.)

The ordering stated in appendix A of the paper compares laws or expressions by their size first, then by their left-hand side or left operand (recursively), then the right one. However, our lists of equation numbers include for instance

• Equation 307: x ◇ x = x ◇ (x ◇ x)
• Equation 322: x ◇ y = x ◇ (x ◇ x)
• Equation 359: x ◇ x = (x ◇ x) ◇ x

which makes it clear that we first consider the shape, and only afterwards consider the ordering of variables. If we really began by looking at the left-hand sides as stated in the paper, then we would have eq307<eq359<eq322. I think the same mistake is made at the end of Chapter 1 of the blueprint.

[Bruno Le Floch]

The second issue is a long-standing bug, at least in the script find_equation_id.py, in the case of balanced equations (same left and right sizes) of total size 8 and above. It does not seem to affect the script generate_eqs_list.py. Because the equation ordering takes into account size and shape recursively, and then variables, it is easily implemented through nested loops. Shapes of given sizes are generated correct sorted by all_shapes (previously generate_shapes) and then filled with variables in a second step. To avoid redundant equations that only differ by swapping left and right sides, we loop only through lhs sizes up to half of the total size, and for balanced equations (same left/right sizes), we compare the lhs and rhs shapes before deciding whether to keep that pair of shapes. This is where the bug lies: the shape comparison is not consistent with the ordering produced by all_shapes, so we end up keeping the "wrong" equation between lhs=rhs and rhs=lhs. The inconsistency is that the shape comparison only takes into account the size at top level, which shows up first for ((x*x)*x)*(x*x) and (x*(x*(x*x)))*x:

• ((x*x)*x)*(x*x) comes before (x*(x*(x*x)))*x according to all_shapes, and this is correct, but
• the shape comparison sees they have the same size, then compares them recursively without any further size comparison, so it compares their left operands (x*x)*x and x*(x*(x*x)), then compares left operands thereof, x*x and x, and finds the first shape to be larger.

In all_eqs (previously generate_all_eqs), this shows up (very slowly since we're talking about equation numbers around 3e8!) by failing to have Equation 295980737: ((x ◇ x) ◇ x) ◇ (x ◇ x) = (x ◇ (x ◇ (x ◇ x))) ◇ x, and instead having ((x ◇ x) ◇ x) ◇ (x ◇ x) = ((x ◇ x) ◇ (x ◇ x)) ◇ x directly (not actually tested, sorry!). In the code to go back and forth from an equation to its id it shows up as mostly non-sensical mappings that are not inverses of each other, because my calculations of ids did not anticipate this problem. I'll fix that.

[Douglas McNeil]

So IIUC the idea is to redefine our algorithm (that is, the explanation) to match what we actually did for problem #1, and since the occasional dabbling with really high equation numbers has been mostly exploratory, just fix the bug for problem #2?

[Terence Tao]

Ugh, sorry for not spotting this earlier. I've tried to implement a fix for #1 in equational#1041.

[Bruno Le Floch]

@Douglas McNeil Yes, that's a good summary of the situation. I have some fix incoming for the second problem. Indeed, we have used some order-8 equations in the Higman-Neumann characterization of groups, but of the form x=RHS, which are not affected by this bug.

@Terence Tao Thanks! I've added a review on Github pointing out typos and related.