Email Gateway (Aug 23 2022 at 09:23): Email Gateway (Aug 23 2022 at 09:23):From: Ken Kubota <mail@kenkubota.de>
Where can I find this paper?
How are the type dependencies in expressing group theory covered, as type abstraction, as suggested by Mike Gordon, still isn’t implemented in HOL?
https://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/#type_abstraction
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-September/msg00045.html
https://sympa.inria.fr/sympa/arc/coq-club/2020-02/msg00138.html (see section: B. Kevin Buzzard on Isabelle/HOL)
Ken Kubota
https://doi.org/10.4444/100
Email Gateway (Aug 23 2022 at 09:23):From: Manuel Eberl <eberlm@in.tum.de>
Where can I find this paper?
See here: https://doi.org/10.1007/s10817-019-09537-9
How are the type dependencies in expressing group theory covered, as type abstraction, as suggested by Mike Gordon, still isn’t implemented in HOL?
I don't know why people keep claiming you need dependent types/type
abstraction/whatever to do abstract algebra.
We've had abstract algebra in Isabelle for well over 10 years (the
HOL-Algebra library, which is distinct from the new experimental
approach presented in the above paper, which is more like a proof of
concept). There was even a paper about the existence of the algebraic
closure of fields at ITP 2020, which is a very advanced result. (I don't
think any other system has that result yet, although Lean is well on its
way and Coq has it at least for countable fields).
We don't have schemes, but that is not, as Kevin suggests, because
Isabelle/HOL is too weak to define schemes – indeed I did it for him a
while ago in response to that very article just to demonstrate that it
can be done and it's not difficult (although whether it is pleasant to
work with them is another matter; I cannot say because I have not
tried). The main reason why we don't have schemes is quite simply
because there are not /that/ many mathematicians in the Isabelle
community and none of the ones who are seemed to care about schemes
enough to formalise them. I barely know what schemes are, and I would
imagine it is the same for most of the Isabelle community, so why should
I formalise something that I know virtually nothing about? In order to
formalise something, it is good to have a good informal understanding of
it first. If I had some concrete goal and schemes were the way to get
there, I would look into it, but otherwise, I'd rather stick to doing
things that are closer to my field of expertise.
That said, it is of course entirely possible that there is some
mathematics that is too tedious to do in Isabelle/HOL due to a lack of
dependent types; some people, like Sébastien Gouëzel, have said
something to that effect. But saying that abstract algebra in general is
not possible without them is certainly a huge overstatement.
The way abstract algebra is done in Isabelle is simply to have some big
enough type and the carrier of your group is then only a subset of that
type and not the entire type. HOL-Algebra additionally also packages the
group operations up into a record and uses locales to bundle all the
group axioms together. It's a bit painful and perhaps not as natural as
it is in Coq and Lean, but it undoubtedly works.
HOL-Analysis has similar "relativised" notions of topologies. Normally,
the topology of a type always spans the entire type and is fixed for
that type using type classes, but one can also have topologies as values
and then say that a set is open w.r.t. a particular topology.
The main disadvantage of this is that you have two parallel
developments: the typeclass-based ones and the relativised ones. That is
certainly a drawback, but people (cf. Mikhail Chekhov) seem to be
working on making this smoother.
Cheers,
Manuel
Email Gateway (Aug 23 2022 at 09:23):From: Lawrence Paulson <lp15@cam.ac.uk>
This is nothing. Too often I hear claims that dependent types are necessary to do formal mathematics. I have seen “proof assistant” defined as “software implementing the propositions-as-types principle". And there is a widespread idea that the “LCF architecture” is an instance of propositions-as-types. Not very long ago, I had to explain at great length how LCF's use of an abstract type eliminated the need to store proofs (to a person exceptionally familiar with functional programming). Such preconceptions seem to be widespread even among some experienced professionals.
Larry
Email Gateway (Aug 23 2022 at 09:24):From: Ken Kubota <mail@kenkubota.de>
It is not legitimate to mix up the question of dependent types (or type abstraction) with other, obviously wrong approaches.
And I find it difficult to call Mike Gordon's suggestion as well as the clear statements by John Harrison, Freek Wiedijk, and others on the limitations of the HOL type system "nothing".
Often some features can be emulated by auxiliary techniques, as this has already been the case with the traditional HOL system.
But then the mathematical expression is less natural, and usually not all formal statements can be expressed.
If there is an obvious dependency, clearly it is desirable to express this symbolically in formal logic.
Ken Kubota
https://doi.org/10.4444/100
Email Gateway (Aug 23 2022 at 09:24):From: Ken Kubota <mail@kenkubota.de>
Am 23.07.2020 um 14:44 schrieb Manuel Eberl <eberlm@in.tum.de>:
Where can I find this paper?
See here: https://doi.org/10.1007/s10817-019-09537-9
Thank you very much.
I will try to have a look at it soon.
How are the type dependencies in expressing group theory covered, as type abstraction, as suggested by Mike Gordon, still isn’t implemented in HOL?
I don't know why people keep claiming you need dependent types/type
abstraction/whatever to do abstract algebra.
The way abstract algebra is done in Isabelle is simply to have some big
enough type and the carrier of your group is then only a subset of that
type and not the entire type. HOL-Algebra additionally also packages the
group operations up into a record and uses locales to bundle all the
group axioms together. It's a bit painful and perhaps not as natural as
it is in Coq and Lean, but it undoubtedly works.HOL-Analysis has similar "relativised" notions of topologies. Normally,
the topology of a type always spans the entire type and is fixed for
that type using type classes, but one can also have topologies as values
and then say that a set is open w.r.t. a particular topology.The main disadvantage of this is that you have two parallel
developments: the typeclass-based ones and the relativised ones. That is
certainly a drawback, but people (cf. Mikhail Chekhov) seem to be
working on making this smoother.
Let me ask directly. Is it possible to:
Your description above doesn't look like a natural representation at all.
a) Circumlocations are necessary ("have some big enough type and the carrier of your group is then only a subset of that type").
b) Duplication of structures ("two parallel developments: the typeclass-based ones and the relativised ones").
c) Auxiliary structures like type classes are needed.
d) Extra work is required to unify the parallel developments ("working on making this smoother").
I'm not too familiar with Isabelle's type classes.
But I vaguely remember that in the past they lead to an inconsistency (antinomy: negative self-reference) in Isabelle/HOL, and the way this was fixed was by manually tracking the dependencies, if I'm not mistaken.
However, this clearly contradicts the very idea of type theory, in which the formal language (the syntax: types) prevents the formulation of antinomies from the very beginning.
One may accept the fix as an auxiliary solution, but not more.
So altogether the impression is, that simply because the formal language (the type system) used here is too poor, a lot of problems and extra work are created.
There is no sense in defending an impoverished type system, in which trivial ideas such as the link (the dependency) between the type and the term level cannot be expressed naturally.
In particular, since it can easily be expressed using the lambda variable binder, as suggested by Mike Gordon.
Ken Kubota
https://doi.org/10.4444/100 <https://doi.org/10.4444/100>
Email Gateway (Aug 23 2022 at 09:24):From: Manuel Eberl <eberlm@in.tum.de>
On 23/07/2020 23:24, Ken Kubota wrote:
Let me ask directly. Is it possible to:
1. Prove a property in an abstract way for all groups (e.g., the
uniqueness of the identity element),
Of course:
lemma (in monoid) one_unique:
assumes "u ∈ carrier G"
and "⋀x. x ∈ carrier G ⟹ u ⊗ x = x"
shows "u = 𝟭"
What you cannot do (due to lack of type-level quantification) is write
down a statement like "there exists a group G such that …" without
fixing the type of G. But I've never seen that cause problems in practice.
- and then, given a certain group, transfer (instantiate) this theorem
for that particular group without having to carry out the proof again?
If so, please provide a link.
All you have to prove is that the structure you're looking at is indeed
a monoid and then you get that theorem. For instance, HOL-Number_Theory
defines
definition residue_ring :: "int ⇒ int ring"
where
"residue_ring m =
⦇carrier = {0..m - 1},
mult = λx y. (x * y) mod m,
one = 1,
zero = 0,
add = λx y. (x + y) mod m⦈"
and then proves that this is a commutative ring for "m > 1". That gives
you for free that the additive and multiplicative subgroup are abelian
groups (and therefore monoids) and you can use the above fact. You can
also talk about subgroups of these groups and apply the result to them.
Your description above doesn't look like a natural representation at all.
a) Circumlocations are necessary ("have some big enough type and the
carrier of your group is then only a subset of that type").
b) Duplication of structures ("two parallel developments: the
typeclass-based ones and the relativised ones").
c) Auxiliary structures like type classes are needed.
d) Extra work is required to unify the parallel developments ("working
on making this smoother").
Yes, it's not great. But if you want to make a system work for practical
use, you always have to make some compromises and/or do a lot of
engineering. If I recall correctly, the Coq people have been investing a
lot of work into their type classes as well because they were found to
be insufficient for practical use. The Lean people recently overhauled
their system as well because (I think) it was too slow and unpredictable.
I'm not too familiar with Isabelle's type classes.
But I vaguely remember that in the past they lead to an inconsistency
(antinomy: negative self-reference) in Isabelle/HOL, and the way this
was fixed was by manually tracking the dependencies, if I'm not mistaken.
The problem wasn't type classes per se, but the low-level mechanism that
they use (overloaded constant definitions). These are now well
understood; I think there's even some kind of mechanised soundness proof
and more is on the way.
However, this clearly contradicts the very idea of type theory, in which
the formal language (the syntax: types) prevents the formulation of
antinomies from the very beginning.
One may accept the fix as an auxiliary solution, but not more.
You may oppose this on a philosophical and aesthetic level and that is
fine (I will hardly prescribe you your sense of aesthetics), but I for
one don't care much about such foundational issues as long as things are
sound. I just want a system that allows me to do stuff, and Isabelle/HOL
usually works great in practice.
So altogether the impression is, that simply because the formal language
(the type system) used here is too poor, a lot of problems and extra
work are created.
There is no sense in defending an impoverished type system, in which
trivial ideas such as the link (the dependency) between the type and the
term level cannot be expressed naturally.
In particular, since it can easily be expressed using the lambda
variable binder, as suggested by Mike Gordon.
I don't know anything about that lambda variable binder since I am not a
foundational guy; perhaps somebody else can comment on that. But I would
be surprised if it didn't make some things more difficult.
You criticise Isabelle/HOL as unnatural because you sometimes have to
express things in a certain way. But when I look at e.g. Coq
developments like the group theory behind Feit–Thompson, I was told they
restrict everything to finite groups represented them as lists. That
doesn't sound like a natural representation to me either. I'm sure they
/could/ have done it in a different, more natural way, but they chose
not to for some (probably technical) reason, and that's my point.
Systems like Coq and Lean also have the difference between Bool and Prop
and between definitional equality and other types of equality. I'm
pretty sure most mathematician find such distinctions very strange.
Isabelle/HOL also has two kinds of equality and a distinction between
bool and prop, but the logic allows hiding the difference completely in
practice.
(Just in case that your opinion is that Lean and Coq are also bad and
some other system X is the real solution: I am focusing on Lean and Coq
because they are the other two really big systems that have stronger
logics than Isabelle/HOL and it only makes sense to compare Isabelle/HOL
to systems of roughly comparable size.)
The way I see it, theorem proving is not a game of type-theoretic
one-upmanship. The objective is not to just pick the most powerful logic
imaginable and then you win. Expressiveness often comes with a price. I
think it is widely agreed upon that Isabelle has exceptionally good
automation and performance, and I'm sure that has a lot to do with the
LCF approach and the foundational choices (although I am hardly an
expert on this). Some Lean people, for instance, told me that their
simplifier is still very slow.
Another big advantage of Isabelle/HOL is that there is a huge library!
In my opinion, good libraries are far more important in practice than
powerful logical foundations. If you want to do some work requiring
analytic combinatorics (an example chosen because it is close to my
heart), the very expressive type systems of Coq and Lean and Agda will
not be particularly helpful, since none of them have any complex
analysis, let alone analytic combinatorics.
You're certainly right that we Isabelle/HOL people sometimes have to go
out of our way to do certain things (such as the duplication of
HOL-Computational_Algebra vs HOL-Algebra) and we are well aware of that.
Occasionally, you have to take a step back and figure out if the extra
work you have to do is still worth doing or whether you are working
against the system more than you are working with it. If that ever
happens, I might well consider switching to another, more suitable
system, but it hasn't happened so far.
If someone were to come along and make a system that offers the
advantages of Isabelle/HOL (structured proofs, good automation,
scalability) with the addition of dependent types, I would very
seriously consider switching as well (although the library issue remains).
Theorem provers are not artworks to be displayed on a wall in a gallery
for everyone to marvel at their beautiful and elegant design. They are
software intended for practical use by many people for a large variety
of different use cases, and they succeed or fail in practical applications.
Isabelle/HOL has worked well for a lots of practical use cases in
computer science and mathematics. If it will someday be the case that
other systems are clearly and unequivocally better, it will probably
just die.
But I think we're still far away from that.
Cheers,
Manuel
Email Gateway (Aug 23 2022 at 09:24):From: Lawrence Paulson <lp15@cam.ac.uk>
For sure. I have been noticing since the 1990s that with certain well-known systems you have to build a new library for each project. Precisely why isn’t clear; perhaps it is quite difficult to judge how heavy a use to make of dependent types. That the most popular Coq library (SSREFLECT) emphasises computable representations of mathematics seems remarkable, since it goes against the natural objective reasoning abstractly.
We have a similar situation ourselves with the Algebra library, where the use of records may have been a mistake. But at least we don’t feel compelled to throw it away and start fresh.
As I keep saying: the precise role of dependent types in the formalisation of mathematics is one of the key scientific questions of our field. It can only be answered empirically.
Larry
Last updated: Nov 21 2024 at 12:39 UTC