Kleene Algebra

TL;DR

This paper introduces Kleene Algebra, a formal system for reasoning about program equivalences using regular expressions, automata, and algebraic laws, with educational exercises and an optional automata theory chapter.

Contribution

It provides an accessible introduction to Kleene Algebra, linking regular expressions, automata, and algebraic proofs of program equivalence, including coalgebra perspectives.

Findings

Equivalence of regular expressions can be proved using KA laws

Automata theory can be developed through coalgebra approach

Kleene Algebra provides a sound framework for program equivalence reasoning

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.