Modal logic and algebraic specifications (Q685423): Difference between revisions

The established approaches to the semantics of algebraic (equational) specifications are based on a category-theoretic perspective. When possible interpretations are viewed as a category, the extreme points -- the initial and final algebras -- present themselves as natural candidates for the canonical interpretation. However, neither choice provides a satisfactory solution for incomplete specifications of abstract data types --- the initial algebra is not abstract enough and the final algebra often does not exist. We argue that in much of the work on algebraic specifications, the categorical viewpoint is simply a convenient technical device to semantically capture the modalities of necessity and possibility. It is actually more natural to consider the semantic problem from the perspective of modal logic, gathering possible interpretations into a Kripke model. When necessity and possibility are added as modal operators in the logical language, a new candidate for the canonical interpretation --- which we call the optimal algebra --- arises naturally. The optimal algebra turns out to be a natural generalization of the final algebra, and provides a satisfactory semantics in situations where the spirit of final algebra semantics is desired but a final algebra does not exist. Optimal semantics has a topological flavor. Our Kripke models are topological spaces in a natural way. In most (but not all) of the interesting cases, the Baire Category Theorem holds for the topology of a Kripke model, in which case the optimal semantics validates exactly those equational properties which hold in dense open subsets of the Kripke model. In analogy to many similar situations, we may regard these as properties that hold almost everywhere in the model.