A proof theory of right-linear (omega-)grammars via cyclic proofs
Anupam Das, Abhishek De
TL;DR
The paper introduces right-linear algebras ($\mathsf{RLA}$) and a cyclic proof system ($\mathsf{CRLA}$) to reason about right-linear μ-expressions for regular languages, proving CRLA is sound and complete for the model $\mathcal{L}(\cdot)$ and enabling extraction of inductive invariants that yield completeness of $\mathsf{RLA}$ (making regular languages the free right-linear algebra). It then extends the framework to ω-words with greatest fixed points via $\nu\mathsf{CRLA}$, achieving soundness and guarded completeness for the $\omega$-regular language model using game-theoretic techniques. The work positions RLAs as a broader alternative to left-handed Kleene algebras, offering a simpler proof-theoretic approach and a robust, extractable invariants methodology for fixed-point reasoning.
Abstract
Right-linear (or left-linear) grammars are a well-known class of context-free grammars computing just the regular languages. They may naturally be written as expressions with (least) fixed points but with products restricted to letters as left arguments, giving an alternative to the syntax of regular expressions. In this work, we investigate the resulting logical theory of this syntax. Namely, we propose a theory of right-linear algebras (RLA) over of this syntax and a cyclic proof system CRLA for reasoning about them. We show that CRLA is sound and complete for the intended model of regular languages. From here we recover the same completeness result for RLA by extracting inductive invariants from cyclic proofs, rendering the model of regular languages the free right-linear algebra. Finally, we extend system CRLA by greatest fixed points, nuCRLA, naturally modelled by languages of omega-words thanks to right-linearity. We show a similar soundness and completeness result of (the guarded fragment of) nuCRLA for the model of omega-regular languages, employing game theoretic techniques.