Zulip Chat Archive

Stream: general

Topic: names


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Tim Daly (Jul 05 2019 at 05:42):

My (admit

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Tim Daly (Jul 05 2019 at 06:25):

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

view this post on Zulip 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.

view this post on Zulip Tim Daly (Jul 05 2019 at 06:28):

Attaching the author's name would give professional credit

view this post on Zulip 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.

view this post on Zulip 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?)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 05 2019 at 06:52):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 05 2019 at 07:12):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 05 2019 at 07:12):

Sure, but that requires writing a lot of glue.

view this post on Zulip 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.

view this post on Zulip Tim Daly (Jul 05 2019 at 07:17):

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

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 05 2019 at 07:19):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Jul 05 2019 at 07:26):

This exists in some other languages already

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 05 2019 at 07:30):

Those primitive proofs are not in a common format

view this post on Zulip Mario Carneiro (Jul 05 2019 at 07:30):

and they are not in a common logic

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 05 2019 at 07:31):

and vice versa

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Tim Daly (Jul 05 2019 at 07:33):

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

view this post on Zulip 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

view this post on Zulip Tim Daly (Jul 05 2019 at 07:36):

Excellent. I'll look up metamath. Thanks.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 05 2019 at 07:40):

not for metamath or MM0 it's not

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 05 2019 at 07:41):

rather than baking everything into the foundation like lean

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Tim Daly (Jul 05 2019 at 20:01):

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.

view this post on Zulip Tim Daly (Jul 05 2019 at 20:02):

(deleted)

view this post on Zulip 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: May 12 2021 at 23:13 UTC