A Unifying Categorical View of Nondeterministic Iteration and Tests

Goncharov S, Uustalu T (2024)

Publication Language: English

Publication Type: Conference contribution

Publication year: 2024

Journal

LIPIcs : Leibniz International Proceedings in Informatics Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik

Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

Series: Leibniz International Proceedings in Informatics (LIPIcs)

Book Volume: 311

Pages Range: 25

Conference Proceedings Title: 35th International Conference on Concurrency Theory (CONCUR 2024)

Event location: Calgary, AB CA

ISBN: 9783959773393

DOI: 10.4230/LIPIcs.CONCUR.2024.25

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.

Authors with CRIS profile

Sergey Goncharov Lehrstuhl für Informatik 8 (Theoretische Informatik)

Involved external institutions

Reykjavik University IS Iceland (IS)

How to cite

APA:

Goncharov, S., & Uustalu, T. (2024). A Unifying Categorical View of Nondeterministic Iteration and Tests. In Rupak Majumdar, Alexandra Silva (Eds.), 35th International Conference on Concurrency Theory (CONCUR 2024) (pp. 25). Calgary, AB, CA: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.

MLA:

Goncharov, Sergey, and Tarmo Uustalu. "A Unifying Categorical View of Nondeterministic Iteration and Tests." Proceedings of the 35th International Conference on Concurrency Theory, CONCUR 2024, Calgary, AB Ed. Rupak Majumdar, Alexandra Silva, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2024. 25.

BibTeX: Download