Document Open Access Logo

A Unifying Categorical View of Nondeterministic Iteration and Tests

Authors Sergey Goncharov , Tarmo Uustalu

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2024.25.pdf
  • Filesize: 0.86 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Axiomatic semantics
Keywords
  • Kleene iteration
  • Elgot iteration
  • Kleene algebra
  • coalgebraic resumptions

Metrics

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

Abstract

We study Kleene iteration in the categorical context. A celebrated completeness result by Kozen introduced Kleene algebra (with tests) as a ubiquitous tool for lightweight reasoning about program equivalence, and yet, numerous variants of it came along afterwards to answer the demand for more refined flavors of semantics, such as stateful, concurrent, exceptional, hybrid, branching time, etc. We detach Kleene iteration from Kleene algebra and analyze it from the categorical perspective. The notion, we arrive at is that of Kleene-iteration category (with coproducts and tests), which we show to be general and robust in the sense of compatibility with programming language features, such as exceptions, store, concurrent behaviour, etc. We attest the proposed notion w.r.t. various yardsticks, most importantly, by characterizing the free model as a certain category of (nondeterministic) rational trees.

Cite As Get BibTex

Sergey Goncharov and Tarmo Uustalu. A Unifying Categorical View of Nondeterministic Iteration and Tests. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CONCUR.2024.25

Author Details

Sergey Goncharov
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Tarmo Uustalu
  • Reykjavik University, Iceland, and Tallinn University of Technology, Estonia

Funding

  • Goncharov, Sergey: German Research Foundation (DFG) project 501369690, Icelandic Research Fund project 228684-052
  • Uustalu, Tarmo: Icelandic Research Fund project 228684-052

