American or British English?

Stream: mathlib4

[Fernando Chu]

Currently, Mathlib uses both American and British English; here are some arbitrary examples:

• MonoFactorisation and Nat.factorization.
• Booleanisation and Localization.
• fibre_antichain' and FiberBundle.

I think having one canonical choice of spellings would be useful both for users and contributors. From what I can tell, American spelling is used the most. Should the contributor guidelines specify this choice?

[Sébastien Gouëzel]

No, it's a personal language choice from the contributors, and we respect these unless there is a clear mistake.

[Sébastien Gouëzel]

(I've just recently asked a contributor to change from disc to disk to avoid a possible confusion with the discriminant)

[Eric Wieser]

I'd also be in favor of making a choice here. Note that the language has initialize built in, so I think we should at least standardize on ize spellings

[Fernando Chu]

/poll Maybe it's useful to have a poll. What should the standard spelling be?
American English
British English
Both, choice of the contributor
Other

[Eric Wieser]

(see https://en.wikipedia.org/wiki/Oxford_spelling for the option I added regarding ize)

[Wrenna Robson]

Eric Wieser said:

(see https://en.wikipedia.org/wiki/Oxford_spelling for the option I added regarding ize)

This is fun.

[Ruben Van de Velde]

Quite surprised (surprized?) by the poll results given how big we are on consistency otherwise (otherwize?)

[Wrenna Robson]

It's really opened my eyz.

[Fernando Chu]

I'm also quite surprised by the poll results. Maybe people that have voted for both are considering a case where the contributor has strong opinions on the spelling, in which case I'd agree that then we should respect this. But I'd imagine that most of the people wouldn't actually mind changing it just so that its consistent with the rest of the library. I.e., we could have both but suggest (not enforce) only one spelling.

[Edward van de Meent]

i guess my opinion is that indeed we should have a standard, but should not enforce it for PRs (since i can see that causing PRs to strand). instead, i can see it as a style recommendation, in addition to accepting style PRs which change spelling exactly when it follows this standard.

[Floris van Doorn]

I think in declaration names we should have a consistent spelling, especially for as long as we're searching for declarations by name.
For documentation I think it should be up to the contributor (standardizing that is more work than it is worth).

[Ruben Van de Velde]

Given the first post in the thread, I assumed we were talking about declarationz

[Damiano Testa]

Maybe we should have a to_american_spelling attribute, analogous to to_additive.

[Jireh Loreaux]

I think that's a joke, but in case not, please no.

[Ruben Van de Velde]

I think it'd be a very interesting engineering challenge, but also please no :)

[Damiano Testa]

I sometimes forget that in writing it is harder to know when something is a joke, but I definitely meant it as a joke! :slight_smile:

[Kenny Lau]

I think we should have a better abbreviation system (sorry, abbrev is not good enough) so that we can just have two spellings for the same thing

[Violeta Hernández]

Ruben Van de Velde said:

Quite surprised (surprized?) by the poll results given how big we are on consistency otherwise (otherwize?)

This feels a bit too bikesheddy even for me. There's a lot of contributors that are from neither the US or the UK, we all have our own idiosyncratic writing styles, and trying to police that just feels excessive (unless we're talking about actual grammatical mistakes, of course)

[Eric Wieser]

As Floris says, writing styles in docstrings are quite a different game to "writing style" in declaration names

[Eric Wieser]

I think we should update #naming to explicitly specify a particular version of english, just as I think we should provide guidelines on whether to use ascii versions of accented words (eliding umlauts etc).

[Violeta Hernández]

How many declaration names do we have that are American/British sensitive? I guess there's disc/disk from earlier, what else?

[Kevin Buzzard]

As has been noted in the first post, there's fibre/fiber and ise/ize.

[Violeta Hernández]

hm. Then I do agree that we should standardize one or the other convention for declaration names. My preference is obviously for American but I don't care too much either way.

[Monica Omar]

Usually in coding languages, the standard is American: color not colour, etc
So I think it should be fiber, not fibre. Same way we have center and not centre.

[Mauricio Collares]

If this is a webdev reference, then I look forward to writing "referer" for familiarity reasons.

[Kim Morrison]

Shall we agree that for naming purposes only, American spellings and avoiding accents is preferred?

[Jakob von Raumer]

Goedel or Godel, then?

[A.]

Kim Morrison said:

Shall we agree that for naming purposes only, American spellings and avoiding accents is preferred?

Would I be correct in interpreting this as the "official" decision and that it trumps the poll?

[Michael Rothgang]

I think there are two distinct questions in this thread:

• how to name declarations (decision: American spelling)
• writing style in comments (where the poll supports "author's discretion, with reasonable local consistency")

[A.]

Ok so there is an official decision for declarations and in the absence of an official decision for comments we respect the poll.

[Kevin Buzzard]

I think that opinions of three maintainers in a thread that many maintainers might not even be reading is not an official decision.

[Floris van Doorn]

A. said:

Would I be correct in interpreting this as the "official" decision and that it trumps the poll?

The poll above is flawed in the sense that it was unclear whether it was about documentation or declaration names (as mentioned in some comments). My message that there should be consistent spelling in declaration names was upvoted by people that voted differently in the poll.
We're now also discussing this within the maintainer stream.

[Violeta Hernández]

I've said this before, but I think avoiding accents when we so liberally use Unicode throughout Lean is a bit of a weird decision.

[Niels Voss]

I think we should use unicode in declaration names iff the benefits exceed the costs. Unicode actually has quite a large cost: it requires a special input system, prevents you from typing Lean on Zulip, GitHub, and the mathlib docs, slows down typing, requires users to memorize more inputs, and can introduce ambiguity, and some software fails to handle it properly (e.g. I had a minor issue with the neovim VSCode extension). Of course, for Lean, the benefits of unicode exceed the costs, but whether this trade-off is worth it is situational, and just because we are using unicode somewhere doesn't mean we should be using it everywhere.

So I guess, the question is, what are the costs and benefits of unicode for declaration names? I think a clear benefit is that it is more faithful to the original names of mathematicians, and the main costs are what I have stated above.

[Timothy Chow]

How much Unicode are we talking about? There are proper names of course (Erdős, Plücker, Čech, Teichmüller, L'Hôpital, etc.). Other than that, I can't think of many commonly used mathematical terms that use Unicode (étale, dévissage, problème des ménages) unless we count Greek letters (σ-algebra, λ-calculus, Δ-matroid), but I would expect most people would be in favor of spelling out Greek letters in declaration names.

[Timothy Chow]

Computer algebra systems have already had to face this issue, and the ones I know of seem to have gotten along fine without using Unicode in function names.

[Timothy Chow]

If the main envisaged use of Unicode is for declaration names is for diacritics, then another possible ambiguity to watch out for is the difference between precomposed characters and combining characters. For example, é can be represented as the precomposed character U+00E9 or as U+0065 followed by the combining acute accent U+0301.

[Ruben Van de Velde]

How about for the Чебышёв polynomials?

[Kevin Buzzard]

Niels Voss said:

Of course, for Lean, the benefits of unicode exceed the costs

There's a big difference between unicode notation (yes please) and unicode being used in declaration names (much less sure).

[Jireh Loreaux]

I think the biggest issue with declaration names, aside from "do we actually want it?", is that it would require a change to core for which unicode characters are allowed in identifiers, otherwise we would have to use quotes for all these unicode identifiers.

[Yury G. Kudryashov]

Ruben Van de Velde said:

How about for the Чебышёв polynomials?

The Russian translations of https://en.wikipedia.org/wiki/Problems_and_Theorems_in_Analysis translated https://en.wikipedia.org/wiki/George_P%C3%B3lya as "Г. Полиа" while the Russian translations of some other books used "Д. Пойа". You can't guess that it's the same person from RU translations only.

[Weiyi Wang]

Чебышёв isn't a translation, is it?

[Yury G. Kudryashov]

It's the Russian original spelling (kind of, the original spelling is Чебышевъ, there was a spelling reform short after the revolution). It reminded me about troubles caused by different transliterations of another name. Sorry if it was offtopic.

[Kim Morrison]

Discussion amongst the maintainers has converged on the consensus that for declaration names, we should be using American English spellings.

[Kim Morrison]

That discussion didn't address using accents. (Certainly we should not be doing any mass edits of the existing library to add or remove use of accents. Further discussion is needed here; my take is that we should avoid accents in declaration names.)

[Kim Morrison]

Would anyone be interested in preparing a PR for #naming about this?

[Floris van Doorn]

leanprover-community/leanprover-community.github.io#703
I took the liberty to document both that declarations use American English spelling, and that documentation is the author's choice.

[Floris van Doorn]

Both of these points seem to have broad consensus, based on polls/reactions in this thread.

[Nick_adfor]

For developers from non-Anglophone countries, this issue can feel like watching a fire from the opposite shore—somewhat distant and abstract.

Since there’s a playful tone here, I’ll share a joke as well. My forum nickname, when translated into Chinese, should be “傅醴柯.” “傅” is a common Chinese surname meaning “to teach” or “master.” “醴” means “sweet wine,” and “柯” refers to an “axe handle” or the stem of a plant—a naming motif found across cultures, where natural elements are often used in personal names. But when transliterated into English, it comes off as somewhat ungrammatical. “Nick” can still work as a name, but “Adfor” is entirely non-existent—I made it up as a playful reference to a “+4” joke.

That said, I still believe that as long as we understand each other or the translator is good enough, anything goes. I remember I even messed up the spelling of "addictive number theory" once, but everyone still knew what I meant. It just takes a little communication, a few jokes, and some correction to get by.