Using underscores in labels

[Alexander van der Vekens]

(Branch of thread "George Hotz, a 5+ hours video complaining about Metamath, with 14000+ views and 163 thumb up", see post https://groups.google.com/d/msg/metamath/XPYuatviNV0/3LtVDyu-DQAJ):

David A. Wheeler:

>> 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". ...

Norman Megill:
>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"?

David A. Wheeler:

Yes, I think squareroot_2_irrational is probably too long ( though as I noted above, I'd be interested to hear other opinions). But changing our label conventions so that underscores are between the abbreviations might be a good idea. That would produce labels of the form sqr_2_irr. That might make it a lot easier for people. Currently you have to know the entire set of abbreviations to read what the parts are. If you don't recognize the first abbreviation, it's harder to understand the rest. If we added underscore separators, it'd be much easier for newcomers to understand the label convention and be able to understand at least some of the parts. As the database gets bigger, it becomes harder and harder to remember all the abbreviations, so having a separator is starting to become more and more justifiable. We could make a few exceptions if you think that's important, e.g., for 2p2e4.

It also wouldn't add that much more space. I'm guessing there is an average of 4 abbreviations in a label, so we'd add an average of 3 underscores to each label. That means the average label would change from 5.8 to 8.8. That is very doable. It is not a killer in disk space, and it is also within your goal length for labels. Even if the average is 6 abbreviations, which I doubt, that would make the average label length 10.8 which isn't really all that bad, especially since the underscores are really just separators and thus easy to remember.

One nice side effect of using underscores as separators in labels is that we can instruct css break on underscores, which could improve the formatting in some cases.

It'd be a pain to rename everything, but that is something that can be done once and could be almost entirely automated.

Related posts afterwards

Mario Carneiro/David A. Wheeler(https://groups.google.com/d/msg/metamath/XPYuatviNV0/zI-ImZDEDQAJ):

On January 4, 2020 10:17:44 AM EST, Mario Carneiro <di....@gmail.com> wrote:
>On Sat, Jan 4, 2020 at 10:08 AM David A. Wheeler
><dwhe...@dwheeler.com>
>wrote:
>
>> But changing our label conventions so that underscores are between
>the
>> abbreviations might be a good idea.
>>
>> It'd be a pain to rename everything, but that is something that can
>be
>> done once and could be almost entirely automated.
>>
>
>I doubt this. Determining where the breaks are would be a highly
>nontrivial
>task that I would not trust to a computer without oversight, and it will
>hit almost all theorems, so this is not an easy task at all.

Oh, oversight would be absolutely necessary. I think a first cut could be partly automated by noticing which symbols exist, finding their df-NAME, and splitting by NAME in that label. But it would clearly take some time.

[Alexander van der Vekens]

I personally do not like to have underscores in labels. They make them longer, and the added value is not so high. Maybe for the given example ("sqr2irr" -> "sqrt_2_irr") this approach looks reasonable (although the "underscore version" is not really more comprehensible compared with sqrt2irr, from my point of view), but here are some additional examples:

• vtocldf -> v_to_cl_d_f
  
• recclzi -> rec_cl_z_i?
• leaddsub -> le_add_sub?
• brprcneu -> br_prc_n_eu?
• elfzom1p1elfzo -> el_fzo_m1_p1_el_fzo or even el_fzo_m_1_p_1_el_fzo?

Do we really want such labels? Are they really more comprehensible? I doubt this...

Alexander

[Norman Megill]

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 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 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

[Alexander van der Vekens]

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.

I wonder, however, where/how the acronym keys are placed. In principle, the three variants of my post mentioned above could be used:

1. First "sentence" of a comment, e.g. $( 3:2+eq+tr+4:3+d A deduction from three chained equalities. ... 
   
2. Special parenthetical, e.g. $( (acronym 3:2+eq+tr+4:3+d) A deduction from three chained equalities. ...
3. Additional information comment, e.g. $( $j acronym 3:2+eq+tr+4:3+d $)  $( A deduction from three chained equalities. ... 

Finally, it is also my opinion not to change the labels, but to use the acronyms in the html pages, either as tooltips (only) or in the pages themselves, as proposed in my post mentioned above:

Such an [acronym (maybe fully expanded)] could be used in the HTML outputs, both in the overview (new column "Title" or "Name" between columns "Label" and "Description") and for a single theorem (in a new line "Title: ..." between "Theorem <label>" and "Description: ....") and in the proofs (new column "Title" or "Name" or "Theorem" between columns "Ref" and "Expression").

Alexander

[Alexander van der Vekens]

On Sunday, January 5, 2020 at 6:23:22 PM UTC+1, Norman Megill wrote:

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.

I agree with Norm that introducing such new concepts like acronyms/keys or titles/names for theorems must be realized step by step. Whether their usage should be mandatory for new theorems very early must be discussed (advantage: consistency, no need for subsequent rework; disadvantage: may not be easy for people who want to contribute). The tools processing the new information can either ignore theorems without that information (as Norm said) or can use other information temporarily, e.g. the tooltips can continue to use the first part of the comment).

Alexander

[David A. Wheeler]

On Sun, 5 Jan 2020 09:23:21 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> I also dislike the idea of have to type 3_eq_tr_4_d instead of 3eqtr4d.

That's unfortunate. Okay, sounds like adding underscores to the
labels is off the table. That's okay, I'm just trying to identify
possible problems & possible solutions.

> 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

In most cases there shouldn't be multiple acronyms, since the acronyms
are mostly the NAME part of df-NAME. 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.

> 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'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.

> 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. ...

> Using the acronym key and acronym table, we could automatically reformat

> the labels throughout set.mm to be any one of the three forms ...

> 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

I don't think we want to do a lot of reformatting, that's a pain, and
in any case we want a *single* label for a given assertion.

But as a tool to help people understand the naming convention, an
acronym key might be very helpful for 2 reasons:
1. It could help new users learn the conventions in general.
I used Metamath for years before
I started to understand the naming convention.
2. It could help anyone (even old timers) understand why something
has a given name. Even if you
understand the convention in principle, most people only work on *parts*
of set.mm, and thus some of the abbreviations are often new.

> 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. :)

I think that metamath.exe should *not* try to reformat labels.

In fact, let's not check against some acronym table, at least for a very long while.
It's simply a hint to the reader about *why* the label has that label.
Trying to do that check would require the kind of detailed convention table that
we don't have today, and it will take us time to build up one.
If we don't do label-checking then the work on
metamath.exe is very easy: don't do anything.

If there's any checking at all, we could simply require
that new $a and $p statements include *an* acronym key.
That, at least, is easy. Once its *existence* is verified, we can use
humans to check it. In fact, once an acronym key is created, it'll
be a lot easier for people to check the label name (is that *really* what you meant?).

> 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...

I think phasing this in, slowly, is the only sane approach.
Thankfully, if it's done slowly it can just be done as part of the normal
process - no big deal.

> 3. It's yet one more thing developers must learn and use when adding new
> theorems.

Yes, though naming is already something developers have to learn if they
want to add something, so it's not much different from the current state.
And any existing acronym keys will help them learn naming, so
it may actually speed up their learning instead of being an impediment.

> 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.

If it's done slowly, phased in, it shouldn't be a big deal.

> 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?

--- David A. Wheeler

[Mario Carneiro]

My understanding of Norm's proposal is that this is a markup feature only. People won't actually look at 3:2+eq+tr+4:3+d -- it's no better than the original in terms of human readability -- but the index of "meanings" of 3:2 and eq and so on can be stored in a separate file so that it can parse 3:2+eq+tr+4:3+d and turn it into an interactive display, like

[3](triple)[eq](equality)[tr](transitivity)[4](fourth variation)[d](deduction form)

where the parentheses are hovers over the bracketed portions. The :NUMBER is necessary for this scheme to work, because otherwise there will be many bad glosses like [2](two) instead of [2](double).

I like this idea. It doesn't pollute the actual labels with additional data, but provides computer markup data for parsing and display purposes.

> 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.

The point is so that we don't have to give up our current ambiguous labeling convention (which is bad for computers but good for humans).

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.

That's what the +'s are for.

> 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. ...

> Using the acronym key and acronym table, we could automatically reformat
> the labels throughout set.mm to be any one of the three forms ...

> 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

I don't think we want to do a lot of reformatting, that's a pain, and
in any case we want a *single* label for a given assertion.

I think it would not be a good idea to change the labels in the public version of set.mm, but the existence of markup data makes it possible to perform a large scale rename like this easily and I don't see any reason why the tooling couldn't support it for people who want it.

 

But as a tool to help people understand the naming convention, an
acronym key might be very helpful for 2 reasons:
1. It could help new users learn the conventions in general.
  I used Metamath for years before
  I started to understand the naming convention.
2. It could help anyone (even old timers) understand why something
  has a given name. Even if you
  understand the convention in principle, most people only work on *parts*
  of set.mm, and thus some of the abbreviations are often new.

My vote would be to have this information show up in hovers over the title of the theorem, e.g. "Theorem [3][eq][tr][4][d]   2508" in the main header. It doesn't need to be everywhere, it's rather noisy after all.

> 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.  :)

I actually think it is time to revisit HTML generation as a whole, see if we can make something better by starting from scratch. The current mechanism is many layers of legacy code written for browsers of the 20th century. I'm sure if we think about the problem for a bit, lay out all the requirements, and consider currently available options, we can find a solution that is less verbose, more maintainable, more extensible, and looks better.

 

But that's probably a discussion for another thread.

I think that metamath.exe should *not* try to reformat labels.

In fact, let's not check against some acronym table, at least for a very long while.
It's simply a hint to the reader about *why* the label has that label.
Trying to do that check would require the kind of detailed convention table that
we don't have today, and it will take us time to build up one.
If we don't do label-checking then the work on
metamath.exe is very easy: don't do anything.

I don't see the problem with it being opt-in. It's just additional data that the web page can display if it is available, it's not something to verify (except possibly for welformedness).

If there's any checking at all, we could simply require
that new $a and $p statements include *an* acronym key.
That, at least, is easy. Once its *existence* is verified, we can use
humans to check it. In fact, once an acronym key is created, it'll
be a lot easier for people to check the label name (is that *really* what you meant?).

I wouldn't sweat any bad glosses. An automatic translation can get 90% or more of the theorems segmented and we can clean up the rest lazily, in the same way as typos on comments.

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?

I wish we would stop using the description comment for metadata like this. This is the sort of thing that makes markup parsing the rats' nest that it is. Just have a separate comment, with a sane computer-readable grammar. (It should also contain the "contributed by" and "usage discouraged" information, which are also metadata. Using english words just fools people into thinking there is no strict grammar.)

Mario

[André L F S Bacci]

On Mon, Jan 6, 2020 at 6:03 AM Mario Carneiro <di....@gmail.com> wrote:

On Sun, Jan 5, 2020 at 10:56 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Sun, 5 Jan 2020 09:23:21 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> I also dislike the idea of have to type 3_eq_tr_4_d instead of 3eqtr4d.

That's unfortunate. Okay, sounds like adding underscores to the
labels is off the table. That's okay, I'm just trying to identify
possible problems & possible solutions.

In most cases there shouldn't be multiple acronyms, since the acronyms
are mostly the NAME part of df-NAME. 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.

My understanding of Norm's proposal is that this is a markup feature only.

I would like to suggest the notion of alternative names. The short and unique label continues, but it can be commented with additional alternative names, what can be latter typed in GUIs to search for labels.

Say... $( $j altname '3_eq_tr_4_d'; altname '2 + 2 = 4'; $)

I'm not suggesting to add altnames to all set.mm initially, but a prevision of this would incentive experiments. To people who really like to have alternative names in all set.mm, external tools could then use external files to annotate the labels they most use, and a central repository could be used to post their personal altnames files to see if some consensus emerge.

André

[Benoit]

On Monday, January 6, 2020 at 7:03:23 AM UTC+1, Mario Carneiro wrote:

I wish we would stop using the description comment for metadata like this. This is the sort of thing that makes markup parsing the rats' nest that it is. Just have a separate comment, with a sane computer-readable grammar. (It should also contain the "contributed by" and "usage discouraged" information, which are also metadata. Using english words just fools people into thinking there is no strict grammar.)

I think this would go in the good direction.  I can make a loose analogy with another math hobby I contributed to: Neil Sloane's Online Encyclopedia of Integer Sequences (OEIS).  Every set.mm proof has its own webpage (in the Metamath Proof Explorer), which in some respects has similarities with each sequence of the OEIS and its webpage (e.g., each has a name/label, a comment, an author, a date, etc.).  The format is explained at http://oeis.org/eishelp2.html with a link to the description of the "internal format" (for an example, see e.g. http://oeis.org/A3).

Benoît

[David A. Wheeler]

On Mon, 6 Jan 2020 01:03:10 -0500, Mario Carneiro <di....@gmail.com> wrote:
> My understanding of Norm's proposal is that this is a markup feature only.
> People won't actually look at 3:2+eq+tr+4:3+d -- it's no better than the
> original in terms of human readability -- but the index of "meanings" of
> 3:2 and eq and so on can be stored in a separate file so that it can parse

> 3:2+eq+tr+4:3+d and turn it into an interactive display...

I think "eq+tr" *is* better for human readability than "eqtr", because then
the human *knows* that it's a combination of "eq" followed by "tr"
(instead of, say, some "eqt" followed by an "r"). So while it's okay for the
label to be unchanged, it *is* useful to have this information near the
assertion itself.

The problem for human readability is the proposed colon notation.
If you're going to use colons, it might be better to have a textual gloss
like "3:triple" instead of "3:2". Then I know which 3 is meant.

> I wish we would stop using the description comment for metadata like this.

I think putting the information in a *separate* file would be a mistake.
In my experience, every time you have separate datasets with the same key
(e.g., a label), you're creating a slow-running disaster.
The datasets will quickly go out of sync, and it will become difficult to *keep*
in sync. In contrast, if the information goes into the description, then
keeping things in sync is quite trivial, and errors become both obvious
and easy to correct later. In addition, if the information is right there,
it's easily accessible to later users and readers; if it's in a separate file,
it will often not be seen.

We could formalize the grammar of the description field & perhaps add some tweaks
to make it easier to parse in detail. I think that would be a better
direction than having a separate file that goes quickly out-of-sync and is rarely viewed.
We want things to be *easy* to maintain (correctly) over time, after all.

--- David A. Wheeler

[Mario Carneiro]

On Mon, Jan 6, 2020 at 12:03 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Mon, 6 Jan 2020 01:03:10 -0500, Mario Carneiro <di....@gmail.com> wrote:
> My understanding of Norm's proposal is that this is a markup feature only.
> People won't actually look at 3:2+eq+tr+4:3+d -- it's no better than the
> original in terms of human readability -- but the index of "meanings" of
> 3:2 and eq and so on can be stored in a separate file so that it can parse
> 3:2+eq+tr+4:3+d and turn it into an interactive display...

I think "eq+tr" *is* better for human readability than "eqtr", because then
the human *knows* that it's a combination of "eq" followed by "tr"
(instead of, say, some "eqt" followed by an "r"). So while it's okay for the
label to be unchanged, it *is* useful to have this information near the
assertion itself.

Humans are generally good at segmentation, and I don't think that the lack of segment markers in labels has been a significant problem historically (and there is some evidence in this thread that putting segment markers in would make readability worse). We can play with alternative displays on the web page and so on, but I would like to keep set.mm (labels and proofs) as they are currently.  

The problem for human readability is the proposed colon notation.
If you're going to use colons, it might be better to have a textual gloss
like "3:triple" instead of "3:2". Then I know which 3 is meant.

The point here is to centralize and enumerate all glosses for the meanings of label segments. Assuming that a program is used for transforming this data into something human readable, it doesn't bother me how it gets stored. But if we have longer glosses then these too need to be defined and possibly kept to a reasonable size.

 

> I wish we would stop using the description comment for metadata like this.

I think putting the information in a *separate* file would be a mistake.
In my experience, every time you have separate datasets with the same key
(e.g., a label), you're creating a slow-running disaster.

I didn't say it should go in a separate *file*, I said a separate comment. We used to have dates in separate comments, after the proof. We could do a similar thing with metadata, either before or after the theorem.

Label glosses are not directly related to theorems (because there is a many-to-many relationship between label segments and theorem labels), so it makes sense to have those stored separately.

 

Mario

[Alexander van der Vekens]

I also like the idea to remove the metadata from the comments and to provide them separately. Another analogy could be taken from Java - the annotations. For ~rucALT, for example, this could be as follows:

  $( $j @acronym r+uc+ALT

         @name real numbers are uncountable

         @author NM

         @since 13-Oct-2004

         @revised 13-May-2013 Mario Carneiro

         @shortened 13-Sep-2020 AV

         @discouraged usage proof_modification

         @references ~ ruc ~ rpnnen

  $)

  $( This proof is a simple corollary of ~ rpnnen , which determines the

      exact cardinality of the reals.  For an alternate proof discussed at

      ~ http://us.metamath.org/mpeuni/mmcomplex.html#uncountable ,

     see ~ ruc . $)
  rucALT $p |- NN ~< RR $=

@acronym, @author, @since would be mandatory, the rest optional. @revised, @shortened could occur more than once. The order may not be fixed (to be discussed).

To put the annotations into separate lines should not be mandatory, so so following would also be possible (but not recommended, in my opinion):

  $( $j @acronym ruc+ALT@name real numbers are uncountable

         @author NM @since 13-Oct-2004 @revised 13-May-2013

         Mario Carneiro @shortened 13-Sep-2020 AV

         @discouraged usage proof_modification @reference ~ ruc

  $)

  $( This proof is a simple corollary of ~ rpnnen , which determines the

      exact cardinality of the reals.  For an alternate proof discussed at

      ~ http://us.metamath.org/mpeuni/mmcomplex.html#uncountable ,

     see ~ ruc . $)
  rucALT $p |- NN ~< RR $=

Currently, the comment is as follows (does not have a "Proof shortened" parenthetical):

 $( Alternate proof of ~ ruc .  This proof is a simple corollary of ~ rpnnen ,
     which determines the exact cardinality of the reals.  For an alternate
     proof discussed at
     ~ http://us.metamath.org/mpeuni/mmcomplex.html#uncountable , see ~ ruc .
     (Contributed by NM, 13-Oct-2004.)  (Revised by Mario Carneiro,
     13-May-2013.)  (Proof modification is discouraged.)
     (New usage is discouraged.) $)
  rucALT $p |- NN ~< RR $=

We could, however, start with providing acronyms and/or names (which was the original intention of this topic) in such a way, but prepared for a future extension.

Alexander

[Norman Megill]

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

[Norman Megill]

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.

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.

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.)

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.

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".

Norm

[Norman Megill]

On Monday, January 6, 2020 at 1:03:23 AM UTC-5, Mario Carneiro wrote:
...

I wish we would stop using the description comment for metadata like this. This is the sort of thing that makes markup parsing the rats' nest that it is. Just have a separate comment, with a sane computer-readable grammar. (It should also contain the "contributed by" and "usage discouraged" information, which are also metadata. Using english words just fools people into thinking there is no strict grammar.)

 I understand your point and agree that is it something we need to revisit longer term.

However, practically speaking, the "(New usage is discouraged.)" and "(Proof modification is discouraged.)" tags are very clear in English to the user and have been quite successful in accomplishing their purpose, especially given that not all tools recognize them or implement them fully.  They are included in the main description so the user will see them and treat the axiom/theorem accordingly.  I think we would want to make sure all major assistants and IDEs adequately support these before hiding them in a $j comment.

As for the acknowledgments, shouldn't they really be part of the description as opposed to a $j directive?  Their purpose is just to inform the reader.   'verify markup' does some cursory checking for consistency, but they don't impact the way the theorem is treated by a proof assistant.  Recall that a few years ago we went the other way, moving the separate proof date stamp into the main comment.

Norm

[Alexander van der Vekens]

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

[ookami]

Hi,

I suggest reading https://en.wikipedia.org/wiki/Naming_convention and https://en.wikipedia.org/wiki/Naming_convention_(programming), the latter gives lists of pros and cons of possible strategies.

One interesting citation:

"The choice of naming conventions can be an enormously controversial issue, with partisans of each holding theirs to be the best and others to be inferior. Colloquially, this is said to be a matter of dogma"

Technically speaking, you are not reduced to just one identifier per theorem. In particular, you can provide a list of search keys, or maintain different conventions in parallel. The user picks his favorite then.

Wolf

[David A. Wheeler]

Norman Megill:

> > 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.
> >

On Mon, 6 Jan 2020 23:39:09 -0800 (PST), "'Alexander van der Vekens' via Metamath" <meta...@googlegroups.com> wrote:

> That's a very good and reasonable guideline! Can it be officially
> documented somewhere?

(and)

> > 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 with both.

I've just created a pull request that tries to document both points. See:

https://github.com/metamath/set.mm/pull/1390

I expect conversations about naming conventions to
occasionally arise. set.mm (and iset.mm!)
are becoming larger & larger, which is a good thing, and
that increase in scale is making it ever more important
to have clear names.

--- David A. Wheeler

[vvs]

Technically speaking, you are not reduced to just one identifier per theorem. In particular, you can provide a list of search keys, or maintain different conventions in parallel. The user picks his favorite then.

Yes, I agree. I'm not fond of any central authority to assign a lot of meaningful identifiers, that role should be best served by software tools. There are too many factors to consider and many possible solutions: hierarchical namespaces, tags, petnames, etc.