Continuous Algebras with Hypotheses

TL;DR

This paper introduces a unifying framework for various Kleene algebra variants and regular tree languages using continuous algebras with hypotheses, providing soundness, completeness, and modular axiomatisation tools.

Contribution

It develops a canonical model for continuous algebras with hypotheses and offers a modular approach to axiomatisation, enabling new completeness results for multiple algebraic structures.

Findings

Canonical model of closed languages is sound and complete.

Tools for modular axiomatisation are established.

New completeness results for specific Kleene algebra variants.

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.