Dialgebraic specification and modeling

Peter Padawitz

Dialgebraic specifications combine algebraic with coalgebraic ones. We present a uniform syntax, semantics and proof system for chains of signatures and axioms such that presentations of visible data types may alternate with those of hidden state types. Each element in the chain matches a design pattern that reflects some least/initial or greatest/final model construction over the respective predecessor in the chain. We sort out twelve such design patterns. Six of them lead to least models, the other six to greatest models. Each construction of the first group has its dual in the second group. All categories used in this approach are classes of structures with many-sorted carrier sets. The model constructions could be generalized to other categories, but this is not a goal of our approach. On the contrary, we aim at applications in software (and, maybe, also hardware) design and will show that for describing and solving problems in this area one need not go beyond categories of sets. Consequently, a fairly simple, though sufficiently powerful, syntax of dialgebraic specifications that builds upon classical algebraic notations as much as possible is crucial here. It captures the main constructions of both universal (co)algebra and relational fixpoint semantics, and thereby extends "Lawvere-style" algebraic theories from product to arbitrary polynomial types and modal logics from one- to many-sorted Kripke frames.

This work is still in progress. A draft paper containing its current state is http://ls5-www.cs.uni-dortmund.de/~peter/Dialg.ps. Slides some of which were presented on the meeting are here: http://ls5-www.cs.uni-dortmund.de/~peter/SwanSlides.pdf.