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

Anupam Das and Abhishek De  University of Birmingham, UK
<EMAIL_ADDRESS>
###### 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 [DP17], 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 [GR62], Schutzenberger [Sch63], and Gruska
[Gru71]. This induces a syntax for CFLs by adding least fixed point operators
to regular expressions, as first noted by Salomaa [Sal73]. Leiß [Lei92] 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 [Thi17] and criteria for
identifying $\mu$-expressions that can be parsed unambiguously [KY19].

Establishing axiomatisations and proof systems for classes of formal languages
has been a difficult challenge. Many _theories_ of regular expressions, such
as Kleene algebras ($\mathsf{KA}$) were proposed in the late 20th century
(see, e.g., e.g. [Con71, Kle56, Koz94]). The completeness of $\mathsf{KA}$ for
the (equational) theory of regular languages, due to Kozen [Koz94] and Krob
[Kro90] independently, is a celebrated result that has led to several
extensions and refinements, e.g. [KS97, KS12, CLS15, KS20]. More recently the
proof theory of $\mathsf{KA}$ has been studied via _infinitary_ systems. On
one hand, [Pal07] proposed an _$\omega$ -branching_ sequent calculus and on
the other hand [DP17, DDP18, HK22] have studied _cyclic_ ‘hypersequential’
calculi.

Inclusion of CFLs is $\Pi^{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_ [ÉL02, EL05, Lei16, LH18], giving
rise to a rich algebraic theory. Indeed Grathwohl, Henglein, and Kozen [GHK13]
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.

$\mu\mathsf{CA}$$\mu\mathsf{HKA}^{\infty}$context-free
languages$\mu\nu\ell\mathsf{HKA}^{\infty}$$\omega$-context-free
languagessoundness, e.g. [GHK13]Theorem 16Theorem 18Theorem 46Theorem
57Theorem 21Proposition 20Proof systemsLanguage models Figure 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 16, is also a consequence of the remaining black ones.

Contributions. In this paper, we propose a _non-wellfounded_ system
$\mu\mathsf{HKA}^{\infty}$ for $\mu$-expressions. It can be seen as an
extension of the cyclic system of [DP17] for regular expressions. Our first
main contribution is the adequacy of this system for CFLs:
$\mu\mathsf{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 alternative proof of completeness of the infinitary
axiomatisation $\mu\mathsf{CA}$ of [GHK13], comprising our second main result.
Our method is inspired by previous techniques in non-wellfounded proof-theory,
namely [Stu08, DDS23], employing ‘projections’ to translate non-wellfounded
proofs to wellfounded ones. Our result is actually somewhat stronger than that
of [GHK13], since our wellfounded proofs are furthermore _cut-free_.

Finally we develop an extension $\mu\nu\ell\mathsf{HKA}$ of (leftmost)
$\mu\mathsf{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\mathsf{HKA}$ for $\mathcal{L}(\cdot)$. Compared to
$\mu\mathsf{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.

### Acknowledgements

This work was supported by a UKRI Future Leaders Fellowship, ‘Structure vs
Invariants in Proofs’, project reference MR/S035540/1. The authors are
grateful to anonymous reviewers for their helpful comments (in particular,
leading to Example 38) and for pointing us to relevant literature such as
[Lan02, LMS04, MHHO05].

##  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:

(1) $e,f,\dots\quad::=0\mid 1\mid X\mid a\mid e+f\mid e\cdot f\mid\mu Xe$

We usually simply write $ef$ instead of $e\cdot f$. $\mu$ is considered a
variable binder, with the _free variables_ $\mathrm{FV}(e)$ of an expression
$e$ defined as expected:

######  Definition 1 (Free variables).

The set of free variables of an expression $e$, written $\mathrm{FV}(e)$, is
defined by:

  * •

$\mathrm{FV}(0):=\varnothing$

  * •

$\mathrm{FV}(1):=\varnothing$

  * •

$\mathrm{FV}(X):=\\{X\\}$

  * •

$\mathrm{FV}(e+f):=\mathrm{FV}(e)\cup\mathrm{FV}(f)$

  * •

$\mathrm{FV}(ae):=\mathrm{FV}(e)$

  * •

$\mathrm{FV}(\mu Xe):=\mathrm{FV}(e)\setminus\\{X\\}$

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 2 (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:

  * •

$\mathcal{L}(0):=\varnothing$

  * •

$\mathcal{L}(1):=\\{\varepsilon\\}$

  * •

$\mathcal{L}(a):=\\{a\\}$

  * •

$\mathcal{L}(A):=A$

  * •

$\mathcal{L}(e+f):=\mathcal{L}(e)\cup\mathcal{L}(f)$

  * •

$\mathcal{L}(ef):=\\{vw:v\in\mathcal{L}(e),w\in\mathcal{L}(f)\\}$

  * •

$\mathcal{L}(\mu Xe(X)):=\bigcap\\{A\supseteq\mathcal{L}(e(A))\\}$

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 Xe(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:

(2) $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 Xp$

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 3.

Henceforth we assume all expressions are guarded.

######  Remark 4 (Why only guarded expressions?).

There are several reasons for employing this convention. Most importantly,
left-guardedness will be required for our treatment of $\omega$-words later
via greatest fixed points, where grammars naturally parse from the left via
_leftmost derivations_. In the current setting, over finite words with only
least fixed points, it makes little difference whether we use only guarded
expressions or not, nor whether we guard from the left or right. However our
convention does simplify some proofs and change some statements; we will
comment on such peculiarities when they are important.

######  Example 5 (Empty language).

In the semantics above, note that the empty language $\varnothing$ is computed
by several expressions, not only $0$ but also $\mu XX$ 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 6 (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 [GR62, Sch63, Gru71]. In fact this holds even under the restriction
to left-guarded expressions, by simulating the _Greibach normal form_ :

######  Theorem 7 (Adequacy, see, e.g., [ÉL02, EL05]).

$L$ is context-free (and $\varepsilon\notin L$) $\iff$ $L=\mathcal{L}(e)$ for
some $e$ left-guarded (and left-productive, respectively).

While this argument is known, it is pertinent to recall it as we are working
with only guarded expressions, and as some of the intermediate concepts will
be useful to us later. First we will need to define a notion of subformula
peculiar to fixed point expressions:

######  Definition 8 (Fisher-Ladner (FL)).

The Fischer-Ladner (FL) closure of an expression $e$, written
$\mathrm{FL}(e)$, is the smallest set of expressions closed under closed
subformulas and, whenever $\mu Xf(X)\in\mathrm{FL}(e)$ then $f(\mu
Xf(X))\in\mathrm{FL}(e)$.

It is well-known that $\mathrm{FL}(e)$ is finite, and in fact has size linear
in that of $e$. Now the $\impliedby$ direction of the Adequacy theorem,
Theorem 7, can be proved by construing $\mathrm{FL}(e)$ as the non-terminals
of an appropriate CFG. Formally, this is broken up into the following two
Propositions.

######  Proposition 9.

$\mathcal{L}(e)$ is context-free, for any closed expression $e$.

###### Proof of Proposition 9.

We construct a CF grammar with nonterminals $X_{f}$ for each
$f\in\mathrm{FL}(e)$, starting nonterminal $X_{e}$, and all productions of
form:

(3) $\begin{array}[]{r@{\quad\rightarrow\quad}l}X_{1}&\varepsilon\\\
X_{a}&a\\\ X_{f+g}&X_{f}\quad|\quad X_{g}\\\ X_{fg}&X_{f}X_{g}\\\ X_{\mu
Xf(X)}&X_{f(\mu Xf(X))}\qed\end{array}$

For the $\implies$ direction of Theorem 7, since we assume only guarded
expressions, we work with grammars in _Greibach normal form_ (GNF). Recall
that a GNF grammar is one for which each production has form $X\to a\vec{X}$
or $X\to\varepsilon$, for $X,\vec{X}$ non-terminals and $a\in\mathcal{A}$. It
is well-known that such grammars exhaust all CF languages [JEH01]. Thus we
obtain a slightly stronger result:

######  Proposition 10 (see, e.g., [ÉL02, EL05]).

$L$ is context-free $\implies$ $L=\mathcal{L}(e)$ for some left-guarded
expression $e$. Moreover if $\varepsilon\notin L$ then $e$ is left-productive.

###### Proof sketch.

We expand the statement to grammars where each non-terminal has a unique
production whose RHS is an arbitrary left-guarded $\mu$-expression, i.e. of
the form $\\{X_{i}\to e_{i}(\vec{X})\\}_{i<n}$ for non-terminals
$\vec{X}=X_{0},\dots,X_{n-1}$. Note that this exhausts all context-free
languages by (a) assuming Greibach normal form for left-guardedness; and (b)
using $+$ to combine multiple productions from the same non-terminal. From
here we proceed by induction on $n$, the number of non-terminals, using
_Bekić’s Theorem_ for resolving equational systems. Namely from $\\{X_{i}\to
e_{i}(\vec{X},X_{n})\\}_{i\leq n}$ we set $e_{n}^{\prime}(\vec{X}):=\mu
X_{n}e_{n}(\vec{X},X_{n})$ and first find solutions $\vec{f}$ to the grammar
$\\{X_{i}\to e_{i}(\vec{X},e_{n}^{\prime}(\vec{X}))\\}_{i<n}$, by inductive
hypothesis. Now we set the solution for $X_{n}$ to be
$f_{n}:=e_{n}^{\prime}(\vec{f})$. Note that, since we did not introduce
identities, the solutions contain $1$ just if there is an $\varepsilon$
production for some non-terminal, by Greibach normal form. ∎

######  Example 11.

Consider the left-guarded expressions $\mathrm{Dyck}_{1}:=\mu X(1+\langle
X\rangle X)$ and $\\{a^{n}b^{n}\\}_{n}:=\mu X(1+aXb)$. As suggested,
$\mathrm{Dyck}_{1}$ indeed computes the language of well-bracketed words over
alphabet $\\{\langle,\rangle\\}$, whereas $\\{a^{n}b^{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 6, 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 5.

##  3\. A non-wellfounded proof system

In this section we extend a calculus $\mathsf{HKA}$ from [DP17] 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 $\Gamma\rightarrow S$ where $\Gamma$ (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}(\Gamma):=\mathcal{L}(\prod\Gamma)$ and
$\mathcal{L}(S):=\bigcup\limits_{\Gamma\in S}\mathcal{L}(\Gamma)$.

<EMAIL_ADDRESS>rules:}}}&{\vbox{\hbox{\kern
13.27773pt\hbox{\vbox{\offinterlineskip\hbox{\kern
7.49995pt\hbox{\hbox{\hbox{$$}}}\kern 7.49995pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{init}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to14.99992pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\rightarrow[\,]$}\kern 0.0pt$}}}}}\kern
0.0pt}}}\qquad{\vbox{\hbox{\kern
13.51915pt\hbox{\vbox{\offinterlineskip\hbox{\kern
9.16667pt\hbox{\hbox{\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}}}\kern
9.16667pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to36.29169pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S},[\Delta]$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\qquad{\vbox{\hbox{\kern
8.58652pt\hbox{\vbox{\offinterlineskip\hbox{\kern
8.06363pt\hbox{\hbox{\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}}}\kern
8.06363pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{k}_{a}^{l}\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to34.08562pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$a,{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow
a{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\qquad{\vbox{\hbox{\kern
8.58652pt\hbox{\vbox{\offinterlineskip\hbox{\kern
8.89694pt\hbox{\hbox{\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}}}\kern
8.89694pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{k}_{a}^{r}\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to35.75224pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},a\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}a$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\\\ \vskip 3.0pt plus 1.0pt minus
1.0pt\cr\text{\parbox{51.21504pt}{{Left logical
rules:}}}&\begin{array}[]{c}{\vbox{\hbox{\kern
10.83743pt\hbox{\vbox{\offinterlineskip\hbox{\kern
18.15196pt\hbox{\hbox{\hbox{$$}}}\kern 18.15196pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle
0\text{-}l\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to36.30394pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}0},{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color@cmyk@fill{0}{0}{1}{.5}\Gamma^{\prime}}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\qquad{\vbox{\hbox{\kern
10.83743pt\hbox{\vbox{\offinterlineskip\hbox{\kern
3.8889pt\hbox{\hbox{\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color@cmyk@fill{0}{0}{1}{.5}\Gamma}^{\prime}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}}}\kern
3.8889pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle 1\text{-}l\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to36.30394pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}1},{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color@cmyk@fill{0}{0}{1}{.5}\Gamma^{\prime}}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\qquad{\vbox{\hbox{\kern
11.50404pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}e},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}f},{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color@cmyk@fill{0}{0}{1}{.5}\Gamma^{\prime}}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\cdot\text{-}l\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to44.71024pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
1.38889pt\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}ef},{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color@cmyk@fill{0}{0}{1}{.5}\Gamma^{\prime}}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}\kern
0.0pt$}}\kern 1.38889pt}}}\kern 0.0pt}}}\\\ \vskip 3.0pt plus 1.0pt minus
1.0pt\cr{{}{}\vbox{\hbox{\kern
15.00406pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}e},{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color@cmyk@fill{0}{0}{1}{.5}\Gamma^{\prime}}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}}\kern
10.00002pt}\hbox{\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}f},{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color@cmyk@fill{0}{0}{1}{.5}\Gamma^{\prime}}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle+\text{-}l\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to83.23639pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
14.5409pt\hbox{\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}e+f},{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color@cmyk@fill{0}{0}{1}{.5}\Gamma^{\prime}}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}}\kern
14.5409pt}}}\kern 0.0pt}}}\qquad{\vbox{\hbox{\kern
11.55527pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}e(\mu
Xe(X))},{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color@cmyk@fill{0}{0}{1}{.5}\Gamma^{\prime}}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mu\text{-}l\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to80.3364pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
6.21703pt\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\mu
Xe(X)},{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color@cmyk@fill{0}{0}{1}{.5}\Gamma^{\prime}}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}\kern
0.0pt$}}\kern 6.21703pt}}}\kern 0.0pt}}}\end{array}\\\ \vskip 3.0pt plus 1.0pt
minus 1.0pt\cr\text{\parbox{59.75095pt}{{Right logical
rules:}}}&\begin{array}[]{c}{\vbox{\hbox{\kern
11.9636pt\hbox{\vbox{\offinterlineskip\hbox{\kern
19.38113pt\hbox{\hbox{\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$}}}\kern
19.38113pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle 0\text{-}r\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to56.72063pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S},[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Delta},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}0},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\Delta^{\prime}}]$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\qquad{\vbox{\hbox{\kern
11.9636pt\hbox{\vbox{\offinterlineskip\hbox{\kern
3.8889pt\hbox{\hbox{\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S},[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Delta},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\Delta^{\prime}}]$}}}\kern
3.8889pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle 1\text{-}r\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to56.72063pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S},[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Delta},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}1},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\Delta^{\prime}}]$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\qquad{\vbox{\hbox{\kern
12.6302pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S},[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Delta},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}e},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}f},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\Delta}]$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\cdot\text{-}r\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to63.58693pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
0.6189pt\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S},[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Delta},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}ef},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\Delta^{\prime}}]$}\kern
0.0pt$}}\kern 0.6189pt}}}\kern 0.0pt}}}\\\ \vskip 3.0pt plus 1.0pt minus
1.0pt\cr{\vbox{\hbox{\kern
16.13022pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S},[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Delta},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}e},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\Delta^{\prime}}],[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Delta},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}f},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\Delta^{\prime}}]$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle+\text{-}r\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to96.1114pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
10.77007pt\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S},[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Delta},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}e+f},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\Delta^{\prime}}]$}\kern
0.0pt$}}\kern 10.77007pt}}}\kern 0.0pt}}}\qquad{\vbox{\hbox{\kern
12.68143pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S},[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Delta},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}e(\mu
Xe(X))},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\Delta^{\prime}}]$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mu\text{-}r\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to100.75308pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
6.21703pt\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S},[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Delta},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\mu
Xe(X)},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\Delta^{\prime}}]$}\kern
0.0pt$}}\kern 6.21703pt}}}\kern 0.0pt}}}\end{array}\end{array}$ Figure 2.
Rules of the system $\mu\mathsf{HKA}$.

