一句话：证明 KAT 的确定性片段不能由任何有限个正则控制流操作生成。
Kleene Algebra with Tests（KAT）为描述非确定性有限状态计算提供了优雅的代数框架：仅用顺序、非确定选择和迭代等有限个非确定性编程构造，即可表达有限原语上的所有非确定性有限状态控制流。本文追问是否存在类似的有限构造集能刻画所有确定性计算。作者证明这样的有限集并不存在：KAT 的确定性片段不能由任何有限个正则控制流操作生成。该结论推广了此前关于传统控制流操作（顺序组合、if-then-else 与 while）表达力的结果，揭示了确定性计算在代数表达上的固有局限性。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2411-14284,
title = {Algebras for Deterministic Computation Are Inherently Incomplete},
author = {Balder ten Cate and Tobias Kappé},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704861}
}