On Tools for Completeness of Kleene Algebra with Hypotheses
Damien Pous, Jurriaan Rot, Jana Wagemaker
TL;DR
This work develops a modular, transformation-based framework for proving completeness of Kleene algebra with hypotheses (KA_H) by translating hypotheses into language-closure models via H^ closures and reductions. It introduces a toolbox for constructing and composing reductions (including homomorphic and automata-based approaches) and demonstrates its versatility by giving modular completeness proofs for KAT, KAO, NetKAT, and several extensions (KAT with a full element, KAT with converse, and positive tests). The core idea is that if KA_H reduces to KA_H' and KA_H' is complete, then KA_H is complete; this yields systematic, reusable proofs and decidability results. The methods provide a unified lens to treat a spectrum of Kleene-algebra variants through canonical language models, enabling structured, scalable proofs across diverse theories with guarded-strings and automata-based interpretations. The results advance both theory and practical verification, offering modular, automata-grounded pathways to completeness for important programming-logics formalisms like KAT, KAO, and NetKAT.
Abstract
In the literature on Kleene algebra, a number of variants have been proposed which impose additional structure specified by a theory, such as Kleene algebra with tests (KAT) and the recent Kleene algebra with observations (KAO), or make specific assumptions about certain constants, as for instance in NetKAT. Many of these variants fit within the unifying perspective offered by Kleene algebra with hypotheses, which comes with a canonical language model constructed from a given set of hypotheses. For the case of KAT, this model corresponds to the familiar interpretation of expressions as languages of guarded strings. A relevant question therefore is whether Kleene algebra together with a given set of hypotheses is complete with respect to its canonical language model. In this paper, we revisit, combine and extend existing results on this question to obtain tools for proving completeness in a modular way. We showcase these tools by giving new and modular proofs of completeness for KAT, KAO and NetKAT, and we prove completeness for new variants of KAT: KAT extended with a constant for the full relation, KAT extended with a converse operation, and a version of KAT where the collection of tests only forms a distributive lattice.