The system $\mu\mathsf{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 $\mathsf{k}$ rules, we write
$aS:=\\{[a,\Gamma]:\Gamma\in S\\}$ and $Sa:=\\{[\Gamma,a]:\Gamma\in S\\}$.

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

Our system differs from the original presentation of $\mathsf{HKA}$ in [DP17]
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 $\mathsf{k}$ rule, for
symmetry. We extend the corresponding notions of non-wellfounded proof
appropriately:

######  Definition 12 (Non-wellfounded proofs).

A preproof (of $\mu\mathsf{HKA}$) is generated _coinductively_ from the rules
of $\mu\mathsf{HKA}$ i.e. it is a possibly infinite tree of sequents (of
height $\leq\omega$) generated by the rules of $\mu\mathsf{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\mathsf{HKA}\vdash^{\infty}\Gamma\rightarrow S$ if $\Gamma\rightarrow S$
has a $\infty$-proof in $\mu\mathsf{HKA}$, and sometimes write
$\mu\mathsf{HKA}^{\infty}$ for the class of $\infty$-proofs of
$\mu\mathsf{HKA}$.

Note that our progress condition on preproofs is equivalent to simply checking
that every infinite branch has infinitely many left-logical or $\mathsf{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 $\mathbf{NL}$, see e.g. [DP17, CD22]).

The need for such a complex hypersequential line structure is justified in
[DP17] by the desideratum of _regular_ completeness for the theory of regular
expressions: intuitionistic ‘Lambek-like’ systems, cf. e.g. [Jip04, Pal07,
DP18] are incomplete (wrt regular cut-free proofs). The complexity of the RHS
of sequents in $\mathsf{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 actually gain _more_ regular proofs of inclusions
between context-free languages. For instance:

$\scriptstyle\mathsf{init}\;$ $\rightarrow[\,]$ $\scriptstyle
1\text{-}l,1\text{-}r\;$ $1\rightarrow[1]$
$\scriptstyle\mathsf{w}\text{-}r,+\text{-}r\;$
$1\rightarrow[1+a(a^{*}b^{*})+(a^{*}b^{*})b]$ $\vdots$
$\scriptstyle\mu\text{-}l,\mu\text{-}r\;$ $\;\bullet$
${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\\{a^{n}b^{n}\\}_{n}}\rightarrow(a^{*}b^{*})$
$\scriptstyle\mathsf{k}_{b}^{r}\;$
${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\\{a^{n}b^{n}\\}_{n}},b\rightarrow[(a^{*}b^{*}),b]$
$\scriptstyle\cdot\text{-}l,\cdot\text{-}r\;$
${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\\{a^{n}b^{n}\\}_{n}b}\rightarrow[(a^{*}b^{*})b]$
$\scriptstyle\mu\text{-}r,+\text{-}r,\mathsf{w}\text{-}r\;$
${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\\{a^{n}b^{n}\\}_{n}b}\rightarrow[(a^{*}b^{*})]$
$\scriptstyle\mathsf{k}_{a}^{l}\;$
$a,{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\\{a^{n}b^{n}\\}_{n}b}\rightarrow[a,(a^{*}b^{*})]$
$\scriptstyle\cdot\text{-}l,\cdot\text{-}r\;$
${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}a\\{a^{n}b^{n}\\}_{n}b}\rightarrow[a(a^{*}b^{*})]$
$\scriptstyle\mathsf{w}\text{-}r,+\text{-}r\;$
${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}a\\{a^{n}b^{n}\\}_{n}b}\rightarrow[1+a(a^{*}b^{*})+(a^{*}b^{*})b]$
$\scriptstyle+\text{-}l\;$
${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}1+a\\{a^{n}b^{n}\\}_{n}b}\rightarrow[1+a(a^{*}b^{*})+(a^{*}b^{*})b]$
$\scriptstyle\mu\text{-}l,\mu\text{-}r\;$ $\;\bullet$
${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\\{a^{n}b^{n}\\}_{n}}\rightarrow[(a^{*}b^{*})]$
Figure 3. A regular $\infty$-proof $R$ of
$\\{a^{n}b^{n}\\}_{n}\rightarrow[(a^{*}b^{*})]$.

######  Example 13.

