A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity

TL;DR

This work reframes Milner's completeness question for regular expressions under the process semantics by replacing the fixed-point rule with coinductive proofs that rely on LLEE-witnessed cycles. It develops cMil, a coinductive reformulation of Mil, and builds two kernel systems, CLC and CC, to capture coinductive provability and its layered witnesses. The paper establishes bidirectional proof transformations: coinductive proofs over Mil− can be turned into Mil derivations, and Mil derivations with RSP* can be mimicked by LLEE-witnessed coinductive proofs, yielding theorem-equivalence Mil ≃ cMil ≃ CLC. This coupling provides a principled pathway toward a completeness proof for Mil by leveraging the more tractable, graph-based cyclic proofs and their coalgebraic characterization. Overall, the results position coinductive proofs as a strategic bridge between traditional equational reasoning and bisimilarity-based process semantics, offering both conceptual insight and practical proof techniques for Mil's completeness problem.

Abstract

Milner (1984) defined an operational semantics for regular expressions as finite-state processes. In order to axiomatize bisimilarity of regular expressions under this process semantics, he adapted Salomaa's proof system that is complete for equality of regular expressions under the language semantics. Apart from most equational axioms, Milner's system Mil inherits from Salomaa's system a non-algebraic rule for solving single fixed-point equations. Recognizing distinctive properties of the process semantics that render Salomaa's proof strategy inapplicable, Milner posed completeness of the system Mil as an open question. As a proof-theoretic approach to this problem we characterize the derivational power that the fixed-point rule adds to the purely equational part Mil$^-$ of Mil. We do so by means of a coinductive rule that permits cyclic derivations that consist of a finite process graph with empty steps that satisfies the layered loop existence and elimination property LLEE, and two of its Mil$^{-}$-provable solutions. With this rule as replacement for the fixed-point rule in Mil, we define the coinductive reformulation cMil as an extension of Mil$^{-}$. In order to show that cMil and Mil are theorem equivalent we develop effective proof transformations from Mil to cMil, and vice versa. Since it is located half-way in between bisimulations and proofs in Milner's system Mil, cMil may become a beachhead for a completeness proof of Mil. This article extends our contribution to the CALCO 2022 proceedings. Here we refine the proof transformations by framing them as eliminations of derivable and admissible rules, and we link coinductive proofs to a coalgebraic formulation of solutions of process graphs.

Figures (19)

• Figure 1: A LLEE-wit-nessed coinductive proof of $(a + b)^* \cdot 0 \mathrel{\textcolor{royalblue}{=}} (a \cdot (a + b) + b)^* \cdot 0\,$ with underlying $\textcolor{firebrick}{1}$-chart $\mathcal{G}$ and LLEE-wit-ness $\Hat{\mathcal{G}}$ (with colored, indexed loop-en-try transitions). The proof uses the abbreviations $\,g \mathrel{{:=}} a + b\,$ and $\,h \mathrel{{:=}} a \cdot (a + b) + b\,$.
• Figure 2: Mimicking an instance $\iota$ of the fixed-point rule $\textrm{\normalfont RSP}^{*}\space$ (above) in Milner's system $\text{\normalfont\sf Mil} = {\text{\normalfont\sf Mil$^{\pmb{-}}$}}{+}{\text{$\textrm{\normalfont RSP}^{*}\space$}}$ by a coinductive proof (below) over ${\text{\normalfont\sf Mil$^{\pmb{-}}$}}{+}{\left\{{\text{premise of $\iota$}}\right\}}$ with LLEE-wit-ness ${\space\Hat{\space\underline{\mathcal{C}}}\space}(\space{\textcolor{red}{f^*}\cdot \textcolor{forestgreen}{0}}\space)$.
• Figure 3: Four $\textcolor{firebrick}{1}$-charts (action labels ignored) that violate at least one loop $\textcolor{firebrick}{1}$-chart condition \ref{['loop:1']}, \ref{['loop:2']}, or \ref{['loop:3']}, and a loop $\textcolor{firebrick}{1}$-chart $\underline{\mathcal{C}}$ with one of its loop sub-$\textcolor{firebrick}{1}$-charts $\textcolor{darkcyan}{\underline{\mathcal{L}}}$.
• Figure 4: Example of a loop elimination process that witnesses LEE/ LLEE for the $\textcolor{firebrick}{1}$-chart $\underline{\mathcal{C}}$. Three single-step loop eliminations from $\underline{\mathcal{C}}$ reach the same result $\underline{\mathcal{C}}"'$ as two multi-step loop eliminations (where the second multi-step is also a single step).
• Figure 5: Two runs of the loop elimination procedure on the $\textcolor{firebrick}{1}$-chart $\underline{\mathcal{E}}$ in the middle: the one to the left witnesses LEE (but not LLEE, due to the removal of the red loop-en-try transition from the body of the green loop subchart removed earlier), its recording is the (not layered) $\text{\normalfont LEE}$-wit-ness $\space\widehat{\space\underline{\mathcal{E}}}^{ (1)}\space$ of $\underline{\mathcal{E}}$; the one to the right witnesses layered LEE ( LLEE), its recording is the LLEE-wit-ness (layered LEE-witn.) $\space\widehat{\space\underline{\mathcal{E}}}^{ (2)}\space$ of $\underline{\mathcal{E}}$.

Theorems & Definitions (107)

• Definition 2.1: star expressions
• Definition 2.2: $\textcolor{firebrick}{1}$-charts, and charts
• Definition 2.3
• Definition 2.4: ($\textcolor{firebrick}{1}$-)bisimulation
• Definition 2.5: process semantics equality
• Definition 2.6: proof system $\text{$\mathcal{E\space L}$}$, ${\textit{Eq}}(\space{\cdot}\space)$-based/$\text{$\mathcal{E\space L}$}$-based proof systems
• Definition 2.7
• Definition 2.8: sub-system, theorem equivalence/subsumption of ${\textit{Eq}}(\space{\cdot}\space)$-based proof systems
• Definition 2.9: derivable, correct, and admissible rules
• Lemma 2.10