Kleene Algebra
Tobias Kappé, Alexandra Silva, Jana Wagemaker
TL;DR
This work presents Kleene Algebra (KA) as a rigorous equational framework for reasoning about program equivalence, connecting regular expressions to automata via language and relational semantics. It develops the coalgebraic foundation, Brzozowski derivatives, and Kleene’s theorem to establish a concrete link between regular expressions and automata, culminating in completeness results that KA captures all true equivalences under its laws. The text then extends KA with tests (KAT) to model program assertions, conditionals, and while-loops, presenting automata, bisimulation, and decision procedures in this richer setting. A substantial portion is devoted to completeness proofs, matrix methods, and coalgebraic machinery, providing a robust basis for decision procedures and extensions like KA with hypotheses, NetKAT, and GKAT. Collectively, the book offers a comprehensive framework for formal verification of program equivalence and transformations, with broad relevance to compiler correctness, optimization, and networked systems.
Abstract
This booklet serves as an introduction to Kleene Algebra (KA), a set of laws that can be used to study general equivalences between programs. It discusses how general programs can be modeled using regular expressions, how those expressions correspond to automata, and how this correspondence can be exploited to obtain the central result of KA, namely that an equivalence of regular expressions is true if and only if it can be proved using the laws of KA. Each chapter closes with a set of exercises to further build intuition and understanding, and there is an optional chapter that develops automata theory through the lens of coalgebra.