Yes, this informal proof was later turned into the LRParser which is part of mmj2 (actually a slight extension of LR which I call KLR), and this is running in set.mm CI IIRC, so I think that issue is already resolved. (The metamath-knife parser isn't quite as powerful and requires hints to resolve tricky cases, and I'm not entirely convinced it is correct or provides a proof of unambiguity when it completes successfully.) I have a paper proof of the correctness of the KLR parser which I've been meaning to publish at some point, but I don't really know who would be interested in that kind of submission...
On Sat, May 31, 2025 at 2:06 AM Jim Kingdon <[email protected]> wrote: > On 5/30/25 12:10, Mario Carneiro wrote: > > > this is one of the most difficult cases in the proof of unambiguity. > > See https://us.metamath.org/downloads/grammar-ambiguity.txt for more > > on this > Has anyone done any work on a tool to automatically check the metamath > grammar for ambiguities? When I was encouraged to add additional syntax > I was told "oh don't worry it won't be ambiguous". I presume that was > true in the particular case which I think was probably > https://us.metamath.org/mpeuni/df-dju.html although I don't remember for > sure whether that is the only syntax I've added. Maybe this isn't quite > up there with the definition checker in terms of likely ways to > introduce unsoundness, but if we did manage to make the grammar > ambiguous it likely would have similar consequences to the things the > definition checker checks for. > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion visit > https://groups.google.com/d/msgid/metamath/3b59996d-72f6-4e7f-aad3-14c31b2daab5%40panix.com > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJSs3sDVFSAmgiArokt4o0QbG4wOR7nuVASfQHJea-Rj33g%40mail.gmail.com.
