A proof theory of (omega-)context-free languages, via non-wellfounded proofs
Anupam Das, Abhishek De
TL;DR
The paper develops a proof-theoretic framework for $(\omega)$-context-free languages by extending hypersequent calculi to $\mu$- and $\nu$-fixed points and defining the language semantics $\mathcal{L}(\cdot)$ for $\mu$-expressions. It proves that for CFLs, $e=f$ is provable iff $\mathcal{L}(e)=\mathcal{L}(f)$, and derives a complete infinitary axiomatisation $\mu\mathsf{CA}$ via projections from a non-wellfounded system $\mu\mathsf{HKA}^\infty$; it then extends to $\omega$-CFLs with $\mu\nu\ell\mathsf{HKA}$, establishing soundness and completeness through a blend of proof- and game-theoretic techniques. These results yield a rigorous non-wellfounded proof-theoretic account of CFLs and $\omega$-CFLs, linking algebraic language theories with infinitary proof systems and enabling canonical axioms for inclusions. The work advances formal language theory by providing a unified, provability-based treatment of least and greatest fixed points in context-free semantics.
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.