Algebras for Deterministic Computation Are Inherently Incomplete

TL;DR

The paper proves that the deterministic fragment of Kleene Algebra with Tests (KAT) cannot be generated by any finite set of regular control-flow operations, extending classical results on control-flow expressivity. It develops a detailed automata-theoretic framework to model deterministic KAT programs, introduces composition operations that mirror regular-control-flow constructs, and uses the L_k family of languages to show that finite compositions cannot capture all deterministic guarded languages. A key positive result shows that an infinitary family of regular-control-flow operations is expressively complete for the deterministic KAT fragment, while also establishing that determinism checking is coNP-complete (polynomial-time for fixed test alphabets). The findings reinforce that compositional, finite-primitives languages like GKAT inherently miss some deterministic behaviors, motivating broader automata-based approaches and informing future work on non-local control flow and related algebraic systems. Overall, the work deepens our understanding of the boundaries between deterministic control flow, regular operations, and algebraic reasoning in program analysis.

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.

Figures (4)

• Figure 1: Visualization of a KAT automaton on $Q = \{ q_1 \}$ (left), with transitions $\delta$ and initialization $\iota$ (right).
• Figure 2: KAT automaton modeling the "repeat $p$ until $t$ changes" program $F$.
• Figure 3: At the top, a map $\mathfrak{s}$ from $\Sigma_2 = \{ p_1, p_2 \}$ to automata over $T = \{ t, t', t" \}$ and $\Sigma = \{ p, p', p" \}$. On the bottom left, an automaton $A = (Q, \delta, \iota)$ over $T_0 = \emptyset$ and $\Sigma_2$, representing the operator $p_1 \cdot p_2$. On the bottom right, the automaton $(Q, \hat{\delta}, \hat{\iota})$ obtained from $A$, with $\hat{\delta}$ and $\hat{\iota}$ derived from $\delta$ and $\iota$ per \ref{['def:delta-hat', 'def:iota-hat']}.
• Figure 4: On the left, the automaton $(Q, \hat{\delta}, \hat{\iota})$ from \ref{['fig:shortcut-drawing']}, drawn suggestively with the transitions "entering" the subautomata or $\mathfrak{s}(p_1)$ and $\mathfrak{s}(p_2)$, along with the tests that are true when this happens, and the states where the automaton resumes after a subautomaton accepts. On the right, the automaton $\textsf{compose}\xspace^\mathfrak{s}(A)$, obtained by following the recipe from \ref{['def:compose-sigma']}.

Theorems & Definitions (56)

• Remark 1
• theorem 2
• definition 1
• theorem 3
• definition 2: kozen-smith-1996
• definition 3: Guarded languages cohen-kozen-smith-1996
• definition 4: Guarded composition cohen-kozen-smith-1996
• definition 5: Language semantics of KAT cohen-kozen-smith-1996
• proposition 1: kozen-smith-1996
• definition 6: Language semantics of GKAT GKATKozenTseng