Stream: new members
Topic: Universal algebra
Hamza Maimoune (Apr 20 2020 at 09:22):
I would like to know if universal algebra would be interesting for Lean? It could factorize a lot of definitions such as closure, stability, morphisms and other stuff.
Mario Carneiro (Apr 20 2020 at 09:24):
Universal algebra would be interesting to investigate, but I would put a big warning if you are investigating this for refactoring purposes, because there is a much higher bar for usability in this case. Just because something is a special case of something else in maths doesn't mean it is actually useful as a generalization in formal maths
Mario Carneiro (Apr 20 2020 at 09:26):
It doesn't hurt to formalize the general theory and look into applications when it is already mostly fully formed, though. What is the actual scope of theorems that can be proven in this context?
Hamza Maimoune (Apr 20 2020 at 09:28):
What do you mean by higher bar of usability?
Mario Carneiro (Apr 20 2020 at 09:28):
I mean that it shouldn't be harder to apply the general theorem in the specific instance than it is to prove the theorem directly in the specific instance
Mario Carneiro (Apr 20 2020 at 09:29):
the shallower the theorems and the more convoluted the generalization the harder it gets to meet this criterion
Mario Carneiro (Apr 20 2020 at 09:30):
The best generalizations are those where the application overhead is minimal and there are still nontrivial theorems to be had. Things like the elementary theory of rings and groups are good examples of this
Johan Commelin (Apr 20 2020 at 09:33):
@Hamza Maimoune As a crazy example: in Lean we have the notion of
add_group. And we automatically duplicate all theorems about groups to theorems about additive groups.
The only difference: notation
Hamza Maimoune (Apr 20 2020 at 09:34):
Did you copy paste the theorems?
Mario Carneiro (Apr 20 2020 at 09:34):
Basically (in an automated way)
Mario Carneiro (Apr 20 2020 at 09:34):
This is done in order to minimize application overhead
Mario Carneiro (Apr 20 2020 at 09:35):
Even though the theories of multiplicative and additive groups are obviously isomorphic, the application overhead of using an additive theorem on a multiplicative group via a translation is sufficiently high that it is easier to just prepare all the theorems in both contexts
Hamza Maimoune (Apr 20 2020 at 09:37):
Therefore, universal algebra would induce a lot of application overhead? If we would implement it, we wouldn't use it to deduce properties on specific algebras, right?
Mario Carneiro (Apr 20 2020 at 09:38):
I'm not saying it necessarily would, only that if you are seriously targeting using it to generalize existing theorems you have to pay very close attention to application overhead and do everything you can to keep it reasonable
Mario Carneiro (Apr 20 2020 at 09:39):
You don't necessarily have to worry about this for the first pass, though. When setting up the initial theory, just do things in the mathematically natural way, and leave application to specific algebras until later
Mario Carneiro (Apr 20 2020 at 09:41):
But easy application to diverse fields is certainly not something that happens for free unless you prepared everything with this in mind beforehand
Hamza Maimoune (Apr 20 2020 at 09:42):
Okay thank you for your answer
Hamza Maimoune (Apr 20 2020 at 09:43):
I'll try to dive into this to see if there is anything useful
Patrick Massot (Apr 20 2020 at 10:44):
@Hamza Maimoune there are two subtly different things here.
In the real world, almost no mathematicians knows anything about universal algebras, because they are not useful for real world mathematics: the benefits are not worth the effort. This fact is not necessarily relevant to formal mathematics. In the real world almost nobody knows about filters. The benefits are not worth the efforts because mathematicians in the real world have no trouble at all saying that everything they prove for limits of sequences hold, mutatis mutandis, for limits of functions etc. But in the formal mathematics world, filters are definitely worth the effort. So it could be that universal algebras are worth the effort in formal mathematics.
But now comes the second aspect of the discussion. Formalized mathematics happen in a formal context, here a flavor of dependent type theory, and in a given software, say Lean but the same would apply elsewhere. Hence there are usability issues, coming from flaws in the foundational theory or in the software. And this has to be weighted against the theoretical benefits. For filters everything is very usable. They blend easily into type theory, and translating back and forth between filters and epsilons is very easy. Hence they are everywhere in formalized maths. Proving theorems about limits of sequences of real numbers as special cases of super abstract theorems about filters is very easy.
Now consider abstract category theory. It's mostly useless in the real world of course (but nice to play with!). In mathlib we have a huge library of category theory, which comes with an gigantic usability barrier. As far as I know, we still have a total of zero specific lemma proved using a general theorem from the category theory library.
Last updated: May 08 2021 at 10:12 UTC