Recall the guarded expressions $\\{a^{n}b^{n}\\}_{n}$ and $(a^{*}b^{*})$ from
Example 11. We have the regular $\infty$-proof $R$ in Fig. 3 of
$\\{a^{n}b^{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 14 (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
$\Pi^{0}_{1}$-complete (see e.g. [JEH01]). In this sense examples of regular
proofs are somewhat coincidental.

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

######  Lemma 15 (Local soundness).

For each inference step,

(4) $\Gamma_{0}\rightarrow S_{0}$$\cdots$$\Gamma_{k-1}\rightarrow S_{k-1}$
$\scriptstyle\mathsf{r}\;$ $\Gamma\rightarrow S$

for some $k\leq 2$, we have: $\forall
i<k\,\mathcal{L}(\Gamma_{i})\subseteq\mathcal{L}(S_{i})\implies\mathcal{L}(\Gamma)\subseteq\mathcal{L}(S)$.

Consequently finite proofs are also sound, by induction on their structure.
For non-wellfounded proofs, we must employ a less constructive argument,
typical of non-wellfounded proof theory:

######  Theorem 16 (Soundness).

$\mu\mathsf{HKA}\vdash^{\infty}\Gamma\rightarrow
S\implies\mathcal{L}(\Gamma)\subseteq\mathcal{L}(S)$.

###### Proof of Theorem 16.

For each sequent $\mathcal{S}=\Gamma\rightarrow S$, define
$n_{\mathcal{S}}\in\mathbb{N}\cup\\{\infty\\}$ for the least length of word
$w\in\mathcal{L}(\Gamma)\setminus\mathcal{L}(S)$ (if there is no such word
then $n_{\mathcal{S}}=\infty$). Now suppose, for contradiction, that $P$ is a
$\infty$-proof of $\mathcal{S}=\Gamma\rightarrow S$, but
$\mathcal{L}(\Gamma)\setminus\mathcal{L}(S)\neq\varnothing$, and so
$n_{\mathcal{S}}\in\mathbb{N}$. By (the contraposition of) Lemma 15 we may
continually choose invalid premisses of rules to build an infinite branch
$(\mathcal{S}_{i}=\Gamma_{i}\rightarrow S_{i})_{i<\omega}$ s.t.
$\mathcal{L}(\Gamma_{i})\setminus\mathcal{L}(S_{i})\neq\varnothing$ for all
$i<\omega$. Moreover, we can guarantee that the sequence
$(n_{\mathcal{S}_{i}})_{i<\omega}$ is monotone non-increasing. For this note
that for each inference step  $\mathcal{S}_{0}$$\cdots$$\mathcal{S}_{k-1}$
$\scriptstyle\mathsf{r}\;$ $\mathcal{S}$ of form as in (4) we have:

  1. (1)

If $\mathsf{r}$ is a $\mathsf{k}$ step, then
$n_{\mathcal{S}}>n_{\mathcal{S}_{0}}$; and,

  2. (2)

Otherwise there is some $i<k$ with $n_{\mathcal{S}}=n_{\mathcal{S}_{i}}$.

In particular, if $\mathsf{r}$ is a $+\text{-}l$ step, we should choose the
$\mathcal{S}_{i}$ admitting the smallest $n_{\mathcal{S}_{i}}$. Now, since $P$
is a $\infty$-proof, $(\mathcal{S}_{i})_{i<\omega}$ must be progressing and
has infinitely many $\mu\text{-}l$ steps. We have two cases:

  * •

If $(\mathcal{S}_{i})_{i<\omega}$ has infinitely many $\mathsf{k}$ steps then
case 1 happens infinitely often along $(n_{\mathcal{S}_{i}})_{i<\omega}$, and
so it is a monotone non-increasing sequent of natural numbers that does not
converge. Contradiction.

  * •

Otherwise $(\mathcal{S}_{i})_{i\geq k}$ is $\mathsf{k}$-step-free, for some
$k<\omega$, and so the number of letters in the LHS of the sequent is monotone
non-decreasing in $i\geq k$. Since there are infinitely many $\mu\text{-}l$
steps, by guardedness the number of producing expressions (whose languages
necessarily are nonempty and do not contain $\varepsilon$) is strictly
increasing, and eventually dominates even $n_{0}\geq n_{i}$. Contradiction. ∎

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

######  Lemma 17 (Invertibility).

Let $\mathsf{r}$ be a logical step as in (4).
$\mathcal{L}(\Gamma)\subseteq\mathcal{L}(S)\implies\mathcal{L}(\Gamma_{i})\subseteq\mathcal{L}(S_{i})$,
for each $i<k$.

######  Theorem 18 (Completeness).

$\mathcal{L}(\Gamma)\subseteq\mathcal{L}(S)\Rightarrow\mu\mathsf{HKA}\vdash^{\infty}\Gamma\rightarrow
S$.

###### Proof sketch.

We describe a bottom-up proof search strategy:

  1. (1)

Apply left logical rules maximally, preserving validity by Lemma 17. Any
infinite branch is necessarily progressing.

  2. (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$. ∎

To flesh out a bit more the Item 2 of the argument above, let us state:

######  Lemma 19 (Membership).

$a_{1}\cdots
a_{n}\in\mathcal{L}(S)\Rightarrow\mu\mathsf{HKA}\vdash^{\infty}a_{1},\dots,a_{n}\rightarrow
S$.

###### Proof idea.

Recall the ‘canonical’ grammar as constructed in (3). We proceed by induction
on a leftmost (or rightmost) derivation (as defined for Muller CFGs in Section
6) of $\vec{a}$ according to this canonical grammar. ∎

##  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 [GHK13], strengthening it to a
‘cut-free’ calculus $\mu\mathsf{HKA}_{\omega}$.

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

  * •

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

  * •

($\mu$-continuity) $e\mu Xf(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\leq f$ for the natural order given
by $e+f=f$. Now, define $\mu\mathsf{HKA}_{\omega}$ to be the extension of
$\mu\mathsf{HKA}$ by the ‘$\omega$-rule’:

$\\{\Gamma,e^{n}(0),\Gamma^{\prime}\rightarrow S\\}_{n<\omega}$
$\scriptstyle\omega\;$ $\Gamma,\mu Xe(X),\Gamma^{\prime}\rightarrow S$

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

######  Proposition 20.

$\mu\mathsf{HKA}_{\omega}\vdash\Gamma\rightarrow
S\implies\mu\mathsf{CA}\vdash\prod\Gamma\leq\sum\limits_{\Delta\in
S}\prod\Delta$.

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

######  Theorem 21.

$\mu\mathsf{HKA}\vdash^{\infty}e\rightarrow f$ $\implies$
$\mu\mathsf{HKA}_{\omega}\vdash e\leq f$

Note that, immediately from Theorem 18 and Proposition 20, we obtain:

######  Corollary 22.

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

To prove Theorem 21 we employ similar techniques to those used for an
extension of _linear logic_ with least and greatest fixed points [DDS23], only
specialised to the current setting. We only sketch the ideas here, referencing
the analogous definitions and theorems from that work at the appropriate
moments.

###  4.1. Projections

Let us consider cedents $\Gamma=\Gamma(f_{1},\dots,f_{k})$ where some
occurrences of $f_{1},\dots,f_{k}$ are distinguished. Note that the
distinguished occurrences of each $f_{i}$ may include some, none or all of the
occurrences of $f_{i}$ in $\Gamma$, including as subexpressions of of
expressions in $\Gamma$. We allow distinct $f_{i}$ and $f_{j}$ to be the same
formula, as long as they distinguish a disjoint set of occurrences.

When $\vec{f}=(\mu X_{1}g_{1}(X_{1}),\dots,\mu X_{k}g(X_{k}))$ and
$\vec{n}\in\mathbb{N}^{k}$, we write
$\vec{f}^{\vec{n}}:=(g_{1}^{n_{1}}(0),\dots,g_{k}^{n_{k}}(0))$, the list
obtained by assigning $\vec{n}$ to $\vec{f}$.

Let us briefly recap the definition of _projection_ in [DDS23, Definition 15],
specialised to our setting:

######  Definition 23 (Projections).

For each $\mu\mathsf{HKA}$ preproof $P$ of $\Gamma(\vec{f})\rightarrow S$ and
$\vec{n}\in\mathbb{N}^{k}$ we define $P(\vec{n})$ a preproof of
$\Gamma(\vec{f}^{\vec{n}})\rightarrow S$ by coinduction on $P$:

  * •

The definition of $P(\vec{n})$ commutes with any step for which a
distinguished formula is not principal for a $\mu\text{-}l$ step.

  * •

If $P$ ends with a step for which a distinguished formula if $\mu\text{-}l$
principal,

(5) $\textstyle{\scriptstyle Q}$ $\Gamma(\mu Xe(X)),e(\mu
Xe(X)),\Gamma^{\prime}(\mu Xe(X))\rightarrow S$ $\scriptstyle\mu\text{-}l\;$
$\Gamma(\mu Xe(X)),\mu Xe(X),\Gamma^{\prime}(\mu Xe(X))\rightarrow S$

then we proceed by case analysis on the number assigned:

$P(0,\vec{n}):={\vbox{\hbox{\kern
10.83743pt\hbox{\vbox{\offinterlineskip\hbox{\kern
35.37411pt\hbox{\hbox{\hbox{$$}}}\kern 35.37411pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle
0\text{-}l\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to70.74825pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma(0),0,\Gamma^{\prime}(0)\rightarrow S$}\kern
0.0pt$}}}}}\kern 0.0pt}}}$ $P(n+1,\vec{n}):={{{}{}{}}\vbox{\hbox{\kern
13.77759pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern 22.43971pt\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\qquad\quad$}}\kern
10.00002pt}\hbox{\hbox{$\qquad$}}\kern
10.00002pt}\hbox{\hbox{$\qquad\quad$}}}}}\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$$}}\vbox{\hbox{$\vbox{\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern 50.00008pt\hbox{\ignorespaces\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{{}{}{{}{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>12.2847pt\hbox{\hbox{\kern 0.0pt\raise-2.69722pt\hbox{$\textstyle{\scriptstyle
Q(n,n+1,\vec{n})}$}}}}}}}}}}$}}\hbox to0.0pt{\hbox{$$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 50.00008pt\hbox{\hbox{$$}}\kern 50.00008pt}}}\kern
0.0pt}}\kern 22.43971pt}\kern 0.0pt\kern 0.0pt\hbox{\hbox
to0.0pt{\hss\hbox{$$}}\vbox{}\hbox
to0.0pt{\hbox{$$}\hss}}\hbox{\hbox{\hbox{$\Gamma(e^{n+1}(0)),e(e^{n}(0)),\Gamma^{\prime}(e^{n+1}(0))\rightarrow
S$}}}}}\kern 0.0pt}}}\kern 1.43518pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle=\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to144.87958pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 2.63925pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma(e^{n+1}(0)),e^{n+1}(0),\Gamma^{\prime}(e^{n+1}(0))\rightarrow
S$}\kern 0.0pt$}}\kern 2.63925pt}}}\kern 0.0pt}}}$

where in the second case we have further distinguished the occurrences of $\mu
Xe(X)$ indicated in the auxiliary formula in (5).

Note that we have technically used a ‘repetition’ rule $=$ in the translation
above to ensure productivity of the translation. However it turns out this is
unnecessary, as $\infty$-proofs are indeed closed under taking projections:

######  Proposition 24.

If $P$ is a $\mu\mathsf{HKA}$ $\infty$-proof, then so is $P(\vec{n})$.

The proof of this result follows the same argument as [DDS23, Proposition 18].
To briefly recall the idea:

###### Proof sketch.

Each maximal branch $B$ of $P(\vec{n})$ is a prefix of some branch
$B^{\prime}$ of $P$, by inspection of the translation, only with some
$\mu\text{-}l$ steps replaced by ‘$=$’ steps or, when $B$ is finite, a
$0\text{-}l$ step. Thus if $B$ is infinite then it must have infinitely many
$\mathsf{k}$ steps, since $B^{\prime}$ must be progressing, and so must have
infinitely many $\mu\text{-}l$ steps too. ∎

In particular we have:

######  Corollary 25 (Projection).

For each $\infty$-proof $P$ of $\Gamma,\mu Xe(X),\Gamma^{\prime}\rightarrow
S$, $P(n)$ is an $\infty$-proof of $\Gamma,e^{n}(0),\Gamma^{\prime}\rightarrow
S$, for each $n<\omega$.

From here it is simple to provide a translation from $\mu\mathsf{HKA}$
$\infty$-proofs to $\mu\mathsf{HKA}_{\omega}$ preproofs, as in Definition 30
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 Sections 5 and 6.

###  4.2. Intermezzo: ancestry and threads

