Hi Norm, thanks for your comments. Some remarks on them below. Alexander
On Tuesday, January 7, 2020 at 12:46:42 AM UTC+1, Norman Megill wrote: > > On Sunday, January 5, 2020 at 1:42:44 PM UTC-5, Alexander van der Vekens > wrote: >> >> Thanks, Norm, for these hints - it could have been expected that the >> discussion about labels is not new... >> >> Your approach, which I like very much, goes in a similar direction as my >> suggestion adding titels/names to the theorems, see >> https://groups.google.com/d/msg/metamath/XPYuatviNV0/C86R2MSqDQAJ. Of >> course, your approach is more systematic - having advantages (e.g. >> consistency,verifiability) and disadvantages (e.g. readability for humans, >> can become very long, especially if fully expanded - for example >> elfzom1p1elfzo >> -> "element_finite set of sequential integers_minus_1_plus_1_element_finite >> set of sequential integers) compared with my suggestion. >> > > The problem is that the label "elfzom1p1elfzo" seems to be trying to fully > describe the theorem, which is a hopeless goal that causes more confusion > than it solves. I don't think anyone (except perhaps the author) could > figure out what the theorem states from this label (or even its expansion), > other than guessing it has something to do with half-open integer ranges > ("fzo"). But its size makes it hard to remember and to type. > This label originated from my early days as beginner using Metamath - in the meantime, I try to use shorter labels, and also changed some labels accordingly (see, for example, wlklenfislenpm1 -> wlklenvm1). Showing the expansion of elfzom1p1elfzo, however, should have been only an example that there may be cases in which the expanded acrynym *could* become very long. > > A label's purpose is to be a short identifier for a theorem. The > description provides more information, and finally the theorem itself > provides all of the information. All 3 of these can be searched to narrow > down candidate theorems to whatever degree of detail you want. The label > does not need to redundantly describe the theorem or its precise content. > I fully agree! > > All we need the label to do is to provide a hint about the nature of the > theorem and to be unique. This theorem is about membership of a successor > in a half-open integer range. The important pieces we need are "el" > (element), "p1" (successor), and "fzo" (half-open integer range). Unless > there are different variations that we need to distinguish, "p1elfzo" would > suffice. That's much easier to remember. Its expansion with an acronym > table would become "successor_element_halfOpenIntegerRange". > > If there are two versions, say one for the more general "N e. ZZ" and this > one for "N e. NN", we can use "p1elfzo" for the general one and "p1elfzonn" > for this one specialized for NN. (I'm not sure why elfzom1p1elfzo is > specialized for NN, but I'm not familiar with its uses.) > From my experience, the number of versions and variants can become very high, as more and more theorems are added to set.mm. With this in mind, the chance that labels become longer (in the future ) is high, even if your suggested rules are obeyed. Our approach to use/expand acronyms should take this into account. For the moment, however, I do not see any problem with your approach. > > Interestingly, "p1elfzo" is the last part of the original label, so the > original label partly had the right idea. > ;-) > It's just that it took it too far and attempted to describe the entire > theorem (unsuccessfully IMO). > :-( > Typically the conclusion is the part the user is most interested in. So a > possible rough guideline is to have the label provide a hint about the > conclusion and not (or rarely) say anything about the > hypotheses/antecedents. > That's a very good and reasonable guideline! Can it be officially documented somewhere? > > We also don't always need to fully describe the conclusion. For example, > "cos0" indicates the theorem provides the value for the cosine of 0, but we > need to look at the theorem itself to see what that value is. "cos0" is a > nice, concise label I would prefer over "cos0eq1". > 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/25495807-ddc8-4a90-bdf2-d55c32f77f72%40googlegroups.com.
