From Types to Sets by Local Type Definitions in Higher-Order Logic
Types in Higher-Order Logic (HOL) are naturally interpreted as nonempty sets—this intuition is reflected in the type definition rule for the HOL-based systems (including Isabelle/HOL), where a new type can be defined whenever a nonempty set is exhibited.
- PDF / 295,803 Bytes
- 19 Pages / 439.37 x 666.142 pts Page_size
- 7 Downloads / 199 Views
Fakult¨ at f¨ ur Informatik, Technische Universit¨ at M¨ unchen, Munich, Germany [email protected] 2 Department of Computer Science, School of Science and Technology, Middlesex University, London, UK 3 Institute of Mathematics Simion Stoilow of the Romanian Academy, Bucharest, Romania
Abstract. Types in Higher-Order Logic (HOL) are naturally interpreted as nonempty sets—this intuition is reflected in the type definition rule for the HOL-based systems (including Isabelle/HOL), where a new type can be defined whenever a nonempty set is exhibited. However, in HOL this definition mechanism cannot be applied inside proof contexts. We propose a more expressive type definition rule that addresses the limitation and we prove its soundness. This higher expressive power opens the opportunity for a HOL tool that relativizes type-based statements to more flexible set-based variants in a principled way. We also address particularities of Isabelle/HOL and show how to perform the relativization in the presence of type classes.
1
Motivation
The proof assistant community is mainly divided in two successful camps. One camp, represented by provers such as Agda [7], Coq [6], Matita [5] and Nuprl [10], uses expressive type theories as a foundation. The other camp, represented by the HOL family of provers (including HOL4 [2], HOL Light [14], HOL Zero [3] and Isabelle/HOL [26]), mostly sticks to a form of classic set theory typed using simple types with rank-1 polymorphism. (Other successful provers, such as ACL2 [19] and Mizar [12], could be seen as being closer to the HOL camp, although technically they are not based on HOL.) According to the HOL school of thought, a main goal is to acquire a sweet spot: keep the logic as simple as possible while obtaining sufficient expressiveness. The notion of sufficient expressiveness is of course debatable, and has been debated. For example, PVS [29] includes dependent types (but excludes polymorphism), HOL-Omega [16] adds first-class type constructors to HOL, and Isabelle/HOL adds ad hoc overloading of polymorphic constants. In this paper, we want to propose a gentler extension of HOL. We do not want to promote new “first-class citizens,” but merely to give better credit to an old and venerable HOL citizen: the notion of types emerging from sets. c Springer International Publishing Switzerland 2016 J.C. Blanchette and S. Merz (Eds.): ITP 2016, LNCS 9807, pp. 200–218, 2016. DOI: 10.1007/978-3-319-43144-4 13
From Types to Sets by Local Type Definitions in Higher-Order Logic
201
The problem that we address in this paper is best illustrated by an example. Let lists : α set → α list set be the constant that takes a set A and returns the set of lists whose elements are in A, and P : α list → bool be another constant (whose definition is not important here). Consider the following statements, where we extend the usual HOL syntax by explicitly quantifying over types at the outermost level: ∀α. ∃xs α list . P xs ∀α. ∀Aα set . A = ∅ −→ (∃xs ∈ lists A. P xs)
(1) (2)
The formula (2) is a relativized form of (1),
Data Loading...
