Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 2/2019

04.06.2018

From Types to Sets by Local Type Definition in Higher-Order Logic

verfasst von: Ondřej Kunčar, Andrei Popescu

Erschienen in: Journal of Automated Reasoning | Ausgabe 2/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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 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.
Vorheriger Artikel The Flow of ODEs: Formalization of Variational Equation and Poincaré Map
Nächster Artikel Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
Let us recall that HOL does not allow for dependent types.
 
2
Dependent type theory has its own pluses and minuses. Even if we came to the conclusion that the pluses prevail, we do not know how to combine dependent types with higher-order logic and the tools built around it. Hence the avoidance of the dependent types. Note that HOL-Omega does not include dependent types either.
 
3
There is always such \(\rho \) since we work with well-typed terms and moreover it is unique.
 
4
In order for this to work, we have silently assumed a connection between \(\mathsf {P}_{\beta \,\mathsf {list}\rightarrow \mathsf {bool}}\) and \(\mathsf {P}_{\alpha \,\mathsf {list}\rightarrow \mathsf {bool}}\), namely that \(\mathsf {P}\) is parametric w.r.t. injection. More precisely that for every binary relation \(R_{\alpha \rightarrow \beta \rightarrow \mathsf {bool}}\) defining an injection of \(\beta \) into \(\alpha \) and for every two lists \({ xs }_{\alpha \,\mathsf {list}}\) and \({ ys }_{\beta \,\mathsf {list}}\) whose elements are pairwise related by R, it holds that \(\mathsf {P}\;{ xs }\) if and only if \(\mathsf {P}\;{ ys }\)—see Sect. 7 for more on parametricity.
 
5
This is Wenzel’s approach [29] to represent axiomatic type classes by internalizing them as predicates on types, i.e., constants of type \(\forall \alpha .\;\mathsf {bool}\). As this particular type is not allowed in Isabelle, Wenzel uses instead \(\alpha \;\mathsf {itself} \rightarrow \mathsf {bool}\), where \(\alpha \;\mathsf {itself}\) is a singleton type.
 
6
Let us recall that \(\forall x.P\;x\) is a shorthand for https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9464-6/MediaObjects/10817_2018_9464_IEq489_HTML.gif and \(\forall x \in A.P\;x\) for https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9464-6/MediaObjects/10817_2018_9464_IEq491_HTML.gif , where \({{\mathsf {All}}}\) and \({{\mathsf {Ball}}}\) are the HOL constants for quantification. Thus the statement about isomorphism between the two quantifications means isomorphism between \({{\mathsf {All}}}\) and \({{\mathsf {Ball}}}\;A\).
 
7
Unless there is a type depending on \(*\).
 
8
The setup requires more than just the name of a relator. Besides making sure that the relator satisfies many natural properties such as monotonicity or compositionality, we use other concepts such as the knowledge that “lists whose elements are in A” can be expressed by \({{\mathsf {lists}}}\;A\). See the complete description of the required structure in the first author’s thesis [33, §4.7].
 
9
These rules are related to Reynolds’s relational parametricity [35] and Wadler’s free theorems [36]. The Transfer tool is a working implementation of Mitchell’s representation independence [37] and it demonstrates that transferring of properties across related types can be organized and largely automated using relational parametricity.
 
10
The type \(\forall \alpha _\varUpsilon .\sigma \) is not directly expressible in HOL but we can use Wenzel’s trick and write \(\alpha _\varUpsilon \,\mathsf {itself} \rightarrow \sigma \); see footnote 5 on page 13.
 
11
We assumed that the type class \(\varUpsilon \) does not have any associated operations. Lifting the description to the most general version of \(\varUpsilon \) is analogous to the approach in Sect. 6.4 and we omit it here.
 
12
In the worst case, we can always set S to be the range of \(f^\mathsf {on}\) and define g by choice.
 
Literatur
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)
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)
4.
Asperti, A., Ricciotti, W., Coen, C.S., Tassi, E.: The Matita interactive theorem prover. In: CADE-23, pp. 64–69 (2011)
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.
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.
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.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) Intelligent Computer Mathematics, pp. 261–279. Springer, Berlin (2015)CrossRef
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)
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.: Type classes and overloading resolution via order-sorted unification. In: Hughes, J. (ed.) Functional Programming Languages and Computer Architecture, LNCS, vol. 523, pp. 1–14. Springer, Berlin (1991)CrossRef
16.
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(4), 271–292 (2008)MathSciNetCrossRefMATH
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)
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)
22.
23.
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)MATH
25.
26.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Berlin (2002)MATH
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)
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)
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)
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)
33.
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)
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.
39.
Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005, LNCS, vol. 3603. Springer, Oxford (2005)
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.
43.
Metadaten
Titel
From Types to Sets by Local Type Definition in Higher-Order Logic
verfasst von
Ondřej Kunčar
Andrei Popescu
Publikationsdatum
04.06.2018
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 2/2019
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-018-9464-6

Weitere Artikel der Ausgabe 2/2019

Journal of Automated Reasoning 2/2019 Zur Ausgabe

OriginalPaper

Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL

OriginalPaper

Proof Pearl: Bounding Least Common Multiples with Triangles

OriginalPaper

Formally Verified Approximations of Definite Integrals

EditorialNotes

Selected Extended Papers of ITP 2016: Preface

OriginalPaper

Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms

OriginalPaper

The Flow of ODEs: Formalization of Variational Equation and Poincaré Map