A proof theory of (omega-)context-free languages, via non-wellfounded proofs

TL;DR

This paper develops a proof-theoretic framework for (omega-)context-free languages using non-wellfounded proofs, fixed points, and game-theoretic methods, providing soundness and completeness results.

Contribution

It introduces a novel proof system for (omega-)context-free languages with fixed points, extending previous systems and establishing soundness and completeness.

Findings

Soundness and completeness of the fixed point proof system for regular expressions.

Infinitary axiomatisation of the equational theory for context-free languages.

Extension of syntax to omega-context-free languages with soundness and completeness.

Abstract

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.