Abstract
Theory graphs have theories as nodes and theory morphisms as edges. They can be seen as generators of categories with the nodes as the objects and the paths as the morphisms. But in contrast to generated categories, theory graphs do not allow for an equational theory on the morphisms. That blocks formalizing important aspects of theory graphs such as isomorphisms between theories.
MMT is essentially a logic-independent language for theory graphs. It previously supported theories and morphisms, and we extend it with morphism equality as a third primitive. We show the importance of this feature in several elementary formalizations that critically require stating and proving certain non-trivial morphism equalities. The key difficulty of this approach is that important properties of theory graphs now become undecidable and require heuristic methods.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The individual theory graphs are implicit in the respective libraries and usually not the subject of specific publications.
- 2.
Both (as well as our running example) are available at https://gl.mathhub.info/MMT/LATIN2/-/tree/devel/source/casestudies/2023-morpheq.
References
Autexier, S., Hutter, D., Mantel, H., Schairer, A.: Towards an evolutionary formal software-development using CASL. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 73–88. Springer, Heidelberg (2000). https://doi.org/10.1007/978-3-540-44616-3_5
Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-pi-calculus modulo. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 102–117. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73228-0_9
Carette, J., Farmer, W.M., Kohlhase, M.: Realms: a structure for consolidating knowledge about mathematical theories. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 252–266. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08434-3_19
Farmer, W.M., Guttman, J.D., Javier Thayer, F.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 567–581. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_192
Farmer, W., Guttman, J., Thayer, F.: IMPS: an interactive mathematical proof system. J. Autom. Reason. 11(2), 213–248 (1993)
Harper, R.: An equational logical framework for type theories (2021). https://arxiv.org/abs/2106.01484
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143–184 (1993)
Kammüller, F., Wenzel, M., Paulson, L.C.: Locales a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 149–165. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48256-3_11
Martin-Löf, P.: An intuitionistic theory of types: predicative part. In: Proceedings of the ’73 Logic Colloquium, pp. 73–118. North-Holland (1974)
Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71209-1_40
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_217
Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230(1), 1–54 (2013)
Rabe, F., Schürmann, C.: A practical module system for LF. In: Cheney, J., Felty, A. (eds.) Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), pp. 40–48. ACM Press (2009)
Rabe, F., Weber, F.: Three case studies on realms. In: Buzzard, K., Kutsia, T. (eds.) Intelligent Computer Mathematics, Informal Proceedings, pp. 46–51. Research Institute for Symbolic Computation (2022)
Srinivas, Y.V., Jüllig, R.: Specware: formal support for composing software. In: Möller, B. (ed.) MPC 1995. LNCS, vol. 947, pp. 399–422. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60117-1_22
Sannella, D., Wirsing, M.: A kernel language for algebraic specification and implementation extended abstract. In: Karpinski, M. (ed.) FCT 1983. LNCS, vol. 158, pp. 413–427. Springer, Heidelberg (1983). https://doi.org/10.1007/3-540-12689-9_122
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Rabe, F., Weber, F. (2023). Morphism Equality in Theory Graphs. In: Dubois, C., Kerber, M. (eds) Intelligent Computer Mathematics. CICM 2023. Lecture Notes in Computer Science(), vol 14101. Springer, Cham. https://doi.org/10.1007/978-3-031-42753-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-031-42753-4_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-42752-7
Online ISBN: 978-3-031-42753-4
eBook Packages: Computer ScienceComputer Science (R0)