RFC: naming convention for `nonneg`/`pos`

Stream: general

[Jireh Loreaux]

This may be an unpopular opinion, but I'm hoping many will see the logic and agree: I think we should change the nonneg/pos naming convention.

I believe this has come up before, in part because it does not reflect standard terminology in French, which, as Anatole has just reminded me, is positif / strictement positif. The point is that "nonnegative" literally interpreted is ¬ x < 0, but we use it to refer to 0 ≤ x, and these are only equivalent in general for linear orders. Nevertheless, we use them in contexts that don't make sense:

• In the context of OrderedSemiring: this feels a bit weird because there may be no negative elements whatsoever, and there is no neg. An example might be C(X, R) where R is an topological ordered (semi)ring. In that case, there are elements which are neither positive nor negative.
• In the context of StarOrderedRing: see for example, the declaration docs#star_mul_self_nonneg and things nearby, where almost always the order will not be linear.
• In the case of the partial order on IsROrC this leads to some odd lemmas (if one reads it as ¬ x < 0) as evidenced in #6488
• In the context of linear maps, the condition 0 ≤ f (i.e., ∀ x, 0 ≤ ⟪f x, x⟫) is generally referred to as "positive"
• Likewise, in matrix theory, a selfadjoint matrix with eigenvalues satisfying 0 ≤ μ is "positive semidefinite"

Some potential replacement conventions are semipos/pos or pos/spos (spos for strictly positive). These changes would also entail semineg/neg or neg/sneg convention for x ≤ 0/x < 0. Of course, this conflicts with naming for -x, but that conflict is already present for the current nonpos/neg convention.

Another consideration is that some lemmas in Std (e.g., docs#Nat.one_pos) would also need to be changed (otherwise it would get tremendously confusing).

[Ruben Van de Velde]

Should PNat become SPNat, then?

[Eric Wieser]

And I suppose ENNReal then becomes EPReal

[Ruben Van de Velde]

Maybe true mathlib style would be not to use either term and use zero_le and zero_lt instead

[Jireh Loreaux]

Actually these exceptions are explicitly covered in the #naming conventions. (plug for the PR to update this page to Lean 4)

[Yury G. Kudryashov]

/poll Naming convention for 0 < x / 0 ≤ x
pos/nonneg (status quo)
pos/semipos
spos/pos
pos/zero_le
zero_lt/zero_le

[Jireh Loreaux]

Note: one reason I really don't like zero_le is that it doesn't generalize nicely to things like linear maps, especially not when referring to the types of those maps that satisfy 0 ≤ f (same for ℝ≥0).

[Yury G. Kudryashov]

Isn't pos for ≤ too French?

[Jireh Loreaux]

As I mentioned above "positive" is standard for 0 ≤ in certain contexts in English. Moreover, I hear plenty of English speakers refer to 0 ≤ as "positive" in casual conversation, even if they use "nonnegative" in more formal situations.

[Rémy Degenne]

I like that the current system uses the same words than the standard English math usage (in most contexts). These are not the words I would have chosen if that standard did not exist and I had to adapt to those unintuitive words when the language I use to do math switched from French to English, but I think that keeping mathlib close to informal math is important. It lowers the barrier to entry.

[Jireh Loreaux]

Another consideration in favor of the spos/pos convention is the analogy with docs#StrictMono / docs#Monotone

[Jireh Loreaux]

fwiw, I have heard native English speakers refer to (0 : ℝ) < x as "x is strictly positive". My advisor was one who often adopted this convention, and he is not a French speaker. Likewise, I think in analysis it is common to refer to a < b as a strict inequality when contrasting with a ≤ b.

[Johan Commelin]

I'm used to saying "strictly positive" since high school, I think... (@Floris van Doorn wasn't that the terminology used at our IMO trainings?)

[Kevin Buzzard]

In the UK I think "strictly positive" is rare, but "strict inequality" is normal for < vs <=

[Anatole Dedecker]

Rémy Degenne said:

