Zulip Chat Archive

Stream: general

Topic: names

Tim Daly (Jul 05 2019 at 05:31):

In the realm of computer algebra it seems that there are commonly accepted names that are used throughout mathematics which we implement. For instance, the sin, integral, subscript, coefficient, etc. In the data structures we find common names like first, last, map, rotate, etc. Sometimes these are not comon but still "reasonably obvious", such as in a DeRham Complex you find a function named "lieDerivative", which is a lie derivative.

So far, in lean and logic I haven't found "universal" naming to be the norm. Even in areas like group theory the naming convention seems non-universal. Given that some of these basic theorems exist in all of the systems, would it be a useful topic to try to converge on a "common core" naming of theorems?

Tim Daly (Jul 05 2019 at 05:40):

An alternative might be to create a "rosetta stone" document, similar to one in computer algebra:
http://axiom-developer.org/axiom-website/rosetta.pdf

Tim Daly (Jul 05 2019 at 05:42):

My (admit

Tim Daly (Jul 05 2019 at 05:43):

My admitedly limited understanding is that "proof irrelevance" implies that if something is proved in one system then it is true. So such a rosetta collection turns into both a cross-reference and a catalog of proven statements.

Tim Daly (Jul 05 2019 at 05:49):

And if a theorem is proven true in one system, couldn't it be stated as an axiom in other systems? So the rosetta stone becomes a catalog of axioms.

Johan Commelin (Jul 05 2019 at 06:15):

Of course you can add axioms... but since there will be a human translation step involved when going from one system to the other, the trust level goes down.

Johan Commelin (Jul 05 2019 at 06:17):

Concerning "common core" names. I think it is very hard to come up with a practical naming system that everyone is happy with. I for one think that it would already be very helpful if we just add those "common core" names in the comments above theorems. For most applications that should also be sufficient.

Tim Daly (Jul 05 2019 at 06:17):

Good point. On the other hand, with a list of proofs (say, from group theory) it would be possible to claim which ones were proven in Lean and which ones are axioms.

Tim Daly (Jul 05 2019 at 06:21):

Assume a rosetta document (perhaps one similar to the Digital Library of Mathematical Functions (DLMF) https://dlmf.nist.gov/ so that one could look up a theorem (because the "reference name" cites chapter/section/theorem. Along with the theorem from "the first prover" would be the actual proof. Theorems proven in other systems could be named in the same section. Theorems not listed are just axioms.

Tim Daly (Jul 05 2019 at 06:24):

The "Digital Library of Mathematical Theorems" (DLMT) would be a useful collection, especially since it would show how to prove a theorem, despite syntactic / semantic mismatch. Indeed, if there was an natural language explanation of the proof it would be even more enlightening.

Tim Daly (Jul 05 2019 at 06:25):

Such an effort would be an interesting sub-forum at conferences.

Tim Daly (Jul 05 2019 at 06:27):

IF a system came up with a shorter or more obvious proof that replace the existing entry.

Tim Daly (Jul 05 2019 at 06:28):

Attaching the author's name would give professional credit

Tim Daly (Jul 05 2019 at 06:34):

William Stein (http://www.sagemath.org/) built a "front end" system that allows users of many systems to have a common way of communicating. This approach might help with the translation problem.

Tim Daly (Jul 05 2019 at 06:39):

Of course, there is the issue of "compatible logics" since, as I understand it, a theorem proven in a classical logic is not necessarily a theorem in constructive logic (Bishop?)

Tim Daly (Jul 05 2019 at 06:49):

If libraries were organized "by the book", it would make it a lot easier to search for theorems. All of the group theory theorems are in the chapter on group theory, for example. That would make it possible to have "library compliance" tests and cross-system proofs.

Johan Commelin (Jul 05 2019 at 06:52):

I don't understand... is the current folder hierarchy in mathlib unclear?

Tim Daly (Jul 05 2019 at 07:11):

As to the issue of "trust" for a theorem from another system... I believe that Coq and Lean share

Johan Commelin (Jul 05 2019 at 07:12):

No... you have to trust the human translation.

Tim Daly (Jul 05 2019 at 07:12):

a common logic. If the proof in one system were output in a common format it seems to me that "proof checking" a Lean proof in Coq or the reverse is possible

Johan Commelin (Jul 05 2019 at 07:12):

Sure, but that requires writing a lot of glue.

Tim Daly (Jul 05 2019 at 07:14):

Folders are a really bad semantic organization. I call it a POS (Pile of Sand) organization... It all sorta-works to sorta-provide some ad hoc map to a tree structure.

Tim Daly (Jul 05 2019 at 07:17):

Mathematics seems more graph-like than tree-like, but maybe that's just me.

Johan Commelin (Jul 05 2019 at 07:17):

How is it different from "by the book" organization with chapters? (Books are linearly ordered, which is probably even worse than POS trees.)

Tim Daly (Jul 05 2019 at 07:18):

Books provide several mechanisms for search that everyone is familiar with. Chapters, sections, indexes, tables, hyperlinks, and surrounding text

Johan Commelin (Jul 05 2019 at 07:19):

We have all that (if you map folders to chapters etc).

Tim Daly (Jul 05 2019 at 07:21):

Every POS organized system I've ever worked on was "obvious" after the first year or so of use.

Mario Carneiro (Jul 05 2019 at 07:23):

Re: Coq <-> Lean, they don't actually have the exact same logic. I've wanted this for a long time, but I think that a wholesale conversion will not work in either direction because DTT is very sensitive to defeq

Tim Daly (Jul 05 2019 at 07:24):

A DLMT website could provide "proof checkable" sources in a common format so systems could proof-check their axioms to increase trust. Sharing such efforts means that systems could specialize (e.g. HoTT axioms)

Mario Carneiro (Jul 05 2019 at 07:26):

This exists in some other languages already

Mario Carneiro (Jul 05 2019 at 07:27):

I don't think Lean is a very good interchange language for proofs coming from many systems

Tim Daly (Jul 05 2019 at 07:30):

I believe that Lean can output a "primitive proof" (don't remember the name) that gets fed to the lowest level proof system. I believe that Coq also has that ability. I will check later today. Given a common core logic they ought to be able to cross-validate proofs.

Mario Carneiro (Jul 05 2019 at 07:30):

Those primitive proofs are not in a common format

Mario Carneiro (Jul 05 2019 at 07:30):

and they are not in a common logic

Mario Carneiro (Jul 05 2019 at 07:31):

so you can't feed a lean proof to Coq, it will complain it is not well typed even if you fix the syntax

Mario Carneiro (Jul 05 2019 at 07:31):

and vice versa

Tim Daly (Jul 05 2019 at 07:32):

So to build Axiom as an Oracle system I have to re-prove every algorithm in every system from scratch? That hardly seems like mathematics to me.

Mario Carneiro (Jul 05 2019 at 07:32):

Like I said, Lean is not an interchange format. That doesn't mean they don't exist

Tim Daly (Jul 05 2019 at 07:33):

I don't need a common interchange for proofs, just for proof checking

Mario Carneiro (Jul 05 2019 at 07:34):

OpenTheory is a reasonably successful interchange format for HOL like systems, and I have heard Dedukti is an interchange format for DTT systems, although I haven't used it. Metamath is also a generic prover that can be used to check any logic including HOL and DTT systems, and I have successfully translated to and from Metamath for this sort of thing

Tim Daly (Jul 05 2019 at 07:36):

Excellent. I'll look up metamath. Thanks.

Mario Carneiro (Jul 05 2019 at 07:36):

There is also my own language MM0, which I recently demonstrated here to translate a large proof from Metamath to Lean (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Prime.20number.20theorem.20in.20lean/near/168472336)

Mario Carneiro (Jul 05 2019 at 07:38):

There aren't a lot of people working on proof translations, but I think it is very important for the theorem proving community to have a more rigorous sense of equivalence of logics, so that it doesn't become some battle royale between the various prover communities.

Tim Daly (Jul 05 2019 at 07:39):

Well I've wandered off into Linear Logic (Pfenning / Balzer) for a bit and that is a somewhat incompatible logic.

Mario Carneiro (Jul 05 2019 at 07:40):

not for metamath or MM0 it's not

Mario Carneiro (Jul 05 2019 at 07:40):

I think Isabelle is also a logical framework, so it might work for this purpose too, I haven't tried

Mario Carneiro (Jul 05 2019 at 07:41):

The idea is that you state your axioms up front, and define the system you are proving theorems in

Mario Carneiro (Jul 05 2019 at 07:41):

rather than baking everything into the foundation like lean

Tim Daly (Jul 05 2019 at 07:43):

Since I'm proving source code algorithms I'm essentially taking that path. The group theory superstructure provides axioms (proven elsewhere) that can be used in the proof of code.

Tim Daly (Jul 05 2019 at 08:19):

Btw, book organization and POS organization are quite compatible. Axiom uses literate programming with all of the source code in book form. The compiler extracts the source code into POS form at compile time. John Kitchin (CMU/Chemical Engineering) (http://kitchingroup.cheme.cmu.edu) is a strong advocate of literate programming.

Tim Daly (Jul 05 2019 at 20:01):

Tim Daly (Jul 05 2019 at 20:02):

(deleted)

Tim Daly (Jul 05 2019 at 20:04):

Re: POS (Pile of Sand) and directory organization: Ted Nelson's Computers for Cynics "The Nightmare of Files and Directories" https://www.youtube.com/watch?v=Qfai5reVrck&list=PLTI2Kz0V2OFlgbkROVmzkfQRW2FrX2KfR&index=2

Last updated: Dec 20 2023 at 11:08 UTC