References

  1. Luca Aceto, Arnaud Carayol, Zoltán Ésik, and Anna Ingólfsdóttir. Algebraic synchronization trees and processes. In Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, and Roger Wattenhofer, editors, Proc. of 39th Int. Coll on Automata, Languages, and Programming, ICALP 2012, Part 2, volume 7392 of Lect. Notes in Comput. Sci., pages 30-41. Springer, 2012. Google Scholar
  2. Michael A. Arbib and Ernest G. Manes. Partially additive categories and flow-diagram semantics. J. Algebra, 62(1):203-227, 1980. URL: https://doi.org/10.1016/0021-8693(80)90212-4.
  3. Steve Awodey. Category Theory. Oxford University Press, 2nd edition, 2010. Google Scholar
  4. David B. Benson and Jerzy Tiuryn. Fixed points in free process algebras, part I. Theor. Comput. Sci., 63(3):275-294, 1989. URL: https://doi.org/10.1016/0304-3975(89)90010-8.
  5. S.L. Bloom, Z. Esik, and D. Taubner. Iteration theories of synchronization trees. Information and Computation, 102(1):1-55, 1993. URL: https://doi.org/10.1006/inco.1993.1001.
  6. Stephen L. Bloom and Zoltán Ésik. Iteration Theories: The Equational Logic of Iterative Processes. Springer, 1993. Google Scholar
  7. Janusz A. Brzozowski. Derivatives of regular expressions. J. ACM, 11(4):481-494, 1964. Google Scholar
  8. Kenta Cho. Total and partial computation in categorical quantum foundations. In Chris Heunen, Peter Selinger, and Jamie Vicary, editors, Proc. of 12th Int. Workshop on Quantum Physics and Logic, QPL 2015, volume 195 of Electron. Proc. in Theor. Comput. Sci., pages 116-135. Open Publishing Assoc., 2015. URL: https://doi.org/10.4204/eptcs.195.9.
  9. Robin Cockett. Itegories & PCAs, 2007. Slides from Fields Institute Meeting on Traces (Ottawa, 2007). URL: https://pages.cpsc.ucalgary.ca/~robin/talks/itegory.pdf.
  10. Robin Cockett and Stephen Lack. Restriction categories III: colimits, partial limits and extensivity. Math. Struct Comput. Sci., 17(4):775-817, 2007. Google Scholar
  11. Manfred Droste and Werner Kuich. Semirings and Formal Power Series, pages 3-28. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-01492-5_1.
  12. Calvin Elgot. Monadic computation and iterative algebraic theories. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium 1973, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 175-230. Elsevier, 1975. Google Scholar
  13. Zoltán Ésik. Equational properties of fixed-point operations in cartesian categories: An overview. Math. Struct. Comput. Sci., 29(6):909-925, 2019. URL: https://doi.org/10.1017/S0960129518000361.
  14. Wan J. Fokkink and Hans Zantema. Basic process algebra with iteration: Completeness of its equational axioms. Comput. J., 37(4):259-268, 1994. URL: https://doi.org/10.1093/comjnl/37.4.259.
  15. Leandro Gomes, Alexandre Madeira, and Luís S. Barbosa. On Kleene algebras for weighted computation. In Simone Cavalheiro and José Fiadeiro, editors, Formal Methods: Foundations and Applications, volume 10623 of Lect. Notes in Comput. Sci., pages 271-286. Springer, 2017. Google Scholar
  16. Sergey Goncharov. Shades of iteration: From Elgot to Kleene. In Alexandre Madeira and Manuel A. Martins, editors, Revised Selected Papers from 26th IFIP WG 1.3 Int. Workshop on Recent Trends in Algebraic Development Techniques, WADT 2022, volume 13710 of Lect. Notes in Comput. Sci., pages 100-120. Springer, 2023. Google Scholar
  17. Sergey Goncharov, Christoph Rauch, and Lutz Schröder. Unguarded recursion on coinductive resumptions. Electron. Notes Theor. Comput. Sci., 319:183-198, 2015. Google Scholar
  18. Sergey Goncharov, Lutz Schröder, and Till Mossakowski. Kleene monads: Handling iteration in a framework of generic effects. In Alexander Kurz, Marina Lenisa, and Andrzej Tarlecki, editors, Proc. of 3rd Int. Conf. Algebra and Coalgebra in Computer Science, CALCO 2009, volume 5728 of Lect. Notes in Comput. Sci., pages 18-33. Springer, 2009. Google Scholar
  19. Sergey Goncharov, Lutz Schröder, Christoph Rauch, and Julian Jakob. Unguarded recursion on coinductive resumptions. Log. Methods in Comput. Sci., 14(3):10:1-10:47, 2018. Google Scholar
  20. Clemens Grabmayer. Milner’s proof system for regular expressions modulo bisimilarity is complete: Crystallization: Near-collapsing process graph interpretations of regular expressions. In Proc. of 37th Ann. ACM/IEEE Symp. on Logic in Computer Science, LICS '22, pages 34:1-34:13, New York, 2022. URL: https://doi.org/10.1145/3531130.3532430.
  21. Niels Grathwohl, Dexter Kozen, and Konstantinos Mamouras. KAT + B! In Proc. of 23rd EACL Ann. Conf. on Computer Science Logic and 29th Ann. ACM/IEEE Symp. on Logic in Computer Science, CSL-LICS 2014, pages 44:1-44:10. ACM, 2014. Google Scholar
  22. Bart Jacobs. New directions in categorical logic, for classical, probabilistic and quantum logic. Log. Methods Comput. Sci., 11(3):24:1-24:76, 2015. URL: https://doi.org/10.2168/LMCS-11(3:24)2015.
  23. S. C. Kleene. Representation of events in nerve nets and finite automata. In Claude Shannon and John McCarthy, editors, Automata Studies, pages 3-41. Princeton University Press, 1956. Google Scholar
  24. Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput., 110(2):366-390, 1994. Google Scholar
  25. Dexter Kozen. Kleene algebra with tests. ACM Trans. Program. Lang. Syst., 19(3):427-443, 1997. Google Scholar
  26. Dexter Kozen and Konstantinos Mamouras. Kleene algebra with products and iteration theories. In Simona Ronchi Della Rocca, editor, Proc. of 22nd EACSL Ann. Conf. on Computer Science Logic, CSL 2013, volume 23 of Leibniz Int. Proc. in Inform., pages 415-431. Dagstuhl Publishing, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.415.
  27. Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer, 1971. Google Scholar
  28. Annabelle McIver, Tahiry M. Rabehaja, and Georg Struth. On probabilistic Kleene algebras, automata and simulations. In Harrie de Swart, editor, Proc. of 12th Int. Conf. on Relational and Algebraic Methods in Computer Science, RAMICS 2011, volume 6663 of Lect. Notes in Comput. Sci., pages 264-279. Springer, 2011. Google Scholar
  29. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lect. Notes in Comput. Sci. Springer, 1980. Google Scholar
  30. Robin Milner. A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci., 28(3):439-466, 1984. Google Scholar
  31. Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93(1):55-92, 1991. Google Scholar
  32. Bernhard Möller. Kleene getting lazy. Sci. Comput. Program., 65(2):195-214, 2007. Google Scholar
  33. Maciej Piróg and Jeremy Gibbons. Monads for behaviour. Electron. Notes Theor. Comput. Sci., 298:309-324, 2013. Google Scholar
  34. Gordon D. Plotkin. A powerdomain construction. SIAM J. Comput., 5(3):452-487, 1976. Google Scholar
  35. J.J.M.M. Rutten. Behavioural differential equations: A coinductive calculus of streams, automata, and power series. Theor. Comput. Sci., 308(1):1-53, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00895-2.
  36. Jacques Sakarovitch. Elements of Automata Theory. Cambridge University Press, 2009. Google Scholar
  37. Alex Simpson and Gordon Plotkin. Complete axioms for categorical fixed-point operators. In Proc. of 15th Ann. IEEE Symp. on Logic in Computer Science, LICS '00, pages 30-41. IEEE, 2000. Google Scholar
  38. Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: Verification of uninterpreted programs in nearly linear time. Proc. ACM Program. Lang., 4(POPL), 2020. URL: https://doi.org/10.1145/3371129.
  39. Daniele Turi and Jan Rutten. On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces. Math. Struct. Comput. Sci., 8(5):481-540, 1998. Google Scholar
  40. Tarmo Uustalu. Generalizing substitution. Theor. Inform. Appl., 37(4):315-336, 2003. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact