Structure-Preserving Diagram Operators - Roux, Navid; Rabe, Florian (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2021)
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.
CRIS-Team Scopus Importer:2021-05-07