Given an inference step $\mathsf{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
$\Gamma,\Gamma^{\prime},\Delta,\Delta^{\prime}$, 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 26 ((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 27.

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

###### Proof sketch.

The $\impliedby$ direction is trivial. For $\implies$ direction we appeal to
König’s lemma. Fix a branch $B$ and take the subtree of its immediate ancestry
graph with nodes the principal formula occurrences along $B$, and edges given
by reachability (‘direct ancestry’). By progressiveness this tree is infinite,
and by inspection of the rules it is finitely branching, thus it must have an
infinite path by König’s Lemma. This path induces an infintely often principal
thread along $B$, which in turn must be infinitely often $\mu\text{-}l$
principal as every other LHS rule strictly decreases the size of formula. ∎

######  Example 28.

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

######  Fact 29 (See, e.g., [Koz83, KMV22]).

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.3. Translation to $\omega$-branching system

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

######  Definition 30 ($\omega$-translation).

For preproofs $P$ define $P^{\omega}$ by coinduction:

  * •

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

  * •

$\left({{{}{}{}}\vbox{\hbox{\kern
11.55527pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern 22.66809pt\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\quad$}}\kern
10.00002pt}\hbox{\hbox{$$}}\kern
10.00002pt}\hbox{\hbox{$\quad$}}}}}\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$$}}\vbox{\hbox{$\vbox{\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern 20.00003pt\hbox{\ignorespaces\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{{}{}{{}{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>10.91982pt\hbox{\hbox{\kern
0.0pt\raise-2.39166pt\hbox{$\textstyle{\scriptstyle P}$}}}}}}}}}}$}}\hbox
to0.0pt{\hbox{$$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
20.00003pt\hbox{\hbox{$$}}\kern 20.00003pt}}}\kern 0.0pt}}\kern
22.66809pt}\kern 0.0pt\kern 0.0pt\hbox{\hbox
to0.0pt{\hss\hbox{$$}}\vbox{}\hbox
to0.0pt{\hbox{$$}\hss}}\hbox{\hbox{\hbox{$\Gamma,e(\mu
Xe(X)),\Gamma^{\prime}\rightarrow S$}}}}}\kern 0.0pt}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mu\text{-}l\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to85.33624pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
6.21703pt\hbox{\hbox{$\kern 0.0pt\hbox{$\Gamma,\mu
Xe(X),\Gamma^{\prime}\rightarrow S$}\kern 0.0pt$}}\kern 6.21703pt}}}\kern
0.0pt}}}\right)^{\omega}\ :=\ {\vbox{\hbox{\kern
7.13489pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\left\\{{{{}{}{}}\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern 6.04955pt\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\quad$}}\kern
10.00002pt}\hbox{\hbox{$\ $}}\kern
10.00002pt}\hbox{\hbox{$\quad$}}}}}\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$$}}\vbox{\hbox{$\vbox{\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern 22.50003pt\hbox{\ignorespaces\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{{}{}{{}{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>12.28479pt\hbox{\hbox{\kern
0.0pt\raise-2.18056pt\hbox{$\textstyle{\scriptstyle
P(n)^{\omega}}$}}}}}}}}}}$}}\hbox to0.0pt{\hbox{$$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 22.50003pt\hbox{\hbox{$$}}\kern 22.50003pt}}}\kern
0.0pt}}\kern 6.04955pt}\kern 0.0pt\kern 0.0pt\hbox{\hbox
to0.0pt{\hss\hbox{$$}}\vbox{}\hbox
to0.0pt{\hbox{$$}\hss}}\hbox{\hbox{\hbox{$\Gamma,e^{n}(0),\Gamma^{\prime}\rightarrow
S$}}}}}\kern 0.0pt}}}\right\\}_{n<\omega}$}}}}\kern 1.43518pt\hbox{\kern
0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\omega\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to78.30182pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
2.69981pt\hbox{\hbox{$\kern 0.0pt\hbox{$\Gamma,\mu
Xe(X),\Gamma^{\prime}\rightarrow S$}\kern 0.0pt$}}\kern 2.69981pt}}}\kern
0.0pt}}}$

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

######  Lemma 31.

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

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

###### Proof sketch.

Each branch of $P^{\omega}$ can be specified by a branch $B$ of $P$ and a
(possibly infinite) sequence of natural numbers
$\vec{n}\in\omega^{\leq\omega}$, specifying at each $\omega$-step which
premiss to follow. Call this $B^{\vec{n}}$. Now, take a progressing thread
along $B$ and consider its smallest i.o.p. $\mu$-formula, say $\mu Xe(X)$. If
$B^{\vec{n}}$ follows, say the $k$th premiss at the first corresponding
principal step for $\mu Xe(X)$ in $B$, write $K$ for height of the $(k+1)$th
unfolding of $\mu Xe(X)$ in $B$. It follows from inspection of the
$\omega$-translation and projections that $B^{\vec{n}}$ has height $\leq K$. ∎

######  Example 32.

Recalling Example 13, let us see the $\omega$-translation of $R$ in (3).
First, let us (suggestively) write $\\{a^{k}b^{k}\\}_{k<n}$ for the $n$th
approximant of $\\{a^{n}b^{n}\\}_{n}$, i.e. $\\{a^{k}b^{k}\\}_{k<0}:=0$ and
$\\{a^{k}b^{k}\\}_{k<n+1}:=1+a\\{a^{k}b^{k}\\}_{k<n}b$. Now $R^{\omega}$ is
given below, left, where recursively $R(0):={\vbox{\hbox{\kern
10.83743pt\hbox{\vbox{\offinterlineskip\hbox{\kern
19.2554pt\hbox{\hbox{\hbox{$$}}}\kern 19.2554pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle
0\text{-}l\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to38.5108pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$0\rightarrow(a^{*}b^{*})$}\kern 0.0pt$}}}}}\kern 0.0pt}}}$ and
$R(n+1)$ is given below, right:

${\vbox{\hbox{\kern
20.64967pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\left\\{{{{}{}{}}\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern 16.42902pt\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\quad$}}\kern
10.00002pt}\hbox{\hbox{$$}}\kern
10.00002pt}\hbox{\hbox{$\quad$}}}}}\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$$}}\vbox{\hbox{$\vbox{\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern 20.00003pt\hbox{\ignorespaces\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{{}{}{{}{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>10.91982pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\textstyle{\scriptstyle
R(n)}$}}}}}}}}}}$}}\hbox to0.0pt{\hbox{$$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 20.00003pt\hbox{\hbox{$$}}\kern 20.00003pt}}}\kern
0.0pt}}\kern 16.42902pt}\kern 0.0pt\kern 0.0pt\hbox{\hbox
to0.0pt{\hss\hbox{$$}}\vbox{}\hbox
to0.0pt{\hbox{$$}\hss}}\hbox{\hbox{\hbox{${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\\{a^{k}b^{k}\\}_{k<n}}\rightarrow[(a^{*}b^{*})]$}}}}}\kern
0.0pt}}}\right\\}_{n<\omega}$}}}}\kern 1.43518pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\omega,\mu\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to94.06075pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 14.05528pt\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\\{a^{n}b^{n}\\}_{n}}\rightarrow[(a^{*}b^{*})]$}\kern
0.0pt$}}\kern 14.05528pt}}}\kern 0.0pt}}}\quad;\
{{}{{{}{}{}}}\vbox{\hbox{\kern
0.34734pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
15.91222pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
13.27773pt\hbox{\vbox{\offinterlineskip\hbox{\kern
7.49995pt\hbox{\hbox{\hbox{$$}}}\kern 7.49995pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{init}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to14.99992pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\rightarrow[\,]$}\kern 0.0pt$}}}}}\kern 0.0pt}}\kern
5.55556pt}\kern 1.43518pt\hbox{\kern 7.72217pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle
1\text{-}l,1\text{-}r\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to26.11104pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\kern 7.72217pt\hbox{\hbox{$\kern
0.0pt\hbox{$1\rightarrow[1]$}\kern 0.0pt$}}}}}\kern 0.0pt}}\kern
8.97766pt}\kern 1.43518pt\kern-0.7pt\hbox{\kern 14.65672pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}}\vbox{\vbox
to1.8pt{\vfill\hbox to44.06638pt{\hrulefill}\kern 1.0pt\hbox
to44.06638pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}\hss}}\kern
1.43518pt\kern-0.7pt\hbox{\kern 14.65672pt\hbox{\hbox{$\kern
0.0pt\hbox{$1\rightarrow[(a^{*}b^{*})]$}\kern 0.0pt$}}}}}\kern 0.0pt}\kern
10.00002pt}\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
10.41891pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
12.88998pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
8.18883pt\hbox{\vbox{\offinterlineskip\hbox{\kern 12.90271pt\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern 13.65123pt\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\quad$}}\kern
10.00002pt}\hbox{\hbox{$$}}\kern
10.00002pt}\hbox{\hbox{$\quad$}}}}}\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$$}}\vbox{\hbox{$\vbox{\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern 20.00003pt\hbox{\ignorespaces\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{{}{}{{}{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>10.91982pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\textstyle{\scriptstyle
R(n)}$}}}}}}}}}}$}}\hbox to0.0pt{\hbox{$$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 20.00003pt\hbox{\hbox{$$}}\kern 20.00003pt}}}\kern
0.0pt}}\kern 13.65123pt}\kern 0.0pt\kern 0.0pt\hbox{\hbox
to0.0pt{\hss\hbox{$$}}\vbox{}\hbox
to0.0pt{\hbox{$$}\hss}}\hbox{\hbox{\hbox{${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\\{a^{k}b^{k}\\}_{k<n}}\rightarrow(a^{*}b^{*})$}}}}}\kern
0.0pt}}\kern 12.90271pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{k}_{b}^{r}\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to93.10794pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\\{a^{k}b^{k}\\}_{k<n}},b\rightarrow[(a^{*}b^{*}),b]$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\kern 1.43518pt\hbox{\kern 8.18883pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\cdot\text{-}l,\cdot\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to93.10794pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 14.0221pt\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\\{a^{k}b^{k}\\}_{k<n}b}\rightarrow[(a^{*}b^{*})b]$}\kern
0.0pt$}}\kern 5.83327pt}}}\kern 0.0pt}}}\kern 1.43518pt\hbox{\kern
26.91208pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mu\text{-}r,+\text{-}r,\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to81.4414pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}\kern 5.83327pt}\kern
1.43518pt\hbox{\kern 29.0579pt\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\\{a^{k}b^{k}\\}_{k<n}b}\rightarrow[(a^{*}b^{*})]$}\kern
0.0pt$}}\kern 7.9791pt}}}\kern 0.0pt}}\kern 0.9179pt}\kern
1.43518pt\hbox{\kern 30.57983pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{k}_{a}^{l}\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to94.94373pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\kern
30.57983pt\hbox{\hbox{$\kern
0.0pt\hbox{$a,{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\\{a^{k}b^{k}\\}_{k<n}b}\rightarrow[a,(a^{*}b^{*})]$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\kern 1.43518pt\hbox{\kern 30.57983pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\cdot\text{-}l,\cdot\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to94.94373pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 34.19093pt\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}a\\{a^{k}b^{k}\\}_{k<n}b}\rightarrow[a(a^{*}b^{*})]$}\kern
0.0pt$}}\kern 3.6111pt}}}\kern 0.0pt}}}\kern 1.43518pt\kern-0.7pt\hbox{\kern
34.19093pt\hbox to0.0pt{\hss\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}}\vbox{\vbox
to1.8pt{\vfill\hbox to87.72153pt{\hrulefill}\kern 1.0pt\hbox
to87.72153pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}\hss}\kern 3.6111pt}\kern
1.43518pt\kern-0.7pt\hbox{\kern 36.83388pt\hbox{\hbox{$\kern
0.0pt\hbox{${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}a\\{a^{k}b^{k}\\}_{k<n}b}\rightarrow[(a^{*}b^{*})]$}\kern
0.0pt$}}\kern 6.25404pt}}}\kern 0.0pt}}}}\kern 1.43518pt\hbox{\kern
14.65672pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle+\text{-}l\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to173.3359pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 6.25404pt}\kern 1.43518pt\hbox{\kern
51.49577pt\hbox{\hbox{${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}1+a\\{a^{k}b^{k}\\}_{k<n}b}\rightarrow[(a^{*}b^{*})]$}}\kern
43.0931pt}}}\kern 0.0pt}}}$

