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.

翻译：Kleene代数（KA）是推理一般程序等价性的重要工具，其具有可判定的完备等式理论。然而，KA并非总能证明特定程序间的等价性。为此，研究者通常在KA中添加编码程序特定知识的假设。传统上，通过一种称为归约的正则表达式映射，我们可以将可判定性与完备性提升至这些更具表达力的系统。显式构造此类归约需要大量人工工作。此外，由于正则性约束，并非所有表达式与假设的组合都存在归约。我们提出一种基于自动机的构造方法，可机械地推导出广泛假设类别的归约。这些归约可以是部分的，此时它们产生部分完备性：即在其定义域内表达式的完备性。这使得我们能够自动确立比现有工作覆盖范围更多等价关系的可证明性。