naming conventions

Stream: general

[Johan Commelin]

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]

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]

please no

[Johan Commelin]

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]

I think that changed in lean 4

[Simon Hudon]

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]

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]

Namespaces help with that

[Tim Daly]

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]

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]

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]

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]

I

[Sebastien Gouezel]

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]

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]

So namespaces are just an extension of the naming convention

[Johan Commelin]

And we would lose projection notation

[Tim Daly]

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

[Kevin Buzzard]

Projection notation is great

[Simon Cruanes]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

Equality is one of the hardest concepts I know.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Tim Daly]

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]

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

[Tim Daly]

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]

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

[Simon Cruanes]

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]

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]

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]

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]

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]

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]

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]

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

[Chris B]

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

[Tim Daly]

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