Zulip Chat Archive

Stream: general

Topic: naming conventions


Johan Commelin (Sep 14 2018 at 16:56):

For elements m : M in a [monoid M] we have the predicate irreducible m. Why is this not called is_irreducible m? It is a Prop after all...

Tim Daly (Feb 08 2020 at 01:29):

Please read: The Hideous Name (http://doc.cat-v.org/bell_labs/the_hideous_name/the_hideous_name.pdf). It is my personal opinion that the naming convention Lean uses will not extend to all of mathematics. It has the "look and feel" of a "single host" name. Consider what happens if the industry were to standardize on names and on a standard for theorems that make it possible to share theorems from Coq, Agda, Lean, etc.

We might try replacing the underscore with the network-standard slash convention.

Mario Carneiro (Feb 08 2020 at 04:06):

please no

Johan Commelin (Feb 08 2020 at 05:50):

Certainly not the underscore. If anything, then the .. But even there I'm convinced it's a bad move. Because that looks way to similar to directories and filenames, where as in Lean namespaces are orthogonal to files. I think it would be a good idea to replace the . in import foo.bar with a slash. Because on isn't importing a namespace but a file.

Mario Carneiro (Feb 08 2020 at 05:55):

I think that changed in lean 4

Simon Hudon (Feb 08 2020 at 06:04):

Using file names instead of names separated by . was considered for Lean 4 but as far as I can see, the idea is pretty much dead.

Tim Daly (Feb 08 2020 at 07:04):

So when there are 10,000 theorems (Axiom has about that order of algorithms), will the names be 60 characters long, 10 of which are underscore? Axiom has 22 GCD algorithms, all called "gcd". In the mathematics literature I summation called sum. In computer science I see sort called 'sort'. Names are important and important to get right. The current naming convention does not feel (to me) like it can scale.

What is there to recommend the current naming convention to the world? Why should everyone use it?

It helps to think of "the 30 year horizon", to try to anticipate problems now.

Simon Hudon (Feb 08 2020 at 07:07):

Namespaces help with that

Tim Daly (Feb 08 2020 at 07:09):

Per the article, though, namespaces don't "extend" the name using the same convention, right? Doesn't a namespace qualified name use a dot?

Kevin Buzzard (Feb 08 2020 at 08:41):

I was a bit incredulous two years ago about the idea of Lean's theorem naming convention scaling to "proper maths" but with both schemes and the perfectoid project I was pleasantly surprised to find that it seemed to work well.

In the course I'm currently teaching I'm in the middle of a proof that four predicates on a collection of maps are equivalent and because the predicates don't really have names (they are all called "the definition of a rational map" by mathematicians) this has caused me a bit of grief with naming the lemmas. But in general namespaces work great for me

Tim Daly (Feb 08 2020 at 08:42):

Consider, for example, that we create a 'proglib'. It would be good if similar ideas had similar names. But a proglib would have a focus of theorems with executable semantics. So the group theory theorems might have different proofs for the same "name".

Tim Daly (Feb 08 2020 at 08:47):

Yet for some of the concepts and for some of the proof, you might appeal to 'mathlib' concepts. Would there be confusion if you import both namespaces?

Tim Daly (Feb 08 2020 at 08:51):

I

Sebastien Gouezel (Feb 08 2020 at 09:35):

Even if you don't import a namespace, the theorems are available, but you have to prefix them with the name of the namespace. For instance, you can use group.mul_assoc all the time, and if you import the namespace group you can just write mul_assoc.

Tim Daly (Feb 08 2020 at 10:20):

If the syntax was changed from group.mul_assoc to group_mul_assoc you'd have a uniform syntax that can be extended to hierarchies.

Tim Daly (Feb 08 2020 at 10:21):

So namespaces are just an extension of the naming convention

Johan Commelin (Feb 08 2020 at 10:26):

And we would lose projection notation

Tim Daly (Feb 08 2020 at 10:33):

Ok. so this isn't popular. What is the key advantage of the current naming scheme?

Kevin Buzzard (Feb 08 2020 at 11:34):

Projection notation is great

Simon Cruanes (Feb 08 2020 at 15:19):

If the syntax was changed from group.mul_assoc to group_mul_assoc you'd have a uniform syntax that can be extended to hierarchies.

But this kind of namespacing is exactly what you find in many programming languages, and it arguably scales pretty well (java, C++, etc.)?

Tim Daly (Feb 08 2020 at 16:45):

As near as I can tell, the current naming convention has some sort of "mental map" for those who understand it. For example, "comm_" seems to imply commutative. Those who don't know the mapping (e.g. me) find it uninformative.

Mario Carneiro (Feb 08 2020 at 17:02):

There is an article about that: https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/naming.md

Mario Carneiro (Feb 08 2020 at 17:05):

To be clear: The main advantage of group.mul_assoc over group_mul_assoc is that lean "understands" the ., while _ is just another character for making names. So you can open group and then refer to group.mul_assoc as simply mul_assoc, while group_mul_assoc has no such syntax sugar, no way to make the name locally shorter.

Mario Carneiro (Feb 08 2020 at 17:08):

You might argue why we don't just use dots then, as in group.mul.assoc, but this has to do with the way that open and projection notation work in practice, such that it is best if group.mul in this case is actually a namespace rather than something you made up on the spot.

Tim Daly (Feb 08 2020 at 17:19):

Ah, Grimoire! Unfortunately, while the naming convention "sort of covers" the concepts that arise in logic, the same approach fails badly when extended to other areas of computational mathematics. Take, for example, "equal". In HoTT this seems to mean univalent. In computer science (e.g. "proglib", this could mean 'eq' as in pointer equality, 'eql' as in surface equality, or 'equal' as in structure equality. In math 'eq' could mean many things depending on the branch of math encoded. And users, by their nature, tend to abuse words they like to give their own meaning of equality.

Unless every library has a header (a logical .h file?? gasp) to define what is meant by 'eq', the naming convention doesn't scale. And since there are notions of encoding all of mathematics, one really wants to think about scale.

But, I admit, it isn't a popular idea so I'll just drop the whole thing.

Mario Carneiro (Feb 08 2020 at 17:26):

In lean, eq means =. That's the only equality in common use. There is also "defeq" but this has no syntax in the language and it never shows up in theorem statements so it doesn't enter into any theorem names

Mario Carneiro (Feb 08 2020 at 17:26):

There are other notions of isomorphism in mathlib but they all have their own names

Mario Carneiro (Feb 08 2020 at 17:28):

The naming convention scales in that each new constant gets a new name. eq means =, so if you use it to mean ~= that's violating the naming convention (unless you are in some weird alternate prelude where the regular eq doesn't exist and ~= is named eq).

Tim Daly (Feb 08 2020 at 17:29):

Equality is one of the hardest concepts I know.

Mario Carneiro (Feb 08 2020 at 17:30):

fyi, "proglib" as you keep saying is actually mathlib (the name is unfortunate but mathlib is about both programming and math)

Mario Carneiro (Feb 08 2020 at 17:31):

I wanted to call it "stdlib" but leo vetoed that

Tim Daly (Feb 08 2020 at 17:32):

As I mentioned previously, 'proglib' has a focus of proofs that have execution semantics, partially with an eye toward proving programs and partially with an eye to program generation. 'mathlib' doesn't seem that way.

Simon Cruanes (Feb 08 2020 at 17:40):

Do you have concrete examples of what such proofs would look like?

Tim Daly (Feb 08 2020 at 17:48):

Not (yet) in Lean... but see http://runtimeverification.com/blog/k-vs-coq-as-language-verification-frameworks-part-1-of-3/ and look at the Coq program listings. This is the kind of thing I am currently wrestling

Tim Daly (Feb 08 2020 at 17:53):

Value equality vs reference equality vs Type equality (especially dependent type equality) are all equalities that show up in programming.

Simon Cruanes (Feb 08 2020 at 17:58):

Ah, so you mean things like the "Software Verification" book? I'm not sure what a generic lib for that would look like, each language has its semantic quirks. Better automation might be possible though…

edit: sorry, I meant Software Foundation: https://softwarefoundations.cis.upenn.edu/

Tim Daly (Feb 08 2020 at 18:03):

What is this "software verification" book? I have "Program Verification" by Nissim Francez. I'm only interested in mathematical algorithms, their specification, pre- and post-conditions (logic rules hypothesis and conclusions), and their proofs. I'd also like to be able to generate proven programs from the proofs, especially if it give insight into the original algorithms but also as a "wrap around" verification since the generated programs should be provable again.

Tim Daly (Feb 08 2020 at 18:09):

My focus (at the moment) is on operational semantics which seems to be encodable into ML style syntax. The operational semantics also seems to match the logic rules kind of semantics. But Lean's = doesn't seem to cover ideas like extensional equality (or I'm just not understanding it yet)

Tim Daly (Feb 08 2020 at 18:12):

By the way, the notion that a program is generated from a proof is interesting. If we try to prove the generated program, does it come out "the same" (dare I say equal?). If so, is there a "fixed point" for proofs?

Tim Daly (Feb 08 2020 at 18:18):

Oh, Pierce's book. Yes, I've been following him closely. I took his Coq course online. But general purpose programs are just too hard for me. Mathematical algorithms have (reasonably) clear specifications. Plus I'm only interested in computational mathematics, not all of software.

Tim Daly (Feb 08 2020 at 18:29):

What we really need is a Computational Mathematics department. Currently the expertise is scattered among Philosophy, Mathematics, and Computer Science. There is no "Computational Mathematics" degree, it seems. Back when I started programming, there was no Computer Science department or degree. You were either in Business (Cobol), Math (Lisp), or Engineering (Fortran). We're in the same state today with Computational Mathematics. However, starting a new department is MUCH harder than proving things because, yaknow... people :-)

Chris B (Feb 09 2020 at 01:29):

But Lean's = doesn't seem to cover ideas like extensional equality (or I'm just not understanding it yet)

Lean defines propositional extensionality as an axiom called propext : constant propext {a b : Prop} : (a ↔ b) → a = b, and functional extensionality as a theorem called funext : theorem funext {f₁ f₂ : Π x : α, β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂. Throw in the congr items from init/logic.lean and you're off to the races.

Tim Daly (Feb 09 2020 at 02:04):

See! You can always depend on the fact that I don't know what I'm talking about. Excellent.

Chris B (Feb 09 2020 at 03:23):

lol I didn't mean it that way. I still learn new stuff about Lean every day.

Tim Daly (Feb 09 2020 at 03:30):

I didn't take it personally. One can't know everything.


Last updated: Dec 20 2023 at 11:08 UTC