symmetric monoidal (∞,1)-category of spectra
Dialgebras subsume the notion of algebras for an endofunctor and coalgebras for an endofunctor. Universal dialgebras were originally introduced by Lambek as “subequalizers”.
Disambiguation: For different notions of certain algebraic structures involving two algebraic operations introduced by Jean-Louis Loday and his school see associative dialgebra and dendriform dialgebra.
For categories $C, D$ and functors $F, G: C \to D$, a dialgebra of $F$ and $G$ (or an $(F, G)$-dialgebra) is an object $X$ in $C$ (the carrier) and a morphism $\alpha\colon F(X) \to G(X)$.
A homomorphism between two $(F, G)$-dialgebras $(X, \alpha)$ and $(Y, \beta)$ is a morphism $m\colon X \to Y$ in $C$ such that the following square commutes (that is, that $\alpha$ and $\beta$ form $X$- and $Y$-components of a natural transformation from $F$ to $G$):
Composition of such morphisms of algebras is given by composition of the underlying morphisms in $C$. This yields the category of $(F, G)$-dialgebras, $\text{Dialg}(F, G)$, which comes with a forgetful functor to $C$.
When $C = D$, then an algebra for an endofunctor is simply an $(F, id_C)$-dialgebra and a coalgebra for an endofunctor is simply an $(id_C, F)$-dialgebra.
Abstractly, the category of dialgebras is the inserter of $F$ and $G$ in the 2-category Cat.
Initial dialgebras provide categorical semantics for inductive-inductive types.
Dialgebras can be used to provide semantics to interactive programs; coalgebras have also been frequently used for the purpose. In contrast, dialgebras provide a natural way to express interactions (using the functor $F$). Semantics in dialgebras is not obtained via final objects (which are frequently absent in categories of dialgebras), but rather via quotients.
Joachim Lambek, Subequalizers, 1970
Peter Freyd, Recursive types reduced to inductive types, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science. IEEE, 1990.
Erik Poll, Jan Zwanenburg, From Algebras and Coalgebras to Dialgebras, Electronic Notes in Theoretical Computer Science 44(1), May 2001, 289-307, (doi:10.1016/S1571-0661(04)80915-0).
Tatsuya Hagino, A Typed Lambda Calculus with Categorical Type Constructors, 2005, link
Thorsten Altenkirch, Peter Morris, Fredrik Nordvall Forsberg, Anton Setzer, A Categorical Semantics for Inductive-Inductive Definitions, CALCO, 2011 link
Vincenzo Ciancia, Interaction and Observation: Categorical Semantics of Reactive Systems Trough Dialgebras, CALCO, 2013 link
Alwin Blok, Interaction, observation and denotation. A study of dialgebras for program semantics Master Thesis, Institute for Logic, Language and Computation, University of Amsterdam. link
Jim de Groot, Dirk Pattinson, Modal Intuitionistic Logics as Dialgebraic Logics, LICS ‘20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science July 2020, 355–369 (doi:10.1145/3373718.3394807).
A dialgebraic account of labeled transition systems is in
Last revised on February 26, 2024 at 20:34:38. See the history of this page for a list of all contributions to it.