A completeness result for equational deduction in coalgebraic specification

Abstract

The use of coalgebras for the specification of dynamical systems with a hidden state space is receiving more and more attention in the years, as a valid alternative to algebraic methods based on observational equivalences. However, to our knowledge, the coalgebraic framework is still lacking a complete equational deduction calculus which enjoys properties similar to those stated in Birkhoff’s completeness theorem for the algebraic case. In this paper we present a sound and complete equational calculus for a restricted class of coalgebras. We compare our notion of coalgebraic equation to others in the literature, and we hint at possible extensions of our framework.