Algebras for Deterministic Computation Are Inherently Incomplete
Balder ten Cate, Tobias Kappé
Abstract
Kleene Algebra with Tests (KAT) provides an elegant algebraic framework for describing non-deterministic finite-state computations. Using a small finite set of non-deterministic programming constructs (sequencing, non-deterministic choice, and iteration) it is able to express all non-deterministic finite state control flow over a finite set of primitives. It is natural to ask whether there exists a similar finite set of constructs that can capture all deterministic computation. We show that this is not the case. More precisely, the deterministic fragment of KAT is not generated by any finite set of regular control flow operations. This generalizes earlier results about the expressivity of the traditional control flow operations, i.e., sequential composition, if-then-else and while.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext fceff4aa-1c6d-4acb-a411-b15f4242c64bCited by top-tier papers1
Ask how each one uses itBuilds on4
- Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear timeSteffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé et al.POPL 2020 · 32 citations
- A Complete Proof System for 1-Free Regular Expressions Modulo BisimilarityClemens Grabmayer, Wan J. FokkinkLICS 2020 · 15 citations
- Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete: Crystallization: Near-Collapsing Process Graph Interpretations of Regular ExpressionsClemens Armin GrabmayerLICS 2022 · 9 citations
- CF-GKAT: Efficient Validation of Control-Flow TransformationsCheng Zhang, Tobias Kappé, David E. Narváez, Nico NausPOPL 2025 · 3 citations
Related papers
- Kleene algebra modulo theories: a framework for concrete KATsMichael Greenberg, Ryan Beckett, Eric Hayden CampbellPLDI 2022 · 7 citations
- On incorrectness logic and Kleene algebra with top and testsCheng Zhang, Arthur Azevedo de Amorim, Marco GaboardiPOPL 2022 · 9 citations
- Algebraic reasoning of Quantum programs via non-idempotent Kleene algebraYuxiang Peng, Mingsheng Ying, Xiaodi WuPLDI 2022 · 13 citations
- Probabilistic Kleene Algebra with Angelic NondeterminismShawn Ong, Stephanie Ma, Dexter KozenPLDI 2025
- An Algebra of Alignment for Relational VerificationTimos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram et al.POPL 2023 · 17 citations
