×

zbMATH — the first resource for mathematics

From types to sets by local type definition in higher-order logic. (English) Zbl 07024458
Summary: 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 consistency. 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.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Kunčar, O., Popescu, A.: From types to sets by local type definition in higher-order logic. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016, LNCS, vol. 9807, pp. 200-218, Springer (2016)
[2] Bove, A., Dybjer, P., Norell, U.: A brief overview of AGDA—a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009, LNCS, vol. 5674, pp. 73-78, Springer (2009) · Zbl 1252.68062
[3] Bertot, Y., Castéran, P.: Interactive theorem proving and program development—Coq’Art: the calculus of inductive constructions. In: Texts in Theoretical Computer Science. An EATCS Series, Springer (2004) · Zbl 1069.68095
[4] Asperti, A., Ricciotti, W., Coen, C.S., Tassi, E.: The Matita interactive theorem prover. In: CADE-23, pp. 64-69 (2011) · Zbl 1341.68179
[5] Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Inc., Upper Saddle River (1986)
[6] The HOL4 Theorem Prover. http://hol.sourceforge.net/
[7] Harrison, J.: HOL Light: a tutorial introduction. In: Srivas, M.K., Camilleri, A.J. (eds.) FMCAD ’96, LNCS, vol. 1166, pp. 265-269, Springer (1996)
[8] Adams, M.: Introducing HOL Zero—(extended abstract). In: Fukuda, K., van der Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010, LNCS, vol. 6327, pp. 142-143, Springer, Berlin (2010)
[9] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—a proof assistant for higher-order logic. part of the Isabelle2015 distribution (2015). https://isabelle.in.tum.de/dist/Isabelle2015/doc/tutorial.pdf · Zbl 0994.68131
[10] Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer, Dordrecht (2000)
[11] Bancerek, G.; Byliński, C.; Grabowski, A.; Korniłowicz, A.; Matuszewski, R.; Naumowicz, A.; Pąk, K.; Urban, J.; Kerber, M. (ed.); Carette, J. (ed.); Kaliszyk, C. (ed.); Rabe, F. (ed.); Sorge, V. (ed.), Mizar: state-of-the-art and beyond, 261-279, (2015), Berlin · Zbl 1417.68201
[12] Shankar, N., Owre, S., Rushby, J.M.: PVS Tutorial. Computer Science Laboratory, SRI International (1993)
[13] Homeier, P.V.: The HOL-Omega logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009, LNCS, vol. 5674, pp. 244-259, Springer (2009) · Zbl 1252.68257
[14] Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: POPL ’89, ACM, pp. 60-76 (1989)
[15] Nipkow, T.; Snelting, G.; Hughes, J. (ed.), Type classes and overloading resolution via order-sorted unification, No. 523, 1-14, (1991), Berlin
[16] Wickerson, J.: Isabelle Users List (2013). https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-February/msg00222.html
[17] Immler, F.: Generic Construction of Probability Spaces for Paths of Stochastic Processes. Master’s Thesis, Institut für Informatik, Technische Universität München (2012)
[18] Aransay, J.; Ballarin, C.; Rubio, J., A mechanized proof of the basic perturbation lemma, J. Autom. Reason., 40, 271-292, (2008) · Zbl 1140.68059
[19] Chan, H., Norrish, M.: Mechanisation of AKS algorithm: part 1—the main theorem. In: Urban, C., Zhang, X. (eds.) ITP 2015, LNCS, vol. 9236, pp. 117-136, Springer (2015) · Zbl 06481859
[20] Coble, A.R.: Formalized information-theoretic proofs of privacy using the HOL4 theorem-prover. In: Borisov, N., Goldberg, I. (eds.) PETS 2008, LNCS, vol. 5134, pp. 77-98, Springer (2008)
[21] Hölzl, J., Heller, A.: Three chapters of measure theory in Isabelle/HOL. In: van Eekelen, M.C.J.D., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011, LNCS, vol. 6898, pp. 135-151, Springer (2011) · Zbl 1342.68287
[22] Maggesi, M.: A formalisation of metric spaces in HOL light (2015). Presented at the Workshop Formal Mathematics for Mathematicians. CICM 2015 (published online). http://www.cicm-conference.org/2015/fm4m/FMM_2015_paper_3.pdf · Zbl 1425.68376
[23] Types to Sets in the Isabelle distribution. https://isabelle.in.tum.de/dist/library/HOL/HOL-Types_To_Sets/index.html
[24] Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993) · Zbl 0779.68007
[25] Harrison, J.: HOL Done Right (1995). http://www.cl.cam.ac.uk/ jrh13/papers/holright.html
[26] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Berlin (2002) · Zbl 0994.68131
[27] Kunčar, O., Popescu, A.: Comprehending Isabelle/HOL’s consistency. In: Yang, H. (ed.) ESOP 2017, LNCS, vol. 10201, pp. 724-749, Springer (2017) · Zbl 06721341
[28] Pitts, A.: Introduction to HOL: a theorem proving environment for higher order logic, chap. The HOL logic, In: Gordon and Melham [15], pp. 191-232 (1993)
[29] Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs ’97, LNCS, vol. 1275, pp. 307-322, Springer (1997)
[30] Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006, LNCS, vol. 4502, pp. 160-174, Springer (2006) · Zbl 1178.68529
[31] Krauss, A., Schropp, A.: A mechanized translation from higher-order logic to set theory. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010, LNCS, vol. 6172, pp. 323-338, Springer (2010) · Zbl 1291.68355
[32] Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013, LNCS, vol. 8307, pp. 131-146, Springer (2013) · Zbl 1426.68284
[33] Kunčar, O.: Types, Abstraction and Parametric Polymorphism in Higher-Order Logic. Ph.D. Thesis, Fakultät für Informatik, Technische Universität München (2016). http://www21.in.tum.de/ kuncar/documents/kuncar-phdthesis.pdf
[34] Traytel, D., Popescu, A., Blanchette, J.C.: Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. In: LICS 2012, IEEE, pp. 596-605 (2012) · Zbl 1362.68251
[35] Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress, pp. 513-523 (1983)
[36] Wadler, P.: Theorems for free! In: FPCA ’89, ACM, pp. 347-359 (1989)
[37] Mitchell, J.C.: Representation independence and data abstraction. In: POPL ’86, ACM, pp. 263-276 (1986)
[38] Harrison, J., The HOL Light theory of Euclidean space, J. Autom. Reason., 50, 173-190, (2013) · Zbl 1260.68373
[39] Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005, LNCS, vol. 3603. Springer, Oxford (2005) · Zbl 1152.68520
[40] Divasón, J., Joosten, S., Thiemann, R., Yamada, A.: A formalization of the Berlekamp-Zassenhaus factorization algorithm. In: CPP, pp. 17-29 (2017)
[41] Kunčar, O.; Popescu, A., Safety and conservativity of definitions in HOL and Isabelle/HOL, Proc. ACM Program. Lang., 24, 1-24, (2017)
[42] The HOL-Algebra Library. http://isabelle.in.tum.de/library/HOL/HOL-Algebra/
[43] Ballarin, C., Locales: a module system for mathematical theories, J. Autom. Reason., 52, 123-153, (2014) · Zbl 1315.68218
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.