I like that the current system uses the same words than the standard English math usage (in most contexts). These are not the words I would have chosen if that standard did not exist and I had to adapt to those unintuitive words when the language I use to do math switched from French to English, but I think that keeping mathlib close to informal math is important. It lowers the barrier to entry.

I think this is probably the main argument against switching. The thing I'm not sure about is how "systematic" it is. Is the situation "this is the common convention, but people frequently change convention if needed" or rather "even with a warning, reading a paper with another convention is confusing"?

[Jireh Loreaux]

For an "unbiased" reference for English language usage, a Google Ngram. Note that these are not comparing exactly the same thing: we're comparing 0 ≤ x under one convention to 0 < x under a different convention. This is because including "positive" would introduce far too many false positives (pun intended! :laughing:).

I expect that "nonnegative" could come up relatively rarely, but a nonzero percentage of the time, in generic English texts. In contrast, I would bet that virtually all occurrences of "strictly positive" are in mathematical texts.

[Jireh Loreaux]

At the very least, it's interesting to see when the hyphenation switch occurred. It's quite clearly 1962, but I'm not sure why.

[Eric Wieser]

Here's the same ngram for x \le 0

[Jeremy Avigad]

With my American undergraduate and graduate training in mathematics, I interpret "x is positive" as "x > 0." Webster agrees with me:
https://www.merriam-webster.com/dictionary/positive
Wikipedia lists both interpretations:
https://en.wikipedia.org/wiki/Sign_(mathematics)#Terminology_for_signs

[Thomas Murrills]

spos is ok if you know what it means, but, well, it's now another thing to know the meaning of (and the s is different than the one in, say, smul). Imo that counts against it.

One other possibility is qualifying both names, maybe as strictlyPos/semiPos—then there's no unqualified pos lying around waiting to be ambiguous! :P

[Thomas Murrills]

I also think there's virtue to banishing pos in the most general cases, such as 0 ≤ x, and reserving it only for when it's part of a very specific thing (such as e.g. positiveDefinite/positiveSemidefinite). The fewer ways there are to spell things, the easier it is to find them—since we can already spell 0 < x/0 ≤ x with the words we have (and, crucially, spell it simply with the words we have)...maybe that's the best option. (By these metrics, of course.)

[Notification Bot]

13 messages were moved from this topic to #general > Strong less than on functions by Eric Wieser.

[Eric Wieser]

(I broke that link, the messages are here)

[Damiano Testa]

Here is my usage in informal maths.

• If I say "nonnegative" I assume that I am clearly asserting that zero is allowed.
• If I say strictly positive, I am clearly asserting that zero is not allowed.
• If I say positive, I personally think that I am excluding zero, but will keep in the back of my mind that I could be misunderstood.

I normally use positive only when I don't really care about the zero case and, depending on context, it could be trivially included or trivially excluded.

Overall, the mathlib convention aligns well with how I would like my audience to parse what I say!

[Kalle Kytölä]

The currently second most popular option zero_lt/zero_le has the virtue of being systematic, but I find it strange that this naming appears to promote $0$ to an important player in results that in my opinion have very little to do with zero! And I fear that the initial impression they leave to the informal mathematician or a newcomer to formalization is not one of awe ("remember to search for results about positive operators by the zero_le substring").

[Kalle Kytölä]

Is it totally heretic to allow pos as a part of naming for both 0 < x and 0 ≤ f, if the word positive is commonly used with that meaning in (English) mathematical literature of the relevant area? (When diasmbiguation is urgently needed, one could still choose to deliberately use the longer strictly_pos/nonneg or even zero_lt/zero_le). Do I dare to even add the heretic ambiguous option to the poll? [EDIT: I did, but I didn't yet dare to vote for it :sweat_smile:.]

[Eric Wieser]

Kalle Kytölä said:

Is it totally heretic to allow pos as a part of naming for both 0 < x and 0 ≤ f, if the word positive is commonly used with that meaning in (English) mathematical literature of the relevant area?

The problem arises when you want to use more general results when working in that area. Now half your lemmas are called nonneg and the other half pos, and the only way to know which one to use is to look for both and see which exists!