A systematic study of mappings between institutions

Abstract

Concerning different notions of mappings between institutions, we believe that the current state of the art is somehow unsatisfactory. On the one hand because of the variety of different concepts proposed in the literature. On the other hand because of the apparent lack of a suitable basis to formally discuss about what they mean and how they relate to each other. In this paper we aim at a systematic study of some of the most important notions of these mappings by proposing a methodology based on the concept of power institutions. Firstly, power institutions allow the investigation of the entire logical structure of an institution along these mappings, i.e., the satisfaction relation together with the satisfaction condition. Secondly, they allow this investigation in a systematic way, i.e., the transformation of the institutional logical structure can be described by means of simpler, more elementary transformations or units which are themselves also power institutions. These units are constructions which denote, e.g., typing reduction along functors between signatures, borrowing of models, common model theory, semantical restriction, and logical semantical restriction. The mappings can then be related to each other by showing that they all comprise a particular number of these more fundamental, elementary transformations.