Top

Published in:

2018 | OriginalPaper | Chapter

Theories as Types

Authors : Dennis Müller, Florian Rabe, Michael Kohlhase

Published in: Automated Reasoning

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Theories are an essential structuring principle that enable modularity, encapsulation, and reuse in formal libraries and programs (called classes there). Similar effects can be achieved by dependent record types. While the former form a separate language layer, the latter are a normal part of the type theory. This overlap in functionality can render different systems non-interoperable and lead to duplication of work.

We present a type-theoretic calculus and implementation of a variant of record types that for a wide class of formal languages naturally corresponds to theories. Moreover, we can now elegantly obtain a contravariant functor that reflects the theory level into the object level: for each theory we obtain the type of its models and for every theory morphism a function between the corresponding types. In particular this allows shallow – and thus structure-preserving – encodings of mathematical knowledge and program specifications while allowing the use of object-level features on models, e.g. equality and quantification.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback

next chapter Datatypes with Shared Selectors

This is sometimes called horizontal subtyping. In that case, the straightforward covariance rule for record types is called vertical subtyping.

Note that it does not matter how the fields of the record are split into \(\varDelta _1\) and \(\varDelta _2\) as long as \(\varDelta _1\) contains all fields that the declaration of x depends on.

It is possible and important in practice to also define \(\varDelta \oplus E\) when the types/definitions in d and e are provably equal. We omit that here for simplicity.

Note that because \(P\cap P'\) depends on the syntactic structure of P and \(P'\), it only approximates the least upper bound of \(\mathtt {Mod}\left( P\right) \) and \(\mathtt {Mod}\left( P'\right) \) and is not stable under, e.g., flattening of P and \(P'\). But it can still be very useful in certain situations.

The computation of \(\max P\) may look like it requires flattening. But it is easy to compute and cache its value for every named theory.

In practice, these substitutions are easy to implement without flattening r because we can cache for every theory which theories it includes and which names it declares.

[Bra13]

Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23(5), 552–593 (2013)MathSciNetCrossRef

[Con+86]

Constable, R., et al.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall, Upper Saddle River (1986)

[Deh+16]

Dehaye, P.-O., et al.: Interoperability in the OpenDreamKit project: the math-in-the-middle approach. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 117–131. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42547-4_9. https://github.com/OpenDreamKit/OpenDreamKit/blob/master/WP6/CICM2016/published.pdfCrossRef

[FGT92]

Farmer, W., Guttman, J., Thayer, F.: Little theories. In: Kapur, D. (ed.) Conference on Automated Deduction, pp. 467–581 (1992)CrossRef

[Gog+93]

Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.: Introducing OBJ. In: Goguen, J., Coleman, D., Gallimore, R. (eds.) Applications of Algebraic Specification Using OBJ. Cambridge (1993)

[Har+12]

Hardin, T., et al.: The FoCaLiZe Essential (2012). http://focalize.inria.fr/

[Har96]

Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996). https://doi.org/10.1007/BFb0031814CrossRef

[Koh+17]

Kohlhase, M., Koprucki, T., Müller, D., Tabelow, K.: Mathematical models as research data via flexiformal theory graphs. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 224–238. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-62075-6_16CrossRef

[LFX]

MathHub MMT/LFX Git Repository. http://gl.mathhub.info/MMT/LFX. Accessed 15 May 2015

[Luo09]

Luo, Z.: Manifest fields and module mechanisms in intensional type theory. In: Berardi, S., Damiani, F., de’Liguoro, U. (eds.) TYPES 2008. LNCS, vol. 5497, pp. 237–255. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02444-3_15CrossRef

[Mat]

Mathematical Components. http://www.msr-inria.fr/projects/mathematical-components-2/

[Mit]

MitM/SMGLoM. https://gl.mathhub.info/MitM/smglom. Accessed 01 Feb 2018

[MRK]

Müller, D., Rabe, F., Kohlhase, M.: Theories as Types. http://kwarc.info/kohlhase/submit/tatreport.pdf

[ORS92]

Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_217CrossRef

[Rab14]

Rabe, F.: How to identify, translate, and combine logics? J. Log. Comput. (2014). https://doi.org/10.1093/logcom/exu079

[Rab17]

Rabe, F.: A modular type reconstruction algorithm. ACM Trans. Comput. Log. (2017). Accepted pending minor revision: https://kwarc.info/people/frabe/Research/rabe_recon_17.pdf

[RK13]

Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230(1), 1–54 (2013)MathSciNetCrossRef

[SW11]

Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. CoRR abs/1102.1323 (2011). arXiv:1102.1323MathSciNetCrossRef

[TB85]

Trybulec, A., Blair, H.: Computer assisted reasoning with MIZAR. In: Joshi, A. (ed.) Proceedings of the 9th International Joint Conference on Artificial Intelligence, pp. 26–28. Morgan Kaufmann (1985)

[Wen09]

Wenzel, M.: The Isabelle/Isar Reference Manual, 3 December 2009. http://isabelle.in.tum.de/documentation.html

[Coq15]

Coq Development Team: The Coq Proof Assistant: Reference Manual. Technical report, INRIA (2015)

Title: Theories as Types
Authors: Dennis Müller
Florian Rabe
Michael Kohlhase
Publisher: Springer International Publishing
Book: Automated Reasoning
Print ISBN: 978-3-319-94204-9

Electronic ISBN: 978-3-319-94205-6

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-319-94205-6_38

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner