I also dislike the idea of have to type 3_eq_tr_4_d instead of 3eqtr4d. 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 3 three 3:2 triple 3:3 thirdVariation 4 four 4:2 quadruple 4:3 fourthVariation eq equality d deductionRule tr transitiveLaw [e.g. bitr] tr:2 transitiveClass [e.g. trss] sqr squareRoot irr irrational irr:2 irreflexive (Above, "2" should probably translate to just "2" rather than "two". I'm being a little extreme for illustration.) 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. For 3eqtr4d, this means: the label has the 2nd meaning of "3", followed by the meaning of "eq", followed by the 1st meaning of "tr", followed by the 3rd meaning of "4", followed by the meaning of "d". Using the acronym key and acronym table, we could automatically reformat the labels throughout set.mm to be any one of the three forms 1. 3eqtr4d 2. 3_eq_tr_4_d 3. triple_equality_transitiveLaw_fourthVariation_deductionRule 1. sqr2irr 2. sqr_2_irr 3. squareRoot_two_irrational depending on the user's preference. 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, in addition to the description excerpt that now appears. 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. :) 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, and we could have whatever tool just process labels that have acronym keys and ignore the rest, until all statements have a key and we decide to make it mandatory. 3. It's yet one more thing developers must learn and use when adding new theorems. 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. 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.) 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/1c4a8c4e-4b38-4736-ab35-5c31c28c7bc8%40googlegroups.com.
