A Unifying Categorical View of Nondeterministic Iteration and Tests
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911959002120192 |
|---|---|
| author | Goncharov, Sergey Uustalu, Tarmo |
| author_facet | Goncharov, Sergey Uustalu, Tarmo |
| contents | 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 behavior, 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_08688 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A Unifying Categorical View of Nondeterministic Iteration and Tests Goncharov, Sergey Uustalu, Tarmo Logic in Computer Science 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 behavior, 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. |
| title | A Unifying Categorical View of Nondeterministic Iteration and Tests |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2407.08688 |