A Unifying Categorical View of Nondeterministic Iteration and Tests
Sergey Goncharov, Tarmo Uustalu
TL;DR
This work develops a robust categorical framework for nondeterministic iteration by introducing Kleene-iteration categories with tests (KiC(T)). It shows these categories unify Kleene iteration, Elgot iteration, and while-loops, while remaining compatible with programmer-language features via a generalized monadic and coalgebraic backbone. A key result is a complete characterization of the free KiCT as a category of nondeterministic rational trees, connecting iteration theory to coalgebraic resumptions and rational tree semantics. The framework accommodates extensions such as the generalized coalgebraic resumption monad transformer and offers a principled path toward handling effects like exceptions and concurrency without sacrificing foundational iteration laws. These insights provide a versatile, modular basis for reasoning about program equivalence and control in diverse semantic settings.
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.