On Sun, Jan 5, 2020 at 10:56 PM David A. Wheeler <[email protected]> wrote:
> 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. > My understanding of Norm's proposal is that this is a markup feature only. People won't actually look at 3:2+eq+tr+4:3+d -- it's no better than the original in terms of human readability -- but the index of "meanings" of 3:2 and eq and so on can be stored in a separate file so that it can parse 3:2+eq+tr+4:3+d and turn it into an interactive display, like [3](triple)[eq](equality)[tr](transitivity)[4](fourth variation)[d](deduction form) where the parentheses are hovers over the bracketed portions. The :NUMBER is necessary for this scheme to work, because otherwise there will be many bad glosses like [2](two) instead of [2](double). I like this idea. It doesn't pollute the actual labels with additional data, but provides computer markup data for parsing and display purposes. > 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. > The point is so that we don't have to give up our current ambiguous labeling convention (which is bad for computers but good for humans). 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. > That's what the +'s are for. > 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. > I think it would not be a good idea to change the labels in the public version of set.mm, but the existence of markup data makes it possible to perform a large scale rename like this easily and I don't see any reason why the tooling couldn't support it for people who want it. > 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. > My vote would be to have this information show up in hovers over the title of the theorem, e.g. "Theorem [3][eq][tr][4][d] 2508" in the main header. It doesn't need to be everywhere, it's rather noisy after all. > 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 actually think it is time to revisit HTML generation as a whole, see if we can make something better by starting from scratch. The current mechanism is many layers of legacy code written for browsers of the 20th century. I'm sure if we think about the problem for a bit, lay out all the requirements, and consider currently available options, we can find a solution that is less verbose, more maintainable, more extensible, and looks better. But that's probably a discussion for another thread. 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. > I don't see the problem with it being opt-in. It's just additional data that the web page can display if it is available, it's not something to verify (except possibly for welformedness). 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?). > I wouldn't sweat any bad glosses. An automatic translation can get 90% or more of the theorems segmented and we can clean up the rest lazily, in the same way as typos on comments. 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? > I wish we would stop using the description comment for metadata like this. This is the sort of thing that makes markup parsing the rats' nest that it is. Just have a separate comment, with a sane computer-readable grammar. (It should also contain the "contributed by" and "usage discouraged" information, which are also metadata. Using english words just fools people into thinking there is no strict grammar.) Mario -- 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/CAFXXJSvpoJfSgs440Gk-4kn9jEzf0p1oHNOmUL3ZMs80%3DHUtAg%40mail.gmail.com.
