(Link)

Authors: Tobias Nipkow (Technical University of Munich), Lawrence C. Paulson (University of Cambridge), and Markus Wenzel (Technical University of Munich)

Reference: The original is Nipkow, Tobias, Markus Wenzel, and Lawrence C. Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Vol. 2283 of Lecture Notes in Computer Science. Springer, 2002; I am reading the updated 2023 version

Why this paper? Cited by Single-set cubical categories and their formalisation with a proof assistant and Formalizing the ∞-Categorical Yoneda Lemma

In the world of interactive theorem provers two systems stand out for their maturity and wide adoption. One is Rocq, until recently known as Coq, about which I have written previously; Isabelle/HOL, the topic of this week’s reading, is the other. Rocq is one of a number of systems (for example, Lean) based on Martin-Löf’s dependent type theory, whereas Isabelle/HOL is one of a number of systems based on the alternative foundation of higher order logic (HOL). These are not the only two options – Mizar, which is older still, takes another route – but I think it is fair to call them the most prominent.

Dependent type theory (as usually implemented) and higher order logic have some similarities, as both are built on total functional programming languages with advanced type features such as parametric polymorphism and type operators: approximately, System Fω in the lambda cube. Note that while a more conventional programming language like Haskell also has these features, it is not total. Totality is required here because it avoids non-terminating programs that would, considered as definitions, lead to logical inconsistency: if foo could be defined to be equal to foo + 1, then we could subtract foo from each side to conclude that 0 = 1. While dependent type theory travels still further up the lambda cube to include types that depend on terms, allowing mathematical statements to be expressed as types, HOL instead adds a separate layer of logic on top of the base calculus. A more subtle distinction is that while types with no elements are a core part of dependent type theory – every false mathematical statement corresponds to such a type – we are not permitted such types in HOL, as the usual rules of logic with quantifiers require the domain(s) of variables to be non-empty. This does not mean we cannot talk about the empty set of mathematics; instead, we must remember that sets and types are not to be conflated in HOL, and nor (unlike in the HoTT version of dependent type theory) are the sets included in the types.

Isabelle is a generic system for implementing logical systems, and HOL is by far its most celebrated instance. This book, first published in 2002 but much updated since, provides a beginner’s tutorial to this system, assuming only some basic logical notation and functional programming. In keeping with the HOL separation of programming and logic, we start with the basics of Isabelle/HOL as a programming language. The interesting point here, returned to several times through the text, is the machinery used to ensure that program definitions are terminating. These techniques range from primitive recursion, where we are forced to write our program in a style that marches at each step towards a base case, to automated tools that can, for example, prove the termination of the notorious thorny Ackermann’s function.

Moving to theorem proving, the basic machinery is based on natural deduction, implemented in a ‘non-dogmatic’ way to prioritise usefulness over the elegance or parsimony of the underlying proof theory. The major emphasis, as is also true for Rocq but perhaps holds even more so for Isabelle/HOL, is on tactics that automatically try to generate proofs. For example unification, a variant of which I’ve blogged about before , is key here to automatically match generic logical or rewrite rules to a particular situation, although this tutorial of course does not labour the implementation details of the underlying algorithms. We instead see some extended examples, mostly from computer science, with the most pleasing to me being a reconstruction of a proof about context-free grammars from the classic textbook of Hopcroft and Ullman which nicely reveals the gaps in the original proof.