Overloading symbol names

[Alexander van der Vekens]

In my latest PR, I provided a function mapping a set of integers to their

least common multiple (~df-lcmf:  ( _lcm `` s ) ) in addition to the operation calculating the least common multiple of two integers (~df-lcm: ( m lcm n ) ), contributed by SR.

For the typesetting, however, I used the same representation "lcm" for both symbols ` lcm ` and ` _lcm ` - because it is clear by the context which definition is used. If you look at the theorems in section 6.1.10  The least common multiple, then there should be no doubt that this overloaded representation is not a problem. Only the definitions look a little bit strange. Actually, the typesettings are different:  lcm used as operation has a leading and a trailing blank, lcm used as function has not (according to our typography conventions).

If anbody has objections against this overloading, and suggestions how the current typesettings could be improved, I am open to change it.

By the way, it seems a little confusing at the first glance that the least common multiple
is defined by a supremum.  Actually, it is an infimum, because the inverse of
"less than" ` ``' < ` is used to turn supremum into infimum - currently we
don't have infimum defined separately. Since this is noted in set.mm on several occations. it may be worth to think about providing a separate definition for infimum...

[Steve Rodriguez]

I see no ambiguity there; it's actually clear to me which gets used where.  The use of infimum made perfect sense given that the supremum is what puts the 'g' in gcd; it's probably best that it be kept in that unseparately-defined limbo state lest needed support theorems blow up set.mm's size...

I'll admit I'm just happy to see lcm in the main area, and better elaborated!  It was part of my own private experiments long ago now with Goldbach—or rather examinations of some proofs of it that are, well, "not generally accepted by the mathematical community"—that couldn't prove or disprove anything one way or another and really just went nowhere.  My already-scant time for that or the Riemann-related stuff I'd hoped to try has since flatlined.

[David A. Wheeler]

>For the typesetting, however, I used the same representation "lcm" for
>both
>symbols ` lcm ` and ` _lcm ` - because it is clear by the context which
>definition is used.

I would prefer that there be a typographic way to distinguish them, though it's fine if the distinguishing mark is subtle. They are different symbols, used in slightly different ways, so I think they should look different.

--- David A.Wheeler

[Norman Megill]

On Sunday, August 30, 2020 at 4:53:58 AM UTC-4 Alexander van der Vekens wrote:

In my latest PR, I provided a function mapping a set of integers to their

least common multiple (~df-lcmf:  ( _lcm `` s ) ) in addition to the operation calculating the least common multiple of two integers (~df-lcm: ( m lcm n ) ), contributed by SR.

For the typesetting, however, I used the same representation "lcm" for both symbols ` lcm ` and ` _lcm ` - because it is clear by the context which definition is used. If you look at the theorems in section 6.1.10  The least common multiple, then there should be no doubt that this overloaded representation is not a problem. Only the definitions look a little bit strange. Actually, the typesettings are different:  lcm used as operation has a leading and a trailing blank, lcm used as function has not (according to our typography conventions).

"Clear by context" makes the implicit assumption that the reader has some higher-level knowledge of material involved.

From the MPE Home Page: "With no prior knowledge of advanced mathematics or even any mathematics at all, you can jump into the middle of any proof, from the most elementary to the most advanced, and understand immediately how the symbols were mechanically manipulated to go from one proof step to another, even if you don't know what the symbols themselves mean." That isn't possible if the reader has to understand context in order to interpret the displayed symbols.

Up to now we have been careful not to overload the displayed symbols (to my knowledge). For example, we distinguish various kinds of "+" with subscripts, unlike most of the literature (which has a different and complementary goal, which is to provide the reader with an informal higher-level understanding).

I find http://us2.metamath.org/mpeuni/lcmfun.html a little jarring even though as a somewhat higher-level user I can distinguish the two lcm's. The "Syntax hints" below the proof become less useful since the two lcm symbols can't be distinguished there.

Norm
 

[Norman Megill]

On Sunday, August 30, 2020 at 4:53:58 AM UTC-4 Alexander van der Vekens wrote:

By the way, it seems a little confusing at the first glance that the least common multiple
is defined by a supremum.  Actually, it is an infimum, because the inverse of
"less than" ` ``' < ` is used to turn supremum into infimum - currently we
don't have infimum defined separately. Since this is noted in set.mm on several occations. it may be worth to think about providing a separate definition for infimum...

Yes, perhaps the time has come to provide infimum and retrofit existing uses of `' <.

Norm 

[Norman Megill]

On Sunday, August 30, 2020 at 9:38:20 AM UTC-4 Norman Megill wrote:

... 

Up to now we have been careful not to overload the displayed symbols (to my knowledge). For example, we distinguish various kinds of "+" with subscripts, unlike most of the literature (which has a different and complementary goal, which is to provide the reader with an informal higher-level understanding).

Actually that isn't strictly true:  we have df-an vs. df-3an, df-sn vs. df-pr, and a few others.  But I still think it would be useful to distinguish the two lcm's in some subtle way, especially since in from a grammatical point of view they are identical (both class constants) and can't be distinguished by parsing, unlike the examples I gave.  An easy way is bold font for one of them, but the aesthetics of that may not be ideal.  Any suggestions?

Norm

[Mario Carneiro]

Well, those are counterexamples to the claim that every syntax constructor uses a unique symbol, but they are not counterexamples to the claim that the mapping from ascii token to HTML display is injective, and until now this property has been maintained, in some cases even when this goes against the traditional notation; pi the constant vs the prime pi function come to mind.

I think that underlining would be the most appropriate distinguishing mark in this case, since we already use underlined versions to indicate "class" versions of set functions, it seems natural that it could be used for the set extension of the integer function.

Mario

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/a0864256-f905-4253-a14e-f87de312791en%40googlegroups.com.

[Alexander van der Vekens]

Since most of the people have objections against using the same (looking) HTML-representation of two different symbols, I will change it. I think Mario's proposal using underlining is a good solution. This will result in the following  typesetting definition for the symbol ` _lcm `.

htmldef "_lcm" as "<U>lcm</U>";
  althtmldef "_lcm" as "<U>lcm</U>";
  latexdef "_lcm" as "\underline{\rm lcm}";

Thanks a lot for your contributions to this discussion.

Alexander

[David A. Wheeler]

On Sun, 30 Aug 2020 08:06:35 -0700 (PDT), "'Alexander van der Vekens' via Metamath" <meta...@googlegroups.com> wrote:
> Since most of the people have objections against using the same (looking)
> HTML-representation of two different symbols, I will change it. I think
> Mario's proposal using underlining is a good solution. This will result in

> the following typesetting definition for the symbol ` _lcm `...

Sounds like a great solution. Thanks for asking!

--- David A. Wheeler