nLab dialgebra

Redirected from "dialgebras".
Note: dialgebra and dialgebra both redirect for "dialgebras".
Contents

Context

Category theory

Algebra

Contents

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,DC, D and functors F,G:CDF, G: C \to D, a dialgebra of FF and GG (or an (F,G)(F, G)-dialgebra) is an object XX in CC (the carrier) and a morphism α:F(X)G(X)\alpha\colon F(X) \to G(X).

A homomorphism between two (F,G)(F, G)-dialgebras (X,α)(X, \alpha) and (Y,β)(Y, \beta) is a morphism m:XYm\colon X \to Y in CC such that the following square commutes (that is, that α\alpha and β\beta form XX- and YY-components of a natural transformation from FF to GG):

F(X) F(m) F(Y) α β G(X) G(m) G(Y). \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 CC. This yields the category of (F,G)(F, G)-dialgebras, Dialg(F,G)\text{Dialg}(F, G), which comes with a forgetful functor to CC.

Remark

When C=DC = D, then an algebra for an endofunctor is simply an (F,id C)(F, id_C)-dialgebra and a coalgebra for an endofunctor is simply an (id C,F)(id_C, F)-dialgebra.

Remark

Abstractly, the category of dialgebras is the inserter of FF and GG 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 FF). Semantics in dialgebras is not obtained via final objects (which are frequently absent in categories of dialgebras), but rather via quotients.

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)

Last revised on February 26, 2024 at 20:34:38. See the history of this page for a list of all contributions to it.