(12- or 24-unit Honours or Masters project)
Kleene algebra is an abstract program algebra, widely used in programming-language semantics, program logics, and verification. Dexter Kozen’s completeness theorem (1994) shows that the equational theory of Kleene algebras coincides with the equational theory of regular expressions over a finite alphabet. This foundational result relies on the fact that matrices over Kleene algebras form a Kleene algebra. This project will mechanise Kozen’s proof in Isabelle/HOL, building on an existing matrix library.
Background
A Kleene algebra is an idempotent semiring equipped with a star operator satisfying a small set of natural axioms. Kozen’s completeness theorem (Information and Computation, 1994) establishes that two regular expressions are equal in every Kleene algebra if and only if they denote the same regular language. The proof constructs, for any regular expression, a matrix-based representation that captures its underlying automaton structure, and shows that this representation is canonical with respect to the Kleene-algebra axioms. A characterisation of Kleene algebras in Isabelle/HOL, including a rich collection of theorems, exists in the Archive of Formal proofs. On top of that characterisation, an in-house mechanisation of matrices over Kleene algebras has been developed. It supplies the structural infrastructure required by Kozen’s proof. The completeness theorem itself has not been mechanised in Isabelle/HOL.
Scope
The project will build on the above mentioned Isabelle implementations and aims to formalise the translation from regular expressions to canonical matrix forms, and the soundness and completeness arguments connecting the two. The development is intended for release on the Archive of Formal Proofs.
References
- D. Kozen, A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events, Information and Computation 110(2), 1994, pp. 366–390.
- A. Armstrong, G. Struth, T. Weber, Kleene Algebra, Archive of Formal Proofs — https://isa-afp.org/entries/Kleene_Algebra.html.
- T. Nipkow, L.C. Paulson, M. Wenzel, Isabelle/HOL — A Proof Assistant for Higher-Order Logic, Springer LNCS 2283.