Naming convention when the name is too long

Stream: general

[Jiang Jiedong]

Hi everyone,

Are there principles on when and how to use abbreviations for excessively long names? For example, I wanted to define something called "IsPerfectoidPseudoUniformizer" and "IsStrongPerfectoidPseudoUniformizer" (35 characters). These names are too long to be used conveniently in a theorem, especially when a line is limited to 100 characters.

However, IsSPPU is too vague and the pseudo-uniformizer is often abbreviated to psu instead of pu. It seems to me that IsStrongPerfectoidPsU or IsStrongPPsU is a better name.

At least I want to ask two explicit questions about this.

1. When is a name too long? Should we avoid creating names (names of definitions at least) with more than ~30 characters in mathlib?
2. Should the abbreviation for the pseudo-uniformizer be PsU, PSU or Psu in upper camel case?

[Yaël Dillies]

Is there any chance you can shorten the name by putting it in a namespace. Eg, without knowing the maths, I would suggest Perfectoid.IsPseudoUniformizer

[Jiang Jiedong]

It is more like IsPerfectoidPseudoUniformizer = IsPseudoUniformizer + something more. So I guess in this case, putting it in a namespace would not be the best choice?

[Andrew Yang]

Maybe IsPseudoUniformizer.IsPerfectoid?

[François G. Dorais]

This is also useful:

open Vector renaming toArray -> vtoa

[Yury G. Kudryashov]

This doesn't help with lemmas names that should include this long name as a part

[François G. Dorais]

I'm not sure I understand. This works fine:

namespace U1.U2
structure S where a : Nat
end U1.U2
open U1 renaming U2.S.a -> b
#check b

[François G. Dorais]

Oh! I just got it! This doesn't work without the dummy U2 structure.

namespace U1
structure U2
namespace U2
def a := 1
end U1.U2
open U1 renaming U2 -> uu
#check uu.a

[François G. Dorais]

It doesn't have to be a structure, anything will work:

namespace U1
def U2 := ((),0)
namespace U2
def a := 1
end U1.U2
open U1 renaming U2 -> uu
#check uu.a

[François G. Dorais]

So the issue is that namespaces aren't "things" unless there is a "thing" with that name. I think that could be fixed.

[Yury G. Kudryashov]

The issue is that according to the naming convention, a lemma about IsStrongPerfectoidPseudoUniformizer should be called something like isStrongPerfectoidPseudoUniformizer_iff_something_else. If you use 2 or 3 notions with very long names in a single lemma, then the theorem name can exceed 100 characters.

[François G. Dorais]

That's the official name. Technically it only has to be used once. That's why renaming is handy!

[Johan Commelin]

Renaming doesn't effect how you name results about a definition, right?
So it will make the statements shorter, but not the names of the statements.

[Jon Eugster]

To answer question 2.: I think the right case would be all capitalized uniformly as if it was a single letter: PSU, isPSU is...PSUniformizer, psu_eq_psuniformizer
(that's only about the capitalisation of abbreviations, not about what's actually the best name in this case)

[David Ang]

Instead of IsEllipticDivisibilitySequence I had IsEllDivSequence with docstrings explaining what they are

[Yury G. Kudryashov]

@Jon Eugster Why PSU, not PsU? ps comes from one word, cf MvPolynomial.

[Jon Eugster]

Maybe Im wrong, my bad. I was thinking of

6. Aronyms like LE are written upper-/lowercase as a group, depending on what the first character would be.

[Ruben Van de Velde]

Should it be MVPolynomial? :innocent:

[Etienne Marion]

Jon Eugster said:

Maybe Im wrong, my bad. I was thinking of

6. Aronyms like LE are written upper-/lowercase as a group, depending on what the first character would be.
   

For me acronyms mean taking first letters of different words and putting them together to get a word. Typically I think "LE" stands for "Less or Equal". So it's not the same as "Ps" which is an abbreviation. Correct me if I'm wrong.

[Jz Pan]

What if you split IsPerfectoidPseudoUniformizer into two classes IsPerfectoid + IsPseudoUniformizer? And in the results only mentions the most important assumption?