On Friday, January 3, 2020 at 6:56:21 PM UTC-5, David A. Wheeler wrote: > > > > 2. Cryptic labels: He is ranting while faced with theorem names on the > HTML > > page of sqr2irr. No clue whatsoever what they mean. Compares this to > more > > explicit names found in competing products, and in program code in > > general. I think there is indeed headroom for improvement here. Maybe a > > pop up showing an explanation while hovering over a name alleviates the > > situation. > > Huh? There *is* a pop up showing an explanation when hovering over a name, > in both the GIF and Unicode versions. Try it out! Just go here: > http://us.metamath.org/mpegif/sqr2irr.html > and hover over any of the theorem names; you'll see the first sentence of > the theorem > comment displayed. For example, step 5 uses breq2 ; just put your > mouse over that and it displays "Equality theorem for a binary > relation..." >
The primary purpose of a label is to identify a theorem uniquely. In books this is accomplished with equation/theorem numbers, which are much more cryptic than our labels but don't seem to bother the readers or at least the author. Principia Mathematica was written entirely with nothing but numeric labels with the exception of a handful of very common cases like Simp and Syl. The reader gets used to "*2..." being mostly about implication, negation, and disjunction, "*3..." about conjunction, "*4..." about biconditional, etc. We try to provide at least a hint of what the theorem is about using our conventions, but an unambiguous description of the theorem is impossible to achieve, and we don't pretend that it does. Information about the theorem is provided by its description and its actual content, just like in books. Both of these are searchable and are the main ways that I locate a theorem whose name I forgot, perhaps assisted by a label with wildcards. Both are instantly available for the reader in a web page proof either by hovering over the label or clicking it. Note that at the top of set.mm I added a link to label conventions. For me personally, an important reason to keep labels short is to make them easier to type. Maybe this isn't everyone's experience, but I find it easier to remember labels that are shorter (especially if they follow a convention, which we try to do). To remember a long label means having to remember all pieces of the label, their order, and, since they are never going to be spelled out in full English, what abbreviations were chosen. There seems to be a threshold label length of maybe around 8 to 10 characters where I start to make mistakes typing it in (after glancing at it in another window) and end up resorting to copy/paste, slowing me down. The Wikiproofs site (wikiproofs.org) seems to be down, but looking it up on archive.org it uses theorem labels like "introduceBiconditionalFromImplicationsInConsequent". Personally I think that would slow me down and I would dislike it. IIRC Jim Kingdon contributed to that project, and it would be interesting to hear his experience with long labels. Currently, the longest label in set.mm is aiffnbandciffatnotciffb, which is in a mathbox. While it attempts to describe the theorem, it doesn't do so unambiguously, and I doubt I could remember its exact spelling even long enough to type it without making a mistake unless I looked directly at it. We would almost certainly change it to a much shorter label should it be moved to the main set.mm. Another smaller consideration is the set.mm file size. Inside of proofs in the current set.mm, there are 1.1 million instances of labels with an average length of 5.8 bytes. Each extra byte of average label length would add a megabyte to the file size. (The 5.8 length is distorted by short labels for syntax axioms, and the average label length for just theorems, which I didn't calculate, would be longer.) > I do agree that the pop-ups are not very discoverable (if you don't know > they > are there, it's not obvious to try it out). Also, hover doesn't work on > most > mobile devices (touch screens generally can't hover), and mobile devices > are > the most common way to view HTML pages (though they CAN detect a > click-down). > > POTENTIAL IMPROVEMENT: > Maybe there'd be a way to the hover information more discoverable > AND modify things so it's invokable in mobile devices (say by onclick). > I don't know how to solve the mobile problem, but for PC browsers perhaps it would be useful to add to each page a sentence on each page saying something like, "Hover over a label link for more information." > > The underlying Metamath language doesn't require short names, it's simply > a > convention in set.mm, iset.mm, and many others. > We do have naming conventions, but it's fair to say that the names aren't > too obvious. > > I'd be fine with longer names, though I don't know if others would be. > In a few cases we have short names that perhaps could be a little longer, > e.g., > "sqr" is currently short for "square root" in set.mm, but that is > arguably > ambiguous with "squre"; we could use "sqrt" instead. > If we want names to be much easier to read for newcomers, though, I think > the obvious way would be to insert separators between the named parts. > The obvious separator is "_", so we could rename "sqr2irr" into > "sqrt_2_irr". > We could even spell things out more fully, e.g., > "squareroot_2_irrational". > Metamath tools won't have any problem with that, and compression tool > like zip will compress that to a similar size, though of course the > expanded file would be a lot bigger. > Our current square and square root conventions are "sq" and "sqr" resp. I'm almost certain I've seen "sqr" used for square root in at least one computer language although I can't recall which one right now. I don't see the problem with omitting the "t" since any confusion is instantly resolved by hovering over the label, if the content of the proof step doesn't make it obvious. If people are truly confused by this, I suppose we can add the "t", but until now no one has complained about it. I don't see the point of "squareroot_2_irrational" - long to type, annoying to shift for the _, and not necessarily easy to remember precisely (is it "2" or "of_2"? does it have "is"? why isn't it "square_root" since they are 2 words in English?). And theorems that can be described unambiguously like this one in a few words are very rare. Our convention is pretty clear on the abbreviations "sqr", "2", and "irr", making "sqr2irr" easy to remember (for me at least) and type. Norm -- 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/eae8c6ec-5da2-4596-81c5-fa1f1e8597a1%40googlegroups.com.
