Central submonads and notions of computation: Soundness, completeness and internal languages

Titouan Carette; Louis Lemonnier; Vladimir Zamdzhiev

doi:10.48550/arXiv.2207.09190

Central submonads and notions of computation: Soundness, completeness and internal languages

Titouan Carette
, Louis Lemonnier
, Vladimir Zamdzhiev

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science
Place of Publication	Boston, Massachusetts
Publisher	Institute of Electrical and Electronics Engineers
Pages	1-13
Number of pages	13
ISBN (Electronic)	9798350335873
ISBN (Print)	9798350335880
DOIs	https://doi.org/10.48550/arXiv.2207.09190 https://doi.org/10.1109/LICS56636.2023.10175687
Publication status	Published - 14 Jul 2023
Event	The 38th Annual ACM/IEEE Symposium on Logic in Computer Science - Boston University, Boston, United States Duration: 26 Jun 2023 → 29 Jun 2023 https://lics.siglog.org/lics23/

Publication series

Name	Proceedings of the ACM/IEEE Symposium on Logic in Computer Science
Publisher	IEEE
ISSN (Print)	1043-6871
ISSN (Electronic)	2575-5528

Symposium

Symposium	The 38th Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated title	LICS 2023
Country/Territory	United States
City	Boston
Period	26/06/23 → 29/06/23
Internet address	https://lics.siglog.org/lics23/

Keywords / Materials (for Non-textual outputs)

computer science
computer languages
computational modeling
semantics
mathematical models

Access to Document

CaretteEtalLCS2023CentralSubmonadsAndNotionsAccepted author manuscript, 364 KBLicence: Creative Commons: Attribution (CC-BY)

Cite this

Carette, T., Lemonnier, L., & Zamdzhiev, V. (2023). Central submonads and notions of computation: Soundness, completeness and internal languages. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 1-13). (Proceedings of the ACM/IEEE Symposium on Logic in Computer Science). Institute of Electrical and Electronics Engineers. https://doi.org/10.48550/arXiv.2207.09190, https://doi.org/10.1109/LICS56636.2023.10175687

Carette, Titouan ; Lemonnier, Louis ; Zamdzhiev, Vladimir. / Central submonads and notions of computation : Soundness, completeness and internal languages. 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science. Boston, Massachusetts : Institute of Electrical and Electronics Engineers, 2023. pp. 1-13 (Proceedings of the ACM/IEEE Symposium on Logic in Computer Science).

@inproceedings{ff96d0df58004422b6cf90704ab4dd59,

title = "Central submonads and notions of computation: Soundness, completeness and internal languages",

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.",

keywords = "computer science, computer languages, computational modeling, semantics, mathematical models",

author = "Titouan Carette and Louis Lemonnier and Vladimir Zamdzhiev",

year = "2023",

month = jul,

day = "14",

doi = "10.48550/arXiv.2207.09190",

language = "English",

isbn = "9798350335880",

series = "Proceedings of the ACM/IEEE Symposium on Logic in Computer Science",

publisher = "Institute of Electrical and Electronics Engineers",

pages = "1--13",

booktitle = "2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science",

address = "United States",

note = "The 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023 ; Conference date: 26-06-2023 Through 29-06-2023",

url = "https://lics.siglog.org/lics23/",

}

Carette, T, Lemonnier, L & Zamdzhiev, V 2023, Central submonads and notions of computation: Soundness, completeness and internal languages. in 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science. Proceedings of the ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, Boston, Massachusetts, pp. 1-13, The 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, United States, 26/06/23. https://doi.org/10.48550/arXiv.2207.09190, https://doi.org/10.1109/LICS56636.2023.10175687

Central submonads and notions of computation: Soundness, completeness and internal languages. / Carette, Titouan; Lemonnier, Louis; Zamdzhiev, Vladimir.
2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science. Boston, Massachusetts: Institute of Electrical and Electronics Engineers, 2023. p. 1-13 (Proceedings of the ACM/IEEE Symposium on Logic in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Central submonads and notions of computation

T2 - The 38th Annual ACM/IEEE Symposium on Logic in Computer Science

AU - Carette, Titouan

AU - Lemonnier, Louis

AU - Zamdzhiev, Vladimir

PY - 2023/7/14

Y1 - 2023/7/14

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

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

KW - computer science

KW - computer languages

KW - computational modeling

KW - semantics

KW - mathematical models

U2 - 10.48550/arXiv.2207.09190

DO - 10.48550/arXiv.2207.09190

M3 - Conference contribution

SN - 9798350335880

T3 - Proceedings of the ACM/IEEE Symposium on Logic in Computer Science

SP - 1

EP - 13

BT - 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science

PB - Institute of Electrical and Electronics Engineers

CY - Boston, Massachusetts

Y2 - 26 June 2023 through 29 June 2023

ER -

Carette T, Lemonnier L, Zamdzhiev V. Central submonads and notions of computation: Soundness, completeness and internal languages. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science. Boston, Massachusetts: Institute of Electrical and Electronics Engineers. 2023. p. 1-13. (Proceedings of the ACM/IEEE Symposium on Logic in Computer Science). doi: 10.48550/arXiv.2207.09190, 10.1109/LICS56636.2023.10175687

Central submonads and notions of computation: Soundness, completeness and internal languages

Abstract

Publication series

Symposium

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Cite this