zbMATH — the first resource for mathematics

Structuring theories with implicit morphisms. (English) Zbl 1444.68293
Fiadeiro, José Luiz (ed.) et al., Recent trends in algebraic development techniques. 24th IFIP WG 1.3 international workshop, WADT 2018, Egham, UK, July 2–5, 2018. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 11563, 154-173 (2019).
Summary: We introduce implicit morphisms as a concept in formal systems based on theories and theory morphisms. The idea is that there may be at most one implicit morphism from a theory \(S\) to a theory \(T\), and if \(S\)-expressions are used in \(T\) their semantics is obtained by automatically inserting the implicit morphism. The practical appeal of implicit morphisms is that they hit the sweet-spot of being extremely simple to understand and implement while significantly helping with structuring large collections of theories.
Concrete applications include elegantly identifying isomorphic theories and extending theories with definitions and theorems as well as efficiently building and maintaining large, fine-granular, and heterogeneous hierarchies of theories. Our results are formulated and implemented in the MMT language and system, and we expect they can be transferred to other morphism-based formalisms relatively easily.
For the entire collection see [Zbl 1428.68017].
68V30 Mathematical knowledge management
Full Text: DOI