nLab dialgebra

Idea

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.

Definition

Definition

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$):

$$\array{ F(X) & \stackrel{F(m)}{\rightarrow} & F(Y) \\ \alpha\downarrow && \downarrow \beta \\ G(X) & \stackrel{G(m)}{\rightarrow} & G(Y) } \,.$$

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$.

Remark

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.

Remark

Abstractly, the category of dialgebras is the inserter of $F$ and $G$ in the 2-category Cat.

Relationship to inductive-inductive types

Initial dialgebras provide categorical semantics for inductive-inductive types.

Relationship to program semantics (process calculi)

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.

Related concepts

• algebra for an endofunctor, coalgebra over an endofunctor

• algebra for a profunctor

• inserter

References

• 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

• Fabrizio Montesi, Marco Peressotti, Linear Logic, the $\pi$-calculus, and their Metatheory: A Recipe for Proofs as Processes (arXiv:2106.11818)