Optimizing SCC equivalent proofs

Stream: Equational

[Mario Carneiro]

How much optimization has been done on the SCC part of the proof? When two laws are equivalent, transitive reduction becomes not uniquely determined. There are two kinds of "moves" one can make here:

• If A and A' are equivalent, prove A -> B instead of A' -> B or A -/> B instead of A' -/-> B
• If {Ai} is an SCC, replace any of the implications with any equivalent presentation of this SCC

There are two reasons one might want to change the representatives:

• Using A instead of A' results in a shorter proof or counterexample proof
• Using a different presentation makes it easier to prove {Ai} is an SCC

[Mario Carneiro]

I'm wondering whether we have already done any kind of optimizations here, and whether we should.

[Vlad Tsyrklevich]

Some of the SCCs themselves are not established optimally, e.g. not a hamiltonian cycle but something with more edges than necessary. It would not be hard to establish the minimal equivalent graph if that's what we wanted, though I'm not sure if we care about deleting the old implications in favor of a more optimized representation.

[Vlad Tsyrklevich]

We could also pick representatives from every SCC to have all inbound/outbound edges go to them.

[Andrés Goens]

how do you check which are the SCCs? is that a python script?

[Andrés Goens]

or does it work with graphiti directly?

[Vlad Tsyrklevich]

The ruby code can import the implications data and compute SCCs, there is python code to do the same for the equation explorer data but I just don't use it.

[Vlad Tsyrklevich]

You can also get the SCCs directly from the graphit datai though, since it uses the condensed graph. See json["general_graph"]["scc_to_node_map"] in https://teorth.github.io/equational_theories/graphiti/graph.json

[Mario Carneiro]

Alex Meiburg said:

It might also be possible to make the SCC computation faster by adding just a _few_ extra theorems. Like for the Eq2 equivalence class, adding a theorem for EqX -> Eq2 directly (instead of relying on dynamically finding a path through other theorems) means that we can verify everything in the SCC by just checking those O(n) extra theorems.

Also Eq1 and Eq2 are special because we literally have a proof that every magma law sits between these two with no regard for the law itself

[Mario Carneiro]

i.e. they aren't just the top and bottom of the proved lattice, they are top and bottom of the full infinite graph

[Alex Meiburg]

Right, I'm aware, that's why just having the EqX -> Eq2 theorems would be necessary.

Mario Carneiro said:

We need to prove SCCs, not non-SCCs

I'm not sure I understand you here

[Alex Meiburg]

I'm saying: we want to show that a whole long list L of equations is in the Eq2 SCC. One way to do this is to (in Lean) walk the graph and find cycles and do Tarjan's algorithm or whatever.
But, if we just directly show that each equation EqX in L has a theorem EqX -> Eq2, then that's enough, and easier to verify I think.
Right now, we don't have such theorems written down. For instance for Eq123, the chain of implications looks like https://teorth.github.io/equational_theories/implications/show_proof.html?pair=123,2
If we just added a theorem Eq123_implies_Eq2 that's the .trans of these, then for a pretty-low overhead in the theorem count, we can really easily verify the SCC.

[Alex Meiburg]

I mention Eq2 in particular because it has such a large SCC.

[Alex Meiburg]

Oh, I now see your new thread https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Optimizing.20SCC.20equivalent.20proofs/near/486128929, which is the same thing.

[Alex Meiburg]

Personally I'm in favor of picking representatives, adding the O(n) theorems necessary to give all outbound/inbound edges/nonedges, and then going from there.

[Mario Carneiro]

Alex Meiburg said:

Right, I'm aware, that's why just having the EqX -> Eq2 theorems would be necessary.

Well no, I'm saying that we don't need these theorems at all

[Mario Carneiro]

Oh whoops you're talking about the other direction

[Mario Carneiro]

Because Eq2 is special, some aspect of this SCC calculation is also specialized to Eq2. I think this should be a sequence of theorems of the form "EqX is trivial", each of which is done by proving either that EqX implies Eq2 or that EqX implies EqY which is known trivial. That is, the transitivity step is being applied explicitly here, we aren't using an algorithm to do the work for us.

[Notification Bot]

9 messages were moved here from #Equational > A final end-to-end theorem in Lean by Mario Carneiro.

[Mario Carneiro]

Here are some pictures of the different SCC shapes. There are 1153 SCCs of size 1, 137 of size 2 (only one possible shape), 61 of size 3 (of which 37 are the optimal cycle, 23 have 4 edges and one has 5 edges), and then these larger graphs:

image.png

[Joachim Breitner]

Pretty!

[Mario Carneiro]

I was hoping that if we look at edges coming into an SCC that there would be a preference for one of the members of the class, but this is almost never the case, and in fact the opposite is true: of the 270 SCCs of size > 1, 23 have 1 "canonical representative" when relating to other SCCs, while 175 have as many representatives as the group size itself. The biggest SCC, for equation 2, has 1496 members and 125 "representatives"

[Mario Carneiro]

Alex Meiburg said:

Personally I'm in favor of picking representatives, adding the O(n) theorems necessary to give all outbound/inbound edges/nonedges, and then going from there.

So this proposal would indeed change a lot of proofs

[Shreyas Srinivas]

A tangential remark: since we are talking about SCCs, Donald Knuth will be talking about Tarjan's SCC algorithm in his Christmas lecture which is sometime in the next two days

[Oisin McGuinness]

Thanks for the alert on this. His talks are always fun and instructive! For those interested, https://www-cs-faculty.stanford.edu/~knuth/musings.html describes the talk, and https://learn.stanford.edu/DonKnuthXmas-2024-Registration.html is the registration page. Talk on December 5 5pm PDT

[Daniel Weber]

How large is $\sum |S|^2$ for SCCs $S$? We could try computing all proofs and then solve approximately the appropriate minimization problem with the proof lengths

[Mario Carneiro]

even an inefficient SCC proof is linear

[Alex Meiburg]

Mario Carneiro said:

So this proposal would indeed change a lot of proofs

Well, we wouldn't need to change anything existing. Just generate the right transitive proofs. Right?

[Mario Carneiro]

that's equivalent to doing nothing

[Mario Carneiro]

since the main proof will end up doing this work if it isn't prepared in advance

[Mario Carneiro]

the point of "optimizing" here is to make it so that the main proof never needs to do the work in the first place

[Mario Carneiro]

in particular, if all implications and non-implications use only SCC representatives, then the proof that the laws in each SCC are equivalent is completely local and we don't need to store a bunch of theorems for later random access

[Mario Carneiro]

the SCC proofs and the hasse proof become independent of each other