Typed Kleene Algebra

Abstract

In previous work we have found it necessary to argue that certain theorems of Kleene algebra hold even when the symbols are interpreted as nonsquare matrices. In this note we define and investigate typed Kleene algebra, a typed version of Kleene algebra in which objects have types s pointing to t. Although nonsquare matrices are the principal motivation, there are many other useful interpretations: traces, binary relations, Kleene algebra with tests. We give a set of typing rules and show that every expression has a unique most general typing (mgt). Then we prove the following metatheorem that incorporates the abovementioned results for nonsquare matrices as special cases. Call an expression 1-free if it contains only the Kleene algebra operators (binary) +, (unary) +, 0, and ., but no occurrence of 1 or *. Then every universal 1-free formula that is a theorem of Kleene algebra is also a theorem of typed Kleene algebra under its most general typing. The metatheorem is false without the restriction to 1-free formulas.