We investigate the proof theory of regular expressions with fixed points, construed as a notation for (omega-)context-free grammars. Starting with a hypersequential system for regular expressions due to Das and Pous, we define its extension by least fixed points and prove soundness and completeness of its non-wellfounded proofs for the standard language model. From here we apply proof-theoretic techniques to recover an infinitary axiomatisation of the resulting equational theory, complete for inclusions of context-free languages. Finally, we extend our syntax by greatest fixed points, now computing omega-context-free languages. We show the soundness and completeness of the corresponding system using a mixture of proof-theoretic and game-theoretic techniques.

翻译：我们研究了带不动点的正则表达式的证明论，将其视为（ω-）上下文无关语法的一种表示法。从Das和Pous提出的用于正则表达式的超序列系统出发，我们定义了该系统的极小不动点扩展，并证明了其非良基证明在标准语言模型中的可靠性和完备性。在此基础上，我们应用证明论技术恢复了所得等式理论的一个无穷公理化系统，该公理化系统对上下文无关语言的包含关系是完备的。最后，我们通过引入极大不动点扩展语法，用于生成ω-上下文无关语言。我们综合运用证明论和博弈论技术，证明了相应系统的可靠性和完备性。