##  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 Xe(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 Xp$.

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

######  Definition 33 (Intended semantics of $\mu\nu$-expressions).

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

Again, since all the operations are monotone, $\mathcal{L}(\nu Xe(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. [CG77, Lin76], defined as the ‘Kleene closure’ of CFLs:

######  Definition 34 ($\omega$-context-free languages).

For $A\subseteq\mathcal{A}^{+}$ we write
$A^{\omega}:=\\{w_{0}w_{1}w_{2}\cdots:\forall i<\omega\,w_{i}\in A\\}$. The
class of $\omega$-CFLs ($\mathsf{CF}^{\omega}$) is defined by:

$\mathsf{CF}^{\omega}\ :=\ \left\\{\bigcup_{i<n}A_{i}B_{i}^{\omega}\ :\
n<\omega;\,A_{i},B_{i}\text{ context-free and }\varepsilon\notin
A_{i},B_{i},\,\forall i<n\right\\}$

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 35.

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

###### Proof.

Given $L=\bigcup_{i=1}^{n}A_{i}B_{i}^{\omega}$, by Proposition 10 let $e_{i}$
and $f_{i}$ be left-productive with $\mathcal{L}(e_{i})=A_{i}$,
$\mathcal{L}(f_{i})=B_{i}$ for $i=1,\dots,n$. Then,
$L=\mathcal{L}(\sum_{i=1}^{n}e_{i}\nu X(f_{i}X))$. ∎

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

######  Definition 36 (System).

The system $\mu\nu\mathsf{HKA}$ extends $\mu\mathsf{HKA}$ by the rules:

(6)
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}e(\nu
Xe(X))},{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color@cmyk@fill{0}{0}{1}{.5}\Gamma^{\prime}}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$
$\scriptstyle\nu\text{-}l\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\nu
Xe(X)},{\color[rgb]{0.5,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{.5}\pgfsys@color@cmyk@fill{0}{0}{1}{.5}\Gamma^{\prime}}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S}$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S},[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Delta},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}e(\nu
Xe(X)},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\Delta^{\prime}}]$
$\scriptstyle\nu\text{-}r\;$
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\Gamma}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}S},[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\Delta},{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\nu
Xe(X)},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\Delta^{\prime}}]$

_Preproofs_ for this system are defined just as for $\mu\mathsf{HKA}$ before.
The definitions of _immediate ancestor_ and _thread_ for $\mu\nu\mathsf{HKA}$
extends that of $\mu\mathsf{HKA}$ from Definition 26 according to the
colouring above in (6).

However we must be more nuanced in defining progress, requiring a definition
at the level of threads as in Section 4. Noting that Fact 29 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 37 (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\mathsf{HKA}$ if each of
its infinite branches has a progressing thread.

$\vdots$ $\scriptstyle\nu\text{-}r\;$ $\;\bullet$
$e\rightarrow[{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\nu
X(afX)}]$ $\scriptstyle\mathsf{k}_{b}\;$
$b,e\rightarrow[b,{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\nu
X(afX)}]$ $\scriptstyle\mathsf{w}\text{-}r\;$
$b,e\rightarrow[b,{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\nu
X(afX)}],[\nu X(aYX),\nu X(afX)]$ $\scriptstyle+\text{-}r\;$
$b,e\rightarrow[b+\nu
X(aYX),{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\nu
X(afX)}]$ $\scriptstyle\mu\text{-}r\;$
$b,e\rightarrow[f,{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\nu
X(afX)}]$ $\scriptstyle\mathsf{k}_{a}\;$
$a,b,e\rightarrow[a,f,{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\nu
X(afX)}]$ $\scriptstyle\cdot\text{-}l,\cdot\text{-}r\;$
$abe\rightarrow[{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}af\nu
X(afX)}]$ $\scriptstyle\nu\text{-}r\;$ $\;\bullet$
$e\rightarrow[\underline{{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\nu
X(afX)}}]$ $\scriptstyle\mathsf{w}\text{-}r\;$
$e\rightarrow[b],[{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\nu
X(afX)}]$ $\scriptstyle+\text{-}r\;$
$e\rightarrow[{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}b+\nu
X(afX)}]$ $\scriptstyle\mu\text{-}r\;$
$e\rightarrow[{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}f}]$
Figure 4. A $\mu\nu\ell\mathsf{HKA}$ $\infty$-preproof of $e\rightarrow[f]$,
where $e:=\nu Z(abZ)$ and $f:=\mu Y(b+\nu X(aYX))$.

######  Example 38.

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 magenta 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\mathsf{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
magenta 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).

### 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\mathsf{HKA}$ in order to maintain soundness for $\mathcal{L}(\cdot)$:

######  Definition 39.

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

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

######  Convention 40.

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

Let us justify both of these restrictions via some examples.

######  Remark 41 (Unsound for non-leftmost).

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

$\vdots$ $\scriptstyle\nu\text{-}r\;$ $\;a,\bullet$
$\rightarrow[a,{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\nu
X(aX)}]$ $\scriptstyle\cdot\text{-}r\;$
$\rightarrow[{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}a\nu
X(aX)}]$ $\scriptstyle\nu\text{-}r\;$ $\;\bullet$
$\rightarrow[{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}\nu
X(aX)}]$

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 magenta, it is not
leftmost due to the topmost displayed $\nu\text{-}r$ step.

######  Remark 42 (Incomplete for unguarded).

On the other hand, without the left-guardedness restriction,
$\mu\nu\ell\mathsf{HKA}^{\infty}$ is not complete. For instance the sequent
$\nu XX\rightarrow[\;],\\{[a,\nu XX]\\}_{a\in\mathcal{A}}$ is indeed valid as
both sides compute all of $\mathcal{P}(\mathcal{A}^{\leq\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\mathsf{HKA}^{\infty}$,
employing game-theoretic methods.

###  6.1. Evaluation puzzle and soundness

Position | Available move(s)
---|---
$(aw,[a,\Delta])$ | $(w,\Delta)$
$(w,[1,\Delta])$ | $(w,\Delta)$
$(w,[e+f,\Delta])$ | $(w,[e,\Delta]),(w,[f,\Delta])$
$(w,[ef,\Delta])$ | $(w,[e,f,\Delta])$
$(w,[\mu Xf(X),\Delta])$ | $(w,[f(\mu Xf(X)),\Delta])$
$(w,[\nu Xf(X),\Delta])$ | $(w,[f(\nu Xf(X)),\Delta])$
Figure 5. Rules of the evaluation puzzle.

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

######  Definition 43.

The evaluation puzzle is a puzzle (i.e. one-player game) whose positions are
pairs $(w,\Gamma)$ where $w\in\mathcal{A}^{\leq\omega}$ and $\Gamma$ 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\mathsf{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 44.

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

${\scriptstyle(\langle^{\omega},[d^{\omega}])}$${\scriptstyle(\langle^{\omega},[dd^{\omega}])}$${\scriptstyle(\langle^{\omega},[d,d^{\omega}])}$${\scriptstyle(\langle^{\omega},[\langle\rangle+\langle
d\rangle d,d^{\omega}])}$${\scriptstyle(\langle^{\omega},[\langle d\rangle
d,d^{\omega}])}$${\dots}$${\scriptstyle(\langle^{\omega},[d,\rangle
d,d^{\omega}])}$${\scriptstyle(\langle^{\omega},[d\rangle
d,d^{\omega}])}$${\scriptstyle(\langle^{\omega},[\langle,d\rangle
d,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, consider the
following play from $(u,[d^{\omega}])$ where $u=(\langle\rangle)^{\omega}$. It
is, indeed winning and its $\nu$-thread is indicated in magenta.

${\scriptstyle(u,[{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}d^{\omega}}])}$${\scriptstyle(u,[d,{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}d^{\omega}}])}$${\scriptstyle(u,[\langle\rangle+\langle
d\rangle
d,{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}d^{\omega}}])}$${\scriptstyle(u,[\langle\rangle,{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}d^{\omega}}])}$${\scriptstyle(u,[\langle,\rangle,{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}d^{\omega}}])}$${\scriptstyle(\rangle
u,[\rangle,{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}d^{\omega}}])}$2

######  Theorem 45 (Evaluation).

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

The proof is rather involved, employing the method of ‘signatures’ common in
fixed point logics, cf. e.g. [NW96], 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 [MHHO05, CKS81].

The next subsection is devoted to a proof of the Evaluation Theorem above.
Before that, let us give an important consquence:

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

######  Theorem 46 (Soundness).

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

###### Proof sketch.

Let $P$ be a $\infty$-proof of $\Gamma\rightarrow S$ and
$w\in\mathcal{L}(\Gamma)$. We show $w\in\mathcal{L}(S)$. First, since
$w\in\mathcal{L}(\Gamma)$ there is a winning play $\pi$ from $(w,\Gamma)$ by
Theorem 45, 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 $[\Gamma_{i}]_{i<\omega}$. By
construction $[\Gamma_{i}]_{i<\omega}$ has an infinite subsequence, namely
whenever it is principal, that forms (the right components of) a winning play
from $(w,\Gamma_{0})$, with $\Gamma_{0}\in S$. Thus indeed
$w\in\mathcal{L}(S)$ by Theorem 45. ∎

###  6.2. Proof of the Evaluation Theorem

Let us now revisit the argument for Theorem 45 more formally. This subsection
may be safely skipped by the reader comfortable with that result.

Write $\sqsubseteq$ for the subformula relation. Recalling Definition 8, let
us write $e\leq_{\mathrm{FL}}f$ if $e\in\mathrm{FL}(f)$, $e<_{\mathrm{FL}}f$
if $e\leq_{\mathrm{FL}}f\not\leq_{\mathrm{FL}}e$ and $e=_{\mathrm{FL}}f$ if
$e\leq_{\mathrm{FL}}f\leq_{\mathrm{FL}}e$.

######  Definition 47 (Dependency order).

Let the dependency order be
$\preceq\,:=\,\leq_{\mathrm{FL}}\times\sqsupseteq$, i.e. $e\preceq f$ if
either $e<_{\mathrm{FL}}f$ or $e=_{\mathrm{FL}}f$ and $f\sqsubseteq e$.

Note that, by the properties of FL closure, $\preceq$ is a well partial order
on expressions. In the sequel, we assume an arbitrary extension of $\preceq$
to a total well-order $\leq$.

