Partial Reductions for Kleene Algebra with Linear Hypotheses

TL;DR

This paper addresses the gap where Kleene algebra with standard language semantics fails to prove many true program equivalences, by introducing a meta-theory of hypotheses and a mechanical, automaton-based method to realize hypothesis closure as reductions. It defines a framework for linear hypotheses $e \leq w$ and develops one-step and saturated automata constructions ($T_0$, $T_H$) to obtain reductions that preserve $H$-closure while remaining within regular languages. When these automata constructions terminate finitely, they yield complete and decidable reasoning for KA extended with the given hypotheses, albeit in a partial (domain-limited) sense for cases where full regularity is not preserved. The work further shows how to compose and modularly apply these reductions, discusses limitations with non-regular closures, and suggests practical applications in automated reasoning tactics for expression equivalences.

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.