A complete calculus for equational deduction in coalgebraic specification

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 coalgebras of a restricted class of polynomial functors. This restriction allows us to borrow some ``algebraic'' notions for the formalization of the calculus. Aditionally, we discuss the notion of `colours' as a suitable dualization of variables in the algebraic case. Then the completeness result is extended to the ``non-ground'' or ``coloured'' case, which is shown to be expressive enough to deal with equations of hidden sort. Finally we discuss some weaknesses of the proposed results with respect to Birkhoff's, and we suggest possible future extensions.