Writing the paper, outstanding tasks 2.0

Stream: Equational

[Terence Tao]

After some hiatus, I am trying to return to wrap up the final core component of the Equational Theories Project, which is to write up the paper reporting on both the mathematics and the workflow of the project, with a tentative plan to submit to the Annals of Formalized Mathematics.

The current draft of the paper is here (note - due to some weird Akamai issue, an error message may temporarily appear before the PDF is accessed). Much of it is in good shape, but certain tasks are still outstanding:

• equational#873 equational#1038 Complete Section 4 "Project Management". Claimed by @Shreyas Srinivas
• equational#922 Complete Section 9 "Higman-Neumann laws". Claimed by @Jose Brox
• equational#926 Expand Section 6.3 "Confluence". Claimed by @Cody Roux
• equational#956 Expand Section 5.6 "Modifying base magma". Claimed by @Douglas McNeil
• equational#924 Write Section 8 "Implications for the finite graph". Currently unclaimed

(There was also equational#1029 to create a section on the full spectrum problem, but perhaps in the interest of getting the paper over the finish line, this can be set aside (or diverted to the blueprint) unless someone volunteers to write it.)

There also are a number of smaller issues (marked in orange text boxes in the paper) that I will try to look at later today. Anyway, if contributors who had claimed these sections can report on how they are proceeding, that would be great. And we still need someone to write up the results for the finite implication graph!

In addition to the writing, the affiliations of contributors at https://github.com/teorth/equational_theories/blob/main/paper/contributions.tex , as well as the contriubtions matrix at https://github.com/teorth/equational_theories/blob/main/paper/contributions.md , are still quite incomplete. If your affiliation or contributions are not correctly reported there, please either submit a PR to update them, or message me so that I can do so directly.

And of course any proofreading, comments, or feedback on the paper by any of the contributors (or other observers) would be very welcome!

[Douglas McNeil]

Okay, finally got my few paragraphs edited, and tracked down references for PySAT/glucose (+minisat which the glucose guys say to reference as well.) They were used in 3475, the one where Terry hit an obstruction and by complete coincidence it found a counterexample just a few hours later, so I remembered. :-)

Not obvious to me where a reference should go to it, as there are a lot of TODOs in automated.tex. I think it most naturally fits in Semi-Automated Counterexample Guidance, IMHO, where we could also mention our use of vampire in the solver mode and mace4, as opposed to vampire/prover9.

[Shreyas Srinivas]

I will try to report by Friday night German time. I should be able to find time to write a substantial portion by then

[Terence Tao]

@Douglas McNeil The most important thing is to get the content in the paper; moving it to a different section is relatively easy if it turns out that it flows better, but we can decide upon that once we see how it looks.

I went through the paper and removed some of the less essential TODOs, but several do remain, particularly some requests for screenshots and examples in the automated section, and some further data for things like the twisting semigroup method which are only briefly described currently.

[Cody Roux]

I'm afraid I'm in a slightly more embarrassing situation: I've written something up for the paper wrt confluence, and it's all correct (and well-known standard stuff) with regards to rewrite theory.

However. What the actual development uses in Confluence.lean is not proving confluence of a rewrite system. Rather it is proving the existence of a canonizer, which is a function NF : Term -> Term which has the properties:

1. NF(t) ~ t
2. t ~ u -> NF(t) = NF(u)

where that last equality is syntactic over terms. This suffices to show that NF is idempotent (and almost the converse, which needs a tiny bit more which appears in the Lean). This can now be used to disprove t ~ u.

I'm not sure this is equivalent to confluence, though the approach is quite similar. At any rate I haven't been able to reduce the latter to the former (though the other direction is easy, simply take NF to be the normal form by reduction of a terminating confluent system).

So. What I wrote is different from what is proven. I can see 4 paths forward:

1. Somehow tie the knot by proving the equivalence. I'm not sure I personally am able to do this, especially in the time alloted.
2. Scrap the existing text and talk about what's done in code.
3. Talk about both, leaving the relationship open for now.
4. (the easiest, I guess) Do nothing.

What do you all think?

[Cody Roux]

Maybe I should add, I can have options 2-4 done by end of business week, but not much sooner I'm afraid.

[Shreyas Srinivas]

One way : write about the existing code as in point 2. Make the description of confluence brief and refer to a standard source for more (maybe Nipkow’s book? You would know better)

[Shreyas Srinivas]

The discussion of confluence would serve as background material for comparison with what you have done.

[Terence Tao]

I guess we've been using the terminology "confluence" rather loosely and imprecisely in our project, but in the paper we should get it right. I agree that option 2 sounds best. Perhaps one can open the section by saying that a well known property of theories that allows for an easy description of a complete rewrite system is confluence (and give references), but that we found it convenient within the project to work instead with a slightly different property, namely existence of a canonizer, and then leave as an open question to determine the precise logical relationship between the two.

[Cody Roux]

Ok thanks for the feedback, I'll try to have something in a day or 2.

I admit that it bugs me to not really understand what's going on with this idempotence: Why is that sufficient here?

I think the trick is that the relation (called $\mathrm{bu}_{\mathrm{rw}}$ in Confluence.lean) is sandwiched between $\rightarrow$ and $\rightarrow^*$, where $\rightarrow$ is the "directed" version of $\simeq$. In this case, $\mathrm{bu}_{\mathrm{rw}}^*$ is equal to $\rightarrow^*$, and idempotence means it merely needs to be applied once.

