Coequational logic for accessible functors (Q618173): Difference between revisions

Coequational logic, first proposed by \textit{J. Adámek} [``A logic of coequations'', Lect. Notes Comput. Sci. 3634, 70--86 (2005; Zbl 1136.03313)], is a specification formalism for generic reactive systems, modelled as coalgebras. Coequations \textit{interdict} certain patterns of behaviour; explicitly, a coequation is an element \(q\) of a cofree coalgebra \(Q_C\) with set \(C\) of colours, and a coalgebra \(S\) satisfies \(q\) if for all colourings of \(S\) the induced unique coalgebra morphism \(S\to Q_C\) factors through the set \(Q_C-\{q\}\). Adámek gave a sound and complete coequational calculus for the case where the coalgebraic type functor is polynomial, i.e., a sum of powers of the identity. In this case, \(Q_C\) consists of coloured trees, and the calculus consists of two simple rules saying that a tree is interdicted if any of its subtrees or recolourings is interdicted, respectively. This result is extended to a more general class of \textit{accessible} functors in the current work. Specifically, it is assumed that the type functor \(H\) is accessible and has a \textit{regular} presentation \(\epsilon: H_\Sigma\to H\) as a quotient \(\epsilon\) of a polynomial functor \(H_\Sigma\) induced by an algebraic signature \(\Sigma\), where regularity of the presentation means that the induced \(\Sigma\)-equations are regular, i.e.\ have the same free variables on both sides. The development is further based on a detailed analysis of how a right inverse \(\eta\) to \(\epsilon_{Q_C}\) induces a canonical choice of representative trees w.r.t.\ the quotient map from the cofree \(H_\Sigma\)-coalgebra over \(C\) to \(Q_C\). The sound and complete deduction system then has child and recolouring rules essentially as before, except that both the subtree relation and the recolouring relation are understood at the level of \(\eta\)-representative trees. It is further shown that the regularity condition is in fact necessary for soundness and completeness of this system \textit{for all choices of \(\eta\)}, under the mild additional assumption that \(H\) has a non-trivial final coalgebra. Some additional results are mentioned on obtaining soundness and completeness for further functors and specific choices of \(\eta\).