An Elementary Proof of the FMP for Kleene Algebra

TL;DR

This work addresses when equations in Kleene algebra ($KA$) are provable and how complete models for KA relate to finite and relational semantics. It proves a novel finite-relational model property (FRMP) for KA and provides an elementary $FMP$ proof that uses transformation automata, avoiding prior techniques based on minimality or bisimilarity. By connecting automata-theoretic constructions (including Antimirov's derivatives) with algebraic solutions, it unifies language, finite-relational, and relational completeness results. The discussion includes a Coq formalization and prospects for extending the approach to concurrent and guarded variants of Kleene algebra (CKA, GKAT).

Abstract

Kleene Algebra (KA) is a useful tool for proving that two programs are equivalent. Because KA's equational theory is decidable, it integrates well with interactive theorem provers. This raises the question: which equations can we (not) prove using the laws of KA? Moreover, which models of KA are complete, in the sense that they satisfy exactly the provable equations? Kozen (1994) answered these questions by characterizing KA in terms of its language model. Concretely, equivalences provable in KA are exactly those that hold for regular expressions. Pratt (1980) observed that KA is complete w.r.t. relational models, i.e., that its provable equations are those that hold for any relational interpretation. A less known result due to Palka (2005) says that finite models are complete for KA, i.e., that provable equivalences coincide with equations satisfied by all finite KAs. Phrased contrapositively, the latter is a finite model property (FMP): any unprovable equation is falsified by a finite KA. Both results can be argued using Kozen's theorem, but the implication is mutual: given that KA is complete w.r.t. finite (resp. relational) models, Palka's (resp. Pratt's) arguments show that it is complete w.r.t. the language model. We embark on a study of the different complete models of KA, and the connections between them. This yields a novel result subsuming those of Palka and Pratt, namely that KA is complete w.r.t. finite relational models. Next, we put an algebraic spin on Palka's techniques, which yield a new elementary proof of the finite model property, and by extension, of Kozen's and Pratt's theorems. In contrast with earlier approaches, this proof relies not on minimality or bisimilarity of automata, but rather on representing the regular expressions involved in terms of transformation automata.

Figures (5)

• Figure 1: Overview of the elementary connections between different (classes of) KAs in terms of the equalities that are satisfied. The grayed out implications follow from containments between classes of models --- e.g., if $\mathfrak{C} \models e = f$ then $\mathfrak{R} \models e = f$ because all relational models are star-continuous.
• Figure 2: Visual representation of an automaton $A_\mathsf{alt}$ accepting the language ${(\mathtt{a}\cdot\mathtt{b})}^*\cdot\mathtt{a}$.
• Figure 3: Template for $A_\mathsf{alt}[-]$, the transformation automaton of $A_\mathsf{alt}$ (\ref{['figure:automaton-alt']}). For the sake of simplicity, no accepting state (relation) has been selected, and only the reachable part of the automaton has been drawn.
• Figure 4: The Antimirov automaton $A_e$ where $e = \mathtt{a} \cdot {(\mathtt{b} \cdot \mathtt{a})}^*$.
• Figure 5: Diagrammatic representation of \ref{['lemma:monoid-to-ka-interp']}. In the diagram on the left, $\{ - \}$ is the map that sends an element of $m$ to the singleton set $\{ m \}$; on the right, $\mathcal{P}(\widetilde{h_1})$ is the pointwise application of $\widehat{h_1}: \Sigma^* \to M$.

Theorems & Definitions (53)

• Definition 2.1
• Remark 2.2
• Remark 2.3
• Definition 2.4
• Definition 2.5: KA of relations
• Definition 2.6: Expressions
• Example 2.7
• Definition 2.8
• Remark 2.9
• Lemma 2.10