A Unifying Categorical View of Nondeterministic Iteration and Tests

TL;DR

This paper develops a categorical framework for nondeterministic iteration and tests, generalizing Kleene algebra to better model complex programming language features like concurrency and exceptions.

Contribution

It introduces Kleene-iteration categories, a categorical abstraction that extends Kleene algebra with tests, accommodating various programming semantics.

Findings

Characterizes free models as categories of nondeterministic rational trees.

Shows compatibility of the framework with exceptions, store, and concurrency.

Provides a robust categorical foundation for reasoning about nondeterministic iteration.

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 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.