Goncharov S (2021)
Publication Type: Conference contribution
Publication year: 2021
Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Book Volume: 198
Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs
Event location: Virtual, Glasgow, GBR
ISBN: 9783959771955
DOI: 10.4230/LIPIcs.ICALP.2021.131
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 iterationbased 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.
APA:
Goncharov, S. (2021). Uniform elgot iteration in foundations. In Nikhil Bansal, Emanuela Merelli, James Worrell (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Virtual, Glasgow, GBR: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.
MLA:
Goncharov, Sergey. "Uniform elgot iteration in foundations." Proceedings of the 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, Virtual, Glasgow, GBR Ed. Nikhil Bansal, Emanuela Merelli, James Worrell, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2021.
BibTeX: Download