Algebras for Deterministic Computation Are Inherently Incomplete
Balder ten Cate, Tobias Kappé
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
引用它的顶会 Paper1
问问它们各自怎么用它它引用的顶会 Paper4
- Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear timeSteffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé 等POPL 2020 · 被引用 32 次
- A Complete Proof System for 1-Free Regular Expressions Modulo BisimilarityClemens Grabmayer, Wan J. FokkinkLICS 2020 · 被引用 15 次
- Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete: Crystallization: Near-Collapsing Process Graph Interpretations of Regular ExpressionsClemens Armin GrabmayerLICS 2022 · 被引用 9 次
- CF-GKAT: Efficient Validation of Control-Flow TransformationsCheng Zhang, Tobias Kappé, David E. Narváez, Nico NausPOPL 2025 · 被引用 3 次
相关 Paper
- Kleene algebra modulo theories: a framework for concrete KATsMichael Greenberg, Ryan Beckett, Eric Hayden CampbellPLDI 2022 · 被引用 7 次
- On incorrectness logic and Kleene algebra with top and testsCheng Zhang, Arthur Azevedo de Amorim, Marco GaboardiPOPL 2022 · 被引用 9 次
- Algebraic reasoning of Quantum programs via non-idempotent Kleene algebraYuxiang Peng, Mingsheng Ying, Xiaodi WuPLDI 2022 · 被引用 13 次
- 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 等POPL 2023 · 被引用 17 次
