Coequational logic for accessible functors
type: Item
instance of: scholarly article
title: Coequational logic for accessible functors
zbMATH Open document ID: 1222.03031
author: Daniel Schwencke
published in: Information and Computation
publication date: 2011-01-14T00:00:00Z
review text: 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 \t…
reviewed by: Lutz Schröder
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 18A99
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 5836752
zbMATH Keywords: coalgebra
zbMATH Keywords: coequational logic
zbMATH Keywords: accessible functor
zbMATH Keywords: representative tree
MaRDI profile type: Publication
full work available at URL: j.ic.2009.10.010
OpenAlex ID: W2040834264
cites work: Computer Science Logic
cites work: Recursive coalgebras of finitary functors
cites work: Terminal coalgebras and free iterative theories
cites work: On tree coalgebras and coalgebra presentations
cites work: Q3996444
cites work: Coalgebras of bounded type
cites work: Q4533390
cites work: A fixpoint theorem for complete categories
cites work: Coalgebraic logic
cites work: Coalgebraic modal logic: soundness, completeness and decidability of local consequence
cites work: Universal coalgebra: A theory of systems
cites work: Coequational logic for finitary functors
cites work: On the final sequence of a finitary set functor
DOI: 10.1016/J.IC.2009.10.010
description: scientific article; zbMATH DE number 5836752