Interpretations as coalgebra morphisms
Manuel A. Martins, Alexandre Madeira, Luís Soares Barbosa · 2010
The concept of logic or deductive system is transversal in computer science. Several notions have been proposed on the literature, some of them, highly abstract in order to capture a wide class of logics. An interesting one is the formalization of a logic as an algebra together with a closure operator over that universe (or, equivalently, as an algebra together with a closure system over its universe (eg. [2])). Palmigiano in [6] related this theory of abstract logic with the theory of coalgebras, another central field in computer science. She shows that an abstract logic can be represented as a C -coalgebra over Set with C the closure system contravariant functor; moreover the coalgebraic morphisms are the strict morphisms between the correspondent original logics, i.e., algebraic morphisms such that the pre-images of closed sets of the target logic are exactly the closed sets of the source logic. In the context of algebraic specification refinement, we came recently interested in relating “equivalent logics” by maps which fail to be signature morphisms, in particular, in [3] and [4], we have studied how refinements can be witnessed by logical interpretation. A logical interpretation is a multifunction f that preserves consequence in the following sense: given two logics A = 〈A,CA〉 and B = 〈B,CB〉, for all {x}∪X ⊆ A, x ∈ CA([X ]) iff f (x) ⊆ CB( f [X ]). A paradigmatic example of an interpretation, is multifunction τ : Fm(Bool)→ Fm(CPC) from boolean equations to propositional terms defined, for any φ ≈ φ ′ ∈ Fm(Bool), by τ(φ ≈ φ ′) = {φ → φ ′,φ ′→ φ}. The aim of the present work is to frame logics and interpretations along the lines of the coalgebraic perspective forward in [6].