######  Definition 48 (Signatures).

Let $M$ and $N$ be finite sets of $\mu$-expressions $\\{\mu
X_{0}e_{0}\succ\cdots\succ\mu X_{n-1}e_{n-1}\\}$ and $\\{\nu
X_{0}e_{0}\succ\cdots\succ\nu X_{n-1}e_{n-1}\\}$ respectively. A
$\mu$-signature (respectively, a $\mu$-signature) is a sequence
$\vec{\alpha}=(\alpha_{i})_{i=0}^{n-1}$ of ordinals indexed by $M$
(respecively, $N$). Signatures are ordered by the lexicographical product
order.

Let us temporarily expand the language of expressions by,

$e,f,\dots\quad::=\quad\dots\quad\mid\quad\mu^{\alpha}Xe\quad\mid\quad\nu^{\alpha}Xe$

where $\alpha$ ranges over ordinals.

######  Definition 49.

Fix a finite set of $\mu$-formulas $\\{\mu X_{0}e_{0}\succ\cdots\succ\mu
X_{n-1}e_{n-1}\\}$ and a $\mu$-signature
$\vec{\alpha}=(\alpha_{i})_{i=0}^{n-1}$. Given an expression $e$, its
corresponding $\mu$-signed formula $e^{\vec{\alpha}}$ is one where every
occurrence $\mu X_{i}e_{i}$ has been replaced by $\mu^{\alpha_{i}}X_{i}e_{i}$.

Similarly, given a finite set of $\nu$-formulas, a $\nu$-signature
$\vec{\alpha}$, and an expression $e$, its corresponding $\nu$-signed formula
$e_{\vec{\alpha}}$ is one where every occurrence of a $\nu$-subformula has
been replaced by its corresponding approximant.

We interpret such expressions by the inflationary and deflationary
constructions respectively:

  * •

$\mathcal{L}(\mu^{0}Xe(X)):=\varnothing$

  * •

$\mathcal{L}(\mu^{\alpha+1}Xe(X)):=\mathcal{L}(e(\mu^{\alpha}Xe(X)))$

  * •

$\mathcal{L}(\mu^{\lambda}Xe(X)):=\bigcup\limits_{\alpha<\lambda}\mathcal{L}(\mu^{\alpha}Xe(X))$,
when $\lambda$ is a limit ordinal.

  * •

$\mathcal{L}(\nu_{0}Xe(X)):=\mathcal{A}^{\leq\omega}$

  * •

$\mathcal{L}(\nu_{\alpha+1}Xe(X)):=\mathcal{L}(e(\nu^{\alpha}Xe(X)))$

  * •

$\mathcal{L}(\nu_{\lambda}Xe(X)):=\bigcap\limits_{\alpha<\lambda}\mathcal{L}(\nu^{\alpha}Xe(X))$,
when $\lambda$ is a limit ordinal.

Finally, we extend the notion of $\mu$ and $\nu$ signatures to lists of
expressions by writing $\Gamma^{\overline{\vec{\alpha}}}$ and
$\Gamma_{\overline{\vec{\alpha}}}$ (parameterised by _lists_ of vectors of
ordinals now, by abuse of notation) for the corresponding $\mu$ and
$\nu$-signed lists of $\Gamma$. Spelt out,
$[e_{1},\dots,e_{n}]^{\vec{\alpha}_{1}::\dots::\vec{\alpha}_{n}}$ is a
shorthand for $[e_{1}^{\vec{\alpha}_{1}},\dots,e_{n}^{\vec{\alpha}_{n}}]$
(similarly for $\nu$-signed). Lists of vectors are lexicographically ordered.

Recall that least and greatest fixed points can be computed as limits of
approximants. In particular, we have,

  * •

$\mathcal{L}(\mu
Xe)=\bigcup\limits_{\alpha\in\mathsf{Ord}}\mathcal{L}(\mu^{\alpha}Xe)$

  * •

$\mathcal{L}(\nu
Xe)=\bigcap\limits_{\alpha\in\mathsf{Ord}}\mathcal{L}(\nu^{\alpha}Xe)$

where $\alpha$ ranges over ordinals. Thus we have immediately:

######  Proposition 50.

Suppose $\Gamma$ is a list of expressions. We have:

  * •

If $w\in\mathcal{L}(\Gamma)$ then there is a $\mu$-signature
$\overline{\vec{\alpha}}$ such that
$w\in\mathcal{L}(\Gamma^{\overline{\vec{\alpha}}})$.

  * •

If $w\notin\mathcal{L}(\Gamma)$ then there is a $\nu$-signature
$\overline{\vec{\alpha}}$ such that
$w\notin\mathcal{L}(\Gamma_{\overline{\vec{\alpha}}})$.

We are now ready to prove our characterisation of evaluation:

###### Proof of Theorem 45.

$(\implies)$ Suppose $w\in\mathcal{L}(\Gamma)$. By Proposition 50, there is a
least $\mu$-signature $\overline{\vec{\alpha}}$ such that
$w\in\mathcal{L}(\Gamma^{\overline{\vec{\alpha}}})$. We will construct a
winning play $(w_{i},\Gamma_{i})_{i\in\lambda}$ and sequence of signatures
$(\overline{\vec{\alpha^{i}}})_{i\in\lambda}$ from $(w,\Gamma)$ such that:

  * •

$(w_{0},\Gamma_{0},\vec{\alpha_{0}})=(w,\Gamma,\overline{\vec{\alpha}})$;

  * •

for all $i\in\lambda$, $\overline{\vec{\alpha^{i}}}$ is a $\mu$-signature such
that $w_{i}\in\mathcal{L}(\Gamma^{\overline{\vec{\alpha^{i}}}})$;

where $\lambda\in\omega+1$. If the play is finite then it is winning by
construction, so assume it is infinite i.e. $\lambda=\omega$.

We will construct it by induction on $i$. The base case is already defined.
For the induction case, assume $\Gamma_{i}=f,\Delta$ and
$\overline{\vec{\alpha}}_{i}=\vec{\alpha}::\overline{\vec{\alpha}}$ and we
will do a case -analysis on $f$.

  * •

Suppose $f=f_{0}+f_{1}$.

$\displaystyle
w_{i}\in\mathcal{L}([f_{0}+f_{1},\Delta]^{\vec{\alpha}::\overline{\vec{\alpha}}})$
$\displaystyle[\text{By induction hypothesis}]$ $\displaystyle\implies
w_{i}\in\mathcal{L}([f_{0}+f_{1}^{\vec{\alpha}},\Delta^{\overline{\vec{\alpha}}}])$
$\displaystyle\implies
w_{i}\in\mathcal{L}([f_{0}^{\vec{\alpha}},\Delta^{\overline{\vec{\alpha}}}])\text{
or
}w_{i}\in\mathcal{L}([f_{1}^{\vec{\alpha}},\Delta^{\overline{\vec{\alpha}}}])$
$\displaystyle\implies
w_{i}\in\mathcal{L}([f_{0},\Delta]^{\overline{\vec{\alpha^{i}}}})\text{ or
}w_{i}\in\mathcal{L}([f_{1},\Delta]^{\overline{\vec{\alpha^{i}}}})$

Wlog, assume
$w_{i}\in\mathcal{L}([f_{0},\Delta]^{\overline{\vec{\alpha^{i}}}})$. Choose
$(w_{i+1},\Gamma_{i+1},\overline{\vec{\alpha^{i+1}}})=(w_{i},[f_{0},\Delta],\overline{\vec{\alpha_{i}}})$.

  * •

Suppose $f=f_{0}\cdot f_{1}$.

$\displaystyle w_{i}\in\mathcal{L}([f_{0}\cdot
f_{1},\Delta]^{\vec{\alpha}::\overline{\vec{\alpha}}})$
$\displaystyle[\text{By induction hypothesis}]$ $\displaystyle\implies
w_{i}\in\mathcal{L}([f_{0}^{\vec{\alpha}},f_{1}^{\vec{\alpha}},\Delta^{\overline{\vec{\alpha}}}])$
$\displaystyle\implies
w_{i}\in\mathcal{L}([f_{0},f_{1},\Delta]^{\vec{\alpha}::\vec{\alpha}::\overline{\vec{\alpha}}})$

Choose
$(w_{i+1},\Gamma_{i+1},\overline{\vec{\alpha^{i+1}}})=(w_{i},[f_{0},f_{1},\Delta],\vec{\alpha}::\vec{\alpha}::\overline{\vec{\alpha}})$.

  * •

Suppose $f=a$ for some $a\in\mathcal{A}$.

$\displaystyle
w_{i}\in\mathcal{L}([a,\Delta]^{\vec{\alpha}::\overline{\vec{\alpha}}})$
$\displaystyle[\text{By induction hypothesis}]$ $\displaystyle\implies
w_{i}\in\mathcal{L}([a^{\vec{\alpha}},\Delta^{\overline{\vec{\alpha}}}])$
$\displaystyle\implies w_{i}=aw^{\prime}\text{ and
}w^{\prime}\in\mathcal{L}(\Delta^{\overline{\vec{\alpha}}})$

Choose
$(w_{i+1},\Gamma_{i+1},\overline{\vec{\alpha^{i+1}}})=(w^{\prime},\Delta,\overline{\vec{\alpha}})$.

  * •

Suppose $f=\nu Xf_{0}$.

$\displaystyle w_{i}\in\mathcal{L}([\nu
Xf_{0},\Delta]^{\vec{\alpha}::\overline{\vec{\alpha}}})$
$\displaystyle[\text{By induction hypothesis}]$ $\displaystyle\implies
w_{i}\in\mathcal{L}([\nu
Xf_{0}^{\vec{\alpha}},\Delta^{\overline{\vec{\alpha}}}])$
$\displaystyle\implies w_{i}\in\mathcal{L}([f_{0}(\nu
Xf_{0})^{\vec{\alpha}},\Delta^{\overline{\vec{\alpha}}}])$
$\displaystyle[\mathcal{L}(\nu Xe,\Gamma)=\mathcal{L}(e(\nu Xe),\Gamma)]$
$\displaystyle\implies w_{i}\in\mathcal{L}([f_{0}(\nu
Xf_{0}),\Delta]^{\vec{\alpha}::\overline{\vec{\alpha}}})$

Choose $(w_{i+1},\Gamma_{i+1},\overline{\vec{\alpha^{i+1}}})=(w_{i},[f_{0}(\nu
Xf_{0}),\Delta],\overline{\vec{\alpha^{i}}})$

  * •

Suppose $f=\mu Xf_{0}$.

$\displaystyle w_{i}\in\mathcal{L}([\mu
Xf_{0},\Delta]^{\vec{\alpha}::\overline{\vec{\alpha}}})$
$\displaystyle[\text{By induction hypothesis}]$ $\displaystyle\implies
w_{i}\in\mathcal{L}([\mu^{\alpha_{j}}Xf_{0},\Delta^{\overline{\vec{\alpha}}}])$
$\displaystyle[\text{where }\vec{\alpha}=(\alpha_{i})]$ $\displaystyle\implies
w_{i}\in\mathcal{L}([f_{0}(\mu^{\beta}Xf_{0}),\Delta^{\overline{\vec{\alpha}}}])$
$\displaystyle[\text{for some }\beta<\alpha_{j}]$ $\displaystyle\implies
w_{i}\in\mathcal{L}([f_{0}(\mu
Xf_{0}),\Delta]^{\vec{\alpha}^{\prime}::\overline{\vec{\alpha}}})$
$\displaystyle[\vec{\alpha}^{\prime}=\vec{\alpha}[\beta/\alpha_{j}]]$

