On Sunday, January 5, 2020 at 4:22:13 PM UTC-5, Alexander van der Vekens wrote: > > Hi Benoît > > On Sunday, January 5, 2020 at 8:21:26 PM UTC+1, Benoit wrote: >> >> Indeed, I think that BASIC also uses "sqr" for "square root", but for >> most modern languages, this is "sqrt". Anyway, "sqr" is indeed ambiguous, >> so I would prefer that in all labels, "sqr" be replaced with "sqrt". >> > Many acronyms we use in label parts are often ambiguous out of context in order to serve as short hints, with the understanding that the description or the theorem itself will provide clarification. The goal isn't to reproduce computer languages. For example, we use "itg" instead of "Integrate" like Mathematica. The majority of our acronyms for parts of labels are 3 or less characters. We have 30K labels built up from short parts, whereas computer languages have the luxury of just a few dozen functions that they can represent using single words or acronyms. For example, they use "sqrt" as the entire label for a single function, whereas for us "sqr" is just one piece of maybe about 150 compound labels.
I'm still not completely sold on the idea that people find "sqr" ambiguous. While BASIC and its dialects may be ugly from a modern computer science point of view, nonetheless it has been and maybe still is one of the most popular languages for beginners. Probably millions of people have written programs in various dialects of BASIC without this confusion. Is there any computer language anywhere that uses "sqr" for square? > >> Another, more important, change within labels would be to replace >> everywhere "rng" with "ring". Indeed, "rng" might refer to "rngs", which >> is a common name for non-unital rings (rings that lost the "i" of >> "identity"). Therefore, it is ambiguous, and it might be more difficult >> than in the "sqr" case to deduce from a simple inspection if the given >> theorem refers to rngs or rings. >> >> >> In principle, I agree with your suggestion to replace "rng" by "ring" for > theorems about unital rings (and `Ring` is unital in set.mm). There are > about 140 labels of theorems (in Parts 10-16 - only these should be > relevant) containing "rng", and I think most of them should be renamed > according to your proposal. In June 2019, I replaced already some labels > (in the context of introducing ZZring) on your advise. On the other hand, > there were changes of labels, replacing "ring" by "rng" for relevant > labels, in 2013/14. There must have been a reason for this. > The reason was simply to be more consistent. We only had one type of ring, and some places used "ring" while others used "rng". I changed them to "rng", picking the shorter of the two choices. I didn't know about the two spellings used in the literature for different kinds of rings. > Especially the label for the definition of a (unital) Ring, df-rng, was > changed from df-ring to df-rng (see also > https://groups.google.com/d/msg/metamath/HDQXr196Yo0/KhDrxgnRBgAJ) in > July 2017, which should be reverted. But the table of abbreviations > contains "rng" as convention to be used for (unital!) rings... > > To continue the discussion, a separate thread should be opened for this > topic (wasn't there a corresponding issue in GitHub?)! > I'm fine with making these changes since there is an ambiguity to be resolved, and it is good to conform somewhat more closely to math texts when it is practical to do so. If no one else has an objection, I don't think we need to open a separate thread. If you (BJ) want to create a PR for this when you find it convenient, please do so and we will accept it. > > Alexander > > PS: Your recent changes of labels, especially impd and expd, are very > helpful for me! > I agree. 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/5d0098d0-9c7e-4671-98f6-053e64dbed0d%40googlegroups.com.
