License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2021.131
URN: urn:nbn:de:0030-drops-142007
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14200/
Go to the corresponding LIPIcs Volume Portal

Goncharov, Sergey

Uniform Elgot Iteration in Foundations

pdf-format:
LIPIcs-ICALP-2021-131.pdf (0.7 MB)

Abstract

Category theory is famous for its innovative way of thinking of concepts by their descriptions, in particular by establishing universal properties. Concepts that can be characterized in a universal way receive a certain quality seal, which makes them easily transferable across application domains. The notion of partiality is however notoriously difficult to characterize in this way, although the importance of it is certain, especially for computer science where entire research areas, such as synthetic and axiomatic domain theory revolve around it. More recently, this issue resurfaced in the context of (constructive) intensional type theory. Here, we provide a generic categorical iteration-based notion of partiality, which is arguably the most basic one. We show that the emerging free structures, which we dub uniform-iteration algebras enjoy various desirable properties, in particular, yield an equational lifting monad. We then study the impact of classicality assumptions and choice principles on this monad, in particular, we establish a suitable categorial formulation of the axiom of countable choice entailing that the monad is an Elgot monad.

BibTeX - Entry

@InProceedings{goncharov:LIPIcs.ICALP.2021.131,
  author =	{Goncharov, Sergey},
  title =	{{Uniform Elgot Iteration in Foundations}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{131:1--131:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14200},
  URN =		{urn:nbn:de:0030-drops-142007},
  doi =		{10.4230/LIPIcs.ICALP.2021.131},
  annote =	{Keywords: Elgot monad, partiality monad, delay monad, restriction category}
}

Keywords: Elgot monad, partiality monad, delay monad, restriction category
Collection: 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)
Issue Date: 2021
Date of publication: 02.07.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI