A Proof Theory of ($\omega$-)Context-Free Languages, via Non-wellfounded Proofs

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 [15], we define its extension by least fixed points and prove the 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.

1 Introduction

The characterisation of context-free languages (CFLs) as the least solutions of algebraic inequalities, sometimes known as the ALGOL-like theorem, is a folklore result attributed to several luminaries of formal language theory including Ginsburg and Rice [21], Schutzenberger [52], and Gruska [23]. This induces a syntax for CFLs by adding least fixed point operators to regular expressions, as first noted by Salomaa [51]. Leiß [38] called these constructs “$\mu$-expressions” and defined an algebraic theory over them by appropriately extending Kleene algebras, which work over regular expressions. Notable recent developments include a generalisation of Antimirov’s partial derivatives to $\mu$-expressions [54] and criteria for identifying $\mu$-expressions that can be parsed unambiguously [34].

Establishing axiomatisations and proof systems for classes of formal languages has been a difficult challenge. Many theories of regular expressions, such as Kleene algebras ($\textsf{KA}$) were proposed in the late 20^th century (see, e.g., [6, 28, 29]). The completeness of $\textsf{KA}$ for the (equational) theory of regular languages, due to Kozen [29] and Krob [35] independently, is a celebrated result that has led to several extensions and refinements, e.g. [7, 31,32,33]. More recently the proof theory of $\textsf{KA}$ has been studied via infinitary systems. On one hand, [49] proposed an $\omega$-branching sequent calculus and on the other hand [12, 15, 25] have studied cyclic ‘hypersequential’ calculi.

Inclusion of CFLs is $\varPi ^0_1$-complete, so any recursive (hence also cyclic) axiomatisation must necessarily be incomplete. Nonetheless various theories of $\mu$-expressions have been extensively studied, in particular Chomsky algebras and $\mu$-semirings [17, 18, 39, 40], giving rise to a rich algebraic theory. Indeed Grathwohl, Henglein, and Kozen [22] have given a complete (but infinitary) axiomatisation of the equational theory of $\mu$-expressions, by extending these algebraic theories with a continuity principle for least fixed points.

Fig. 1.

Summary of our main contributions. Each arrow $\rightarrow$ denotes an inclusion of equational theories, over an appropriate language of $\mu$-expressions. The gray arrow, Theorem 11, is also a consequence of the remaining black ones. (Color figure online)

Contributions. In this paper, we propose a non-wellfounded system $\mu \textsf{HKA}^\infty$ for $\mu$-expressions. It can be seen as an extension of the cyclic system of [15] for regular expressions. Our first main contribution is the adequacy of this system for CFLs: $\mu \textsf{HKA}^\infty$ proves $e=f$ just if the CFLs computed by e and f, $\mathcal {L}(e)$ and $\mathcal {L}(f)$ respectively, are the same. We use this result to obtain an alternative proof of completeness of the infinitary axiomatisation $\mu \textsf{CA}$ of [22], comprising our second main result. Our method is inspired by previous techniques in non-wellfounded proof theory, namely [11, 53], employing ‘projections’ to translate non-wellfounded proofs to wellfounded ones. Our result is actually somewhat stronger than that of [22], since our wellfounded proofs are furthermore cut-free.

Finally we develop an extension $\mu \nu \ell \textsf{HKA}$ of (leftmost) $\mu \textsf{HKA}$ by adding greatest fixed points, $\nu$, for which $\mathcal {L}(\cdot )$ extends to a model of $\omega$-context-free languages. Our third main contribution is the soundness and completeness of $\mu \nu \ell \textsf{HKA}$ for $\mathcal {L}(\cdot )$. Compared to $\mu \textsf{HKA}$, the difficulty for metalogical reasoning here is to control interleavings of $\mu$ and $\nu$, both for soundness argument and in controlling proof search for completeness. To this end, we employ game theoretic techniques to characterise word membership and control proof search.

All our main results are summarised in Fig. 1. Due to space constraints many proofs and auxiliary material are omitted, but may be found in a full version [9].

2 A Syntax for Context-Free Grammars

Throughout this work we make use of a finite set $\mathcal {A}$ (the alphabet) of letters, written $a,b,\dots$, and a countable set $\mathcal {V}$ of variables, written $X,Y,\dots$. When speaking about context-free grammars (CFGs), we always assume non-terminals are from $\mathcal {V}$ and the terminals are from $\mathcal {A}$.

We define ($\mu$-)expressions, written e, f,  etc., by:

$$\begin{aligned} e,f,\dots \quad :\,\!:=0 \mid 1 \mid X \mid a \mid e+ f \mid e\cdot f \mid \mu X e \end{aligned}$$

(1)

We usually simply write ef instead of $e\cdot f$. $\mu$ is considered a variable binder, with the free variables $\textrm{FV}(e)$ of an expression e defined as expected. We sometimes refer to expressions as formulas, and write $\sqsubseteq$ for the subformula relation.

$\mu$-expressions compute languages of finite words in the expected way:

Definition 1

(Language Semantics). Let us temporarily expand the syntax of expressions to include each language $A\subseteq \mathcal {A}^*$ as a constant symbol. We interpret each closed expression (of this expanded language) as a subset of $\mathcal {A}^*$ as follows:

Note that all the operators of our syntax correspond to monotone operations on $\mathcal {P}(\mathcal {A}^*)$, with respect to $\subseteq$. Thus $\mathcal {L}(\mu X e(X))$ is just the least fixed point of the operation $A \mapsto \mathcal {L}(e(A))$, by the Knaster-Tarski fixed point theorem.

The productive expressions, written p, q etc. are generated by:

$$\begin{aligned} p,q,\dots \quad :\,\!:=\quad a \quad \mid \quad p + q \quad \mid \quad p\cdot e \quad \mid \quad e\cdot p \quad \mid \quad \mu X p \end{aligned}$$

(2)

We say that an expression is guarded if each variable occurrence occurs free in a productive subexpression. Left-productive and left-guarded are defined in the same way, only omitting the clause $e\cdot p$ in the grammar above. For convenience of exposition we shall employ the following convention throughout:

Convention 2

Henceforth we assume all expressions are guarded.

Example 3

(Empty language). In the semantics above, note that the empty language $\varnothing$ is computed by several expressions, not only 0 but also $\mu X X$ and $\mu X (aX)$. Note that whle the former is unguarded the latter is (left-)guarded. In this sense the inclusion of 0 is somewhat ‘syntactic sugar’, but it will facilitate some of our later development.

Example 4

(Kleene star and universal language). For any expression e we can compute its Kleene star $e^* :=\mu X (1 + eX)$ or $e^* :=\mu X (1 + Xe)$. These definitions are guarded just when e is productive. Now, note that we also have not included a symbol $\top$ for the universal language $\mathcal {A}^*$. We can compute this by the expression $\left( \sum \mathcal {A}\right) ^*$, which is guarded as $\sum \mathcal {A}$ is productive.

It is well-known that $\mu$-expressions compute just the context-free (CF) languages [21, 23, 52]. In fact this holds even under the restriction to left-guarded expressions, by simulating the Greibach normal form:

Theorem 5

(Adequacy, see, e.g., [17, 18]).L is context-free (and $\varepsilon \notin L$) $\iff$ $L=\mathcal {L}(e)$ for some e left-guarded (and left-productive, respectively).

Example 6

Consider the left-guarded expressions $\textrm{Dyck}_{1} :=\mu X(1 + \langle X \rangle X)$ and $\{a^nb^n\}_n:=\mu X(1+ a X b)$. As suggested, $\textrm{Dyck}_{1}$ indeed computes the language of well-bracketed words over alphabet $\{\langle , \rangle \}$, whereas $\{a^nb^n\}_n$ computes the set of words $\vec{a}\vec{b}$ with $|\vec{a}| = |\vec{b}|$. We can also write $(a^*b^*):=\mu X(1 + aX + Xb)$, which is guarded but not left-guarded. However, if we define Kleene $*$ as in Example 4, then we can write $a^*$ and $b^*$ as left-guarded expressions and then take their product for an alternative representation of $(a^*b^*)$. Note that the empty language $\varnothing$ is computed by the left-guarded expression $\mu X (aX)$, cf. Example 3.

3 A Non-wellfounded Proof System

In this section we extend a calculus $\textsf{HKA}$ from [15] for regular expressions to all $\mu$-expressions, and prove soundness and completeness of its non-wellfounded proofs for the language model $\mathcal {L}(\cdot )$. We shall apply this result in the next section to deduce completeness of an infinitary axiomatisation for $\mathcal {L}(\cdot )$, before considering the extension to greatest fixed points later.

A hypersequent has the form $\varGamma \rightarrow S$ where $\varGamma$ (the LHS) is a list of expressions (a cedent) and S (the RHS) is a set of such lists. We interpret lists by the product of their elements, and sets by the sum of their elements. Thus we extend our notation for language semantics by $\mathcal {L}(\varGamma ):=\mathcal {L}(\prod \varGamma )$ and $\mathcal {L}(S) :=\bigcup \limits _{\varGamma \in S } \mathcal {L}(\varGamma )$.

Fig. 2.

Rules of the system $\mu \textsf{HKA}$.

The system $\mu \textsf{HKA}$ is given by the rules in Fig. 2. Here we use commas to delimit elements of a list or set and square brackets [, ] to delimit lists in a set. In the $\textsf{k}$ rules, we write $aS :=\{[a,\varGamma ] : \varGamma \in S\}$ and $Sa :=\{[\varGamma ,a]:\varGamma \in S\}$.

For each inference step, as typeset in Fig. 2, the principal formula is the distinguished formula occurrence in the lower sequent, while any distinguished formula occurrences in upper sequents are auxiliary. (Other colours may be safely ignored for now).

Our system differs from the original presentation of $\textsf{HKA}$ in [15] as (a) we have general fixed point rules, not just for the Kleene $*$; and (b) we have included both left and right versions of the $\textsf{k}$ rule, for symmetry. We extend the corresponding notions of non-wellfounded proof appropriately:

Definition 7

(Non-wellfounded Proofs). A preproof (of $\mu \textsf{HKA}$) is generated coinductively from the rules of $\mu \textsf{HKA}$ i.e. it is a possibly infinite tree of sequents (of height $\le \omega$) generated by the rules of $\mu \textsf{HKA}$. A preproof is regular or cyclic if it has only finitely many distinct subproofs. An infinite branch of a preproof is progressing if it has infinitely many $\mu \text {-}l$ steps. A preproof is progressing, or a $\infty$ -proof, if all its infinite branches are progressing. We write $\mu \textsf{HKA}\vdash ^{\infty }\varGamma \rightarrow S$ if $\varGamma \rightarrow S$ has a $\infty$-proof in $\mu \textsf{HKA}$, and sometimes write $\mu \textsf{HKA}^\infty$ for the class of $\infty$-proofs of $\mu \textsf{HKA}$.

Note that our progress condition on preproofs is equivalent to simply checking that every infinite branch has infinitely many left-logical or $\textsf{k}$ steps, as $\mu \text {-}l$ is the only rule among these that does not decrease the size of the LHS. This is simpler than usual conditions from non-wellfounded proof theory, as we do not have any alternations between the least and greatest fixed points. Indeed we shall require a more complex criterion later when dealing with $\omega$-languages. Note that, as regular preproofs may be written naturally as finite graphs, checking progressiveness for them is efficiently decidable (even in $\textbf{NL}$, see e.g. [8, 15]).

The need for such a complex hypersequential line structure is justified in [15] by the desideratum of regular completeness for the theory of regular expressions: intuitionistic ‘Lambek-like’ systems, cf. e.g. [16, 26, 49] are incomplete (wrt regular cut-free proofs). The complexity of the RHS of sequents in $\textsf{HKA}$ is justified by consideration of proof search for, say, $a^* \rightarrow (aa)^* + a(aa)^*$ and $(a+b)^* \rightarrow a^*(ba^*)^*$, requiring reasoning under sums and products, respectively.

In our extended system, we gain more regular proofs of inclusions between context-free languages. For instance:

Fig. 3.

A regular $\infty$-proof R of $\{a^nb^n\}_n\rightarrow [(a^*b^*)]$.

Example 8

Recall the guarded expressions $\{a^nb^n\}_n$ and $(a^*b^*)$ from Example 6. We have the regular $\infty$-proof R in Fig. 3 of $\{a^nb^n\}_n\rightarrow [(a^*b^*)]$, where $\bullet$ marks roots of identical subproofs. Note that indeed the only infinite branch, looping on $\bullet$, has infinitely many $\mu \text {-}l$ steps.

Remark 9

(Impossibility of General Regular Completeness). At this juncture let us make an important point: it is impossible to have any (sound) recursively enumerable system, let alone regular cut-free proofs, complete for context-free inclusions, since this problem is $\varPi ^0_1$-complete (see e.g. [27]). In this sense examples of regular proofs are somewhat coincidental.

It is not hard to see that each rule of $\mu \textsf{HKA}$ is sound for language semantics:

Lemma 10

(Local Soundness). For each inference step,

(3)

for some $k\le 2$, we have: $\forall i<k \, \mathcal {L}(\varGamma _i) \subseteq \mathcal {L}(S_i) \implies \mathcal {L}(\varGamma )\subseteq \mathcal {L}(S)$.

Consequently wellfounded $\mu \textsf{HKA}$ proofs are also sound for $\mathcal {L}(\cdot )$, by induction on their structure. For non-wellfounded proofs, we must employ a less constructive argument, typical of non-wellfounded proof theory:

Theorem 11

(Soundness).$\mu \textsf{HKA}\vdash ^{\infty }\varGamma \rightarrow S \implies \mathcal {L}(\varGamma )\subseteq \mathcal {L}(S)$.

Proof

(Sketch). For contradiction, we use (the contrapositive of) Lemma 10 to construct an infinite ‘invalid’ branch B, along with an associated sequence of words $(w_i)_{i<\omega }$ of non-increasing length separating the LHS from the RHS. Now, either B has infinitely many $\textsf{k}$ steps, meaning $(|w_i|)_{i<\omega }$ has no least element, or there are only finitely many $\textsf{k}$ steps, in which case $|w_i|$ is eventually dominated by the number of productive expressions in the sequent, by guardedness.

By inspection of the rules of $\mu \textsf{HKA}$ we have:

Lemma 12

(Invertibility). Let $\textsf{r}$ be a logical step as in (3). $\mathcal {L}(\varGamma )\subseteq \mathcal {L}(S) \implies \mathcal {L}(\varGamma _i)\subseteq \mathcal {L}(S_i)$, for each $i<k$.

Theorem 13

(Completeness).$\mathcal {L}(\varGamma )\subseteq \mathcal {L}(S) \Rightarrow \mu \textsf{HKA}\vdash ^{\infty }\varGamma \rightarrow S$.

In fact, we can obtain a stronger result for left-guarded sequents, namely the ‘leftmost completeness’ as we will see later in Sect. 5. There leftmostness is necessary for soundness, but here completeness is rather straightforward.

Proof

(Sketch). We describe a bottom-up proof search strategy:

• 1. labelitem:applyspslhsspsrulesspsmaximallyspsmuspsonly Apply left logical rules maximally, preserving validity by Lemma 12. Any infinite branch is necessarily progressing.

• 2. This can only terminate at a sequent of the form $a_1, \dots , a_n \rightarrow S$ with $\vec{a} \in \mathcal {L}(S)$, whence we mimic a ‘leftmost’ parsing derivation for $\vec{a}$ wrt S.

4 Completeness of an Infinitary Cut-Free Axiomatisation

While our completeness result above was relatively simple to establish we can use it, along with proof theoretic techniques, to deduce completeness of an infinitary axiomatisation of the theory of $\mu$-expressions. In fact we obtain an alternative proof of the result of [22], strengthening it to a ‘cut-free’ calculus $\mu \textsf{HKA}_{\omega }$.

Write $\mu \textsf{CA}$ for the set of axioms consisting of:

• $(0,1,+,\cdot )$ forms an idempotent semiring (aka a dioid).

• ($\mu$-continuity) $e\mu X f(X) g = \sum \limits _{n<\omega } ef^n(0)g$.

We are using the notation $f^n(0)$ defined by $f^0(0):=0$ and $f^{n+1}(0) :=f (f^n(0))$. We also write $e\le f$ for the natural order given by $e + f = f$. Now define $\mu \textsf{HKA}_{\omega }$ to be the extension of $\mu \textsf{HKA}$ by the ‘$\omega$-rule’:

By inspection of the rules we have soundness of $\mu \textsf{HKA}_{\omega }$ for $\mu \textsf{CA}$:

Proposition 14

$\mu \textsf{HKA}_{\omega }\vdash \varGamma \rightarrow S \implies \mu \textsf{CA}\vdash \prod \varGamma \le \sum \limits _{\varDelta \in S}\prod \varDelta$.

Here the soundness of the $\omega$-rule above is immediate from $\mu$-continuity in $\mu \textsf{CA}$. Note, in particular, that $\mu \textsf{CA}$ already proves that $\mu Xe(X)$ is indeed a fixed point of $e(\cdot )$, i.e. $e(\mu Xe(X)) = \mu X e(X)$ [22]. The main result of this section is:

Theorem 15

$\mu \textsf{HKA}\vdash ^{\infty }e\rightarrow f$ $\implies$ $\mu \textsf{HKA}_{\omega }\vdash e\le f$

Note that, immediately from Theorem 13 and Proposition 14, we obtain:

Corollary 16

$\mathcal {L}(e) \subseteq \mathcal {L}(f) \implies \mu \textsf{HKA}_{\omega }\vdash e\le f \implies \mu \textsf{CA}\vdash e\le f$

To prove Theorem 15 we employ similar techniques to those used for an extension of linear logic with least and greatest fixed points [11], only specialised to the current setting.

Lemma 17

(Projection). For each $\infty$-proof P of $\varGamma , \mu X e(X),\varGamma ' \rightarrow S$ there are $\infty$-proofs P(n) of $\varGamma , e^n(0), \varGamma ' \rightarrow S$, for each $n < \omega$.

The definition of P(n) is somewhat subtle, relying on a form of ‘signature’ common in fixed point logics, restricted to $\omega$. See [11, Definition 15, Proposition 18] for a formal definition and proof of the analogous result. We shall thus use the notation P(n) etc. freely in the sequel.

From here it is simple to provide a translation from $\mu \textsf{HKA}$ $\infty$-proofs to $\mu \textsf{HKA}_{\omega }$ preproofs, as in Definition 22 shortly. However, to prove the image of the translation is wellfounded, we shall need some structural proof theoretic machinery, which will also serve later use when dealing with greatest fixed points in Sects. 5 and 6.

4.1 Intermezzo: Ancestry and Threads

Given an inference step $\textsf{r}$, as typeset in Fig. 2, we say a formula occurrence f in an upper sequent is an immediate ancestor of a formula occurrence e in the lower sequent if they have the same colour; furthermore if e and f are occur in a cedent $\varGamma ,\varGamma ',\varDelta ,\varDelta '$, they must be the matching occurrences of the same formula (i.e. at the same position in the cedent); similarly if e and f occur in the RHS context S, they must be matching occurrences in matching lists.

Construing immediate ancestry as a directed graph allows us to characterise progress by consideration of its paths:

Definition 18

((Progressing) Threads). Fix a preproof P. A thread is a maximal path in the graph of immediate ancestry. An infinite thread on the LHS is progressing if it is infinitely often principal (i.o.p.) for a $\mu \text {-}l$ step.

Our overloading of terminology is suggestive:

Proposition 19

P is progressing $\Leftrightarrow$ each branch of P has a progressing thread.

This has a somewhat subtle proof, relying on König’s lemma on the ancestry graph of a progressing branch in order to recover a progressing thread.

Example 20

Recall the $\infty$-proof in Example 8. The only infinite branch, looping on $\bullet$, has a progressing thread indicated in .

Fact 21

(See, e.g., [30, 36]) Any i.o.p. thread has a unique smallest i.o.p. formula, under the subformula relation. This formula must be a fixed point formula.

4.2 Translation to $\omega$-Branching System

We are now ready to give a translation from $\mu \textsf{HKA}^\infty$ to $\mu \textsf{HKA}_{\omega }$.

Definition 22

($\omega$-Translation). For preproofs P define $P^\omega$ by coinduction:

• $\cdot ^\omega$ commutes with any step not a $\mu \text {-}l$.

• 

Theorem 15 now follows immediately from the following result, obtained by analysis of progressing threads in the image of the $\omega$-translation:

Lemma 23

P is progressing $\implies$ $P^\omega$ is wellfounded.

The proof of Lemma 23 follows the same argument as for the analogous result in [11, Lemma 23].

Example 24

Recalling Example 8, let us see the $\omega$-translation of R in 3. First, let us (suggestively) write $\{a^kb^k\}_{k< n}$ for the n^th approximant of $\{a^nb^n\}_n$, i.e. $\{a^kb^k\}_{k< 0} :=0$ and $\{a^kb^k\}_{k< n+1} :=1 + a \{a^kb^k\}_{k< n} b$. Now $R^\omega$ is given below, left, where recursively and $R(n+1)$ is given below, right:

5 Greatest Fixed Points and $\omega$-Languages

We extend the grammar of expressions from (1) by:

$$ e,f \dots \quad :\,\!:=\quad \dots \quad \mid \quad \nu X e(X) $$

We call such expressions $\mu \nu$-expressions when we need to distinguish them from ones without $\nu$. The notions of a (left-)productive and (left-)guarded expression are defined in the same way, extending the grammar of (2) by the clause $\nu X p$.

As expected $\mu \nu$-expressions denote languages of finite and infinite words:

Definition 25

(Intended Semantics of $\mu \nu$-Expressions). We extend the notation vw to all $v,w\in \mathcal {A}^{\le \omega }$ by setting $vw = v$ when $|v|= \omega$. We extend the definition of $\mathcal {L}(\cdot )$ from Definition 1 to all $\mu \nu$-expressions by setting $\mathcal {L}(\nu X e(X)) :=\bigcup \{ A \subseteq \mathcal {L}(e(A)) \}$ where now A varies over subsets of $\mathcal {A}^{\le \omega }$.

Again, since all the operations are monotone, $\mathcal {L}(\nu X e(X))$ is indeed the greatest fixed point of the operation $A\mapsto \mathcal {L}(e(A))$, by the Knaster-Tarski theorem. In fact ($\omega$-)languages computed by $\mu \nu$-expressions are just the ‘$\omega$-context-free languages’ ($\omega$-CFLs), cf. [5, 42], defined as the ‘Kleene closure’ of CFLs:

Definition 26

($\omega$-Context-Free Languages). For $A\subseteq \mathcal {A}^{+}$ we write $A^\omega :=\{w_0w_1w_2\cdots : \forall i<\omega \, w_i \in A\}$. The class of $\omega$ -CFLs ($\textsf{CF}^\omega$) is defined by:

$$\begin{aligned} \textsf{CF}^\omega \ :=\ \left\{ \bigcup _{i<n} A_iB_i^{\omega } \ : \ n<\omega ; \, A_i,B_i \text { context-free and } \varepsilon \notin A_i,B_i, \, \forall i<n \right\} \end{aligned}$$

It is not hard to see that each $\omega$-CFL is computed by a $\mu \nu$-expression, by noting that $\mathcal {L}(e)^\omega = \mathcal {L}(\nu X (eX))$:

Proposition 27

$L\in \textsf{CF}^\omega \implies L = \mathcal {L}(e)$ for some left-productive e.

We shall address the converse of this result later. First let us present our system for $\mu \nu$-expressions, a natural extension of $\mu \textsf{HKA}$ earlier:

Definition 28

(System). The system $\mu \nu \textsf{HKA}$ extends $\mu \textsf{HKA}$ by the rules:

(4)

Preproofs for this system are defined just as for $\mu \textsf{HKA}$ before. The definitions of immediate ancestor and thread for $\mu \nu \textsf{HKA}$ extends that of $\mu \textsf{HKA}$ from Definition 18 according to the colouring above in (4).

However we must be more nuanced in defining progress, requiring a definition at the level of threads as in Sect. 4. Noting that Fact 21 holds for our extended language with $\nu$s as well as $\mu$s, we call an i.o.p. thread a $\mu$ -thread (or $\nu$ -thread) if its smallest i.o.p. formula is a $\mu$-formula (or $\nu$-formula, respectively).

Definition 29

(Progress). Fix a preproof P. We say that an infinite thread $\tau$ along a (infinite) branch B of P is progressing if it is i.o.p. and it is a $\mu$-thread on the LHS or it is a $\nu$-thread on the RHS. B is progressing if it has a progressing thread. P is a $\infty$-proof of $\mu \nu \textsf{HKA}$ if each of its infinite branches has a progressing thread.

Example 30

Write $e :=\nu Z (abZ)$ and $f :=\mu Y(b + \nu X (aYX))$. The sequent $e\rightarrow [f]$ has a preproof given in Fig. 4. This preproof has just one infinite branch, looping on $\bullet$, which indeed has a progressing thread following the formulas. The only fixed point infinitely often principal along this thread is $\nu X (afX)$, which is principal at each $\bullet$. Thus this preproof is a proof and $e\rightarrow [f]$ is a theorem of $\mu \ell \textsf{HKA}^{\infty }$.

Note that, even though this preproof is progressing, the infinite branch’s smallest i.o.p. formula on the RHS is not a $\nu$-formula, e.g. given by the thread, as f is also i.o.p. Let us point out that (a) the progressiveness condition only requires existence of a progressing thread, even if other threads are not progressing (like the unique LHS thread above).

Fig. 4.

A $\mu \nu \ell \textsf{HKA}$ $\infty$-preproof of $e\rightarrow [f]$, where $e :=\nu Z (abZ)$ and $f :=\mu Y(b + \nu X (aYX))$.

Some Necessary Conventions: Left-Guarded and Leftmost

Crucially, due to the asymmetry in the definition of the product of infinite words, we must employ further conventions to ensure soundness and completeness of $\infty$-proofs for $\mathcal {L}(\cdot )$. Our choice of conventions is inspired by the usual ‘leftmost’ semantics of ‘$\omega$-CFGs’, which we shall see in the next section.

First, we shall henceforth work with a lefmost restriction of $\mu \nu \textsf{HKA}$ in order to maintain soundness for $\mathcal {L}(\cdot )$:

Definition 31

A $\mu \nu \textsf{HKA}$ preproof is leftmost if each logical step has principal formula the leftmost formula of its cedent, and there are no $\textsf{k}_{}^r$-steps. Write $\mu \nu \ell \textsf{HKA}$ for the restriction of $\mu \nu \textsf{HKA}$ to only leftmost steps and $\mu \nu \ell \textsf{HKA}^{\infty }$ for the class of $\infty$-proofs of $\mu \nu \ell \textsf{HKA}$.

We must also restrict ourselves to left-guarded expressios in the sequel:

Convention 32

Henceforth, all expressions are assumed to be left-guarded.

Let us justify both of these restrictions via some examples.

Remark 33

(Unsound for Non-leftmost). Unlike the $\mu$-only setting it turns out that $\mu \nu \textsf{HKA}^{\infty }$ is unsound without the leftmost restriction, regardless of left-guardedness. For instance consider the preproof,

where $a,\bullet$ roots the same subproof as $\bullet$, but for an extra a on the left of every RHS. Of course the endsequent is not valid, as the LHS denotes $\{\varepsilon \}$ while the RHS denotes $\{a^\omega \}$. Note also that, while it is progressing thanks to the thread in , it is not leftmost due to the topmost displayed $\nu \text {-}r$ step.

Remark 34

(Incomplete for Unguarded). On the other hand, without the left-guardedness restriction, $\mu \nu \ell \textsf{HKA}^{\infty }$ is not complete. For instance the sequent $\nu X X \rightarrow [\;] , \{ [a , \nu X X]\}_{a \in \mathcal {A}}$ is indeed valid as both sides compute all of $\mathcal {P}(\mathcal {A}^{\le \omega })$: any word is either empty or begins with a letter. However the only available (leftmost) rule application, bottom-up, is $\nu \text {-}l$, which is a fixed point of leftmost proof search, obviously not yielding a progressing preproof.

6 Metalogical Results: A Game-Theoretic Approach

Now we return to addressing the expressiveness of both the syntax of $\mu \nu$-expressions and our system $\mu \nu \ell \textsf{HKA}^{\infty }$, employing game-theoretic methods.

6.1 Evaluation Puzzle and Soundness

Fig. 5.

Rules of the evaluation puzzle.

As an engine for our main metalogical results about $\mu \nu \ell \textsf{HKA}$, and for a converse to Proposition 27, we first characterise membership via games:

Definition 35

The evaluation puzzle is a puzzle (i.e. one-player game) whose positions are pairs $(w,\varGamma )$ where $w\in \mathcal {A}^{\le \omega }$ and $\varGamma$ is a cedent, i.e. a list of $\mu \nu$-expressions. A play of the puzzle runs according to the rules in Fig. 5: puzzle-play is deterministic at each state except when the expression is a sum, in which case a choice must be made. During a play of the evaluation puzzle, formula ancestry and threads are defined as for $\mu \nu \ell \textsf{HKA}$ preproofs, by associating each move with the LHS of a left logical rule. A play is winning if:

• it terminates at the winning state $(\varepsilon ,[\;])$; or,

• it is infinite and has a $\nu$-thread (along its right components).

Example 36

Define $d:=\mu X(\langle \rangle + \langle X\rangle X)$, the set of non-empty well-bracketed words. Let $d^\omega :=\nu Y dY$. Let us look at a play from $(\langle ^\omega ,[d^\omega ])$.

The play continues without $d^\omega$ ever being principal (essentially, going into deeper and deeper nesting to match a $\langle$ with a $\rangle$). Since even the first match is never made there is no hope of progress. The play (and, in fact, any play) is thus losing. On the other hand the following play from $(u,[d^\omega ])$, where $u=(\langle \rangle )^\omega$ is indeed winning, with progressing $\nu$-thread indicated in .

Theorem 37

(Evaluation).$w \in \mathcal {L}(\varGamma )$ $\Leftrightarrow$ there is a winning play from $(w,\varGamma )$.

The proof is rather involved, employing the method of ‘signatures’ common in fixed point logics, cf. e.g. [48], which serve as ‘least witnesses’ to word membership via carefully managing ordinal approximants for fixed points. Here we must be somewhat more careful in the argument because positions of our puzzle include cedents, not single formulas: we must crucially assign signatures to each formula of a cedent. Working with cedents rather than formulas allows the evaluation puzzle to remain strictly single player. This is critical for expressivity: alternating context-free grammars and pushdown automata compute more than just CFLs [4, 45].

We can now prove the soundness of $\mu \nu \ell \textsf{HKA}^{\infty }$ by reduction to Theorem 37:

Theorem 38

(Soundness).$\mu \nu \ell \textsf{HKA}\vdash ^{\infty }\varGamma \rightarrow S$ $\implies$ $\mathcal {L}(\varGamma )\subseteq \mathcal {L}(S)$.

Proof

(Sketch). Let P be a $\infty$-proof of $\varGamma \rightarrow S$ and $w\in \mathcal {L}(\varGamma )$. We show $w\in \mathcal {L}(S)$. First, since $w\in \mathcal {L}(\varGamma )$ there is a winning play $\pi$ from $(w,\varGamma )$ by Theorem 37, which induces a unique (maximal) branch $B_\pi$ of P which must have a progressing thread $\tau$. Now, since $\pi$ is a winning play from (w, e), $\tau$ cannot be on the LHS, so it is an RHS $\nu$-thread following, say, a sequence of cedents $[\varGamma _i]_{i<\omega }$. By construction $[\varGamma _i]_{i<\omega }$ has an infinite subsequence, namely whenever it is principal, that forms (the right components of) a winning play from $(w,\varGamma _0)$, with $\varGamma _0 \in S$. Thus indeed $w \in \mathcal {L}(S)$ by Theorem 37.

6.2 $\omega$-Context-Freeness via Muller Grammars

We can now use the adequacy of the evaluation puzzle to recover a converse of Proposition 27. For this, we need to recall a grammar-formulation of $\textsf{CF}^\omega$, due to Cohen and Gold [5] and independently Nivat [46, 47].

A Muller ($\omega$-)CFG (MCFG) is a CFG $\mathcal {G}$, equipped with a set $F\subseteq \mathcal {P}(\mathcal {V})$ of accepting sets of productions. We define a rewrite relation $\rightarrow _{\mathcal {G}}\, \subseteq (\mathcal {V}\cup \mathcal {A})^* \times (\mathcal {V}\cup \mathcal {A})^*$, leftmost reduction, by $\vec{a} X v \rightarrow _{\mathcal {G}}\vec{a} u v$ whenever $\vec{a} \in \mathcal {A}^*$, $X\rightarrow u$ is a production of $\mathcal {G}$ and $v \in (\mathcal {V}\cup \mathcal {A})^*$. A leftmost derivation is just a maximal (possibly infinite) sequence along $\rightarrow _{\mathcal {G}}$. We say $\mathcal {G}$ accepts $w \in \mathcal {A}^{ \le \omega }$ if there is a leftmost derivation $\delta$ such that $\delta$ converges to w and the set of infinitely often occurring states that are LHSs of productions along $\delta$ is in F. We write $\mathcal {L}(\mathcal {G})$ for the set of words $\mathcal {G}$ accepts.

Theorem 39

([5, 46, 47]). Let $L\subseteq \mathcal {A}^{\omega }$. $L\in \textsf{CF}^\omega \Leftrightarrow L=\mathcal {L}(\mathcal {G})$ for a MCFG $\mathcal {G}$.

Now we have a converse of Proposition 27 by:

Proposition 40

For each expression e there is a MCFG $\mathcal {G}$ s.t. $\mathcal {L}(e) = \mathcal {L}(\mathcal {G})$.

Proof

(sketch). Given a $\mu \nu$-expression e, we construct a grammar just like in the proof of Theorem 5, but with extra clause $X_{\nu X f(X)} \rightarrow X_{f(\nu X f(X))}$. We maintain two copies of each non-terminal, one and one normal so that a derivation also ‘guesses’ a ‘on the fly’. Now set F, the set of acceptable sets, to include all sets extending some , for E with the smallest expression a $\nu$-formula, by normal non-terminals. Now any accepting leftmost derivation of a word w from describes a winning play of the evaluation puzzle from (w, e) and vice-versa.

6.3 Proof Search Game and Completeness

In order to prove completeness of $\mu \nu \ell \textsf{HKA}^{\infty }$, we need to introduce a game-theoretic mechanism for organising proof search, in particular so that we can rely on determinacy principles thereof.

Definition 41

(Proof Search Game). The proof search game (for $\mu \nu \ell \textsf{HKA}$) is a two-player game played between Prover $(\textbf{P})$, whose positions are inference steps of $\mu \nu \ell \textsf{HKA}$, and Denier $(\textbf{D})$, whose positions are sequents of $\mu \nu \ell \textsf{HKA}$. A play of the game starts from a particular sequent: at each turn, $\textbf{P}$ chooses an inference step with the current sequent as conclusion, and $\textbf{D}$ chooses a premiss of that step; the process repeats from this sequent as long as possible.

An infinite play of the game is won by $\textbf{P}$ (aka lost by $\textbf{D}$) if the branch constructed has a progressing thread; otherwise it is won by $\textbf{D}$ (aka lost by $\textbf{P}$). In the case of deadlock, the player with no valid move loses.

Proposition 42

(Determinacy ($\exists 0\#$)). The proof search game is determined, i.e. from any sequent $\varGamma \rightarrow S$, either $\textbf{P}$ or $\textbf{D}$ has a winning strategy.

Note that the winning condition of the proof search game is (lightface) analytic, i.e. $\varSigma ^1_1$: “there exists a progressing thread”. Lightface analytic determinacy lies beyond $\textrm{ZFC}$, as indicated equivalent to the existence of $0\#$ [24]. Further consideration of our metatheory is beyond the scope of this work.

It is not hard to see that $\textbf{P}$-winning-strategies are ‘just’ $\infty$-proofs. Our goal is to show a similar result for $\textbf{D}$, a sort of ‘countermodel construction’.

Lemma 43

$\textbf{D}$ has a winning strategy from $\varGamma \rightarrow S$ $\implies$ $\mathcal {L}(\varGamma )\setminus \mathcal {L}(S) \ne \varnothing$.

Before proving this, let us point out that Lemma 12 applies equally to the system $\mu \nu \textsf{HKA}$. We also have the useful observation:

Proposition 44

(Modal).$\mathcal {L}(a\varGamma ) \subseteq \{\varepsilon \} \cup \bigcup \limits _{a\in \mathcal {A}}\mathcal {L}(aS_a) \implies \mathcal {L}(\varGamma ) \subseteq \mathcal {L}(S_a)$.

This follows directly from the definition of $\mathcal {L}(\cdot )$. Now we can carry out our ‘countermodel construction’ from $\textbf{D}$-winning-strategies:

Proof

(Sketch, of Lemma 43). Construct a $\textbf{P}$-strategy $\mathfrak {p}$ that is deadlock-free by always preserving validity, relying on Lemma 12 and Proposition 44. Now, suppose $\mathfrak {d}$ is a $\textbf{D}$-winning-strategy and play $\mathfrak {p}$ against it to construct a play $B = (\mathcal {S}_i)_{i<\omega } = ( \varGamma _i \rightarrow S_i)_{i<\omega }$. Note that indeed this play must be infinite since (a) $\mathfrak {p}$ is deadlock-free; and (b) $\mathfrak {d}$ is $\textbf{D}$-winning. Now, let $w = \prod \limits _{\textsf{k}_{a}^l \in B} a$ be the product of labels of $\textsf{k}$ steps along B, in the order they appear bottom-up. We claim $w \in \mathcal {L}(\varGamma )\setminus \mathcal {L}(S)$:

• $w \in \mathcal {L}(\varGamma )$. By construction $[\varGamma _i]_i$ has a subsequence forming an infinite play $\pi$ of the evaluation puzzle from $(w,\varGamma )$. Since the play B is won by $\textbf{D}$, B cannot have a $\mu$-thread so it must have a $\nu$-thread (since it is i.o.p.), and so $\pi$ is winning. Thus $w \in \mathcal {L}(\varGamma )$ by Theorem 37.

• $w \notin \mathcal {L}(S)$. Take an arbitrary play $\pi$ of the evaluation puzzle from some $(w,\varDelta )$ with $\varDelta \in S$. This again induces an infinite sequence of cedents $[\varDelta _i]_{i<\omega }$ along the RHSs of B. Now, $[\varDelta _i]_{i<\omega }$ cannot have a $\nu$-thread by assumption that B is winning for $\textbf{D}$, and so $\pi$ is not a winning play of the evaluation puzzle from $(w,\varDelta )$. Since the choices of $\varDelta \in S$ and play $\pi$ were arbitrary, indeed we have $w\notin \mathcal {L}(S)$ by Theorem 37.

Now from Proposition 42 and Lemma 43, observing that $\textbf{P}$-winning-strategies are just $\infty$-proofs, we conclude:

Theorem 45

(Completeness).$\mathcal {L}(\varGamma )\subseteq \mathcal {L}(S) \implies \mu \nu \ell \textsf{HKA}\vdash ^{\infty }\varGamma \rightarrow S$.

7 Complexity Matters and Further Perspectives

In this section we make further comments, in particular regarding the complexity of our systems, at the level of arithmetical and analytical hierarchies. These concepts are well-surveyed in standard textbooks, e.g. [44, 50], as well as various online resources.

Complexity and Irregularity for Finite Words. The equational theory of $\mu$-expressions in $\mathcal {L}(\cdot )$ is $\varPi ^0_1$-complete, i.e. co-recursively-enumerable, due to the same complexity of universality of context-free grammars (see, e.g., [27]). In this sense there is no hope of attaining a finitely presentable (e.g. cyclic, inductive) system for the equational theory of $\mu$-expressions in $\mathcal {L}(\cdot )$. However it is not hard to see that our wellfounded system $\mu \textsf{HKA}_{\omega }$ enjoys optimal $\varPi ^0_1$ proof search, thanks to invertibility and termination of the rules, along with decidability of membership checking. Indeed a similar argument is used by Palka in [49] for the theory of ‘$*$-continuous action lattices’. Furthermore let us point out that our non-wellfounded system also enjoys optimal proof search: $\mu \textsf{HKA}\vdash ^{\infty }\varGamma \rightarrow S$ is equivalent, by invertibility, to checking that every sequent $\vec{a} \rightarrow S$ reachable by only left rules in bottom-up proof search has a polynomial-size proof (bound induced by length of leftmost derivations). This is a $\varPi ^0_1$ property.

Complexity and Inaxiomatisability for Infinite Words. It would be natural to wonder whether a similar argument to Sect. 4 gives rise to some infinitary axiomatisation of the equational theory of $\mu \nu$-expressions in $\mathcal {L}(\cdot )$. In fact, it turns out this is impossible: the equational theory of $\omega$-CFLs is $\varPi ^1_2$-complete [19], so there is no hope of a $\varPi ^0_1$ (or even $\varSigma ^1_2$) axiomatisation. In particular, the projection argument of Sect. 4 cannot be scaled to the full system $\mu \nu \ell \textsf{HKA}$ because $\cdot$ does not distribute over $\bigcap$ in $\mathcal {L}(\cdot )$, for the corresponding putative ‘right $\omega$ steps’ for $\nu$. For instance $0 = ((aa)^* \cap a(aa)^*) a^* \ne (aa)^*a^* \cap a(aa)^*a^* = aa^*$. Indeed let us point out that here it is crucial to use our hypersequential system $\textsf{HKA}$ as a base rather than, say, the intuitionistic systems of other proof theoretic works for regular expressions (and friends) [16, 49]: the appropriate extension of those systems by $\mu$s and $\nu$s should indeed enjoy an $\omega$-translation, due to only one formula on the right, rendering them incomplete.

Again let us point out that $\infty$-provability in $\mu \nu \ell \textsf{HKA}$, in a sense, enjoys optimal complexity. By determinacy of the proof search game, $\mu \nu \ell \textsf{HKA}\vdash ^{\infty }\varGamma \rightarrow S$ if and only if there is no $\textbf{D}$-winning-strategy from $\varGamma \rightarrow S$. The latter is indeed a $\varPi ^1_2$ statement: “for every $\textbf{D}$-strategy, there exists a play along which there exists a progressing thread”.

Comparison to [22]. Our method for showing completeness of $\mu \textsf{HKA}_{\omega }$ is quite different from the analogous result of [22] which uses the notion of ‘rank’ for $\mu$-formulas, cf. [1]. Our result is somewhat stronger, giving cut-free completeness, but it could be possible to use ranks directly to obtain such a result too. More interestingly, the notion of projections and $\omega$-translation should be well-defined (for LHS $\mu$ formulas) even in the presence of $\nu$s, cf. [11], whereas the rank method apparently breaks down in such extensions. This means that our method should also scale to $\mu \nu \textsf{HKA}$ $\infty$-proofs where, say, each infinite branch has a LHS $\mu$-thread. It would be interesting to see if this method can be used to axiomatise some natural fragments of $\omega$-context-free inclusions.

Note that, strictly speaking, our completeness result for $\mu \textsf{CA}$ was only given for the guarded fragment. However it is known that $\mu \textsf{CA}$ (and even weaker theories) already proves the equivalence of each expression to one that is even left-guarded, by formalising conversion to Greibach normal form [18].

8 Conclusions

In this work we investigated of the proof theory of context-free languages (CFLs) over a syntax of $\mu$-expressions. We defined a non-wellfounded proof system $\mu \textsf{HKA}^\infty$ and showed its soundness and completeness for the model $\mathcal {L}(\cdot )$ of context-free languages. We used this completeness result to recover the same for a cut-free $\omega$-branching system $\mu \textsf{HKA}_{\omega }$ via proof-theoretic techniques. This gave an alternative proof of the completeness for the theory of $\mu$-continuous Chomsky algebras from [22]. We extended $\mu$-expressions by greatest fixed points to obtain a syntax for $\omega$-context-free languages. We studied an extension by greatest fixed points, $\mu \nu \ell \textsf{HKA}^{\infty }$ and showed its soundness and completeness for the model $\mathcal {L}(\cdot )$ of context-free languages, employing game theoretic techniques.

Since inclusion of CFLs is $\varPi ^0_1$-complete, no recursively enumerable (r.e.) system can be sound and complete for their equational theory. However, by restricting products to a letter on the left one can obtain a syntax for right-linear grammars. Indeed, for such a restriction complete cyclic systems can be duly obtained [10]. It would be interesting to investigate systems for related decidable or r.e. inclusion problems, e.g. inclusions of context-free languages in regular languages, and inclusions of visibly pushdown languages [2, 3].

The positions of our evaluation puzzle for $\mu \nu$-expressions use cedents to decompose products, similar to the stack of a pushdown automaton, rather than requiring an additional player. Previous works have similarly proposed model-checking games for (fragments/variations of) context-free expressions, cf. [37, 43], where more complex winning conditions seem to be required. It would be interesting to compare our evaluation puzzle to those games in more detail.

Note that our completeness result, via determinacy of the proof search game, depends on the assumption of (lightface) analytic determinacy. It is natural to ask whether this is necessary, but this consideration is beyond the scope of this work. Let us point out, however, that even $\omega$-context-free determinacy exceeds the capacity of $\textrm{ZFC}$ [20, 41].

Finally, it would be interesting to study the structural proof theory arising from systems $\mu \textsf{HKA}^\infty$ and $\mu \nu \textsf{HKA}^{\infty }$, cf. [16]. It would also be interesting to see if the restriction to leftmost $\infty$-proofs can be replaced by stronger progress conditions, such as the ‘alternating threads’ from [13, 14], in a similar hypersequential system for predicate logic. Note that the same leftmost constraint was employed in [25] for an extension of $\textsf{HKA}$ to $\omega$-regular languages.