Background:
Dexter Kozen’s famous completeness theorem for Kleene algebras relies on a fairly intricate proof that n*n matrices over a Kleene algebra are themselves a Kleene algebra. The proof relies on an induction over the size of the matrix, and decomposing matrices by splitting them into multiple submatrices. Recently, we have formalised this proof (and fleshed out several omitted details of the proof) by mechanising it in the proof assistant Isabelle/HOL, however this proof is significantly more involved than the one in the paper, primarily because of the enormous amount of proof obligations, typically omitted in a paper proof, concerning the dimensions of the various (sub)matrices.
Dependent types may be the solution to improve the elegance of this proof’s mechanisation. For example the proof assistant Lean represents matrices as functions from finite Fin types, and includes operators for extracting submatrices. The proof assistant Agda would also support such an encoding, but others (such as inductive types) are also possible. Both Agda and Lean have library support for Kleene algebras but no mechanisation of the completeness proof.
Research Questions and Tasks:
This project would be to mechanise Kozen’s proof in one of these proof assistants (Agda or Lean), and make use of dependently-typed representations of matrices to eliminate (or greatly reduce) the tedious proof obligations about dimensions encountered in our Isabelle mechanisation.
Requirements:
Knowledge of mathematical logic is a must. Experience with proof assistants is highly desirable as is an interest in learning about dependent types. Despite the topic of the proof, it’s actually not necessary to understand much about Kleene algebras to start work on this project.