Formalizing the Kleene Star for Matrices

The Kleene star was introduced by Stephen Kleene in the context of regular expressions to denote a finite (i.e., zero or more) number of iterations. For instance, {"a", "b", "c"}* = {ε, "a", "b", "c", "aa", "ab", "ac", "ba", "bb", "bc", "ca", "cb", "cc", ...}.

The Kleene star can be defined not just for regular expressions and languages, but also in many other contexts where a notion of iteration is available. In particular, iterated matrix multiplication gives rise to a definition of the Kleene star for square matrices.

In this project, you will formalize the Kleene star for matrices in the interactive proof assistant Isabelle. You will translate the textbook definition of the Kleene star into a precise (machine-readable) definition and give detailed (machine-checkable) proofs of its most important properties.

This project will allow you to become familiar with Isabelle, one of the world's leading software tools to assist with the development of formal proofs.

Work environment:
Isabelle (Linux, Windows (via Cygwin) or Mac)
Required knowledge/skills:
Basic linear algebra, first-order logic
Tjark Weber

Last modified: 2013-03-02