基于循环证明的右线性（omega）文法证明理论

右线性（或左线性）文法是一类著名的上下文无关文法，仅计算正则语言。它们自然地可以写成带有（最小）不动点的表达式，但乘积被限制为以字母作为左参数，从而提供了正则表达式语法的一种替代方案。在本工作中，我们研究了该语法所导出的逻辑理论。具体而言，我们提出了基于该语法的右线性代数（RLA）理论以及用于对其进行推理的循环证明系统 CRLA。我们证明了 CRLA 对于正则语言的预期模型是可靠且完备的。由此，我们通过从循环证明中提取归纳不变式，恢复了 RLA 的相同完备性结果，使得正则语言模型成为自由右线性代数。最后，我们通过最大不动点扩展了系统 CRLA，得到 nuCRLA，得益于右线性，它由 omega 字语言自然建模。我们运用博弈论技术证明了 nuCRLA（及其受卫片段）对于 omega 正则语言模型具有类似的可靠性与完备性结果。