Choose $(w_{i+1},\Gamma_{i+1},\overline{\vec{\alpha^{i+1}}})=(w_{i},[f_{0}(\nu
Xf_{0}),\Delta],\vec{\alpha}^{\prime}::\overline{\vec{\alpha}})$ works.

We now claim that this play is winning. Suppose not. Then, the smallest
formula principal infinitely often is $\mu$. We follow its thread and obtain a
strictly decreasing sequence of ordinals. Contradiction.

$(\impliedby)$ For the converse direction, we will prove the contrapositive.
Suppose $w\not\in\mathcal{L}(\Gamma)$. Fix an arbitrary play
$\pi=(w_{i},\Gamma_{i})_{i\in\lambda}$ from $(w,\Gamma)$ for some
$\lambda\in\omega+1$. By inspection of the puzzle rules, non-membership is
preserved i.e. we always have $w_{i}\notin\mathcal{L}(\Gamma_{i})$. By
Proposition 50, there are $\nu$-signatures $\overline{\vec{\alpha_{i}}}$ such
that $w_{i}\notin\mathcal{L}(\Gamma_{\overline{\vec{\alpha_{i}}}})$. Following
an argument like above, the signature corresponding to a thread is a monotone
non-increasing sequence. Moreover, if $\pi$ is winning, it is strictly
decreasing. Therefore, $\pi$ is not winning. ∎

###  6.3. $\omega$-context-freeness via Muller grammars

We can now use the adequacy of the evaluation puzzle to recover a converse of
Proposition 35. For this, we need to recall a grammar-formulation of
$\mathsf{CF}^{\omega}$, due to Cohen and Gold [CG77] and independently Nivat
[Niv77, Niv78].

A Muller ($\omega$-)CFG (MCFG) is a CFG $\mathcal{G}$, equipped with a set
$F\subseteq\mathcal{P}(\mathcal{V})$ of acceptable sets. 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}Xv\rightarrow_{\mathcal{G}}\vec{a}uv$ whenever
$\vec{a}\in\mathcal{A}^{*}$, $X\to 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}^{\leq\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 51 ([CG77, Niv77, Niv78]).

Let $L\subseteq\mathcal{A}^{\omega}$. $L\in\mathsf{CF}^{\omega}\Leftrightarrow
L=\mathcal{L}(\mathcal{G})$ for a MCFG $\mathcal{G}$.

Now we have a converse of Proposition 35 by:

######  Proposition 52.

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 (3), but
with extra clause $X_{\nu Xf(X)}\to X_{f(\nu Xf(X))}$. We maintain two copies
of each non-terminal, one magenta and one normal, so that a derivation also
‘guesses’ a $\nu$-thread ‘on the fly’. Formally, the magenta productions of
our grammar are:

$\begin{array}[]{r@{\quad\rightarrow\quad}l}{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}X_{1}}&\varepsilon\\\
{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}X_{a}}&a\\\
{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}X_{f+g}}&{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}X_{f}}\quad|\quad{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}X_{g}}\\\
{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}X_{fg}}&{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}X_{f}}X_{g}\quad|\quad
X_{f}{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}X_{g}}\\\
{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}X_{\mu
Xf(X)}}&{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}X_{f(\mu
Xf(X))}}\\\
{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}X_{\nu
Xf(X)}}&{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}X_{f(\nu
Xf(X))}}\end{array}$

Productions for normal non-terminals have only normal non-terminals on their
RHSs.

Now set $F$, the set of acceptable sets, to include all sets extending some
$\\{{\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}X_{f}}:f\in
E\\}$, for $E$ with smallest expression a $\nu$-formula, by normal non-
terminals. Now any accepting leftmost derivation of a word $w$ from
${\color[rgb]{0.93359375,0.109375,0.7421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.93359375,0.109375,0.7421875}X_{e}}$
describes a winning play of the evaluation puzzle from $(w,e)$ and vice-versa.
∎

###  6.4. Proof search game and completeness

