Patrick Nicodemus (Oct 29 2023 at 00:22): Patrick Nicodemus (Oct 29 2023 at 00:22):This is a question about the long term future of isabelle and whether it would be possible to implement (classical, extensional) dependent type theory on top of HOL in isabelle.
Jacobs has proved that there is a (surface) embedding of dependent type theory into HOL, and they implemented a prototype.
It is well known that Martin-Lof type theory with extensional equality has undecidable type checking.
However there may be heuristics that are good enough, especially if the user is considering dependent types A -> Type where A is a simple type without much interesting structure. The Lean theorem prover (which is based on intensional dependent type theory) implements a definitional equality which is known to be undecidable, but its heuristics for type judgements appear to be effective in most cases.
In addition, automated theorem provers have gotten better over the years and it may be possible to use them in some cases to resolve the validity of typing judgements.
The research group at KWARC has implemented a dependent type theory in their logical framework, called MMT, where typing judgements are dispatched to the HOL-based theorem prover Leo-III.
So in conclusion what I am asking is: would isabelle developers ever consider implementing a dependently typed layer over HOL together with a translation from dependent type theory into HOL? Is it possible for Isabelle users to write such an interface using the logical framework features of isabelle? It would be nice to take advantage of the strong automation of Sledgehammer while also having the more expressive/concise code of dependent type theory. In my opinion the additional verbosity of HOL makes it easier to introduce mistakes into a definition of a complex concept.
Patrick Nicodemus (Oct 29 2023 at 05:13):I just found the paper "Modular Reasoning in Isabelle" by Florian Kammueller which discusses a way to implement dependent types in HOL. If anybody has any more recent work I would be curious to see it
Wenda Li (Oct 29 2023 at 11:13):There has been some HoTT in Isabelle, which could be relevant.
Patrick Nicodemus (Oct 29 2023 at 23:55):Wenda Li said:
There has been some HoTT in Isabelle, which could be relevant.
Thank you! This is super cool. My question is motivated by desires for good/strong automation in dependent type theory leveraging stuff like Sledgehammer in the HOL ecosystem. I think design of dependent type theory is a broad spectrum and homotopy type theory is pretty far away from the design choices that would enable us to take advantage of sledgehammer. The difference between a deep embedding and shallow embedding is kind of a spectrum too, but I doubt it's possible to give an embedding of HoTT in HOL that would be "shallow", so realistically this project is unlikely to be able to draw on HOL's powerful automation.
Yutaka Nagashima (Oct 30 2023 at 01:32):Hi @Patrick Nicodemus,
You might already be aware, but Isabelle has the src/CTT and src/Cube modules. These aren't based on Isabelle/HOL, just so you know.
but its heuristics for type judgments appear to be effective in most cases.
I'm intrigued by the heuristics used for type judgments. Do you know if they're documented anywhere?
Also, if you're looking for input from other Isabelle developers, you might consider sending an email to the mailing list.
I've noticed that some developers don't frequent Zulip.
Regards,
Yutaka
Patrick Nicodemus (Oct 30 2023 at 14:54):@Yutaka Nagashima
Thank you very much for your response. I knew of src/CTT as Lawrence Paulson has blogged about it and it is included in the 2023 version of "Isabelle's Logics" from the Isabelle documentation. I may have heard of src/Cube but I have yet to look into it.
Just to clarify, I say that Lean has undecidable definitional equality and thus type inference, but it is a "milder" undecidability than full-blown extensional type theory. This will affect Lean users who work with, for example, transfinite induction, but for most users it does not affect them.
As far as I am aware, Mario Carneiro's Master's thesis is the most comprehensive theoretical treatment of Lean. https://github.com/digama0/lean-type-theory/releases. I don't know what heuristics are used but the thesis does discuss the distinction between the "ideal" definitional equality (which is undecidable) and the actual definitional equality which is is implemented in practice in the type checking algorithm. This is probably a good point of departure.
Henrik Böving (Oct 30 2023 at 22:41):Note that this thesis only covers the Lean 3 type theory, there are changes in the Lean 4 one which are documented (even though much less formalized) in Sebastian Ullrich's PhD thesis.
Jonathan Julian Huerta y Munive (Oct 31 2023 at 11:07):I'd like to provide more details to the discussion above. The traditional approach to compare formal systems is through ZFC set theory. In this regard, HoTT (as MLTT with one univalent universe) requires assuming the existence of 2 inaccessible cardinals to be shown consistent in ZFC (see here). In contrast, Isabelle's HOL can be shown consistent just with ZFC. So, in this sense, HoTT is more expressive than HOL. In practice, this means that you cannot show sound your implementation of MLTT inside HOL. Thus, an "implementation" of a(n expressive) dependent type theory actually means writing the syntax and rules of inference of MLTT inside HOL (without showing their soundness). The moment you do this, you have to provide specific automation for your MLTT construction. Even without implementing an expressive system, Isabelle's automation does not suffice on all domains. For instance, proving basic algebraic properties (e.g. factorisation or quotient manipulation) is a challenge for Sledgehammer (see here complemented with these benchmarks that require manual proofs of real-arithmetical facts). In this sense, it is difficult to imagine that HOL's Sledgehammer automation would become immediately effective for an internal MLTT.
would Isabelle developers ever consider implementing a dependently typed layer over HOL together with a translation from dependent type theory into HOL?
This depends on many things. Who are the Isabelle developers? The AFP managers and Makarius Wenzel? It is not likely that they will do this because they have other projects on queue. All AFP contributors? One of them, in the future, might. The main obstacle is that developing one of these formal systems requires a lot of time and effort (even with Isabelle's HOL automation). So you will need to have a very convincing argument to do such a demanding project or a lot of free time. Given the preamble above, increased automation does not seem to be convincing enough.
Is it possible for Isabelle users to write such an interface using the logical framework features of Isabelle? Yes, as pointed above, HoTT in Isabelle is already a thing (Isabelle/HoTT) and a formalisation of category theory in Isabelle/HOL (see here) might be relevant for your interests too.
Patrick Nicodemus (Oct 31 2023 at 12:20):Jonathan Julian Huerta y Munive said:
I'd like to provide more details to the discussion above. The traditional approach to compare formal systems is through ZFC set theory. In this regard, HoTT (as MLTT with one univalent universe) requires assuming the existence of 2 inaccessible cardinals to be shown consistent in ZFC (see here). In contrast, Isabelle's HOL can be shown consistent just with ZFC. So, in this sense, HoTT is more expressive than HOL. In practice, this means that you cannot show sound your implementation of MLTT inside HOL. Thus, an "implementation" of a(n expressive) dependent type theory actually means writing the syntax and rules of inference of MLTT inside HOL (without showing their soundness). The moment you do this, you have to provide specific automation for your MLTT construction. Even without implementing an expressive system, Isabelle's automation does not suffice on all domains. For instance, proving basic algebraic properties (e.g. factorisation or quotient manipulation) is a challenge for Sledgehammer (see here complemented with these benchmarks that require manual proofs of real-arithmetical facts). In this sense, it is difficult to imagine that HOL's Sledgehammer automation would become immediately effective for an internal MLTT.
would Isabelle developers ever consider implementing a dependently typed layer over HOL together with a translation from dependent type theory into HOL?
This depends on many things. Who are the Isabelle developers? The AFP managers and Makarius Wenzel? It is not likely that they will do this because they have other projects on queue. All AFP contributors? One of them, in the future, might. The main obstacle is that developing one of these formal systems requires a lot of time and effort (even with Isabelle's HOL automation). So you will need to have a very convincing argument to do such a demanding project or a lot of free time. Given the preamble above, increased automation does not seem to be convincing enough.Is it possible for Isabelle users to write such an interface using the logical framework features of Isabelle? Yes, as pointed above, HoTT in Isabelle is already a thing (Isabelle/HoTT) and a formalisation of category theory in Isabelle/HOL (see here) might be relevant for your interests too.
Thank you Jonathan.
As other commenters have mentioned homotopy type theory I can see why you brought it up here. I also may have partially contributed this by mentioning lean, a proof assistant based on intensional type theory.
However, this thread is not about homotopy type theory, the univalence axiom, and so on. The type theory I am asking about is extensional, classical dependent type theory, which is inconsistent with the univalence axiom. I consider homotopy type theory and extensional dtt to be very different logical systems! Their models look nothing alike. Extensional dependent type theory admits a fairly naive translation into set theory. The Univalence axiom requires a sophisticated interpretation using Kan complexes. I fully agree with you that implementation of homotopy type theory in Isabelle/HOL would be a "deep" embedding but I have explicitly cited in my OP researchers who have constructed shallow embeddings of extensional dependent type theory in HOL.
Not to over simplify the point but HOL users already use mock dependent types in the form of maps 'a =>' b set and in my opinion what i am asking for is closer to syntactic sugar on top of this which attempts to filter out nonsense in the formalization, rather than a full blown embedding of infinity groupoids in HOL.
Jonathan Julian Huerta y Munive (Nov 01 2023 at 00:19):Hi @Patrick Nicodemus, I understood that you were not focusing on HoTT, which is why I wrote that I wanted to "provide more detail" and wrote about "expressive dependent type theorys". Perhaps, I should have added "for readers interested on the topic". Sorry for not being specific enough. I think the automation argument still applies. However, I have found this blog post by Larry Paulson whose references might be useful for your interests.
Kevin Kappelmann (Nov 02 2023 at 14:51):Patrick Nicodemus said:
...
Not to over simplify the point but HOL users already use mock dependent types in the form of maps'a =>' b setand in my opinion what i am asking for is closer to syntactic sugar on top of this which attempts to filter out nonsense in the formalization, rather than a full blown embedding of infinity groupoids in HOL.
Hi Patrick, I'm working on such a system and the necessary automation (a soft type system). You can already find some toy examples here: https://github.com/kappelmann/Isabelle-Set/
The automation is currently mediocre at best and that's what I am working on right now.
Patrick Nicodemus (Nov 07 2023 at 23:17):Kevin Kappelmann said:
Patrick Nicodemus said:
...
Not to over simplify the point but HOL users already use mock dependent types in the form of maps'a =>' b setand in my opinion what i am asking for is closer to syntactic sugar on top of this which attempts to filter out nonsense in the formalization, rather than a full blown embedding of infinity groupoids in HOL.Hi Patrick, I'm working on such a system and the necessary automation (a soft type system). You can already find some toy examples here: https://github.com/kappelmann/Isabelle-Set/
The automation is currently mediocre at best and that's what I am working on right now.
Super cool, that's great to see.
Last updated: Apr 28 2024 at 08:19 UTC