Structure-Preserving Diagram Operators
Roux N, Rabe F (2021)
Publication Type: Conference contribution
Publication year: 2021
Journal
Publisher: Springer Science and Business Media Deutschland GmbH
Book Volume: 12669 LNCS
Pages Range: 142-163
Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Event location: Dublin
ISBN: 9783030737849
DOI: 10.1007/978-3-030-73785-6_8
Abstract
Theory operators are meta-level operators in logic that map theories to theories. Often these are functorial in that they can be extended to theory morphisms and possibly enjoy further valuable properties such as preserving inclusions. Thus, it is possible to apply them to entire diagrams at once, often in a way that the output diagram mimics any morphisms or modular structure of the input diagram. Our results are worked out using the Mmt language for structured theories instantiated with the logical framework LF for basic theories, but they can be easily transferred to other languages. We investigate how Mmt/LF diagram operators can be defined conveniently and give multiple examples.
Authors with CRIS profile
How to cite
APA:
Roux, N., & Rabe, F. (2021). Structure-Preserving Diagram Operators. In Markus Roggenbach (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 142-163). Dublin, IE: Springer Science and Business Media Deutschland GmbH.
MLA:
Roux, Navid, and Florian Rabe. "Structure-Preserving Diagram Operators." Proceedings of the 25th International Workshop on Algebraic Development Techniques, WADT 2020, Dublin Ed. Markus Roggenbach, Springer Science and Business Media Deutschland GmbH, 2021. 142-163.
BibTeX: Download