Re: [isabelle] "Simple Type Theory is not too Simple": comments, questions, opinion



Dear Lawrence Paulson/All,

Thank you for your replies. Also, I do apologize for starting such a long and slightly chaotic thread yesterday. I will try to be more to the point today.

I would like to clarify that my thread was hardly about the entire formalization study that is presented in [1], but, primarily, about the proposal to develop a new library for topology based on the locale + explicit locale parameters/explicit carrier set approach. The pattern that is proposed in [1] is the one that I advocated in the first half of 2019. However, at the time, your reaction to this idea seemed to vary from possibly mildly critical to tentatively inquisitive. Given that my own experience with formal methods and Isabelle was minimal at the time, I kept worrying about whether I am, indeed, doing something wrong and how much my work would be criticized, if I was to make an attempt to publish it. The only person who seemed to be mildly supportive of this idea at the time was Fabian Immler (https://mailman46.in.tum.de/pipermail/isabelle-dev/2019-April/016894.html): not surprisingly, my own approach evolved from Fabian Immler and Bohua Zhan's approach to the formalization of elements of algebra in [2] and the examples associated with [3]. The support of Fabian Immler was sufficient for me to continue that work. However, to this date, I had some concerns about how it could be received, and my non-conventional approach to topology was one. of the contributing factors. Of course, I was very surprised to see that, in [1], nearly an entire section was dedicated to advocating the use of what I would consider being the same pattern that seemed to lack your support at the time of its proposal. In any case, I welcome this event as good news, as it reinforces my self-esteem and my belief in my own ideas :-). 

On Wed, Apr 21, 2021 Lawrence Paulson wrote

The current HOL-Analysis library is huge. It has been refactored already and without doubt it will undergo further refactorings in the future. It is however in no way deprecated, nor even HOL-Algebra, although the latter deserves to be. To replace either would take an enormous amount of manpower, which we don’t have.
What we can expect to see our series of experiments trying to push the boundaries of what we can formalise, with an eye in particular to further developing this locale methodology, which seems to work so well.

Thank you for ameliorating my concerns. I became slightly worried because it seemed to me that the remarks scattered around sections 1-3 of [1] suggested that the existing approaches are meant to be, somehow, replaced by the new library.

On Wed, Apr 21, 2021 Lawrence Paulson wrote

I would be happy to see improvements to our own work... The AFP already contains many alternative formalisations of the same mathematical ideas, and there is no plan to impose any one approach.


Of course. However, a very specific approach was advertised in [1] for a very specific purpose. I would like to think that I am reasonably well acquainted with this approach and I encountered a number of problems with it in the past. Given that, according to [1], there seem to be plans for the development of further libraries or extending the topology library associated with [1], I thought that it may be appropriate to mention the problems that I have encountered and the solution that I have converged upon. It was also a chance for me to promote an idea that I wanted to mention on the mailing list for some time, i.e. mimicking records with multiple inheritance. 

On Wed, Apr 21, 2021 Lawrence Paulson wrote

This particular paper on schemes was in response to a challenge made by Kevin Buzzard concerning the expressiveness of simple type theory.


I am aware of this, although I did not explicitly demonstrate my awareness in the thread that I started yesterday (indeed, I should have emphasized that the thread was about only one aspect of [1], and not the entire article). 

I believe that I have seen a number of very speculative and (seemingly) not well-informed remarks made by Kevin Buzzard about Isabelle/HOL. However, having said this, given the opportunity, I hope you will not hold it against me if I will make an attempt to highlight some of the limitations of Isabelle/HOL that I have encountered in my own work. Unfortunately, I have developed a belief that, indeed, Isabelle/HOL (I am not referring to the extensions of Isabelle/HOL like ZFC in HOL or HOTG) has a very limited scope of applicability, as far as the formalization of even modestly modern mathematics is concerned. The primary reason for this is that there does not seem to be any way to reason about certain conventional and sufficiently large categories (although, in this case, the size alone does not seem to be the obstacle). Thus, for example, we might wish to be able to treat continuous maps from R to C (viewed as topological spaces) as morphisms in something similar to the category Top (whatever can be achieved taking into consideration the size limitation of Isabelle/HOL). If entities like R and C are modelled as distinct types, effectively, we would want to have the objects of Top to be a large collection of distinct types. I have to admit that I am not aware how one can achieve this and, it seems, neither do some of the long-standing members of the community: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-September/msg00097.html. However, the situation gets even worse, if one wishes to consider even larger categories, like CAT. From my perspective, unless it is possible to circumvent these issues, indeed, it seems that Isabelle/HOL has a very limited scope of applicability as far as the formalization of mathematics is concerned. 

Even if I will not stand corrected with regard to what is stated in the previous paragraph (somehow, I hope I will), I would like to be very clear that I still consider Isabelle to have more potential than any other proof assistant (by now, I have gained at least a minimal experience in nearly all of them). No other proof assistant seems to offer anything that comes close to the flexibility and extensibility offered by Isabelle/Pure, Isabelle/Isar, Isabelle/ML and Isabelle/Scala, as well as the convenience of the Isabelle/jEdit environment. I have especially high hopes for the projects like ZFC in HOL [4], HOTG [5] and Isabelle/ZF [6], but I also hope to see a canonical variant of some dependent type theory (e.g. Isabelle/HoTT [7]?) becoming a part of the standard Isabelle package one day. However, for now, I would single out ZFC in HOL and HOTG as the most convenient and promising systems for the formalization of mathematics. 

Kind Regards,
Mikhail Chekhov

[1] Bordg A, Paulson L, Li W. Simple Type Theory is not too Simple: Grothendieck’s Schemes without Dependent Types. arXiv:210409366 [cs, math] [Internet]. 2021; Available from: http://arxiv.org/abs/2104.09366
[2] Immler F, Zhan B. Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL. In: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. New York: ACM; 2019. p. 65–77. (CPP 2019).
[3] Kunčar O, Popescu A. From Types to Sets by Local Type Definitions in Higher-Order Logic. In: Blanchette JC, Merz S, editors. Interactive Theorem Proving. Cham: Springer International Publishing; 2016. p. 200–18.
[4] Paulson LC. Zermelo Fraenkel Set Theory in Higher-Order Logic. Archive of Formal Proofs. 2019
[5] Chen J, Kappelmann K, Krauss A. https://bitbucket.org/cezaryka/tyset/src [Internet]. HOTG. Available from: https://bitbucket.org/cezaryka/tyset/src
[6] Paulson LC, Grabczewski K. Mechanizing set theory. J Autom Reasoning. 1996 Dec 1;17(3):291–323.
[7] Chen J. An Implementation of Homotopy Type Theory in Isabelle/Pure. arXiv:191100399 [cs, math] [Internet]. 2019 Oct 31; Available from: http://arxiv.org/abs/1911.00399


On Wed, Apr 21, 2021 at 2:17 PM Lawrence Paulson <lp15 at cam.ac.uk> wrote:
I think the Isabelle community as a whole welcomes all demonstrations of useful methodologies for formalising mathematics. This particular paper on schemes was in response to a challenge made by Kevin Buzzard concerning the expressiveness of simple type theory. Other methodologies could be demonstrated by tackling the same example. It is indeed a long series of definitions and proofs, but now that both the paper and the formal development are available, it should be easier for other groups to give it a try. I would be happy to see improvements to our own work.

The AFP already contains many alternative formalisations of the same mathematical ideas, and there is no plan to impose any one approach.

Larry

> On 20 Apr 2021, at 20:01, Mikhail Chekhov <mikhail.chekhov.w at gmail.com> wrote:
>
> In conclusion, I strongly believe that the best solution for the library design in Isabelle/HOL is the use of the record+locale approach like in HOL-Algebra, i.e. exposing every mathematical structure as a term of some record-like type, while providing a mechanism that could act as a forgetful functor on such structures (alternatively, upcasting) and multiple inheritance. As the code after my signature demonstrates this is far from being impossible.
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.