Result: A free construction of Kleene algebras with tests
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Further Information
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⊆ 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⊆; 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.