Continuous Algebras with Hypotheses
arXiv:2605.18450
The paper introduces a unified framework for many Kleene algebra variants by using continuous algebras ordered by complete lattices, gives a canonical model of closed languages, and provides a generic sound axiomatisation that can be extended modularly to obtain completeness results for specific cases.
Abstract
In the literature on Kleene algebra (KA), a number of variants have been proposed such as Kleene algebra with tests, commutative KA, bi-KA, and concurrent KA. The equational theories of some of these structures have then been studied in the presence of additional assumptions, called hypotheses. We propose a unifying framework encompassing all the previous structures, as well as regular tree languages. This is done by considering algebras ordered by complete lattices, where least fixpoints can be computed. We provide a canonical model consisting of closed languages, which we prove sound and complete with respect to all continuous models. Then we study quasi-equational axiomatisations. It is illusory to hope for a generic axiomatisation which would be sound and complete for all instances. Instead, we provide a generic axiomatisation which we prove sound and we setup tools that make it possible to get complete ones in a modular way, building on previous works from the literature. We showcase these tools by proving new completeness results for commutative KA, bi-KA, and regular tree languages, in each case extended with various hypotheses.