On Sun, 5 Jan 2020 09:23:21 -0800 (PST), Norman Megill <[email protected]> wrote: > I also dislike the idea of have to type 3_eq_tr_4_d instead of 3eqtr4d.
That's unfortunate. Okay, sounds like adding underscores to the labels is off the table. That's okay, I'm just trying to identify possible problems & possible solutions. > I mentioned an idea here that in principle might appease everyone:: > > https://groups.google.com/d/msg/metamath/G1xyJb6RjfI/q6P_IaKHBAAJ > which links in particular to > http://us.metamath.org/mpegif/mmnotes2004.txt (search for "13-May-04"). > > At the time I thought it was a bit of obsessive overkill and wasn't really > serious about doing it, but maybe the time has come to revisit it. > > Basically we start with David's convention table to produce a table of > acronyms and their expansions in English. (Or we modify the existing table > so this information can be extracted.) When an acronym has multiple > meanings, we add ":2", ":3",... to the secondary meanings. I chose not to > put ":1" after the primary meaning, which would normally be the most common > usage. > Some examples of entries in the acronym table would be: > > 2 two > 2:2 double > 2:3 secondVariation In most cases there shouldn't be multiple acronyms, since the acronyms are mostly the NAME part of df-NAME. And while the ":NUMBER" will prevent some kinds of overlap, I think for most people the :NUMBER won't help understand what is being labelled. > irr irrational > irr:2 irreflexive In cases where there's ambiguity, and you're willing to use extra characters, I think it'd be better to use extra characters that are *meaningful* instead of an arbitrary ":NUMBER". E.g., "irrfx" for irreflexive. It's also pointless to try to completely eliminate ambiguity anyway if there are no separators in the labels. Without separators like "_", sometimes the same sequence of characters will map to multiple expansions. > In the description of each statement, we add an acronym key. For 3eqtr4d > and sqr2irr they would be: > > 3:2+eq+tr+4:3+d > sqr+2+irr > This acronym key would be delimited somehow to identify it, maybe enclosed > in braces or vertical bars. Note that "+" and ":" are characters not > allowed in labels. ... > Using the acronym key and acronym table, we could automatically reformat > the labels throughout set.mm to be any one of the three forms ... > Or we could leave the labels unchanged > (my preference), and the fully expanded version could appear in the tool > tip when the user hovers over "3eqtr4d" or "sqr2irr" in a proof I don't think we want to do a lot of reformatting, that's a pain, and in any case we want a *single* label for a given assertion. But as a tool to help people understand the naming convention, an acronym key might be very helpful for 2 reasons: 1. It could help new users learn the conventions in general. I used Metamath for years before I started to understand the naming convention. 2. It could help anyone (even old timers) understand why something has a given name. Even if you understand the convention in principle, most people only work on *parts* of set.mm, and thus some of the abbreviations are often new. > Advantages: > 1. It will encourage consistent naming. > 2. It will likely encourage or require that many existing labels be changed > to conform to this scheme, thus making them more consistent with our > conventions. > 3. It will provide a guideline for naming new theorems, since the developer > will be have to choose from the acronym table (occasionally adding to it) > rather than making up ad hoc labels that no one else understands. > 4. It will hopefully appease anyone complaining that "sqr2irr" is cryptic. > > Disadvantages: > 1. It's yet another markup that must be added to metamath.exe to compute > the tooltips, reformat all labels if requested, and check the acronym keys > against the acronym table in 'verify markup'. Our markup language is > getting more and more complex and has almost become a way to sneak in > complications to the language without actually modifying the language. :) I think that metamath.exe should *not* try to reformat labels. In fact, let's not check against some acronym table, at least for a very long while. It's simply a hint to the reader about *why* the label has that label. Trying to do that check would require the kind of detailed convention table that we don't have today, and it will take us time to build up one. If we don't do label-checking then the work on metamath.exe is very easy: don't do anything. If there's any checking at all, we could simply require that new $a and $p statements include *an* acronym key. That, at least, is easy. Once its *existence* is verified, we can use humans to check it. In fact, once an acronym key is created, it'll be a lot easier for people to check the label name (is that *really* what you meant?). > 2. It will be a huge amount of work to add 30K acronym keys. Actually it > could be phased in slowly over a long period of time by interested people... I think phasing this in, slowly, is the only sane approach. Thankfully, if it's done slowly it can just be done as part of the normal process - no big deal. > 3. It's yet one more thing developers must learn and use when adding new > theorems. Yes, though naming is already something developers have to learn if they want to add something, so it's not much different from the current state. And any existing acronym keys will help them learn naming, so it may actually speed up their learning instead of being an impediment. > 4. As Mario mentioned, if reformatting all labels throughout set.mm is > done, there would be a huge amount of the work manually adjusting formulas. If it's done slowly, phased in, it shouldn't be a big deal. > 5. The fully expanded version would double or triple the size of set.mm. > (Actually I don't see that ever happening with the full set.mm, although > maybe it would be done in a "beginner's" subset of set.mm for learning > purposes.) I don't understand this. I *think* all that needs to be added is a little "acronym key" in the comment of each assertion, so we're only talking about adding around 15 characters to the lead comment of each assertion. E.g., adding something like "[sqr+2+irr]" to sqr2irr, producing: $( [sqr+2+irr] The square root of 2 is irrational. See ~ zsqrelqelz for a generalization to all non-square integers. The proof's core is proven in ~ sqr2irrlem , which shows that if ` A / B = sqr ( 2 ) ` , then ` A ` and ` B ` are even, so ` A / 2 ` and ` B / 2 ` are smaller representatives, which is absurd. An older version of this proof was included in _The Seventeen Provers of the World_ compiled by Freek Wiedijk. It is also the first "top 100" mathematical theorems whose formalization is tracked by Freek Wiedijk on his _Formalizing 100 Theorems_ page at ~ http://www.cs.ru.nl/~~freek/100/ . (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) $) sqr2irr $p |- ( sqr ` 2 ) e/ QQ $= Did you have something else in mind? --- David A. Wheeler -- 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 on the web visit https://groups.google.com/d/msgid/metamath/E1ioJUw-0007Bw-BD%40rmmprod07.runbox.
