nLab
dialgebra

Contents

Context

Category theory

Algebra

Contents

Idea

Dialgebras subsume the notion of algebras for an endofunctor and coalgebras for an endofunctor.

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.

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

  • 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

Last revised on September 3, 2019 at 05:01:17. See the history of this page for a list of all contributions to it.