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.

翻译：右线性（或左线性）文法是一类著名的上下文无关文法，仅能生成正则语言。这类文法可自然地表示为带有（最小）不动点的表达式，但其乘积运算被限制为以字母作为左参数，从而为正则表达式的语法提供了另一种选择。在本工作中，我们研究了这种语法所对应的逻辑理论。具体而言，我们针对该语法提出了右线性代数（RLA）理论，并设计了一个用于推理的循环证明系统CRLA。我们证明了CRLA对于正则语言的预期模型是可靠且完备的。由此，通过从循环证明中提取归纳不变量，我们恢复了RLA的相同完备性结果，这表明正则语言模型即为自由右线性代数。最后，我们通过引入最大不动点将系统CRLA扩展为nuCRLA，由于右线性的特性，该系统可自然地由ω-词的语言建模。我们利用博弈论技术证明了nuCRLA（的受保护片段）对ω-正则语言模型具有类似的可靠性与完备性结果。