Email Gateway (Aug 14 2022 at 10:41): Email Gateway (Aug 14 2022 at 10:41):From: Talia Ringer <tringer@cs.washington.edu>
Hi all, hope you're doing well.
In the fall, I'm teaching my second iteration of the Proof Automation
<https://dependenttyp.es/classes/598fa2022.html> class. Last semester, the
main thing students struggled with was grasping the foundations of
different proof assistants, since I didn't spend enough time explaining
them. This semester I'm spending a few extra lectures on this.
For one of those lectures, I'd like to look at the foundations of
Isabelle/HOL. I'm curious if you all have any recommended readings both for
me and for my students.
Really two things are important to teach here, I think:
- ephemeral proof objects / LCF-style proving (vs. Coq's explicit proof
objects)
- the HOL logic itself
For the former, I know the history very well, but I still find it a little
hard to grasp the specifics well enough to teach them. Like, in the
abstract, I understand that proofs in Isabelle/HOL are correct by
construction, and so the kernel is more like the set of functions that can
be used to construct the proof to begin with, at the very core, via some
clever ML engineering. And then explicit proof objects can be reconstructed
from those calls to the kernel if desired, and checked by an independent
kernel, but actually doing so is not very common.
I think I just want something a bit more concrete than that. Can someone
link me to the Isabelle/HOL kernel so I can show it to the class, for
example? And how does automation interact with this in a way such that
guarantees are preserved? What are good readings for this---maybe the
original LCF work? I vaguely recall the paper that defines the type
signature for tactics discussing this kind of thing.
For the latter, I know the HOL is a classical higher-order logic based on
the simply-typed predicate calculus. What confuses me a lot is the
separation of the type system from the logic itself, especially since by
Curry-Howard one could imagine the logic itself as being analogous to a
type system, I assume one that would *not *be simply typed. What are the
practical implications of this, also? Last semester, students were very
confused about what dependent types bought that would be too hard to
express in Isabelle/HOL.
Anyways, I'd appreciate any pointers for either of those, to take me from
my current understanding to knowing enough to really teach this well.
Talia
Email Gateway (Aug 14 2022 at 12:26):From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Talia,
Regarding the LCF approach: I wrote a blogpost here: https://lawrencecpaulson.github.io/2022/01/05/LCF.html
I cite Mike Gordon's “From LCF to HOL: a short history”, but I forgot to include a free link. It’s here:
https://www.cl.cam.ac.uk/archive/mjcg/papers/HolHistory.pdf
It’s interesting that many people today, even those firmly in the programming languages community, struggle with the idea that implementing type “thm” as an abstract data type immediately ensures soundness, through type-checking alone. (And they somehow conflate this with Curry–Howard, which is not connected in any way.) Maybe it’s because ADTs were trendy in the 1970s, before they were shunted aside by OOP, where the data abstraction barriers are intentionally porous.
If you want to go further back in time, see "A Metalanguage for interactive proof in LCF”:
https://dl.acm.org/doi/10.1145/512760.512773
Starting on page 124 you’ll find a detailed description of how to implement the syntax, inference rules and tactics of a simple logic.
The Isabelle kernel is here:
https://isabelle.in.tum.de/repos/isabelle/file/tip/src/Pure/thm.ML
Of course, it’s not just that file but everything that comes before, including tonnes of basic library code supporting syntax and even concurrency.
Larry
Email Gateway (Aug 14 2022 at 13:51):From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Talia,
Regarding higher-order logic, you may find something of value in Section 5 of my bio of Mike Gordon:
https://arxiv.org/abs/1806.04002
I don’t know what you mean by "the separation of the type system from the logic itself”. Types are intrinsic to higher-order logic. Church’s original paper, after all, is entitled "A Formulation of the Simple Theory of Types” (https://doi.org/10.2307/2266170).
By the way, Curry–Howard with simple types gives you only intuitionistic propositional logic.
Regarding "what dependent types bought that would be too hard to express in Isabelle/HOL”: to my mind, this remains one of the key scientific questions of our field. Dependent types are obviously more expressive, and yet dependent type systems have rigidities that we don’t have in simple type theory. A term has a unique type, so x : T(i) does not imply x : T(j) even if i=j, unless i and j are definitionally equal, a concept that’s all but meaningless in simple type theory. It’s notable that an Isabelle/HOL team was able to formalise schemes on their first attempt when none of us even knew what a scheme was, while the Lean team required three attempts. And we didn’t copy them either.
Larry
Email Gateway (Aug 14 2022 at 14:15):From: Talia Ringer <tringer@cs.washington.edu>
Thanks, all helpful!
With respect to separation of types and logic, by some lens, if you have
universal quantification over terms, you can view this as analogous to a
kind of dependent type. And yet the type system for the logic itself is
simply typed, so there is separation between the type system that would be
analogous to the logic by Curry-Howard, and the type system actually used
inside of the logic. I think this is what is so counterintuitive to the
types folks like me.
Email Gateway (Aug 14 2022 at 14:17):From: Talia Ringer <tringer@cs.washington.edu>
(By Curry-Howard, I don't mean the limited correspondence between STLC and
propositional logic, I mean the generalized version wherein any logic can
be viewed as a type system. IME this is what people mean by Curry-Howard
these days.)
Email Gateway (Aug 14 2022 at 17:23):From: Lawrence Paulson <lp15@cam.ac.uk>
As a general remark, I think we’ve gone too far from Curry–Howard as revealing beautiful similarities between the formal systems for propositions and types, from a formal representation of Heating’s conception of intuitionistic logic. Now it is something that’s expected to solve all problems. Yet from the very beginning, there were practical issues. AUTOMATH incorporated related ideas, but people immediately saw the need for proof irrelevance. Now many type theories have a proof-irrelevant layer, which separates the types and propositions again.
A philosophical difficulty, for me, is seeing the name of intuitionism’s arch-enemy (Curry) connected with a form of “constructive logic” that is formalistic enough that Curry would feel right at home.
Larry
Email Gateway (Aug 15 2022 at 01:31):From: Ken Kubota <mail@kenkubota.de>
Regarding "what dependent types bought that would be too hard to express in Isabelle/HOL”: to my mind, this remains one of the key scientific questions of our field. Dependent types are obviously more expressive, and yet dependent type systems have rigidities that we don’t have in simple type theory. A term has a unique type, so x : T(i) does not imply x : T(j) even if i=j, unless i and j are definitionally equal, a concept that’s all but meaningless in simple type theory.
Dependent type systems are not necessarily restricted to terms with a unique type, they also can be implemented as a “Curry-style” system as defined in the classical sense:
"Systems of intersection types are usually “Curry-style” systems, in which types are assigned to untyped terms by rules and an infinite number of types may be assigned to one term, rather than “Church-style” systems, in which each term has a unique built-in type."
http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf <http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf> (p. 40)
Bibliographical reference: [Cardone and Hindley, 2009] in: https://owlofminerva.net/files/fom_2018.pdf <https://owlofminerva.net/files/fom_2018.pdf>
For example, in my logic R0, types are related to sets, such that a term has a type as soon it is established that it fulfils the definition of the set. For example, the term 3 can have both the type N (for natural numbers) and the type R (for real numbers).
You can also implement substitution at the type level such that "x : T(i) does" (!) "imply x : T(j)" "if i=j".
This was intended for R0, but not implemented, since further research is needed: "An implementation of a substitution rule directly at the type (subscript) level appeared too experimental to the author and was removed, since further case studies (here using the recursion operator R) should be undertaken."
https://www.owlofminerva.net/files/formulae.pdf#page=12 <https://www.owlofminerva.net/files/formulae.pdf#page=12>
Since HOL was created for practical purposes (hardware verification), it uses a natural deduction variant of Church's type theory from 1940:
Mike Gordon on the development of HOL: “The design of HOL was largely taken ‘off the shelf,’ the theory being classical higher order logic and the implementation being LCF. The development of the system was, at first, primarily driven by hardware verification case studies.” [Gordon, 2000, p. 174] – https://owlofminerva.net/files/fom_2018.pdf#page=15 <https://owlofminerva.net/files/fom_2018.pdf#page=15>
However, Church's original simple theory of types is a Hilbert-style system, which is (from a logical point of view) more concise.
The most elegant reformulation of Church's theory of types is Peter B. Andrews' logic Q0 (which is, of course, a Hilbert-style system):
https://plato.stanford.edu/archives/sum2018/entries/type-theory-church/#ForBasEqu <https://plato.stanford.edu/archives/sum2018/entries/type-theory-church/#ForBasEqu>
Bibliographical reference: [Andrews, 2002, pp. 210–215] in: https://owlofminerva.net/files/fom_2018.pdf <https://owlofminerva.net/files/fom_2018.pdf>
Referring to the famous quote from Andy Pitts in the HOL handbook:
Andrew M. Pitts on the natural deduction system HOL in comparison to the axiomatic (Hilbert-style) deductive system Q0: “From a logical point of view, it would be better to have a simpler substitution primitive, such as ‘Rule R’ of Andrews’ logic Q0, and then to derive more complex rules from it.” [Gordon and Melham, 1993, p. 213] – https://owlofminerva.net/files/fom_2018.pdf#page=6 <https://owlofminerva.net/files/fom_2018.pdf#page=6>
Peter B. Andrews on equality as the basic primitive notion: “A formulation of type theory based on these ideas was introduced by Church in [Church, 1940], and proved complete by Henkin in [Henkin, 1950]. In this system equality can be defined using connectives and quantifiers. However, it is also possible to define connectives and quantifiers in terms of equality. Equality is a very basic and simple notion, so instead of using Church’s formulation of type theory, we shall use a slight variant of it (first introduced in [Henkin, 1963] and simplified in [Andrews, 1963]) in which equality is taken as the basic primitive notion.” [Andrews, 2002, p. 208] – https://owlofminerva.net/files/fom_2018.pdf#page=5 <https://owlofminerva.net/files/fom_2018.pdf#page=5>
I have never been convinced of the philosophical relevance of the Curry-Howard isomorphism.
Mathematics should be expressed naturally (Andrews), hence directly, unencoded, not encoded in some manner.
Finding parallels in mathematical structures may be fascinating for some mathematicians, but I do not see any foundational character of this isomorphism in a philosophical sense.
The Curry-Howard isomorphism seems to be of incidental nature, and not of foundational nature.
Ken Kubota
https://doi.org/10.4444/100
Am 14.08.2022 um 19:22 schrieb Lawrence Paulson <lp15@cam.ac.uk>:
As a general remark, I think we’ve gone too far from Curry–Howard as revealing beautiful similarities between the formal systems for propositions and types, from a formal representation of Heating’s conception of intuitionistic logic. Now it is something that’s expected to solve all problems. Yet from the very beginning, there were practical issues. AUTOMATH incorporated related ideas, but people immediately saw the need for proof irrelevance. Now many type theories have a proof-irrelevant layer, which separates the types and propositions again.
A philosophical difficulty, for me, is seeing the name of intuitionism’s arch-enemy (Curry) connected with a form of “constructive logic” that is formalistic enough that Curry would feel right at home.
Larry
On 14 Aug 2022, at 15:15, Talia Ringer <tringer@cs.washington.edu> wrote:
Thanks, all helpful!
With respect to separation of types and logic, by some lens, if you have universal quantification over terms, you can view this as analogous to a kind of dependent type. And yet the type system for the logic itself is simply typed, so there is separation between the type system that would be analogous to the logic by Curry-Howard, and the type system actually used inside of the logic. I think this is what is so counterintuitive to the types folks like me.
On Sun, Aug 14, 2022, 6:51 AM Lawrence Paulson <lp15@cam.ac.uk> wrote:
Dear Talia,
Regarding higher-order logic, you may find something of value in Section 5 of my bio of Mike Gordon:
https://arxiv.org/abs/1806.04002
I don’t know what you mean by "the separation of the type system from the logic itself”. Types are intrinsic to higher-order logic. Church’s original paper, after all, is entitled "A Formulation of the Simple Theory of Types” (https://doi.org/10.2307/2266170).
By the way, Curry–Howard with simple types gives you only intuitionistic propositional logic.
Regarding "what dependent types bought that would be too hard to express in Isabelle/HOL”: to my mind, this remains one of the key scientific questions of our field. Dependent types are obviously more expressive, and yet dependent type systems have rigidities that we don’t have in simple type theory. A term has a unique type, so x : T(i) does not imply x : T(j) even if i=j, unless i and j are definitionally equal, a concept that’s all but meaningless in simple type theory. It’s notable that an Isabelle/HOL team was able to formalise schemes on their first attempt when none of us even knew what a scheme was, while the Lean team required three attempts. And we didn’t copy them either.
Larry
On 14 Aug 2022, at 11:40, Talia Ringer <tringer@cs.washington.edu> wrote:
For the latter, I know the HOL is a classical higher-order logic based on the simply-typed predicate calculus. What confuses me a lot is the separation of the type system from the logic itself, especially since by Curry-Howard one could imagine the logic itself as being analogous to a type system, I assume one that would not be simply typed. What are the practical implications of this, also? Last semester, students were very confused about what dependent types bought that would be too hard to express in Isabelle/HOL.
Last updated: Apr 19 2024 at 16:20 UTC