Partial Reductions for Kleene Algebra with Linear Hypotheses
Abstract
Kleene algebra (KA) is an important tool for reasoning about general program equivalences, with a decidable and complete equational theory. However, KA cannot always prove equivalences between specific programs. For this purpose, one adds hypotheses to KA that encode program-specific knowledge. Traditionally, a map on regular expressions called a reduction then lets us lift decidability and completeness to these more expressive systems. Explicitly constructing such a reduction requires significant labour. Moreover, due to regularity constraints, a reduction may not exist for all combinations of expression and hypothesis. We describe an automaton-based construction to mechanically derive reductions for a wide class of hypotheses. These reductions can be partial, in which case they yield partial completeness: completeness for expressions in their domain. This allows us to automatically establish the provability of more equivalences than what is covered in existing work.
Cite
@article{arxiv.2601.14114,
title = {Partial Reductions for Kleene Algebra with Linear Hypotheses},
author = {Liam Chung and Tobias Kappé},
journal= {arXiv preprint arXiv:2601.14114},
year = {2026}
}