Document Open Access Logo

Uniform Elgot Iteration in Foundations

Author Sergey Goncharov

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2021.131.pdf
  • Filesize: 0.73 MB
  • 16 pages

Document Identifiers

Author Details

Sergey Goncharov
  • University Erlangen-Nürnberg, Germany

Funding

  • Goncharov, Sergey: Support by Deutsche Forschungsgemeinschaft (DFG) under project GO 2161/1-2 is gratefully acknowledged.

Cite As Get BibTex

Sergey Goncharov. Uniform Elgot Iteration in Foundations. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 131:1-131:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ICALP.2021.131

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Constructive mathematics
Keywords
  • Elgot monad
  • partiality monad
  • delay monad
  • restriction category

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Jiří Adámek, Stefan Milius, and Lawrence S. Moss. On well-founded and recursive coalgebras. In Jean Goubault-Larrecq and Barbara König, editors, Foundations of Software Science and Computation Structures, pages 17-36. Springer International Publishing, 2020. Google Scholar
  2. Jirí Adámek, Stefan Milius, and Jiri Velebil. Elgot algebras. Log. Meth. Comput. Sci., 2, 2006. Google Scholar
  3. Jirı Adámek, Stefan Milius, and Jirı Velebil. Iterative algebras: How iterative are they. Theory Appl. Categ, 19:61-92, 2008. Google Scholar
  4. Jiří Adámek, Stefan Milius, and Jiří Velebil. Elgot theories: a new perspective of the equational properties of iteration. Math. Struct. Comput. Sci., 21:417-480, 2011. Google Scholar
  5. Thorsten Altenkirch, Nils Danielsson, and Nicolai Kraus. Partiality, revisited - the partiality monad as a quotient inductive-inductive type. In Javier Esparza and Andrzej Murawski, editors, Foundations of Software Science and Computation Structures, FOSSACS 2017, volume 10203 of LNCS, pages 534-549, 2017. Google Scholar
  6. Steve Awodey. Category Theory. Oxford University Press, Inc., New York, NY, USA, 2nd edition, 2010. Google Scholar
  7. Andrej Bauer. An injection from the Baire space to natural numbers. Mathematical Structures in Computer Science, 25(7):1484–1489, 2015. Google Scholar
  8. Stephen Bloom and Zoltán Ésik. Iteration theories: the equational logic of iterative processes. Springer, 1993. Google Scholar
  9. Anna Bucalo, Carsten Führmann, and Alex K. Simpson. An equational notion of lifting monad. Theor. Comput. Sci., 294(1/2):31-60, 2003. Google Scholar
  10. Venanzio Capretta. General recursion via coinductive types. Log. Meth. Comput. Sci., 1(2), 2005. Google Scholar
  11. James Chapman, Tarmo Uustalu, and Niccolò Veltri. Quotienting the delay monad by weak bisimilarity. In Theoretical Aspects of Computing, ICTAC 2015, volume 9399 of LNCS, pages 110-125. Springer, 2015. Google Scholar
  12. James Chapman, Tarmo Uustalu, and Niccolò Veltri. Quotienting the delay monad by weak bisimilarity. Mathematical Structures in Computer Science, 29(1):67–92, 2019. Google Scholar
  13. J Robin B Cockett and Stephen Lack. Restriction categories I: categories of partial maps. Theoretical computer science, 270(1-2):223-259, 2002. Google Scholar
  14. Tim Lukas Diezel and Sergey Goncharov. Towards Constructive Hybrid Semantics. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), volume 167 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:19, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. Google Scholar
  15. Calvin Elgot. Monadic computation and iterative algebraic theories. In Logic Colloquium 1973, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 175-230. Elsevier, 1975. Google Scholar
  16. Martín H. Escardó and Cory M. Knapp. Partial Elements and Recursion via Dominances in Univalent Type Theory. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:16, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  17. Sergey Goncharov, Christoph Rauch, and Lutz Schröder. Unguarded recursion on coinductive resumptions. In Mathematical Foundations of Programming Semantics, MFPS 2015, ENTCS, 2015. Google Scholar
  18. Sergey Goncharov and Lutz Schröder. A relatively complete generic Hoare logic for order-enriched effects. In Proc. 28th Annual Symposium on Logic in Computer Science (LICS 2013), pages 273-282. IEEE, 2013. Google Scholar
  19. Sergey Goncharov, Lutz Schröder, Christoph Rauch, and Julian Jakob. Unguarded recursion on coinductive resumptions. Logical Methods in Computer Science, 14(3), 2018. Google Scholar
  20. Sergey Goncharov, Lutz Schröder, Christoph Rauch, and Maciej Piróg. Unifying guarded and unguarded iteration. In Javier Esparza and Andrzej Murawski, editors, Foundations of Software Science and Computation Structures, FoSSaCS 2017, volume 10203 of LNCS, pages 517-533. Springer, 2017. Google Scholar
  21. J. M. E. Hyland. First steps in synthetic domain theory. In Category Theory, volume 1144 of LNM, pages 131-156. Springer, 1992. Google Scholar
  22. J.M.E. Hyland. The effective topos. In A.S. Troelstra and D. van Dalen, editors, The L. E. J. Brouwer Centenary Symposium, volume 110 of Studies in Logic and the Foundations of Mathematics, pages 165-216. Elsevier, 1982. Google Scholar
  23. Peter T Johnstone. On a topological topos. Proceedings of the London mathematical society, 3(2):237-271, 1979. Google Scholar
  24. Andrè Joyal, Ross Street, and Dominic Verity. Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society, 119:447-468, April 1996. Google Scholar
  25. Cory M. Knapp. Partial functions and recursion in univalent type theory. PhD thesis, University of Birmingham, UK, 2018. Google Scholar
  26. Anders Kock. Strong functors and monoidal monads. Archiv der Mathematik, 23(1):113-120, 1972. Google Scholar
  27. Bill Lawvere. An elementary theory of the category of sets. Proceedings of the National Academy of Sciences of the United States of America, 52:1506-1511, 1964. Google Scholar
  28. Saunders Mac Lane. Categories for the Working Mathematician. Springer, 1971. Google Scholar
  29. Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93:55-92, 1991. Google Scholar
  30. Egbert Rijke and Bas Spitters. Sets in homotopy type theory. Mathematical Structures in Computer Science, 25(5):1172–1202, 2015. Google Scholar
  31. Guiseppe Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford, 1986. Google Scholar
  32. Alex Simpson and Gordon Plotkin. Complete axioms for categorical fixed-point operators. In Logic in Computer Science, LICS 2000, pages 30-41, 2000. Google Scholar
  33. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  34. Tarmo Uustalu. Generalizing substitution. ITA, 37:315-336, 2003. Google Scholar
  35. Tarmo Uustalu and Niccolò Veltri. The delay monad and restriction categories. In Dang Van Hung and Deepak Kapur, editors, Theoretical Aspects of Computing - ICTAC 2017, pages 32-50. Springer International Publishing, 2017. Google Scholar
  36. Tarmo Uustalu and Niccolò Veltri. Partiality and container monads. In Bor-Yuh Evan Chang, editor, APLAS, volume 10695 of Lecture Notes in Computer Science, pages 406-425. Springer, 2017. Google Scholar
  37. Niccoló Veltri. A Type-Theoretical Study of Nontermination. PhD thesis, Tallinn University of Technology, 2017. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact