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.
|Formal Definitions and Theory (acm D.3.1), Semantics of Programming Languages (acm F.3.2), Mathematical Logic (acm F.4.1), Deduction and Theorem Proving (acm I.2.3)|
|Equational classes, universal algebra (msc 03C05), Equational logic, Mal'cev (Mal'tsev) conditions (msc 08B05), Rings and algebras with additional structure (msc 16Wxx), Semantics (msc 68Q55), Abstract data types; algebraic specification (msc 68Q65)|
|Software Engineering [SEN]|
Corradini, A. (1997). A complete calculus for equational deduction in coalgebraic specification. Software Engineering [SEN]. CWI.