Roberto Bruni, José Meseguer and Ugo Montanari,
Unpublished, 1999.
Keywords: Double Categories, 2-Categories, Tile Logic, Rewriting Logic, Strategies, PMEqtl, Maude
(Postscript)Abstract
2-categories and double categories are respectively the natural semantic ground for rewriting logic (RL) and tile logic (TL). Since 2-categories can be regarded as a special case of double categories, then RL can be easily embedded into TL, where also rewriting synchronization is considered. Since RL is the semantic basis of several existing languages, it is useful to map TL back into RL to have an executable framework for tile specifications. We extend the results of a previous work of two of the authors, focusing on tile systems where the algebraic structures for configurations and observations rely on some common auxiliary structure (e.g., for pairing, projecting, etc.). The new model theory required to relate the categorical models of the two logics is an extended version of the theory of 2-categories, and is defined using partial membership equational logic. More concretely, this semantic mapping yields a rewriting logic implementation of tile logic, where a meta-layer is required to control the rewritings, so that only tile proofs are computed.
