Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages

TItouan Carette, Louis Lemonnier, Vladimir Zamdzhiev

TL;DR

This paper develops a comprehensive theory of the centre of strong monads on symmetric monoidal categories, showing that under mild conditions the centre is a commutative submonad and giving three equivalent characterizations. It generalizes from Set to broad categories, provides a non-centralisable counterexample, and connects centers to Lawvere theories. The authors then introduce central submonads as a more flexible, computationally friendly generalization and develop a full computational interpretation via the Central Submonad Calculus (CSC), including syntactic models, categorical models, denotational semantics, and an internal-language correspondence with completeness results. Overall, the work ties together categorical structure, denotational semantics, and programming-language syntax to support robust modeling of central (commuting) effects in higher-order languages, with clear directions for future study of commutants, distributive laws, and arrows.

Abstract

Monads in category theory are algebraic structures that can be used to model computational effects in programming languages. We show how the notion of "centre", and more generally "centrality", i.e. the property for an effect to commute with all other effects, may be formulated for strong monads acting on symmetric monoidal categories. We identify three equivalent conditions which characterise the existence of the centre of a strong monad (some of which relate it to the premonoidal centre of Power and Robinson) and we show that every strong monad on many well-known naturally occurring categories does admit a centre, thereby showing that this new notion is ubiquitous. More generally, we study central submonads, which are necessarily commutative, just like the centre of a strong monad. We provide a computational interpretation by formulating equational theories of lambda calculi equipped with central submonads, we describe categorical models for these theories and prove soundness, completeness and internal language results for our semantics.

Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages

TL;DR

This paper develops a comprehensive theory of the centre of strong monads on symmetric monoidal categories, showing that under mild conditions the centre is a commutative submonad and giving three equivalent characterizations. It generalizes from Set to broad categories, provides a non-centralisable counterexample, and connects centers to Lawvere theories. The authors then introduce central submonads as a more flexible, computationally friendly generalization and develop a full computational interpretation via the Central Submonad Calculus (CSC), including syntactic models, categorical models, denotational semantics, and an internal-language correspondence with completeness results. Overall, the work ties together categorical structure, denotational semantics, and programming-language syntax to support robust modeling of central (commuting) effects in higher-order languages, with clear directions for future study of commutants, distributive laws, and arrows.

Abstract

Monads in category theory are algebraic structures that can be used to model computational effects in programming languages. We show how the notion of "centre", and more generally "centrality", i.e. the property for an effect to commute with all other effects, may be formulated for strong monads acting on symmetric monoidal categories. We identify three equivalent conditions which characterise the existence of the centre of a strong monad (some of which relate it to the premonoidal centre of Power and Robinson) and we show that every strong monad on many well-known naturally occurring categories does admit a centre, thereby showing that this new notion is ubiquitous. More generally, we study central submonads, which are necessarily commutative, just like the centre of a strong monad. We provide a computational interpretation by formulating equational theories of lambda calculi equipped with central submonads, we describe categorical models for these theories and prove soundness, completeness and internal language results for our semantics.
Paper Structure (26 sections, 20 theorems, 38 equations, 7 figures)

This paper contains 26 sections, 20 theorems, 38 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Related Work
  3. Background
  4. Strong and Commutative Monads
  5. Semantics of the $\lambda$-calculus with effects
  6. Denotational semantics.
  7. Premonoidal Structure of Strong Monads
  8. The Centre of a Strong Monad
  9. The Centre of a Monad on $\mathbf{Set}$
  10. The General Construction of the Centre
  11. A Non-centralisable Monad
  12. Examples of Centres of Strong Monads
  13. Categories whose Strong Monads are Centralisable
  14. Specific Examples of Centralisable Monads
  15. Relationship with Lawvere theories
  16. ...and 11 more sections

Key Result

Proposition 2.7

If $\iota : {\mathcal{T}} \Rightarrow {\mathcal{P}}$ is a submonad morphism, then the functor ${\mathcal{I}}:{\mathbf C}_{\mathcal{T}}\to {\mathbf C}_{\mathcal{P}},$ defined by ${\mathcal{I}}(X) = X$ on objects and ${\mathcal{I}}(f:X\to {\mathcal{T}} Y) = \iota_Y\circ f \colon X \to {\mathcal{P}} Y$

Figures (7)

  • Figure 1: Grammars and typing rules.
  • Figure 2: Equational rules.
  • Figure 3: Grammars and typing rules.
  • Figure 4: Equational rules for types.
  • Figure 5: Type conversion rules.
  • ...and 2 more figures

Theorems & Definitions (88)

  • Definition 2.1: Monad
  • Definition 2.2: Strong Monad
  • Definition 2.3: Commutative Monad
  • Remark 2.4
  • Definition 2.5: Morphism of Strong Monads jacobs-coalgebra
  • Definition 2.6: Kleisli category
  • Proposition 2.7: jacobs-coalgebra
  • Definition 2.8: Premonoidal Centre power-premonoidal
  • Remark 2.9
  • Definition 3.1: Centre
  • ...and 78 more