I fully agree with Norm that we should not change our general
conventions/usage of labels as "identifiers": they should be short, concise
and consistent (besides the primary property of being unique). Of course we
should still continue to improve the conventions and their usage.
Since labels and comments seem to be not sufficient to understand theorems
and their proofs, the introduction of "names" or "titles" for theorems may
help. Actually, many comments consists of a name/title only (besides the
parentheticals),
e.g. ~necom: $( Commutation of inequality. (Contributed by NM,
14-May-1999.) $),
or the first sentence is like a name/title,
e.g. ~cramer: $( Cramer's rule. According to Wikipedia ... $).
In many cases, however, the comment contains more information, and a
name/title cannot be "extracted" easily/automatically,
e.g. ~ixpn0: $( The infinite Cartesian product of a family ` B ( x ) ` with
an empty
member is empty. The converse of this theorem is equivalent to the
Axiom of Choice, see ~ ac9 . (Contributed by Mario Carneiro,
22-Jun-2016.) $)
I think the name/title of this theorem could be "Infinite Cartesian product
with empty member". To identify names/titles of theorems, we either can use
conventions (for example the first sentence of a comment, or the part of
the first sentence up to the first punctuation mark) or a special
parenthetical - for ~ixpn0 for example:
$( (Title: Infinite Cartesian product with empty member) The infinite
Cartesian product of a family ` B ( x ) ` with an empty ...
or an additional information comment - for ~ixpn0 for example:
$( $j title Infinite Cartesian product with empty member $)
$( The infinite Cartesian product of a family ` B ( x ) ` with an empty ...
Such a name/title could be used in the HTML/LATEX 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"). At
least such a name/title could be used as hover information (instead of
using the first part of the comment, which could contain more informatioin
than necessary/useful, e.g. for ~usgrass the hover text is "An edge is a
subset of vertices, analogous to ~ umgrass . (Contributed by Alexander..."
- "An edge is a subset of vertices" would be better/sufficient).
What do you think about this approach?
On Saturday, January 4, 2020 at 4:12:24 AM UTC+1, Norman Megill wrote:
>
> On Friday, January 3, 2020 at 6:56:21 PM UTC-5, David A. Wheeler wrote:
>>
>>
>> > 2. Cryptic labels: He is ranting while faced with theorem names on the
>> HTML
>> > page of sqr2irr. No clue whatsoever what they mean. Compares this to
>> more
>> > explicit names found in competing products, and in program code in
>> > general. I think there is indeed headroom for improvement here. Maybe
>> a
>> > pop up showing an explanation while hovering over a name alleviates the
>> > situation.
>>
>> Huh? There *is* a pop up showing an explanation when hovering over a
>> name,
>> in both the GIF and Unicode versions. Try it out! Just go here:
>> http://us.metamath.org/mpegif/sqr2irr.html
>> and hover over any of the theorem names; you'll see the first sentence of
>> the theorem
>> comment displayed. For example, step 5 uses breq2 ; just put your
>> mouse over that and it displays "Equality theorem for a binary
>> relation..."
>>
>
> The primary purpose of a label is to identify a theorem uniquely. In
> books this is accomplished with equation/theorem numbers, which are much
> more cryptic than our labels but don't seem to bother the readers or at
> least the author. Principia Mathematica was written entirely with nothing
> but numeric labels with the exception of a handful of very common cases
> like Simp and Syl. The reader gets used to "*2..." being mostly about
> implication, negation, and disjunction, "*3..." about conjunction, "*4..."
> about biconditional, etc. We try to provide at least a hint of what the
> theorem is about using our conventions, but an unambiguous description of
> the theorem is impossible to achieve, and we don't pretend that it does.
> Information about the theorem is provided by its description and its actual
> content, just like in books. Both of these are searchable and are the main
> ways that I locate a theorem whose name I forgot, perhaps assisted by a
> label with wildcards. Both are instantly available for the reader in a web
> page proof either by hovering over the label or clicking it.
>
> Note that at the top of set.mm I added a link to label conventions.
>
> For me personally, an important reason to keep labels short is to make
> them easier to type. Maybe this isn't everyone's experience, but I find it
> easier to remember labels that are shorter (especially if they follow a
> convention, which we try to do). To remember a long label means having to
> remember all pieces of the label, their order, and, since they are never
> going to be spelled out in full English, what abbreviations were chosen.
> There seems to be a threshold label length of maybe around 8 to 10
> characters where I start to make mistakes typing it in (after glancing at
> it in another window) and end up resorting to copy/paste, slowing me down.
>
> The Wikiproofs site (wikiproofs.org) seems to be down, but looking it up
> on archive.org it uses theorem labels like
> "introduceBiconditionalFromImplicationsInConsequent". Personally I think
> that would slow me down and I would dislike it. IIRC Jim Kingdon
> contributed to that project, and it would be interesting to hear his
> experience with long labels.
>
> Currently, the longest label in set.mm is aiffnbandciffatnotciffb, which
> is in a mathbox. While it attempts to describe the theorem, it doesn't do
> so unambiguously, and I doubt I could remember its exact spelling even long
> enough to type it without making a mistake unless I looked directly at it.
> We would almost certainly change it to a much shorter label should it be
> moved to the main set.mm.
>
> Another smaller consideration is the set.mm file size. Inside of proofs
> in the current set.mm, there are 1.1 million instances of labels with an
> average length of 5.8 bytes. Each extra byte of average label length would
> add a megabyte to the file size. (The 5.8 length is distorted by short
> labels for syntax axioms, and the average label length for just theorems,
> which I didn't calculate, would be longer.)
>
>
>> I do agree that the pop-ups are not very discoverable (if you don't know
>> they
>> are there, it's not obvious to try it out). Also, hover doesn't work on
>> most
>> mobile devices (touch screens generally can't hover), and mobile devices
>> are
>> the most common way to view HTML pages (though they CAN detect a
>> click-down).
>>
>> POTENTIAL IMPROVEMENT:
>> Maybe there'd be a way to the hover information more discoverable
>> AND modify things so it's invokable in mobile devices (say by onclick).
>>
>
> I don't know how to solve the mobile problem, but for PC browsers perhaps
> it would be useful to add to each page a sentence on each page saying
> something like, "Hover over a label link for more information."
>
>
>>
>> The underlying Metamath language doesn't require short names, it's simply
>> a
>> convention in set.mm, iset.mm, and many others.
>> We do have naming conventions, but it's fair to say that the names aren't
>> too obvious.
>>
>> I'd be fine with longer names, though I don't know if others would be.
>> In a few cases we have short names that perhaps could be a little longer,
>> e.g.,
>> "sqr" is currently short for "square root" in set.mm, but that is
>> arguably
>> ambiguous with "squre"; we could use "sqrt" instead.
>> 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".
>> We could even spell things out more fully, e.g.,
>> "squareroot_2_irrational".
>> Metamath tools won't have any problem with that, and compression tool
>> like zip will compress that to a similar size, though of course the
>> expanded file would be a lot bigger.
>>
>
> Our current square and square root conventions are "sq" and "sqr" resp.
> I'm almost certain I've seen "sqr" used for square root in at least one
> computer language although I can't recall which one right now. I don't see
> the problem with omitting the "t" since any confusion is instantly resolved
> by hovering over the label, if the content of the proof step doesn't make
> it obvious. If people are truly confused by this, I suppose we can add the
> "t", but until now no one has complained about it.
>
> 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"? does it have "is"? why isn't it "square_root" since
> they are 2 words in English?). And theorems that can be described
> unambiguously like this one in a few words are very rare. Our convention
> is pretty clear on the abbreviations "sqr", "2", and "irr", making
> "sqr2irr" easy to remember (for me at least) and type.
>
> 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/1f28ae3a-18a6-4350-93f3-104f6951bd61%40googlegroups.com.
