Algebras for Deterministic Computation are Inherently Incomplete
summary
Claim: the deterministic fragment of Kleene Algebra with Tests (KAT) cannot be generated by any finite set of regular control-flow operators. The proof converts expressions to finite automata with relational semantics, defines k-dense automata, and constructs an infinite family of deterministic CAT expressions (n-state patterns) each provably inexpressible from any fixed finite operator set, yielding an infinite strict hierarchy. The construction uses automata composition arguments and generalizes classical 1970s/Kosaraju observations.
AI-written summary · about
chapters (10)
- 0:00Deterministic computation challenges
- 2:36Non-local flow control
- 6:30Local control flow primitives
- 7:11Kleene algebra with tests (KAT)
- 10:22Deterministic expressions in KAT
- 11:25Repeat-while-changes pattern
- 12:50KAT fragments expressivity
- 14:17Proof idea: automata and density
- 16:48Open questions and future work
- 17:58Q&A
related talks
18mProbabilistic Kleene Algebra with Angelic Nondeterminism
19mWell-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny
14mAdequacy for Algebraic Effects Revisited
31mFibred Categories of Tree Automata
18mActive Learning of Symbolic NetKAT Automata
20mStacKAT: Infinite State Network Verification
30mType-Checking Heterogeneous Sequences in a Simple Embeddable Type System
22mHigher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification