Stepwise refinement of algebraic specifications is a well known formal method- ology for program development. However, traditional notions of refinement based on signa- ture morphisms are often too rigid to capture a number of relevant transformations in the context of software design, reuse, and adaptation. This paper proposes a new approach to refinement in which signature morphisms are replaced by logical interpretations as a means to witness refinements. The approach is first presented in the context of equational logic, and later generalised to deductive systems of arbitrary dimension. This allows, for example, refining sentential into equational specifications and the latter into modal ones.
As related work one should also mention @cite_71 @cite_53 where interpretations between theories are studied in the abstract framework of @math -institutions. The first reference is a generalisation of the work of Maibaum and his collaborators, whereas the second one generalises the way algebraic semantics on sentential logics is dealt with in abstract algebraic logic to the abstract setting of @math -institutions. Similar developments could arise by considering institutions and their (co-)morphisms @cite_29 @cite_15 @cite_62 . The work of Meseguer @cite_10 on , in which a theory of interpretations between logical systems is developed, should also be mentioned.
@cite_62 @cite_53 @cite_29 @cite_71 @cite_15 @cite_10
1533562965 1982879916 2010883554 1726442598
Seven years of COMPASS.- Inductively defined relations: A brief tutorial extended abstract.- On the role of category theory in the area of algebraic specifications.- Unification of theories: A challenge for computing science.- The larch shared language: Some open problems.- The lambda calculus as an abstract data type.- Unifying theories in different institutions.- Interchange format for inter-operability of tools and translation.- Experiments with partial evaluation domains for rewrite specifications.- Class-sort polymorphism in GLIDER.- Deontic concepts in the algebraic specification of dynamic systems: The permission case.- Reification - Changing viewpoint but preserving truth.- A category-based equational logic semantics to constraint programming.- Concurrent state transformations on abstract data types.- A view on implementing processes: Categories of circuits.- Combining algebraic and set-theoretic specifications.- Minimal term rewriting systems.- InterACT: An interactive theorem and completeness prover for algebraic specifications with conditional equations.- Rewriting and reasoning with set-relations II: The non-ground case completeness.- Termination of curryfied rewrite systems.- Formal specifications and test: Correctness and oracle.- Behavioural equivalence, bisimulation, and minimal realisation.- Using limits of parchments to systematically construct institutions of partial algebras.- Behavioural specifications in type theory.- Swinging data types.- Context institutions.- Object-oriented functional programming and type reconstruction.- Moving between logical systems.- Modular algebraic specifications and the orientation of equations into rewrite rules.- A model for I O in equational languages with don't care non-determinism.- Tool design for structuring mechanisms for algebraic specification languages with initial semantics. Various aspects of the work of Blok and Rebagliato on the algebraic semantics for deductive systems are studied in the context of logics formalized as π-institutions. Three kinds of semantics are surveyed: institution, matrix (system) and algebraic (system) semantics, corresponding, respectively, to the generalized matrix, matrix and algebraic semantics of the theory of sentential logics. After some connections between matrix and algebraic semantics are revealed, it is shown that every (finitary) N -rule based extension of an N -rule based π-institution possessing an algebraic semantics also possesses an algebraic semantics. This result abstracts one of the main theorems of Blok and Rebagliato. An attempt at a Blok-Rebagliato-style characterization of those π-institutions with a mono-unary category of natural transformations on their sentence functors having an algebraic semantics is also made. Finally, a necessary condition for a π-institution to possess an algebraic semantics is provided. c There is a population explosion among the logical systems used in computing science. Examples include first-order logic, equational logic, Horn-clause logic, higher-order logic, infinitary logic, dynamic logic, intuitionistic logic, order-sorted logic, and temporal logic; moreover, there is a tendency for each theorem prover to have its own idiosyncratic logical system. The concept of institution is introduced to formalize the informal notion of “logical system.” The major requirement is that there is a satisfaction relation between models and sentences that is consistent under change of notation. Institutions enable abstracting away from syntactic and semantic detail when working on language structure “in-the-large”; for example, we can define language features for building large logical system. This applies to both specification languages and programming languages. Institutions also have applications to such areas as database theory and the semantics of artificial and natural languages. A first main result of this paper says that any institution such that signatures (which define notation) can be glued together, also allows gluing together theories (which are just collections of sentences over a fixed signature). A second main result considers when theory structuring is preserved by institution morphisms. A third main result gives conditions under which it is sound to use a theorem prover for one institution on theories from another. A fourth main result shows how to extend institutions so that their theories may include, in addition to the original sentences, various kinds of constraint that are useful for defining abstract data types, including both “data” and “hierarchy” constraints. Further results show how to define institutions that allow sentences and constraints from two or more institutions. All our general results apply to such “duplex” and “multiplex” institutions. The structural property of π-institutions which requires consequence to be preserved under changes of language is weakened. The proposed weakly structural π-institutions encompass logics in which consequence does depend on the choice of non-logical symbols by associating locality conditions with signatures or signature morphisms. They also enable new logics to be defined by reusing existing ones, extending and adapting them in order to build formalisms that better fit the applications whose specification they are intended to support.