On Sunday, January 5, 2020 at 10:56:11 PM UTC-5, David A. Wheeler wrote: > > On Sun, 5 Jan 2020 09:23:21 -0800 (PST), Norman Megill wrote: >
... > > > > 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. That would be true only for the "principle" part (NAME) of a label, such as "div", matching the definition label. There might be 100 uses of the definition that need to be distinguished, combining pieces made of short acronyms that are likely to have multiple meanings. > 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. > If you don't like the colon, we could have "3(2)eq(1)tr(1)4(3)d(1)" or any other syntax, as long as it allows the user to look up the meanings of acronym parts and/or allows the software to generate a tooltip with the acronyms expanded. All I care about is to have the ability for the software to look up the parts automatically to avoid manual effort to check them by hand. I suppose we could also have "3(triple)eq(equality)tr(transitiveLaw)4(fourthVariation)d(deductionRule)", although it seems like an unnecessary duplication of information in the acronym table. > > > 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 doesn't matter if "irrational" has the same acronym "irr" as "irreflexive" because the two concepts usually occur in different contexts. "pssirr" seems simple and natural for "proper subset is irreflexive". "Proper subset is irrational" would be a nonsense interpretation, just as would be "square root of 2 is irreflexive" for "sqr2irr". On the other hand, "pssirrfx" seems awkward and harder to remember. At first glance I'd wonder what the "fx" is for since we usually have label components with 1 to 3 characters. And I'd have to remember that it's arbitrarily "pssirrfx" rather than "pssirrfl" or "pssirrfv". There are always going to be many acronyms that mean multiple things out of context (and sometimes even in context, such as the "3" in "3eqtr3d"). We can't fix that without making the labels much longer, more time consuming to type, and harder to remember. The purpose of the proposed acronym key is to provide an easy way for a new user to look up, or see in a tooltip, what a label's acronym parts stand for, until over time they get used to them. > 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. Yes, that is a purpose of the acronym key, which resolves both ambiguity caused by juxtaposition and ambiguity caused by multiple meanings of an acronym piece in a label. ... > > 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? Sorry if I was not clear. I meant that if we replaced all labels with the long version like "triple_equality_transitiveLaw_fourthVariation_deductionRule", then because labels are referenced 1.1 million times in proofs we might add perhaps 50MB to the set.mm size. Of course we don't want to do that. Although it's something that may (or may not) help a beginner with a toy subset of set.mm. 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/733ea8c8-f26c-4d3e-800c-cf7e8ffbd6be%40googlegroups.com.