In order to prove completeness of $\mu\nu\ell\mathsf{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 53 (Proof search game).

The _proof search game_ (for $\mu\nu\ell\mathsf{HKA}$) is a two-player game
played between Prover $(\mathbf{P})$, whose positions are inference steps of
$\mu\nu\ell\mathsf{HKA}$, and Denier $(\mathbf{D})$, whose positions are
sequents of $\mu\nu\ell\mathsf{HKA}$. A play of the game starts from a
particular sequent: at each turn, $\mathbf{P}$ chooses an inference step with
the current sequent as conclusion, and $\mathbf{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 $\mathbf{P}$ (aka lost by $\mathbf{D}$)
if the branch constructed has a progressing thread; otherwise it is won by
$\mathbf{D}$ (aka lost by $\mathbf{P}$). In the case of deadlock, the player
with no valid move loses.

######  Proposition 54 (Determinacy ($\exists 0\\#$)).

The proof search game is determined, i.e. from any sequent $\Gamma\rightarrow
S$, either $\mathbf{P}$ or $\mathbf{D}$ has a winning strategy.

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

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

######  Lemma 55.

$\mathbf{D}$ has a winning strategy from $\Gamma\rightarrow S$ $\implies$
$\mathcal{L}(\Gamma)\setminus\mathcal{L}(S)\neq\varnothing$.

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

######  Proposition 56 (Modal).

$\mathcal{L}(a\Gamma)\subseteq\\{\varepsilon\\}\cup\bigcup\limits_{a\in\mathcal{A}}\mathcal{L}(aS_{a})\implies\mathcal{L}(\Gamma)\subseteq\mathcal{L}(S_{a})$.

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

###### Proof of Lemma 55.

Construct a $\mathbf{P}$-strategy $\mathfrak{p}$ that is deadlock-free by
always preserving validity, relying on Lemmas 17 and 56. In more detail
$\mathfrak{p}$ does the following:

  1. (1)

Apply leftmost logical steps (on LHS or RHS) as long as possible.

  2. (2)

If the LHS is empty and the RHS contains an empty list, then weaken the
remainder of the RHS and apply $\mathsf{init}$.

  3. (3)

Otherwise, if the LHS has form $a\Gamma$ and RHS has form $aS_{a},S$, where
$S$ contains only lists that are empty or begin with some $b\neq a$, then
apply $\mathsf{w}\text{-}r$ and $\mathsf{k}_{a}^{l}$ to obtain the sequent
$\Gamma\rightarrow S_{a}$ and go back to 1.

Now each iteration of 1 must terminate by left-guardedness and leftmostness.
This must end at a valid sequent, by Lemma 17, each of whose lists are either
or begin with a letter, by inspection of the rules. Now, if the LHS is empty,
then the RHS must contain an empty list, and so step 2 successfully terminates
the preproof. If the LHS has form $a\Gamma$, then step 3 applies and preserves
validity by Proposition 56. Note that any infinite play of $\mathfrak{p}$ must
repeat step 3 infinitely often, as each iteration of 1 terminates, and so has
infinitely many $\mathsf{k}^{l}$ steps and is not ultimately stable.

Now, suppose $\mathfrak{d}$ is a $\mathbf{D}$-winning-strategy and play
$\mathfrak{p}$ against it to construct a play
$B=(\mathcal{S}_{i})_{i<\omega}=(\Gamma_{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 $\mathbf{D}$-winning. Now, let
$w=\prod\limits_{\mathsf{k}_{a}^{l}\in B}a$ be the product of labels of
$\mathsf{k}$ steps along $B$, in the order they appear bottom-up. We claim
$w\in\mathcal{L}(\Gamma)\setminus\mathcal{L}(S)$:

  * •

$w\in\mathcal{L}(\Gamma)$. By construction $[\Gamma_{i}]_{i}$ has a
subsequence forming an infinite play $\pi$ of the evaluation puzzle from
$(w,\Gamma)$. Since the play $B$ is won by $\mathbf{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}(\Gamma)$ by Theorem 45.

  * •

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

∎

Now from Propositions 54 and 55, observing that $\mathbf{P}$-winning-
strategies are just $\infty$-proofs, we conclude:

######  Theorem 57 (Completeness).

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

##  7\. Complexity matters and further perspectives

In this subsection 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.
[MW85, Sac17], as well as various online resources.

Complexity and irregularity for finite words. The equational theory of
$\mu$-expressions in $\mathcal{L}(\cdot)$ is actually $\Pi^{0}_{1}$-complete,
i.e. co-recursively-enumerable, due to the same complexity of universality of
context-free grammars (see, e.g., [JEH01]). 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\mathsf{HKA}_{\omega}$ enjoys
optimal $\Pi^{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 [Pal07] for the theory of ‘$*$-continuous action
lattices’. Furthermore let us point out that our non-wellfounded system also
enjoys optimal proof search: $\mu\mathsf{HKA}\vdash^{\infty}\Gamma\rightarrow
S$ is equivalent, by invertibility, to checking that _every_ sequent of form
$\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 $\Pi^{0}_{1}$ property.

Complexity and inaxiomatisability for infinite words. It would be natural to
wonder whether a similar argument to Section 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 $\Pi^{1}_{2}$-complete [Fin09], so there is no hope
of a $\Pi^{0}_{1}$ (or even $\Sigma^{1}_{2}$) axiomatisation. In particular,
the projection argument of Section 4 cannot be scaled to the full system
$\mu\nu\ell\mathsf{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^{*}\neq(aa)^{*}a^{*}\cap
a(aa)^{*}a^{*}=aa^{*}$. Indeed let us point out that here it is crucial to use
our hypersequential system $\mathsf{HKA}$ as a base rather than, say, the
intuitionistic systems of other proof theoretic works for regular expressions
(and friends) [Pal07, DP18]: 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\mathsf{HKA}$,
in a sense, enjoys optimal complexity. By determinacy of the proof search
game, $\mu\nu\ell\mathsf{HKA}\vdash^{\infty}\Gamma\rightarrow S$ if and only
if there is _no_ $\mathbf{D}$-winning-strategy from $\Gamma\rightarrow S$. The
latter is indeed a $\Pi^{1}_{2}$ statement: “ _for every_
$\mathbf{D}$-strategy, _there exists_ a play along which _there exists_ a
progressing thread”.

Comparison to [GHK13]. Our method for showing completeness of
$\mu\mathsf{HKA}_{\omega}$ is quite different from the analogous result of
[GHK13] which uses the notion of ‘rank’ for $\mu$-formulas, cf. [AKS14]. 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.
[DDS23], whereas the rank method apparently breaks down in such extensions.
This means that our method should also scale to $\mu\nu\mathsf{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\mathsf{CA}$ was
only given for the guarded fragment. However it is known that $\mu\mathsf{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 [EL05].

##  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\mathsf{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\mathsf{HKA}_{\omega}$ via proof-theoretic techniques. This gave an
alternative proof of the completeness for the theory of $\mu$-continuous
Chomsky algebras from [GHK13]. 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\mathsf{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 $\Pi^{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 [DD24]. 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 [AM04, AM09].

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.
[Lan02, LMS04], 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 $\mathrm{ZFC}$ [Fin13, LT17].

Finally, it would be interesting to study the _structural_ proof theory
arising from systems $\mu\mathsf{HKA}^{\infty}$ and
$\mu\nu\mathsf{HKA}^{\infty}$, cf. [DP18]. 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 [DG22, DG23], in a
similar hypersequential system for predicate logic. Note that the same
leftmost constraint was employed in [HK22] for an extension of $\mathsf{HKA}$
to _$\omega$ -regular languages_.

## References

  * [AKS14] Luca Alberucci, Jürg Krähenbühl, and Thomas Studer.  Justifying induction on modal $\mu$-formulae.  Logic Journal of the IGPL, 22(6):805–817, 03 2014.
  * [AM04] Rajeev Alur and P. Madhusudan.  Visibly pushdown languages.  In Proceedings of the Thirty-Sixth Annual ACM Symposium on Theory of Computing, STOC ’04, page 202–211, New York, NY, USA, 2004. Association for Computing Machinery.
  * [AM09] Rajeev Alur and P. Madhusudan.  Adding nesting structure to words.  J. ACM, 56(3), may 2009.
  * [CD22] Gianluca Curzi and Anupam Das.  Cyclic implicit complexity.  In Christel Baier and Dana Fisman, editors, LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, August 2 - 5, 2022, pages 19:1–19:13, Haifa, 2022. ACM.
  * [CG77] Rina S Cohen and Arie Y Gold.  Theory of $\omega$-languagesi, ii: Characterizations of $\omega$-context-free languages.  Journal of Computer and System Sciences, 15(2):169–208, 1977.
  * [CKS81] Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer.  Alternation.  J. ACM, 28(1):114–133, jan 1981.
  * [CLS15] James Cranch, Michael R. Laurence, and Georg Struth.  Completeness results for omega-regular algebras.  Journal of Logical and Algebraic Methods in Programming, 84(3):402–425, 2015.  13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2012).
  * [Con71] John H. Conway.  Regular algebra and finite machines.  Chapman and Hall mathematics series. Chapman and Hall, 1971.
  * [DD24] Anupam Das and Abhishek De.  A proof theory of right-linear (omega-)grammars via cyclic proofs.  CoRR, abs/2401.13382, 2024.
  * [DDP18] Anupam Das, Amina Doumane, and Damien Pous.  Left-handed completeness for kleene algebra, via cyclic proofs.  In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors, LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 57 of EPiC Series in Computing, pages 271–289. EasyChair, 2018.
  * [DDS23] Anupam Das, Abhishek De, and Alexis Saurin.  Comparing Infinitary Systems for Linear Logic with Fixed Points.  In Patricia Bouyer and Srikanth Srinivasan, editors, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023), volume 284 of Leibniz International Proceedings in Informatics (LIPIcs), pages 40:1–40:17, Dagstuhl, Germany, 2023\. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
  * [DG22] Anupam Das and Marianna Girlando.  Cyclic proofs, hypersequents, and transitive closure logic.  In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 509–528. Springer, 2022.
  * [DG23] Anupam Das and Marianna Girlando.  Cyclic hypersequent system for transitive closure logic.  J. Autom. Reason., 67(3):27, 2023.
  * [DP17] Anupam Das and Damien Pous.  A cut-free cyclic proof system for kleene algebra.  In Renate A. Schmidt and Cláudia Nalon, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017, Proceedings, volume 10501 of Lecture Notes in Computer Science, pages 261–277. Springer, 2017.
  * [DP18] Anupam Das and Damien Pous.  Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices).  In Dan R. Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), volume 119 of Leibniz International Proceedings in Informatics (LIPIcs), pages 19:1–19:18, Dagstuhl, Germany, 2018. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
  * [ÉL02] Zoltán Ésik and Hans Lei$\beta$.  Greibach normal form in algebraically complete semirings.  In Julian Bradfield, editor, Computer Science Logic, pages 135–150, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg.
  * [EL05] Zoltán Ésik and Hans Leiß.  Algebraically complete semirings and greibach normal form.  Annals of Pure and Applied Logic, 133(1):173–203, 2005.  Festschrift on the occasion of Helmut Schwichtenberg’s 60th birthday.
  * [Fin09] Olivier Finkel.  Highly undecidable problems for infinite computations.  RAIRO - Theoretical Informatics and Applications, 43(2):339–364, 2009.
  * [Fin13] Olivier Finkel.  The determinacy of context-free games.  The Journal of Symbolic Logic, 78(4):1115–1134, 2013.
  * [GHK13] Niels Bjørn Bugge Grathwohl, Fritz Henglein, and Dexter Kozen.  Infinitary axiomatization of the equational theory of context-free languages.  Electronic Proceedings in Theoretical Computer Science, 126:44–55, August 2013.
  * [GR62] Seymour Ginsburg and H Gordon Rice.  Two families of languages related to algol.  Journal of the ACM (JACM), 9(3):350–371, 1962.
  * [Gru71] Jozef Gruska.  A characterization of context-free languages.  Journal of Computer and System Sciences, 5(4):353–364, 1971.
  * [Har78] Leo Harrington.  Analytic determinacy and $0\\#$.  Journal of Symbolic Logic, 43(4):685–693, 1978.
  * [HK22] Emile Hazard and Denis Kuperberg.  Cyclic proofs for transfinite expressions.  In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 23:1–23:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022\.
  * [JEH01] Jeffrey D. Ullman John E. Hopcroft, Rajeev Motwani.  Introduction to automata theory, languages, and computation.  Addison-Wesley, 2nd ed edition, 2001.
  * [Jip04] Peter Jipsen.  From semirings to residuated kleene lattices.  Studia Logica, 76:291–303, 03 2004.
  * [Kle56] S. C. Kleene.  Representation of Events in Nerve Nets and Finite Automata, pages 3–42.  Princeton University Press, Princeton, 1956.
  * [KMV22] Clemens Kupke, Johannes Marti, and Yde Venema.  Succinct Graph Representations of $\mu$-Calculus Formulas.  In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), volume 216 of Leibniz International Proceedings in Informatics (LIPIcs), pages 29:1–29:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
  * [Koz83] Dexter Kozen.  Results on the propositional $\mu$-calculus.  Theoretical Computer Science, 27(3):333–354, 1983.  Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982.
  * [Koz94] D. Kozen.  A completeness theorem for kleene algebras and the algebra of regular events.  Information and Computation, 110(2):366–390, 1994.
  * [Kro90] Daniel Krob.  A complete system of B-rational identities.  In Michael S. Paterson, editor, Automata, Languages and Programming, pages 60–73, Berlin, Heidelberg, 1990. Springer Berlin Heidelberg.
  * [KS97] Dexter Kozen and Frederick Smith.  Kleene algebra with tests: Completeness and decidability.  In Dirk van Dalen and Marc Bezem, editors, Computer Science Logic, pages 244–259, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg.
  * [KS12] Dexter Kozen and Alexandra Silva.  Left-handed completeness.  In Wolfram Kahl and Timothy G. Griffin, editors, Relational and Algebraic Methods in Computer Science, pages 162–178, Berlin, Heidelberg, 2012\. Springer Berlin Heidelberg.
  * [KS20] Dexter Kozen and Alexandra Silva.  Left-handed completeness.  Theoretical Computer Science, 807:220–233, 2020.  In memory of Maurice Nivat, a founding father of Theoretical Computer Science - Part II.
  * [KY19] Neelakantan R. Krishnaswami and Jeremy Yallop.  A typed, algebraic approach to parsing.  In PLDI, PLDI 2019, page 379–393, New York, NY, USA, 2019. Association for Computing Machinery.
  * [Lan02] Martin Lange.  Local model checking games for fixed point logic with chop.  In Lubos Brim, Petr Jancar, Mojmír Kretínský, and Antonín Kucera, editors, CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings, volume 2421 of Lecture Notes in Computer Science, pages 240–254. Springer, 2002.
  * [Lei92] Haas Leiß.  Towards kleene algebra with recursion.  In Egon Börger, Gerhard Jäger, Hans Kleine Büning, and Michael M. Richter, editors, Computer Science Logic, pages 242–256, Berlin, Heidelberg, 1992. Springer Berlin Heidelberg.
  * [Lei16] Hans Leiss.  The Matrix Ring of a mu-Continuous Chomsky Algebra is mu-Continuous.  In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1–6:15, Dagstuhl, Germany, 2016. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
  * [LH18] Hans Leiß and Mark Hopkins.  C-dioids and $\mu$-continuous chomsky-algebras.  In Jules Desharnais, Walter Guttmann, and Stef Joosten, editors, Relational and Algebraic Methods in Computer Science, pages 21–36, Cham, 2018\. Springer International Publishing.
  * [Lin76] Matti Linna.  On $\omega$-sets associated with context-free languages.  Information and Control, 31(3):272–293, 1976.
  * [LMS04] Christof Löding, P. Madhusudan, and Olivier Serre.  Visibly pushdown games.  In Kamal Lodaya and Meena Mahajan, editors, FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings, volume 3328 of Lecture Notes in Computer Science, pages 408–420. Springer, 2004.
  * [LT17] Li, Wenjuan and Tanaka, Kazuyuki.  The determinacy strength of pushdown $\omega$-languages.  RAIRO-Theor. Inf. Appl., 51(1):29–50, 2017.
  * [MHHO05] Etsuro Moriya, Dieter Hofbauer, Maria Huber, and Friedrich Otto.  On state-alternating context-free grammars.  Theoretical Computer Science, 337(1-3):183–216, 2005.
  * [MW85] R. Mansfield and G. Weitkamp.  Recursive Aspects of Descriptive Set Theory.  Oxford logic guides. Oxford University Press, 1985.
  * [Niv77] Maurice Nivat.  Mots infinis engendrés par une grammaire algébrique.  RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, 11(4):311–327, 1977.
  * [Niv78] Maurice Nivat.  Sur les ensembles de mots infinis engendrés par une grammaire algébrique.  RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, 12(3):259–278, 1978.
  * [NW96] Damian Niwiński and Igor Walukiewicz.  Games for the $\mu$-calculus.  Theoretical Computer Science, 163(1):99–116, 1996.
  * [Pal07] Ewa Palka.  An infinitary sequent system for the equational theory of *-continuous action lattices.  Fundamenta Informaticae, 78(2):295–309, 2007.
  * [Sac17] Gerald E. Sacks.  Higher Recursion Theory.  Perspectives in Logic. Cambridge University Press, 2017.
  * [Sal73] Arto Salomaa.  Formal Languages.  ACM monograph series. Academic Press, 1973.
  * [Sch63] M.P. Schützenberger.  On context-free languages and push-down automata.  Information and Control, 6(3):246–264, 1963.
  * [Stu08] Thomas Studer.  On the proof theory of the modal mu-calculus.  Studia Logica, 89(3):343–363, 2008.
  * [Thi17] Peter Thiemann.  Partial derivatives for context-free languages.  In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures, pages 248–264, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg.