Memoizing finite magmas for kernel-friendly reduction

Stream: Equational

[Joachim Breitner]

Here is a thought for how to speed up type checking of proofs that a certain finite magma satisfies or doesn't satisfy an equation. In https://github.com/teorth/equational_theories/pull/19 the magma operation is given as a polynomial, and in another topic I saw tables. Now calculating that polynomial at every evaluation of the operator is a bit wasteful. A table sounds better, and certainly the proof could first construct the full table from the polynomial, and then work with that.

But the kernel doesn’t support (effiicent) arrays, and lists are wasteful again. So my idea, which I’ll try now, is to encode the full table in one big number $t$. First I flatten the table as a list $$t_i$ of $n$ entries (with index $i = (a-1)\cdot n + b$ to look up $a \circ b$ ), and then encode that in a single large Nat as $\sum_i t_i*n^i$. Reading off that number is a matter of one division and one modulo operation. Since all these operations work in the type checker using native operations, this might be noticably faster.

(Maybe this is all going to be futile because the kernel’s caching mechanism already has a similar effect; we’ll see.)

[Joachim Breitner]

Not sure if it is going to help a lot, but it was a nice exercise: https://github.com/teorth/equational_theories/blob/937546f1d3acf0cd92b891162a6fb43369accfb9/equational_theories/MemoFinOp.lean

[Yuyang Zhao]

Joachim Breitner said:

But the kernel doesn’t support (effiicent) arrays, and lists are wasteful again.

How about a tree data structure like docs#Lean.PersistentArray ?

[Daniel Weber]

I think the magmas involved are small enough that a tree won't be noticeably better

[Daniel Weber]

I wonder if the table could be encoded using CHT, so only a single modulo is needed

[Joachim Breitner]

CHT?

[Daniel Weber]

Sorry, CRT (Chinese remainder theorem)

[Joachim Breitner]

How would that work? If i first have to find the $i$ th prime number to make a lookup I have not gained much :-) So I may be thinking of the wrong thing.

[Daniel Weber]

It doesn't have to be primes, you can also use e.g. $2520 i + 1$

[Daniel Weber]

Actually I think it would be best to encode it in base $2^{\lceil \log_2(n) \rceil}$ and then use shifting and bitwise and to find the data

[Joachim Breitner]

I was thinking the same (shifting). In the next version. Its probably not the bottleneck anyways :sweat_smile:

[Terence Tao]

By the way there were some specific finite magmas in this MathOverflow answer that might be particularly useful to establish anti-implications. But perhaps just brute forcing over all small magmas is already fast enough.

[Terence Tao]

There may already be a list of all small magmas up to equivalence somewhere on the internet EDIT: https://oeis.org/A001329 is a starting point

[Joachim Breitner]

We can see if Nicholas’ project (equational#19) covers these anti-implications. But if not we can of of course use the same lean representation to throw in more magmas.

[Terence Tao]

Oof. According to the OEIS there are already 2483527537094825 non-isomorphic magmas of order 5. So yeah maybe some targeted finite magmas would be a better approach than brute-forcing over all

[Nicholas Carlini]

I've brute forced all finite magmas up to order 4 and it did not contribute many more counterexamples than searching random polynomials did.

[Nicholas Carlini]

(Or, I think I did. I enumerated all 4^(4*4) tables and checked each of these across every equation. Is that a full brute force?)

[Edward van de Meent]

if we're lucky, the smallest number of counterexamples needed is the lenght of the maximum chain in the implication graph (excluding equivalent equations)... i wonder how close to that we can get!

[Joachim Breitner]

Nicholas Carlini said:

(Or, I think I did. I enumerated all 4^(4*4) tables and checked each of these across every equation. Is that a full brute force?)

Very brute indeed!

[Nicholas Carlini]

I guess what I meant was: I don't think this skips over anything, but I don't think it did