A proof theory of right-linear (ω-)grammars via cyclic proofs

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. Finally we extend CRLA by greatest fixed points, νCRLA, naturally modelled by languages of ω-words thanks to right-linearity. We show a similar soundness and completeness result of (the guarded fragment of) νCRLA for the model of ω-regular languages, this time requiring game theoretic techniques to handle interleaving of fixed points.