Is that right?

[Bruno Le Floch]

Rather than completely scrapping the text on confluence, it makes sense to put it in the blueprint perhaps? This will also make it easier to answer your question.

[Bruno Le Floch]

Sorry for the confusion: looking at the output of git blame, I think @Cody Roux is talking about the existing section "6.3. Confluence" in the paper.

[Cody Roux]

Correct

[Cody Roux]

Ok I think I finally cracked it! This was bugging me greatly. Basically the Confluence.lean code introduces a function R : Free -> Free, with a curious property: R w is always a sub-word of w. I'm tempted to call this "weakly collapsing".

It then defines a function bu R : Free -> Free which is the bottom-up application of R, and proves (somewhat painstakingly) that such a function is idempotent. Huh.

Finally it proves that for a bunch of specific Rs, they are weakly collapsing, and bu R sends related terms to "on the nose" equal terms:

   w ~ w -> bu R w = bu R w'

Only this last property really matters to refute equalities, by contraposition. So why the emphasis on idempotence? I know that canonizers, which send elements of an equivalence class to a unique representative, are idempotent. But this is not a sufficient condition!

What I've figured out is that with a few additional hypotheses on R, this _can_ be made sufficient! And it turns out that in each individual example, these hypotheses are true (I think).

The hypotheses I came up with:

1. R sends terms to one in the class: R w ~ w.
2. R is weakly collapsing.
3. if w ~ w', and _every subterm_ of w and w' is a fixed point for R, then R w = R w' "on the nose". I'd call this a "weak canonizer".

Then bu R is a canonizer for ~, and preserves equivalence classes.

This seems all a bit messy, though it seems like a new observation. It's quite a bit easier to prove that R is a weak canonizer than a full one.

I intend to write this up briefly, but I can also ditch all this and simply say that we somehow build canonizers for a bunch of equations.

[Cody Roux]

What does this have to do with confluence? I'm not sure, but if you take R to be the rule that sends the LHS to the RHS of an equation, then I think being a weak canonizer implies some sort of non-overlap which should imply confluence, maybe.

[Terence Tao]

So I'm trying to extract the "executive summary" here. If I understand correctly, confluence is a standard property that permits the construction of a complete rewriting system, and hence the ability to prove or refute all implications out of a given law; but we chose (for whatever reason) to work with a slightly different property (having a weak canonizer) that has similar consequences, but we do not know if it is logically equivalent to confluence. We could pose the logical relationship between the two properties as an open question. (It sounds like there are several other variations on these properties that could be discussed, but confluence is the most popular one in the literature, so it makes sense to focus primarily on the relationship with that one.)

[Cody Roux]

I guess I agree with that summary. I'm a little mystified with what's going on in Confluence.lean, and Confluence1.lean etc., and why they're called Confluence at all.

The above theorem is how I make sense of it. As I've noted, a confluent and normalizing system trivially gives rise to a canonizer, since normal forms are unique.

In retrospect it's actually a little too bad we didn't formalize the standard notion confluence, since it could have handled other systems, like the "putnam" system x (y x) ~ y.

And in retrospect I'm sorry I took this task way back without actually understanding what was being done in the code. I feel like I dropped the ball there.

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

I'll ask the question tomorrow again, with more clarity

[Cody Roux]

Ok, for what I hope is the last time: I am pretty sure I now understand what is going on in the Confluence_i.lean files, and (mostly) how it relates to actual confluence as usually understood in the theory of TRSes.

Basically all the equations considered can be oriented and shown to be "non self overlapping" and this is sufficient to show that the bu R defined in Confluence.lean is a canonizer by induction on derivations.

I have a latex proof that I've written up, but I'm gonna try to write it in Lean for peace of mind.

What a relief! I'll submit a PR tonight with the Latex stuff though.

Edit: I have a lean proof! ish. The termination checker doesn't much like induction on dependent families...

[Shreyas Srinivas]

Quick note: Table 2 has a huge horizontal overflow. I suggest contracting the size of this overflow by using a multiline header row which specifies the units and order of magnitude. It will make the table cleaner and fit inside the pagewidth.

[Shreyas Srinivas]

I have pushed more material on equational#1038. The primary goal of the uploaded content is to describe why project management is needed in the first place. The biggest part of it describes what it means to trust lean and what the limitations are. I am trying to keep dangerous words like "types" out of the description. A secondary goal is to explain this stuff to mathematicians through a math venue that they can refer and cite later. I felt this was relevant since there are loads of mathy people interested in lean who are unaware of these basic things and aren't on Zulip. Further, the stuff I described is basically folklore for ITP users but recent interactions with the outside world have taught me that there is very little understanding of what lean is actually doing out there.

The only thing that remains is describing the project dashboard, CI, use of Zulip, and all that. I will push those tomorrow. I will also review and shorten the story I have written so far.

[Terence Tao]

Sounds good so far! Feel free to adjust the table as part of your PR.

[Jose Brox]

Terence Tao ha dicho:

• equational#922 Complete Section 9 "Higman-Neumann laws". Claimed by @Jose Brox

Hi again! Sorry for my delay in answering (as @Shreyas Srinivas mentioned elsewhere, the other tasks I had postponed to work on this finally caught up with me, along with the end of the academic year, then holidays, then the start of the new academic year).

@Bruno Le Floch and I just started planning the writing of the Higman-Neumann section, I hope we will have it ready soon.