A Free Construction of Kleene Algebras with Tests

摘要

In this paper we define Kleene algebra with tests in a slightly more general way than Kozen's definition. Then we give an explicit construction of the free Kleene algebra with tests generated by a pair of sets. We also show that the category KAT of Kleene algebras with tests and the category KAT is contained in of Kozen's Kleene algebras with tests are related by an adjunction. This fact shows that an infinitely-generated free Kleene algebra with tests in the sense of Kozen can be obtained as the image of our free algebra under the left adjoint from KAT to KAT is contained in; moreover, the image is isomorphic to itself. Therefore, our free Kleene algebra with tests is isomorphic to Kozen and Smith's free Kleene algebra with tests if their construction available. Finally, we show that Kozen and Smith's free Kleene algebra with tests can be presented as a coproduct of Kleene algebras. This is induced from our free construction.