Partial Reductions for Kleene Algebra with Linear Hypotheses

TL;DR

This paper introduces an automaton-based method to automatically derive partial reductions in Kleene algebra with hypotheses, enabling broader automated reasoning about program equivalences beyond existing approaches.

Contribution

It presents a mechanical construction for deriving partial reductions in Kleene algebra, expanding the scope of automated reasoning for program equivalences.

Findings

Automaton-based construction for partial reductions

Partial reductions enable partial completeness in reasoning

Automatically establishes more equivalences than previous methods

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.