Free Kleene algebras with domain
Brett McLean

TL;DR
This paper characterizes free algebras of binary relations with domain and Kleene algebra operations, showing their structure, axiomatization, and decidability of their equational theory.
Contribution
It identifies the structure of free algebras with domain and extends to Kleene algebra with domain, providing axiomatizations and decidability results.
Findings
Elements are pointed labelled finite rooted trees
Regular sets of trees form free algebras with union and reflexive transitive closure
Equational theory of Kleene algebras with domain is decidable
Abstract
First we identify the free algebras of the class of algebras of binary relations equipped with the composition and domain operations. Elements of the free algebras are pointed labelled finite rooted trees. Then we extend to the analogous case when the signature includes all the Kleene algebra with domain operations; that is, we add union and reflexive transitive closure to the signature. In this second case, elements of the free algebras are 'regular' sets of the trees of the first case. As a corollary, the axioms of domain semirings provide a finite quasiequational axiomatisation of the equational theory of algebras of binary relations for the intermediate signature of composition, union, and domain. Next we note that our regular sets of trees are not closed under complement, but prove that they are closed under intersection. Finally, we prove that under relational semantics the…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Algebra and Logic · Advanced Topics in Algebra · Rings, Modules, and Algebras
