}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-36.55992pt}{-4.27081pt}\pgfsys@lineto{-13.7599pt}{-4.27081pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-14.99983pt}{-4.27081pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.55992pt}{-4.27081pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} {\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.58961pt}{-1.71805pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{e}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{}{}{}{{}}{{
{\pgfsys@beginscope{{}}
\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{} {}{}{} {}{}{}
\pgfsys@moveto{2.07988pt}{2.39986pt}\pgfsys@curveto{1.69989pt}{0.95992pt}{0.85313pt}{0.27998pt}{0.0pt}{0.0pt}\pgfsys@curveto{0.85313pt}{-0.27998pt}{1.69989pt}{-0.95992pt}{2.07988pt}{-2.39986pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{14.73206pt}{-4.27081pt}\pgfsys@lineto{35.4522pt}{-4.27081pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{14.93204pt}{-4.27081pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{35.65218pt}{-4.27081pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} {\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{21.17912pt}{-1.71805pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{m}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$

we obtain the desired factorization of $\phi$:

${\mathbb{S}}$${\phi_{C}\,\mathbb{S}}$${\mathbb{R}}$$\scriptstyle{\phi_{\mathsf{colors}}}$$\scriptstyle{\phi_{\mathsf{nodes}}}$
${C_{\mathbb{S}}^{*}}$${V_{\mathbb{S}}}$${C_{\mathbb{S}}}$${(\phi_{C}\,C_{\mathbb{S}})^{*}}$${V_{\mathbb{S}}}$${\phi_{C}\,C_{\mathbb{S}}}$${C_{\mathbb{R}}^{*}}$${V_{\mathbb{R}}}$${C_{\mathbb{R}}}$$\scriptstyle{e^{*}}$$\scriptstyle{i}$$\scriptstyle{o}$$\scriptstyle{e}$$\scriptstyle{m^{*}}$$\scriptstyle{ie^{*}}$$\scriptstyle{oe}$$\scriptstyle{\phi_{V}}$$\scriptstyle{m}$$\scriptstyle{i^{\prime}}$$\scriptstyle{o^{\prime}}$

######  Lemma 42.

Every map of species $\psi:\mathbb{S}\to\mathbb{S}^{\prime}$ injective on
nodes induces a commutative diagram

${{\mathcal{F}\,\,\mathbb{S}}}$${{\mathcal{F}\,\,\mathbb{S}^{\prime}}}$${{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\mathbb{S}}}}}$${{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\mathbb{S}^{\prime}}}}}$$\scriptstyle{p_{\mathbb{S}}}$$\scriptstyle{\mathcal{F}\,\,\psi}$$\scriptstyle{p_{\mathbb{S}^{\prime}}}$$\scriptstyle{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\psi}}}$
(14)

where the canonical functor of operads from $\mathcal{F}\,\,\mathbb{S}$ to the
pullback of $p_{\mathbb{S}^{\prime}}$ along
$\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\psi}}$ is fully faithful.

######  Proof 3.6.

Every map of species $\psi:\mathbb{S}\to\mathbb{S}^{\prime}$ induces a pair of
naturality squares

${{\mathbb{S}}}$${{\mathbb{S}^{\prime}}}$${{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\mathbb{S}}}}}$${{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\mathbb{S}^{\prime}}}}}$$\scriptstyle{\psi_{\mathbb{S}}}$$\scriptstyle{\psi}$$\scriptstyle{\phi_{\mathbb{S}^{\prime}}}$$\scriptstyle{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\psi}}}$
${{\mathcal{F}\,\,\mathbb{S}}}$${{\mathcal{F}\,\,\mathbb{S}^{\prime}}}$${{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\mathbb{S}}}}}$${{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\mathbb{S}^{\prime}}}}}$$\scriptstyle{p_{\mathbb{S}}}$$\scriptstyle{\mathcal{F}\,\,\psi}$$\scriptstyle{p_{\mathbb{S}^{\prime}}}$$\scriptstyle{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\psi}}}$
(15)

in $\mathrm{Spec}$ and $\mathrm{Oper}$ respectively, where the functors of
operads $p_{\mathbb{S}}$ and $p_{\mathbb{S}^{\prime}}$ associated to the
universal grammars are the units of the contour / splicing adjunction. Note
that these naturality squares will in general _not_ be pullback squares. By
Lemma 30, we know that the pullback of $p_{\mathbb{S}^{\prime}}$ along
$\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\psi}}$ is obtained from a
corresponding pullback in the category of species

${{\mathbb{R}}}$${{\mathbb{S}^{\prime}}}$${{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\mathbb{S}}}}}$${{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\mathbb{S}^{\prime}}}}}$$\scriptstyle{\rho}$$\scriptstyle{\pi}$${\lrcorner}$$\scriptstyle{\phi_{\mathbb{S}^{\prime}}}$$\scriptstyle{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\psi}}}$
${\mathcal{F}\,\,\mathbb{R}}$${\mathcal{F}\,\,\mathbb{S}}$${{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\mathbb{S}}}}}$${{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\mathbb{S}^{\prime}}}}}$$\scriptstyle{r}$$\scriptstyle{\mathcal{F}\,\,\pi}$${\lrcorner}$$\scriptstyle{p_{\mathbb{S}^{\prime}}}$$\scriptstyle{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\psi}}}$
(16)

where the pullback species $\mathbb{R}$ has colors defined as tuples
$(R,(R_{1}^{u},R_{2}^{d}))$ of a color $R$ of $\mathbb{S}^{\prime}$ and colors
$R_{1}$, $R_{2}$ of $\mathbb{S}$ such that ${\psi(R_{1})=\psi(R_{2})=R}$, and
where the $n$-ary nodes of $\mathbb{R}$ are defined as pairs $(x,f)$ of a
$n$-ary node $x$ of $\mathbb{S}^{\prime}$ and an $n$-ary operation $f$ of
$\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\mathbb{S}}}$, necessarily of the
form $f=(y,0){-}\dots-(y,n)$ for $y$ the unique $n$-ary node of $\mathbb{S}$
such that $\psi(y)=x$, by assumption that
$\psi:\mathbb{S}\to\mathbb{S}^{\prime}$ is injective of nodes. The canonical
map of species ${\mathbb{S}}\to{\mathbb{R}}$ induced by the left-hand sides of
(15) and (16) transports every color $R$ of $\mathbb{S}$ to the color
$((\psi(R)^{u},\psi(R)^{d}),R)$ and every $n$-ary node $y$ of $\mathbb{S}$ to
the $n$-ary node $(\psi(y),(y,0){-}\dots-(y,n))$ of $\mathbb{R}$. From this
follows that the canonical map of species ${\mathbb{S}}\to{\mathbb{R}}$ is
injective on colors and bijective on nodes. Moreover, there are no nodes in
$\mathbb{R}$ whose colors are outside of the image of $\mathbb{S}$. We
conclude that the canonical functor of operads
$\mathcal{F}\,\,\mathbb{S}\to\mathcal{F}\,\,\mathbb{R}$ induced by the right-
hand sides of (15) and (16) is fully faithful.

Now, let $G=(\mathcal{C},\mathbb{S},S,p)$ be any categorical context-free
grammar, and by Prop. 41 consider the corresponding $\mathcal{C}$-chromatic
grammar
$G_{\mathsf{nodes}}=(\mathcal{C},\phi_{C}\,\mathbb{S},(A,B),p_{\mathsf{nodes}})$,
where $p(S)=(A,B)$. We have a commutative diagram

${{\mathcal{F}\,\,\mathbb{S}}}$${{\mathcal{F}\,\,\phi_{C}\,\mathbb{S}}}$${{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\mathbb{S}}}}}$${{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\phi_{C}\,\mathbb{S}}}}}$${\mathcal{W}\,{\mathcal{C}}}$$\scriptstyle{p_{\mathbb{S}}}$$\scriptstyle{\mathcal{F}\,\,\phi_{\mathsf{colors}}}$$\scriptstyle{p_{\phi_{C}\,\mathbb{S}}}$$\scriptstyle{\mathcal{W}\,{\mathcal{C}\,{\mathcal{F}\,\,\phi_{\mathsf{colors}}}}}$$\scriptstyle{\mathcal{W}\,{q_{G}}}$$\scriptstyle{\mathcal{W}\,{q_{G_{\mathsf{nodes}}}}}$
(17)

where the commutativity of the lower triangle follows from the equation
$\phi=\phi_{\mathsf{colors}}\phi_{\mathsf{nodes}}$ and the contour / splicing
adjunction. Note also that
$p_{\mathsf{colors}}:=\mathcal{C}\,{\mathcal{F}\,\,\phi_{\mathsf{colors}}}$ is
a ULF functor of categories by Prop. 38 and also finitary because
$\phi_{\mathsf{colors}}$ is finitary (and even finite). From this follows that
$M_{\mathsf{colors}}=(\mathcal{C}\,{\mathcal{F}\,\,\phi_{C}\,\mathbb{S}},\mathcal{C}\,{\mathcal{F}\,\,\mathbb{S}},p_{\mathsf{colors}},S^{u},S^{d})$
defines a finite-state automaton. By the intersection construction (Cor. 33)
together with Lemma 42 and the strong translation principle (Prop. 5), we
deduce that

$p_{\mathsf{colors}}\,TC_{\mathbb{S},S}\,=\,TC_{\phi_{C}\,\mathbb{S},(A,B)}\,\cap\,\mathcal{L}_{M_{\mathsf{colors}}}.$

Finally, using that $G$ is the image of the universal grammar
$\mathsf{Univ}_{\mathbb{S},S}$ and considering the commutative diagram (17),
we conclude:

$\mathcal{L}_{G}=q_{G}\,TC_{\mathbb{S},S}=q_{G_{\mathsf{nodes}}}\,p_{\mathsf{colors}}\,TC_{\mathbb{S},S}=q_{G_{\mathsf{nodes}}}\,(TC_{\phi_{C}\,\mathbb{S},(A,B)}\,\cap\,\mathcal{L}_{M_{\mathsf{colors}}}).$

######  Theorem 43.

$L\subseteq\mathcal{C}(A,B)$ is a CFL of arrows iff it is a functorial image
of the intersection of a $\mathcal{C}$-chromatic tree contour language with a
regular language.

For the original example of Figure 2, the colors-nodes factorization

${\mathbb{S}}$${\mathcal{W}\,{\Sigma}\quad=\quad\mathbb{S}}$${\phi_{C}\,\mathbb{S}}$${\mathcal{W}\,{\Sigma}}$$\scriptstyle{\phi}$$\scriptstyle{\phi_{{\mathsf{colors}}}}$$\scriptstyle{\phi_{\mathsf{nodes}}}$

of Prop. 41 may be visualized as below:

Some examples of contour words in the tree contour language
$TC_{\phi_{C}\,\mathbb{S},(*,*)}$ and their corresponding images under the
functor $q_{G_{\mathsf{nodes}}}$ include:

Observe that only the first contour word encodes a valid parse tree mapping to
a word of the language. Finally, the “coloring automaton”
$M_{\mathsf{colors}}$ derived by the contour construction may be depicted by
the following transition diagram:

$\mathsf{S}^{u}$$\mathsf{NP}^{u}$$\mathsf{VP}^{u}$$\mathsf{NP}^{d}$$\mathsf{VP}^{d}$$\mathsf{S}^{d}$$\mathsf{1_{0}}$$\mathsf{2_{0}}$$\mathsf{3_{0}}$$\mathsf{1_{1}}$$\mathsf{4_{0}}$$\mathsf{4_{1}}$$\mathsf{1_{2}}$

The reader can verify that the automaton only accepts the first contour word
above.

######  Remark 44.

We view the use of contour words rather than Dyck words as a mild improvement
of the original theorem by Chomsky and Schützenberger, since it removes the
need for choosing arbitrarily between left brackets and right brackets to map
to empty words. But there is a close relationship between tree contour words
and Dyck words, and the original representation can be recovered if desired.
As suggested by the right-hand side of Figure 6, there is an easy mapping from
contour words to Dyck words defined by translating each corner $(x,i)$ of an
$n$-ary node $x$ as follows:

$(x,i)\mapsto\begin{cases}[x_{0}\ ]x_{0}&i=n=0\\\ [x_{0}\ [x_{1}&i=0<n\\\
]x_{i}\ [x_{i+1}&0>i<n\\\ ]x_{n}\ ]x_{0}&0>i=n\end{cases}$

This translation doubles the number of letters, and has a visual
interpretation as decomposing each corner of the contour into alternating
actions of walking along an edge and turning around a node. Indeed, the
geometric content is so clear that we are optimistic there should be a good
categorical explanation, as a way of faithfully embedding any contour category
into a larger “bipartite” contour category where every arrow has been factored
in two. We leave this to future work, adding that the situation appears
intriguingly analogous to the embedding of the _oriented cartographic group_
used to represent maps on oriented surfaces into the _unoriented cartographic
group_ used to represent maps on not necessarily orientable surfaces (cf.
[SV90, JS94]), a link that we think is worth developing further.

###  3.5. Related work

As already mentioned, our proof that (generalized) context-free languages are
closed under intersection with regular languages may be seen as a
decomposition of the Bar-Hillel construction [BHPS61]. In a similar spirit,
Ludmann, Pogodalla, and De Groote have recently analyzed Kanazawa’s proof that
languages generated by abstract categorial grammars are closed under
intersection with regular languages, and shown that it defines a pullback in
an appropriate category [LPdG22].

The representation theorem is one of many results appearing in Chomsky and
Schützenberger’s joint article on “The algebraic theory of context-free
languges” [CS63]. The theorem was sketched in a technical report by Chomsky
[Cho62] with attribution to their collaboration, while the first detailed
proof seems to have been by Schützenberger [Sch63]. The original formulation
used _two-sided_ 777The two-sided Dyck language on an alphabet of $2n$ letters
$x_{\pm i}$ $(1\leq i\leq n)$ may be defined as the kernel of the canonical
homomorphism $\phi:\mathrm{Mon}\langle
x_{-n},\dots,x_{-1},x_{+1},\dots,x_{+n}\rangle\to\mathrm{Grp}\langle
x_{1},\dots,x_{n}\rangle$ from the free monoid on $2n$ generators to the free
group on $n$ generators defined by $\phi(x_{+i})=x_{i}$ and
$\phi(x_{-i})=x_{i}^{-1}$. Dyck languages, but would have worked just as well
with ordinary (one-sided) Dyck languages and most standard treatments of the
theorem now adopt that formulation [Koz97, §G]. Numerous variations of the
representation theorem and extensions to other classes of languages have since
been established, see [CS16] for an overview and bibliography.

The contour / splicing adjunction is fundamental to our analysis of the
representation theorem, providing an unexpected geometric lens on context-free
languages that is evocative of Girard’s geometry of interaction. Although the
adjunction is not identified, this geometric perspective is also apparent in
Slavnov’s recent work [Sla20] (inspired both by abstract categorial grammars
and by linear logic proof-nets), wherein he constructs a compact closed
monoidal category of _word cobordisms_ reminiscent of the operad of spliced
words.

After the original version of this article was published [MZ22], the contour /
splicing adjunction was subsequently analyzed and extended by Earnshaw,
Hefford, and Román, who described applications to process algebra [EHR23,
Rom23]. They noticed that the splicing functor
$\mathcal{W}:\mathrm{Cat}\to\mathrm{Oper}$ is closely related to a
construction by Day and Street [DS04, Example 7.3], of a canonical promonoidal
structure on $\mathcal{C}^{\mathrm{op}}\otimes\mathcal{C}$ for any
$\mathcal{V}$-enriched category $\mathcal{C}$. We have also been further
exploring the adjunction from a mathematical perspective, in ongoing work with
Peter Faul.

##  4\. Conclusion

We have seen that the classical notions of context-free grammar and of non-
deterministic finite state automaton can be reformulated and generalized in a
categorical setting, in a way that seems to have significant explanatory
power. Clearly many natural questions arise in regards to integrating the deep
body of work on automata theory and formal language theory within this
setting, some of which we have already signalled. Another obvious question is
how to define pushdown automata over categories. We find it remarkable that
when one considers the nodes of a species as the production rules of a
context-free grammar, the corners of its contour category correspond exactly
to the _items_ used in LR parsing and Earley parsing [Knu65, Ear70], which we
think suggests contour categories have a role to play in analyzing left-to-
right parsing algorithms from a categorical perspective. One of our original
motivations for studying context-free grammars as functors and looking at
parsing as a lifting problem was to develop a better understanding of the
universal properties of algorithms like these, having in mind that such an
understanding could then be transferred to other settings including type
checking and type inference algorithms. This attempt at unification is
supported by the emergence of a number of categorical and fibrational
structures which seem to connect these different kinds of symbolic systems,
revealing that they are founded on many of the same basic patterns.

## Acknowledgment

We thank Peter Faul for many exciting discussions of the contour / splicing
adjunction, Thea Li for stimulating conversations about determinization and
$\epsilon$-removal for categorical automata, and Farzad Jafarrahmani for
fruitful interactions related to the material in the Addendum. We also
gratefully acknowledge Bryce Clarke for many helpful insights into the
contents of the paper, which improved some of the proofs, and for telling us
about [Par12]. We thank Daniela Petrişan, Thomas Colcombet, and the other
members of the working group on “Categories for Automata and Language Theory”
at IRIF for helping us to better understand the relationship with [CP20] and
with other works. We thank Benjamin Steinberg for telling us about [Jon96],
which led us to [TSG88, WT86]. Finally, special thanks to Hayo Thielecke for
giving a very lucid presentation of LL and LR parsing using abstract machines
in 2017, which was one of our original sources of inspiration.

## References

  * [AL19] Benedikt Ahrens and Peter LeFanu Lumsdaine.  Displayed categories.  Logical Methods in Computer Science, 15(1), 2019.  doi:10.23638/LMCS-15(1:20)2019.
  * [B0́0] Jean Bénabou.  Distributors at work.  Notes from a course at TU Darmstadt in June 2000, taken by Thomas Streicher, 2000.  URL: https://www2.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf.
  * [Bed88] M.A. Bednarczyk.  Categories of asynchronous systems.  PhD thesis, University of Sussex, 1988.
  * [BF00] Marta Bunge and Marcelo P. Fiore.  Unique factorisation lifting functors and categories of linearly-controlled processes.  Mathematical Structures in Computer Science, 10:137–163, 2000.  doi:10.1017/S0960129599003023.
  * [BHPS61] Y. Bar-Hillel, M. Perles, and E. Shamir.  On formal properties of simple phrase structure grammars.  Z. Phonetik, Sprachwissen. Kommun., 14(2):143–172, 1961.  doi:doi:10.1524/stuf.1961.14.14.143.
  * [BJT97] Hans-Joachim Baues, Mamuka Jibladze, and Andy Tonks.  Cohomology of monoids in monoidal categories.  Contemporary Mathematics, 202, 1997.  doi:10.1090/conm/202/02597.
  * [BLL98] F. Bergeron, G. Labelle, and P. Leroux.  Combinatorial Species and Tree-Like Structures.  Cambridge University Press, 1998.  Translated by Margaret Readdy.  doi:10.1017/CBO9781107325913.
  * [BM06] Nicolas Baudru and Rémi Morin.  Unfolding synthesis of asynchronous automata.  In Dima Grigoriev, John Harrison, and Edward A. Hirsch, editors, Computer Science – Theory and Applications, pages 46–57, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg.
  * [BN00] Marta Bunge and Susan Niefeld.  Exponentiability and single universes.  Journal of Pure and Applied Algebra, 148:217–250, 2000.  doi:10.1016/S0022-4049(98)00172-8.
  * [CDG+08] Hubert Comon, Max Dauchet, Rémi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi.  Tree Automata Techniques and Applications, 2008.  URL: https://hal.inria.fr/hal-03367725.
  * [CE12] Bruno Courcelle and Joost Engelfriet.  Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach, volume 138 of Encyclopedia of mathematics and its applications.  Cambridge University Press, 2012.  doi:10.1017/CBO9780511977619.
  * [Cho62] Noam Chomsky.  Context-free grammars and push-down storage.  Quarterly Progress Report 65, Research Laboratory of Electronics, M.I.T., 1962.  URL: http://hdl.handle.net/1721.1/53697.
  * [Con71] John Horton Conway.  Regular Algebra and Finite Machines.  Chapman and Hall, 1971.  Reprinted in Dover Books on Mathematics, 2012.
  * [CP20] Thomas Colcombet and Daniela Petrişan.  Automata minimization: a functorial approach.  Logical Methods in Computer Science, 16(1):32:1–32:28, 2020.  doi:10.23638/LMCS-16(1:32)2020.
  * [CS63] N. Chomsky and M. P. Schützenberger.  The algebraic theory of context-free languages.  In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems, volume 35 of Studies in Logic and the Foundations of Mathematics, pages 118–161. North-Holland, 1963.  doi:10.1016/S0049-237X(08)72023-8.
  * [CS16] Stefano Crespi-Reghizzi and Pierluigi San Pietro.  An enduring trail of language characterizations via homomorphism (talk), March 21–25 2016.  Conference dedicated to the scientific legacy of M. P. Schützenberger (Bordeaux).  URL: https://mps2016.labri.fr/archives/crespi.pdf.
  * [dG01] Philippe de Groote.  Towards abstract categorial grammars.  In Association for Computational Linguistic, 39th Annual Meeting and 10th Conference of the European Chapter, Proceedings of the Conference, July 9-11, 2001, Toulouse, France, pages 148–155. Morgan Kaufmann Publishers, 2001.  doi:10.3115/1073012.1073045.
  * [dGP04] Philippe de Groote and Sylvain Pogodalla.  On the expressive power of abstract categorial grammars: Representing context-free formalisms.  J. Log. Lang. Inf., 13(4):421–438, 2004.  doi:10.1007/s10849-004-2114-x.
  * [DS02] Manfred Droste and R. M. Shortt.  From petri nets to automata with concurrency.  Appl. Categorical Struct., 10(2):173–191, 2002.  doi:10.1023/A:1014305610452.
  * [DS04] Brian Day and Ross Street.  Quantum categories, star autonomy, and quantum groupoids.  In Galois Theory, Hopf Algebras, and Semiabelian Categories, pages 187–225. American Mathematical Society, 2004.
  * [Ear70] Jay Earley.  An efficient context-free parsing algorithm.  Commun. ACM, 13(2):94–102, 1970.  doi:10.1145/362007.362035.
  * [EHR23] Matt Earnshaw, James Hefford, and Mario Román.  The produoidal algebra of process decomposition.  CoRR, abs/2301.11867, 2023.  arXiv:2301.11867, doi:10.48550/ARXIV.2301.11867.
  * [Eil74] Samuel Eilenberg.  Automata, Languages, and Machines: volume A.  Pure and applied mathematics. Academic Press, 1974.
  * [ES22] Matthew Earnshaw and Pawel Sobociński.  Regular monoidal languages.  In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors, 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria, volume 241 of LIPIcs, pages 44:1–44:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.  doi:10.4230/LIPICS.MFCS.2022.44.
  * [FGHW08] M. Fiore, N. Gambino, M. Hyland, and G. Winskel.  The cartesian closed bicategory of generalised species of structures.  Journal of the London Mathematical Society, 77(1):203–220, 2008\.  doi:10.1112/jlms/jdm096.
  * [FJSZ22] Uli Fahrenberg, Christian Johansen, Georg Struth, and Krzysztof Ziemianski.  A Kleene theorem for higher-dimensional automata.  In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland, volume 243 of LIPIcs, pages 29:1–29:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.  URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.29, doi:10.4230/LIPICS.CONCUR.2022.29.
  * [GHK17] Niels Bjørn Bugge Grathwohl, Fritz Henglein, and Dexter Kozen.  Infinitary axiomatization of the equational theory of context-free languages.  Fundam. Informaticae, 150(3-4):241–257, 2017.  doi:10.3233/FI-2017-1469.
  * [GM10] Eric Goubault and Samuel Mimram.  Formal relationships between geometrical and classical models for concurrency.  In Lisbeth Fajstrup, Eric Goubault, and Martin Raussen, editors, Proceedings of the workshop on Geometric and Topological Methods in Computer Science, GETCO 2010, Aalborg, Denmark, January 11-15, 2010, volume 283 of Electronic Notes in Theoretical Computer Science, pages 77–109. Elsevier, 2010.  URL: https://doi.org/10.1016/j.entcs.2012.05.007, doi:10.1016/J.ENTCS.2012.05.007.
  * [GR62] Seymour Ginsburg and H. Gordon Rice.  Two families of languages related to ALGOL.  Journal of the ACM, 9(3):350–371, 1962.  doi:10.1145/321127.321132.
  * [Gue20] Léonard Guetta.  Polygraphs and discrete Conduché $\omega$-functors.  Higher Structures, 4(2):134–166, 2020.  doi:10.21136/HS.2020.11.
  * [Her00] Claudio Hermida.  Representable multicategories.  Advances in Mathematics, 151(2):164–225, 2000.  doi:10.1006/aima.1999.1877.
  * [Her04] Claudio Hermida.  Fibrations for abstract multicategories.  In George Janelidze, Bodo Pareigis, and Walter Tholen, editors, Galois Theory, Hopf Algebras, and Semiabelian Categories, volume 43 of Fields Institute Communications. American Mathematical Society, 2004.  doi:10.1090/fic/043/11.
  * [HM00] Jean-François Husson and Rémi Morin.  On recognizable stable trace languages.  In Jerzy Tiuryn, editor, Foundations of Software Science and Computation Structures, Third International Conference, FOSSACS 2000, Held as Part of the Joint European Conferences on Theory and Practice of Software,ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings, volume 1784 of Lecture Notes in Computer Science, pages 177–191. Springer, 2000.  doi:10.1007/3-540-46432-8\\_12.
  * [HMU07] John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman.  Introduction to automata theory, languages, and computation, 3rd Edition.  Pearson international edition. Addison-Wesley, 2007.
  * [Hyl08] Martin Hyland.  Abstract and concrete models for recursion.  In O. Grumberg, T. Nipkow, and C. Pfaller, editors, Proceedings of the NATO Advanced Study Institute on Formal Logical Methods for System Security and Correctness, pages 175–198. IOS Press, 2008.
  * [Joh99] Peter Johnstone.  A note on discrete Conduché fibrations.  Theory and Applications of Categories, 5(1):1–11, 1999.
  * [Jon96] Peter R Jones.  Profinite categories, implicit operations and pseudovarieties of categories.  Journal of Pure and Applied Algebra, 109(1):61–95, 1996.  doi:10.1016/0022-4049(95)00074-7.
  * [Joy81] André Joyal.  Une théorie combinatoire des séries formelles.  Advances in Mathematics, 42(1):1–82, 1981.  doi:10.1016/0001-8708(81)90052-9.
  * [Joy86] André Joyal.  Foncteurs analytiques et espèces de structures.  In Gilbert Labelle and Pierre Leroux, editors, Combinatoire énumérative, Lecture Notes in Mathematics, pages 126–159, Berlin, Heidelberg, 1986. Springer Berlin Heidelberg.  doi:10.1007/BFb0072514.
  * [JS94] Gareth A. Jones and David Singerman.  Maps, hypermaps, and triangle groups.  In L. Schneps, editor, The Grothendieck Theory of Dessins d’Enfants, number 200 in London Mathematical Society Lecture Note Series. Cambridge University Press, 1994.  doi:10.1017/CBO9780511569302.006.
  * [Knu65] Donald E. Knuth.  On the translation of languages from left to right.  Information and Control, 8(6):607–639, 1965.  doi:10.1016/S0019-9958(65)90426-2.
  * [Koz97] Dexter Kozen.  Automata and Computability.  Undergrad. texts in comp. science. Springer, 1997.
  * [Lam89] Joachim Lambek.  Multicategories revisited.  Contemporary Mathematics, 92:217–239, 1989.  doi:10.1090/conm/092.
  * [Law86] F. W. Lawvere.  State categories and response functors.  Unpublished, May 1986.
  * [Lee89] René Leermakers.  How to cover a grammar.  In Julia Hirschberg, editor, 27th Annual Meeting of the Association for Computational Linguistics, 26-29 June 1989, University of British Columbia, Vancouver, BC, Canada, Proceedings, pages 135–142. ACL, 1989\.  doi:10.3115/981623.981640.
  * [Lei04] Tom Leinster.  Higher Operads, Higher Categories, volume 298 of London Mathematical Society Lecture Note Series.  Cambridge University Press, 2004.  doi:10.1017/CBO9780511525896.
  * [LL09] Martin Lange and Hans Leiß.  To CNF or not to CNF? An efficient yet presentable version of the CYK algorithm.  Informatica Didact., 8, 2009.  URL: https://www.informaticadidactica.de/index.php?page=LangeLeiss2009_en.
  * [LM10] F. W. Lawvere and M. Menni.  The Hopf algebra of Möbius intervals.  Theory and Applications of Categories, 24(10):221–265, 2010.  URL: http://www.tac.mta.ca/tac/volumes/24/10/24-10abs.html.
  * [LPdG22] Pierre Ludmann, Sylvain Pogodalla, and Philippe de Groote.  Multityped abstract categorial grammars and their composition.  In Agata Ciabattoni, Elaine Pimentel, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information, and Computation, pages 105–122, 2022\.  doi:10.1007/978-3-031-15298-6_7.
  * [Mac98] Saunders Mac Lane.  Categories for the Working Mathematician.  Springer, 1998.
  * [Maz89] Antoni Mazurkiewicz.  Basic notions of trace theory.  In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, pages 285–363, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg.
  * [Mel21] Paul-André Melliès.  Asynchronous template games and the Gray tensor product of 2-categories.  In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Roma, Italy, 2021, 2021.
  * [MM07] Paul-André Mellies and Samuel Mimram.  Asynchronous games: innocence without alternation.  In Proceedings of the 18th International Conference on Concurrency Theory, CONCUR 2007, volume 4703 of LNCS, pages 395–411. Springer Verlag, 2007.
  * [MN24] Vincent Moreau and Lê Thành Dung Nguyên.  Syntactically and semantically regular languages of lambda-terms coincide through logical relations.  In 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024, February 19-23, 2024, Naples, Italy, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.
  * [Mor05] Rémi Morin.  Concurrent automata vs. asynchronous systems.  In Joanna Jedrzejowicz and Andrzej Szepietowski, editors, Mathematical Foundations of Computer Science 2005, 30th International Symposium, MFCS 2005, Gdansk, Poland, August 29 - September 2, 2005, Proceedings, volume 3618 of Lecture Notes in Computer Science, pages 686–698. Springer, 2005.  doi:10.1007/11549345\\_59.
  * [MSS02] Martin Markl, Steve Schnider, and Jim Stasheff.  Operads in Algebra, Topology and Physics, volume 96 of Mathematical Surveys and Monographs.  American Mathematical Society, 2002.  doi:10.1090/surv/096.
  * [MW67] Jorge E. Mezei and Jesse B. Wright.  Algebraic automata and context-free sets.  Information and Control, 11(1/2):3–29, 1967.  doi:10.1016/S0019-9958(67)90353-1.
  * [MZ13] Paul-André Melliès and Noam Zeilberger.  Type refinement and monoidal closed bifibrations.  Unpublished, arXiv:1310.0263, October 2013.  URL: https://arxiv.org/abs/1310.0263.
  * [MZ15] Paul-André Melliès and Noam Zeilberger.  Functors are type refinement systems.  In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 3–16. ACM, 2015.  doi:10.1145/2676726.2676970.
  * [MZ16] Paul-André Melliès and Noam Zeilberger.  A bifibrational reconstruction of Lawvere’s presheaf hyperdoctrine.  In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pages 555–564. ACM, 2016.  doi:10.1145/2933575.2934525.
  * [MZ18] Paul-André Melliès and Noam Zeilberger.  An Isbell duality theorem for type refinement systems.  Mathematical Structures in Computer Science, 28(6):736–774, 2018\.  doi:10.1017/S0960129517000068.
  * [MZ22] Paul-André Melliès and Noam Zeilberger.  Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem.  In MFPS 2022 - 38th conference on Mathematical Foundations for Programming Semantics, July 2022.  doi:10.46298/entics.10508.
  * [Par12] Robert Paré.  Mealy morphisms of enriched categories.  Applied Categorical Structures, 20(3):251–273, 2012.  doi:10.1007/S10485-010-9238-8.
  * [Rom23] Mario Román.  Monoidal Context Theory.  PhD thesis, Tallinn University of Technology, 2023.
  * [Ros95] Kimmo I. Rosenthal.  Quantaloids, enriched categories and automata theory.  Applied Categorical Structures, 3(3):279–301, 1995.  doi:10.1007/BF00878445.
  * [RS59] Michael O. Rabin and Dana S. Scott.  Finite automata and their decision problems.  IBM Journal of Research and Development, 3(2):114–125, 1959.
  * [Sal09] Sylvain Salvati.  Recognizability in the simply typed lambda-calculus.  In WoLLIC, volume 5514 of LNCS, pages 48–60, 2009.  doi:1007/978-3-642-02261-6_5.
  * [Sch63] M. P. Schützenberger.  On context-free languages and push-down automata.  Information and control, 6(3):246–264, 1963.
  * [Sch15] Gilles Schaeffer.  Planar maps.  In Miklós Bóna, editor, Handbook of Enumerative Combinatorics, pages 335–396. CRC, 2015.  URL: http://www.lix.polytechnique.fr/~schaeffe/Master/HB.pdf.
  * [Shu] Michael Shulman.  LNL polycategories and doctrines of linear logic.  Logical Methods in Computer Science, 19(2):1:1–1:54.  doi:10.46298/lmcs-19(2:1)2023.
  * [Sip13] Michael Sipser.  Introduction to the theory of computation, 3rd edition.  Cengage Learning, 2013.
  * [Sla20] Sergey Slavnov.  Classical linear logic, cobordisms and categorial grammars, 2020.  arXiv:1911.03962.  URL: https://arxiv.org/abs/1911.03962.
  * [SMFK91] Hiroyuki Seki, Takashi Matsumura, Mamoru Fujii, and Tadao Kasami.  On multiple context-free grammars.  Theoretical Computer Science, 88(2):191–229, 1991.  doi:https://doi.org/10.1016/0304-3975(91)90374-B.
  * [SS88] Seppo Sippu and Eljas Soisalon-Soininen.  Parsing Theory - Volume I: Languages and Parsing, volume 15 of EATCS Monographs on Theoretical Computer Science.  Springer, 1988.  doi:10.1007/978-3-642-61345-6.
  * [Ste01] Benjamin Steinberg.  Finite state automata: a geometric approach.  Transactions of the American Mathematical Society, 353(9):3409–3464, 2001.
  * [Str96] Ross Street.  Categorical structures.  In M. Hazewinkel, editor, Handbook of Algebra, volume 1, pages 529–577. North-Holland, 1996.
  * [SV90] G. Shabat and V. Voevodsky.  Drawing curves over number fields.  In P. Cartier, Luc Illusie, Nicholas M. Katz, Gérard Laumon, Yuri I. Manin, and Kenneth A. Ribet, editors, The Grothendieck festschrift III, number 88 in Progress in Mathematics, pages 199–227. Birkhäuser, 1990.  URL: https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/drawing_curves_published.pdf.
  * [TSG88] Denis Thérien and Małgorzata Sznajder-Glodowski.  Finite categories and regular languages.  In Mathematical Problems in Computation Theory, volume 21 of Banach Center Publications, pages 395–402. 1988.
  * [Wal89] R. F. C. Walters.  A note on context-free languages.  Journal of Pure and Applied Algebra, 62(2):199–203, 1989.  doi:10.1016/0022-4049(89)90151-5.
  * [WT86] Alex Weiss and Denis Thérien.  Varieties of finite categories.  Informatique théorique et applications, 20(3):357–366, 1986.
  * [Zie87] Wieslaw Zielonka.  Notes on finite asynchronous automata.  RAIRO – Theoretical Informatics and Applications, 21:99–135, 1987\.

##  Addendum A gCFLs as initial models of gCFGs

We begin to explore here another more abstract perspective on (generalized)
context-free grammars and context-free languages, under which a CFG defines a
kind of theory that generates a CFL as its _initial model_. On the one hand,
this viewpoint encompasses the old idea of treating CFGs as defining certain
systems of polynomial equations and CFLs as minimal solutions to those systems
of equations (cf. [GR62, MW67], [Con71, Ch. 10], [GHK17]). At the same time,
our categorical formulation is in the broad spirit of functorial semantics of
algebraic theories à la Lawvere, adapted to an operadic and fibrational
setting. We will see that one benefit of this perspective is that it enables
us to consider a more expansive notion of “language” generated by a grammar,
recovering the traditional notion of formal language as subset of words (or
subset of arrows/constants) as a special case.

Before stating the general definitions, let us give an example. The Dyck
language of well-bracketed words over an alphabet $\Sigma$ containing a pair
of brackets ‘$[$’ and ‘$]$’ may be generated by either of the following
context-free grammars with a single non-terminal:

$G_{1}\ \ =\begin{array}[]{rcl}S&\to&\epsilon\\\ S&\to&[S]\\\
S&\to&SS\end{array}\qquad G_{2}\ \ =\begin{array}[]{rcl}S&\to&\epsilon\\\
S&\to&[S]S\end{array}$ (18)

Although the language $L=\mathcal{L}_{G_{1}}=\mathcal{L}_{G_{2}}$ generated by
both grammars is the same, $G_{1}$ and $G_{2}$ may be seen as implicitly
stating two different equations _satisfied_ by this language,

$\displaystyle L$ $\displaystyle=\epsilon+[L]+LL$ (19) $\displaystyle L$
$\displaystyle=\epsilon+[L]L$ (20)

where we have written $+$ for union (and implicitly make use of the spliced
concatenation of languages as defined in Prop. 4(2)). Equation (19) has other
solutions besides the language of Dyck words, such as the total language
$L=\Sigma^{*}$, while interestingly (20) only admits a unique solution.
However, in both cases one can easily establish that the context-free language
generated by the grammar provides the unique _minimal_ solution to the
corresponding equation, in the sense that it is included in any other
solution.

To describe the proper abstract setting for such systems of equations, we need
to introduce here some fibrational concepts for functors of operads, for which
we again find it useful to adapt some conventions from our type refinement
systems work. Extending the notation from §1.6, we write
$\alpha:R_{1},\dots,R_{n}\ThisStyle{\Rightarrow_{f}^{q}}R$ to indicate that
$\alpha:R_{1},\dots,R_{n}\to R$ is an operation in $\mathcal{E}$ with image
$q(\alpha)=f$ in $\mathcal{B}$, relative to a functor of operads
$q:\mathcal{E}\to\mathcal{B}$. We sometimes omit the superscript and write
$\alpha:R_{1},\dots,R_{n}\ThisStyle{\Rightarrow_{f}}R$ if $q$ is clear from
context. We write $\mathcal{E}_{f}(R_{1},\dots,R_{n};R)$ for the set of
operations
$\\{\,{\alpha\mid\alpha:R_{1},\dots,R_{n}\ThisStyle{\Rightarrow_{f}^{q}}R}\,\\}$.
A cone in an operad $\mathcal{O}$ is a family of operations
$(g_{i}:\Delta_{i}\to A)_{i\in I}$ in $\mathcal{O}$ with the same output color
$A$.

Let $q:\mathcal{E}\to\mathcal{B}$ be a functor of operads. A cone
$(\alpha_{i}:\Omega_{i}\ThisStyle{\Rightarrow_{g_{i}}^{q}}R)_{i\in I}$ in
$\mathcal{E}$ is said to be minimal over a cone $(g_{i}:\Delta_{i}\to A)_{i\in
I}$ in $\mathcal{B}$ (relative to $q$) if for every operation
$f:\Gamma,A,\Gamma^{\prime}\to B$ in $\mathcal{B}$ with $|\Gamma|=k$, the
function

$(-\circ_{k}\alpha_{i})_{i\in
I}\quad:\quad\mathcal{E}_{f}(\Theta,R,\Theta^{\prime};S)\longrightarrow\prod_{i\in
I}\mathcal{E}_{f\circ_{k}g_{i}}(\Theta,\Omega_{i},\Theta^{\prime};S)$

induced by precomposition with the elements of the cone is invertible. In this
case, we say that $R$ equipped with the cone
$(\alpha_{i}:\Omega_{i}\ThisStyle{\Rightarrow_{g_{i}}^{q}}R)_{i\in I}$ is a
minimal lift of the cone $(g_{i})_{i\in I}$ to the family of lists of colors
$(\Omega_{i}\ThisStyle{\sqsubset^{q}}\Delta_{i})_{i\in I}$ refining the inputs
of the $g_{i}$’s. Equivalently,
$(\alpha_{i}:\Omega_{i}\ThisStyle{\Rightarrow_{g_{i}}^{q}}R)_{i\in I}$ is a
minimal cone when for every operation $f$ as above and any cone
$(\beta_{i}:\Theta,\Omega_{i},\Theta^{\prime}\ThisStyle{\Rightarrow_{f\circ_{k}g_{i}}^{q}}S)_{i\in
I}$ over the cone $(f\circ_{k}g_{i}:\Gamma,\Delta_{i},\Gamma^{\prime}\to
B)_{i\in I}$, there exists a unique operation
$\bar{\beta}:\Theta,R,\Theta^{\prime}\ThisStyle{\Rightarrow_{f}^{q}}S$ such
that $\beta_{i}=\bar{\beta}\circ_{k}\alpha_{i}$ for all $i\in I$.

In the special case of a singleton family, an operation
$\alpha:\Omega\ThisStyle{\Rightarrow_{g}}R$ of $\mathcal{E}$ is a minimal cone
just in case it is (strongly) opcartesian in the sense of Hermida relative to
a functor of multicategories [Her00, Her04], which extends the classical
notion of opcartesian arrow relative to a functor of categories. In this case,
we say that $R$ is the pushforward of $\Omega$ along $g$, generalizing the
image of a subset along a function. On the other hand, in the special case of
a minimal cone $(\alpha_{i}:R_{i}\ThisStyle{\Rightarrow_{{id_{B}}}}R)_{i\in
I}$ of operations in $\mathcal{E}$ all lying over the same identity operation
in $\mathcal{B}$, we say that $R$ is the fiberwise coproduct of the $R_{i}$,
generalizing the union of subsets of a set. This means in particular that we
have an isomorphism

$\mathcal{E}_{f}(\Theta,R,\Theta^{\prime};S)\cong\prod_{i\in
I}\mathcal{E}_{f}(\Theta,R_{i},\Theta^{\prime};S)$

for every compatible operation $f$. We briefly considered minimal cones in the
same sense (relative to a functor of categories) in [MZ13], there referred to
as “weighted union types”. Definition A is also in a similar spirit to the
very general notion of “extremal cone” recently introduced by Shulman in his
work on LNL polycategories and doctrines of linear logic [Shu], which inspired
our terminology.

Given a cone $(g_{i}:\Gamma_{i}\to A)_{i\in I}$ and a family of lists of
colors $\Omega_{i}\ThisStyle{\sqsubset}\Gamma_{i}$ refining the inputs of the
$g_{i}$’s, there exists at most one minimal lift
$(\alpha_{i}:\Omega_{i}\ThisStyle{\Rightarrow_{g_{i}}^{q}}R)_{i\in I}$ of
$(g_{i})_{i\in I}$ to $(\Omega_{i})_{i\in I}$, up to canonical isomorphism.
Indeed, if $(\alpha_{i}:\Omega_{i}\ThisStyle{\Rightarrow_{g_{i}}}R)_{i\in I}$
and
$(\alpha^{\prime}_{i}:\Omega_{i}\ThisStyle{\Rightarrow_{g_{i}}}R^{\prime})_{i\in
I}$ are two minimal lifts, the universal property immediately implies there is
a unique isomorphism $\bar{\beta}:R\cong R^{\prime}$ in $\mathcal{E}$ lying
over the identity $id_{A}$ in $\mathcal{B}$ such that
$\alpha^{\prime}_{i}=\bar{\beta}\circ\alpha_{i}$ for all $i\in I$. We indicate
the presence of such a canonical isomorphism by $R\equiv R^{\prime}$, and
write $\sum_{i\in I}g_{i}\,\Omega_{i}$ for some choice of object $R$ coming
together with a minimal cone

$\big{(}in_{j}:\Omega_{j}\ThisStyle{\Rightarrow_{g_{j}}}\sum_{i\in
I}g_{i}\,\Omega_{i}\big{)}_{j\in I}$

The notation is motivated by the fact that if the functor
$q:\mathcal{E}\to\mathcal{B}$ has sufficient fibrational structure, then the
minimal lift may be decomposed as a fiberwise coproduct of pushforwards (cf.
[MZ13, p.13], [Shu, Thm. 4.28]).

######  Proposition 45.

Let $q:\mathcal{E}\to\mathcal{B}$ be a functor of operads. The following are
equivalent:

  1. (1)

There is a minimal lift $\sum_{i\in I}g_{i}\,\Omega_{i}\ThisStyle{\sqsubset}A$
of every cone $(g_{i}:\Gamma_{i}\to A)_{i\in I}$ in $\mathcal{B}$ to any
family of lists of colors $\Omega_{i}\ThisStyle{\sqsubset}\Gamma_{i}$ in
$\mathcal{E}$.

  2. (2)

$q$ has all pushforwards and fiberwise coproducts, i.e., for any operation
$g:\Gamma\to A$ and list of colors $\Omega\ThisStyle{\sqsubset}\Gamma$ there
is a pushforward $g\,\Omega\ThisStyle{\sqsubset}A$, and for any family of
colors $(R_{i}\ThisStyle{\sqsubset}A)_{i\in I}$, there is a fiberwise
coproduct $\sum_{i\in I}R_{i}\ThisStyle{\sqsubset}A$.

Moreover, the equivalence holds while maintaining any bound $|I|<\kappa$ on
the cardinalities of the indexing sets of the cones $(g_{i})_{i\in I}$ in (1)
and the families of colors $(R_{i})_{i\in I}$ in (2).

######  Proof A.1.

The implication $(1)\Rightarrow(2)$ is immediate. For the implication
$(2)\Rightarrow(1)$, we build the minimal lift of $(g_{i}:\Gamma_{i}\to
A)_{i\in I}$ to $(\Omega_{i}\ThisStyle{\sqsubset}\Gamma_{i})_{i\in I}$ by
constructing the family of pushforwards
$(R_{i}=g_{i}\,\Omega_{i}\ThisStyle{\sqsubset}A)_{i\in I}$ and taking their
fiberwise coproduct $\sum_{i\in I}R_{i}\ThisStyle{\sqsubset}A$. Since the
indexing set $I$ is left unchanged, existence of minimal lifts of cones of
cardinality $<\kappa$ is equivalent to existence of pushforwards and finite
fiberwise coproducts of cardinality $<\kappa$.

When either of the equivalent conditions of Prop. 45 holds with
$\kappa=\omega$, and moreover $q$ comes equipped with a choice of minimal
lifts, then we say that $q$ has polynomials, or is a “polynomial refinement
system”. The terminology is motivated by the fact that the set of colors of
$\mathcal{E}$ is closed under taking finite sums of monomials weighted by
operations of $\mathcal{B}$, and moreover that such polynomial expressions
satisfy expected laws up to canonical isomorphism.

######  Proposition 46.

The following identities hold

$\displaystyle\sum_{i\in I}\sum_{j\in J}R_{ij}$
$\displaystyle\equiv\sum_{(i,j)\in I\times J}R_{ij}$ (21) $\displaystyle
f(\Theta,\sum_{i\in I}R_{i},\Theta^{\prime})$ $\displaystyle\equiv\sum_{i\in
I}f(\Theta,R_{i},\Theta^{\prime})$ (22) $\displaystyle
f(g_{1}\,\Omega_{1},\dots,g_{n}\,\Omega_{n})$
$\displaystyle\equiv(f\circ(g_{1},\dots,g_{n}))(\Omega_{1},\dots,\Omega_{n})$
(23) $\displaystyle id(R)$ $\displaystyle\equiv R$ (24)

in the sense that whenever the minimal lift on one side exists then so does
the other, with a canonical isomorphism between them.

We are now ready to define models of generalized context-free grammars and
explain the sense in which an initial model provides a minimal solution to a
system of polynomial equations. The definition depends only on the grammar’s
underlying functor $p:\mathcal{F}\,\,\mathbb{S}\to\mathcal{O}$, which we refer
to as a bare gCFG (analogous to the bare NDFA we considered in §2). A model of
an arbitrary functor of operads $p:\mathcal{D}\to\mathcal{O}$ inside another
functor $q:\mathcal{E}\to\mathcal{B}$ is just a commuting square of functors:

${\mathcal{D}}$${\mathcal{E}}$${\mathcal{O}}$${\mathcal{B}}$$\scriptstyle{p}$$\scriptstyle{\tilde{M}}$$\scriptstyle{q}$$\scriptstyle{M}$
(25)

By extension, we say that $(M,\tilde{M})$ is a model of a gCFG $G$ if it is a
model of its underlying bare gCFG $p:\mathcal{F}\,\,\mathbb{S}\to\mathcal{O}$.
Note that the commutative square (25) just says that the pair of functors
$(M,\tilde{M})$ form a _morphism of functors_ from $p$ to $q$, or a _morphism
of refinement systems_ in the terminology of [MZ18]. But sometimes we want
more of a model of a gCFG, namely that the morphism $(M,\tilde{M}):p\to q$
picks out a selection of minimal cones in the following sense. A model
$(M,\tilde{M})$ of a bare gCFG $p:\mathcal{F}\,\,\mathbb{S}\to\mathcal{O}$
(with associated map of species $\phi:\mathbb{S}\to\mathcal{O}$) in
$q:\mathcal{E}\to\mathcal{B}$ is said to be exact if for every color $R$ of
$\mathbb{S}$, the cone of nodes in $\mathbb{S}$ with output color $R$

$\mathbb{S}_{R}=(x:R_{1},\dots,R_{k}\ThisStyle{\Rightarrow_{g}^{\phi}}R)_{x\in\mathbb{S}}$

is mapped to a $q$-minimal cone in $\mathcal{E}$

$\tilde{M}{\mathbb{S}_{R}}=(\tilde{M}x:\tilde{M}{R_{1}},\dots,\tilde{M}{R_{k}}\ThisStyle{\Rightarrow_{M{g}}^{q}}\tilde{M}R)_{x\in\mathbb{S}}.$

Thus, if we express the existence of minimal cones using the sum-of-
pushforward notation introduced above, an exact model $(M,\tilde{M})$ of a
gCFG corresponds to a solution for the system of equations

$\tilde{M}{R}\equiv\sum_{R_{1},\dots,R_{k}\ThisStyle{\Rightarrow_{g}^{\phi}}R}\,M{g}(\tilde{M}{R_{1}},\dots,\tilde{M}{R_{k}})$
(26)

with one such equation for each color of $\mathbb{S}$. Let us emphasize that
although such a solution interprets each non-terminal as the apex of a minimal
cone, the solution itself is not necessarily minimal globally. However, we
will establish as Proposition 48 below that under good conditions (namely,
when $q$ has polynomials), if $(M,\tilde{M})$ is the _initial model_ of $p$ in
$q$, then it is also exact and therefore the initial exact model. To make this
statement precise, we first have to define what are morphisms of models.

Recall that given two functors of operads $L,M:\mathcal{O}\to\mathcal{P}$ with
the same source and target, a _natural transformation_ $\theta:L\Rightarrow M$
is defined as a family of unary operations $\theta_{R}:LR\to MR$ in
$\mathcal{P}$ such that

$M{f}\circ(\theta_{R_{1}},\dots,\theta_{R_{n}})=\theta_{R}\circ
L{f}\quad:\quad L{R_{1}},\dots,L{R_{n}}\longrightarrow M{R}$ (27)

for every operation $f:R_{1},\dots,R_{n}\to R$ in $\mathcal{O}$.

Let $(L,\tilde{L})$ and $(M,\tilde{M})$ be models of $p$ in $q$. A morphism of
models $(L,\tilde{L})\Longrightarrow(M,\tilde{M})$ is given by a pair of
natural transformations $\theta:L\Rightarrow M$ and
$\tilde{\theta}:\tilde{L}\Rightarrow\tilde{M}$ such that the diagram below
commutes

${\mathcal{D}}$${\mathcal{E}}$${\mathcal{O}}$${\mathcal{B}}$$\scriptstyle{p}$$\scriptstyle{\tilde{L}}$$\scriptstyle{\tilde{M}}$$\scriptstyle{q}$$\scriptstyle{L}$$\scriptstyle{M}$$\scriptstyle{\tilde{\theta}}$$\scriptstyle{\theta}$
(28)

in the sense that the natural transformations obtained by whiskering are equal
$q\circ\tilde{\theta}=\theta\circ p$. In other words, a morphism of models is
a _2-morphism_
$(\theta,\tilde{\theta}):(L,\tilde{L})\Longrightarrow(M,\tilde{M}):p\to q$. We
define morphisms of exact models in the same way – that is, we do not impose
any extra conditions. Given two functors of operads $p$ and $q$, we write
$\mathrm{Mod}(p,q)$ for the category of models of $p$ in $q$ and 2-morphisms
between them. Similarly, when $p$ is a bare gCFG, we write
$\mathrm{ExMod}(p,q)$ for the full subcategory of $\mathrm{Mod}(p,q)$ spanned
by the exact models.

Definitions A and A do not require the target $q:\mathcal{E}\to\mathcal{B}$ to
have polynomials. However, when it does, models of a bare gCFG
$p:\mathcal{F}\,\,\mathbb{S}\to\mathcal{O}$ admit an equivalent
characterization as _algebras of an endofunctor_

$(-)^{p}:\mathrm{DiscMod}(p,q)\to\mathrm{DiscMod}(p,q)$

on the category of _discrete models_ of $p$ in $q$, defined by
$\mathrm{DiscMod}(p,q):=\mathrm{Mod}(p\circ incl,q)$, where
$incl:\mathcal{F}\,\,|\mathbb{S}|\to\mathcal{F}\,\,\mathbb{S}$ is the
inclusion from the free operad over the discrete species $|\mathbb{S}|$ with
same set of colors as $\mathbb{S}$ and no nodes. Note that a discrete model
$(M,\tilde{M})$ is the data of a functor $M:\mathcal{O}\to\mathcal{B}$
together with a family of colors $\tilde{M}R\ThisStyle{\sqsubset^{q}}MA$ for
every color $R\ThisStyle{\sqsubset^{p}}A$ of $\mathbb{S}$.

For any discrete model $(M,\tilde{M})$ of a bare gCFG $p$ in $q$, we can
construct a new discrete model $(M,\tilde{M}^{p})$ where the family of colors
$\tilde{M}^{p}{R}$ is defined by the sum of pushforwards:

$\tilde{M}^{p}{R}=\sum_{R_{1},\dots,R_{k}\ThisStyle{\Rightarrow_{g}^{\phi}}R}\,M{g}(\tilde{M}{R_{1}},\dots,\tilde{M}{R_{k}})$

This defines an endofunctor on $\mathrm{DiscMod}(p,q)$ since the pushforward
and fiberwise coproduct are functorial. Moreover, by precomposition with
$incl$, every ordinary model $(M,\tilde{M})$ of $p$ in $q$ has an underlying
discrete model (which we will also denote $(M,\tilde{M})$ for ease of
notation), equipped with a canonical $(-)^{p}$-algebra structure given by the
family of unary operations

$\alpha^{\tilde{M}}_{R}:\tilde{M}^{p}{R}\Rightarrow\tilde{M}{R}$

obtained by applying the universal property of the sum-of-pushforwards to the
cone of operations $\tilde{M}\mathbb{S}_{R}$.

######  Proposition 47.

The assignment of a $(-)^{p}$-algebra structure
$\alpha^{\tilde{M}}:\tilde{M}^{p}\Rightarrow\tilde{M}$ to any model
$(M,\tilde{M})$ of a bare gCFG $p$ in a polynomial refinement system $q$
induces an isomorphism

$\mathrm{Mod}(p,q)\cong{(-)^{p}}\text{-}\mathrm{Alg}$

between the category of models of $p$ in $q$ and the category of algebras for
the endofunctor $(-)^{p}:\mathrm{DiscMod}(p,q)\to\mathrm{DiscMod}(p,q)$. This
restricts to an isomorphism

$\mathrm{ExMod}(p,q)\cong{(-)^{p}}\text{-}\mathrm{Fix}$

between the subcategory of exact models of $p$ in $q$ and the subcategory of
$(-)^{p}$-algebras with an invertible algebra structure.

Since the mapping $(M,\tilde{M})\mapsto(M,\tilde{M}^{p})$ preserves the
underlying interpretation $M:\mathcal{O}\to\mathcal{B}$ of the base operad, it
in fact defines a family of endofunctors

$(-)^{p}_{M}:\mathrm{DiscMod}_{M}(p,q)\to\mathrm{DiscMod}_{M}(p,q)$

where we write $\mathrm{DiscMod}_{M}(p,q)$ for the subcategory of discrete
models of $p$ in $q$ with underlying base interpretation $M$, and with
morphisms between them such that the natural transformation in the bottom part
of (28) is the identity $\theta=id_{M}$. We similarly write
$\mathrm{Mod}_{M}(p,q)$ and $\mathrm{ExMod}_{M}(p,q)$ for the corresponding
subcategories of models and exact models with base interpretation $M$. It
follows from Proposition 47 that we have isomorphisms:

$\displaystyle\mathrm{Mod}_{M}(p,q)$
$\displaystyle\cong{(-)^{p}_{M}}\text{-}\mathrm{Alg}$ (29)
$\displaystyle\mathrm{ExMod}_{M}(p,q)$
$\displaystyle\cong{(-)^{p}_{M}}\text{-}\mathrm{Fix}$ (30)

We can use these alternative characterizations of models of a gCFG to
immediately derive the existence of initial exact models (globally, or with a
given base interpretaion $M$) from the existence of initial models.

######  Proposition 48.

For every bare gCFG $p$ and polynomial refinement system $q$, any initial
object in $\mathrm{Mod}(p,q)$ (respectively, in $\mathrm{Mod}_{M}(p,q)$) is
also an initial object in $\mathrm{ExMod}(p,q)$ (resp.
$\mathrm{ExMod}_{M}(p,q)$).

######  Proof A.2.

By the previous proposition, if $(M,\tilde{M})$ is initial in
$\mathrm{Mod}(p,q)$ then
$\alpha^{\tilde{M}}:\tilde{M}^{p}\Rightarrow\tilde{M}$ is an initial
$(-)^{p}$-algebra. By Lambek’s Lemma, $\alpha^{\tilde{M}}$ is invertible and
hence $(M,\tilde{M})$ is exact, and therefore an initial object of
$\mathrm{ExMod}(p,q)$ since it is a full subcategory of $\mathrm{Mod}(p,q)$.
The same argument works even if $\tilde{M}$ is only initial seen as an object
$(M,\tilde{M})$ of $\mathrm{Mod}_{M}(p,q)$.

Proposition 48 motivates us to introduce the following terminology. Let $G$ be
a gCFG with underlying bare gCFG $p:\mathcal{F}\,\,\mathbb{S}\to\mathcal{O}$
and start symbol $S\ThisStyle{\sqsubset^{p}}A$. Let
$q:\mathcal{E}\to\mathcal{B}$ be a polynomial refinement system, and suppose
that there is an initial model $(M,\tilde{M})$ of $p$ in $q$ (which is hence
unique up to canonical isomorphism by universality, and an exact model by
Prop. 48). We then speak of the $q$-language of $G$, written
$\mathcal{L}_{G}^{q}$, as the interpretation
$\tilde{M}\,S\ThisStyle{\sqsubset^{q}}M\,A$ of the start symbol in this
initial model. Similarly, given a base interpretation functor
$M:\mathcal{O}\to\mathcal{B}$, if $\tilde{M}$ is initial in
$\mathrm{Mod}_{M}(p,q)$, then we speak of the $q$-language relative to $M$ of
$G$, written $\mathcal{L}_{G}^{M,q}$. We will see that the language of
constants of a gCFG in the sense of Def. 1.8 may be recovered as a particular
case of $q$-language, for $q=\mathsf{sub}:\mathrm{Subset}\to\mathrm{Set}$
defined below. However, every gCFG also generates another $q$-language that is
in a sense more canonical, as we now explain.

For any operad $\mathcal{P}$, there is an operad ${\mathcal{P}}^{\to}$ whose
colors are given by the unary operations $u$ of $\mathcal{P}$, and whose
$n$-ary operations $u_{1},\dots,u_{n}\to u$ are given by pairs $(f_{s},f_{t})$
of $n$-ary operations of $\mathcal{P}$ such that
$f_{t}\circ(u_{1},\dots,u_{n})=u\circ f_{s}$. This operad comes equipped with
two evident functors
$\mathsf{src},\mathsf{tgt}:{\mathcal{P}}^{\to}\to\mathcal{P}$ defined by first
and second projection. In the case $\mathcal{P}=\mathrm{Set}$, the operad
${\mathrm{Set}}^{\to}$ has unary functions $f:Y\to X$ as colors.

######  Proposition 49.

$\mathsf{tgt}:{\mathrm{Set}}^{\to}\to\mathrm{Set}$ has polynomials, with
pushforwards and fiberwise coproducts constructed as follows:

  * •

Let $u_{1}:Y_{1}\to X_{1},\dots,u_{n}:Y_{n}\to X_{n}$ be an $n$-tuple of unary
functions, and let $f:X_{1},\dots,X_{n}\to X$ be an $n$-ary function. The
pushforward of $(u_{1},\dots,u_{n})$ along $f$ is given by their parallel
composition $f\circ(u_{1},\dots,u_{n})$, interpreted as a unary function from
the cartesian product $Y_{1}\times\dots\times Y_{n}\to X$.

  * •

Let $(u_{i}:Y_{i}\to X)_{i\in I}$ be a collection of unary functions into the
same set. Their fiberwise coproduct is given by the cotupling $[u_{i}]_{i\in
I}:\coprod_{i\in I}Y_{i}\to X$.

Now, every operad $\mathcal{O}$ comes equipped with a canonical functor

$\mathop{\mathrm{con}_{\mathcal{O}}}{}:\mathcal{O}\to\mathrm{Set}$

(we omit the subscript when clear from context) defined on colors by taking
$\mathop{\mathrm{con}}A=\mathcal{O}(\cdot;A)=\\{\,{c\mid c:A}\,\\}$ to be the
set of constants of color $A$ in $\mathcal{O}$, and on operations
$f:A_{1},\dots,A_{n}\to B$ by taking $\mathop{\mathrm{con}}f$ to be the
function $(c_{1},\dots,c_{n})\mapsto f\circ(c_{1},\dots,c_{n})$ that sends any
$n$-tuple of constants to the constant defined by parallel composition into
the inputs of $f$. For example, in the case of an operad of spliced arrows,
$\mathop{\mathrm{con}}:\mathcal{W}\,{\mathcal{C}}\to\mathrm{Set}$ sends a
color $(A,B)$ to the homset $\mathcal{C}(A,B)$, and an operation
$w_{0}{-}\dots-w_{n}:(A_{1},B_{1}),\dots,(A_{n},B_{n})\to(A,B)$ to the
function

$\mathop{\mathrm{con}}(w_{0}{-}\dots-
w_{n}):\mathcal{C}(A_{1},B_{1})\times\dots\times\mathcal{C}(A_{n},B_{n})\to\mathcal{C}(A,B)$

that maps an $n$-tuple of arrows $(u_{1},\dots,u_{n})$ to their spliced
composition $w_{0}u_{1}w_{1}\dots u_{n}w_{n}$. A functor
$\mathcal{O}\to\mathrm{Set}$ is also called an “operad algebra”, and an
important property of $\mathop{\mathrm{con}_{\mathcal{O}}}$ is that it is the
initial $\mathcal{O}$-algebra, in the sense that it has a unique natural
transformation $!_{M}:\mathop{\mathrm{con}_{\mathcal{O}}}\Rightarrow M$ to any
other functor $M:\mathcal{O}\to\mathrm{Set}$. This natural transformation is
defined by the family of functions $\mathop{\mathrm{con}}A\to MA$ sending a
constant $c:A$ of $\mathcal{O}$ to the element $Mc$ of $MA$ determined by the
algebra structure.

For any functor of operads $p:\mathcal{D}\to\mathcal{O}$, we can therefore
build a triangle

${\mathcal{D}}$${\mathrm{Set}}$${\mathcal{O}}$$\scriptstyle{p}$$\scriptstyle{\mathop{\mathrm{con}_{\mathcal{D}}}}$$\scriptstyle{\mathop{\mathrm{con}_{\mathcal{O}}}}$$\scriptstyle{\mathop{\mathrm{con}_{p}}}$
(31)

where the natural transformation
$\mathop{\mathrm{con}_{p}}={}!_{\mathop{\mathrm{con}_{\mathcal{O}}}\circ\,p}$
is uniquely determined by initiality of $\mathop{\mathrm{con}_{\mathcal{D}}}$.
Concretely, $\mathop{\mathrm{con}_{p}}$ is given by the family of functions
sending any constant in $\mathcal{D}$ to the corresponding constant in
$\mathcal{O}$ obtained by mapping along the functor $p$. Now, in general,
giving a natural transformation $\theta:L\Rightarrow
M:\mathcal{O}\to\mathcal{P}$ is equivalent to giving a functor
$\tilde{\theta}:\mathcal{O}\to{\mathcal{P}}^{\to}$ such that
$\mathsf{src}\circ\tilde{\theta}=L$ and $\mathsf{tgt}\circ\tilde{\theta}=M$.
In particular, the natural transformation (31) induces a functor
$\mathop{\widetilde{\mathrm{con}}_{p}}:{\mathcal{D}}\to{\mathrm{Set}}^{\to}$
making the below square commute:

${{\mathcal{D}}}$${{\mathrm{Set}}^{\to}}$${\mathcal{O}}$${\mathrm{Set}}$$\scriptstyle{p}$$\scriptstyle{\mathop{\widetilde{\mathrm{con}}_{p}}}$$\scriptstyle{\mathsf{tgt}}$$\scriptstyle{\mathop{\mathrm{con}_{\mathcal{O}}}}$
(32)

######  Proposition 50.

The morphism
$(\mathop{\mathrm{con}_{\mathcal{O}}},\mathop{\widetilde{\mathrm{con}}_{p}}):p\to\mathsf{tgt}$
is an initial object in $\mathrm{Mod}(p,\mathsf{tgt})$.

######  Proof A.3.

Let $M:\mathcal{O}\to\mathrm{Set}$ and
$\tilde{M}:{\mathcal{D}}\to{\mathrm{Set}}^{\to}$ be any pair of functors
forming a morphism $(M,\tilde{M}):p\to\mathsf{tgt}$. A 2-morphism
$(\theta,\tilde{\theta}):(\mathop{\mathrm{con}_{\mathcal{O}}},\mathop{\widetilde{\mathrm{con}}_{p}})\Rightarrow(M,\tilde{M}):p\to\mathsf{tgt}$
is given by a pair of natural transformations
$\theta:\mathop{\mathrm{con}_{\mathcal{O}}}\Rightarrow M$ and
$\tilde{\theta}:\mathop{\widetilde{\mathrm{con}}_{p}}\Rightarrow\tilde{M}$
such that $\mathsf{tgt}\circ\tilde{\theta}=\theta\circ p$, or equivalently a
pair $\theta:\mathop{\mathrm{con}_{\mathcal{O}}}\Rightarrow M$ and
$\rho:\mathop{\mathrm{con}_{\mathcal{D}}}\Rightarrow\mathsf{src}\circ\tilde{M}$
which combined with the natural transformations
$\mathop{\mathrm{con}_{\mathcal{D}}}\Rightarrow
p\circ\mathop{\mathrm{con}_{\mathcal{O}}}$ and
$\mathsf{src}\circ\tilde{M}\Rightarrow p\circ M$ form a family of commutative
squares

${\mathop{\mathrm{con}}R}$${\mathsf{src}(\tilde{M}{R})}$${\mathop{\mathrm{con}}A}$${M{A}}$$\scriptstyle{\rho_{R}}$$\scriptstyle{\theta_{A}}$
(33)

in $\mathrm{Set}$ for every color $R\ThisStyle{\sqsubset}A$ of $\mathcal{D}$.
But such a pair of natural transformations $\theta$ and $\rho$ exist uniquely
by initiality of $\mathop{\mathrm{con}_{\mathcal{O}}}$ and
$\mathop{\mathrm{con}_{\mathcal{D}}}$ respectively, while the square (33)
commutes by initiality of $\mathop{\mathrm{con}_{\mathcal{D}}}$ since it is a
composite of natural transformations.

######  Corollary 51.

Every bare gCFG generates an initial model in
$\mathsf{tgt}:{\mathrm{Set}}^{\to}\to\mathrm{Set}$.

In the case of a categorical CFG, the initial model in $\mathsf{tgt}$
interprets every non-terminal $R\ThisStyle{\sqsubset}(A,B)$ as the set
$\mathop{\mathrm{con}}R$ of parse trees with root label $R$, equipped with the
function

$\mathop{\mathrm{con}_{p}}R\ \ :\
\mathop{\mathrm{con}_{\mathcal{F}\,\,\mathbb{S}}}R\longrightarrow\mathcal{C}(A,B)$

mapping a tree $\alpha:R$ to the underlying arrow
$p(\alpha)\in\mathcal{C}(A,B)$ that it derives. In particular, the language
$\mathcal{L}_{G}^{\mathsf{tgt}}=\mathop{\mathrm{con}}(S)\to\Sigma^{*}$
generated by an ordinary context-free grammar may be considered as a kind of
“proof-relevant” language, in the sense that it encodes not just a subset of
words generated by $G$ but also the set of parse trees of every word in the
language. Notably, a given word may have more than one derivation, and all of
those distinct derivations are incorporated into its $\mathsf{tgt}$-language.

To recover the language generated by a grammar in the traditional sense,
consider next the operad $\mathrm{Subset}$ whose colors are pairs $(X,U)$ of a
set $X$ and of a subset $U\subseteq X$, and whose operations
$f:(X_{1},U_{1}),\dots,(X_{n},U_{n})\to(X,U)$ are functions
$f:X_{1}\times\dots\times X_{n}\to X$ such that

$x_{1}\in U_{1},\dots,x_{n}\in U_{n}$ implies $f(x_{1},\dots,x_{n})\in U$.

$\mathrm{Subset}$ comes equipped with an evident forgetful functor
$\mathsf{sub}:\mathrm{Subset}\to\mathrm{Set}$ sending any subset $(X,U)$ to
its base $X$.

######  Proposition 52.

$\mathsf{sub}$ has pushforwards and fiberwise coproducts, given respectively
by taking the image of an $n$-tuple of subsets $R_{1}\subseteq
X_{1},\dots,R_{n}\subseteq X_{n}$ along an $n$-ary function
$f:X_{1},\dots,X_{n}\to X$ to define the subset $f(R_{1},\dots,R_{n})\subseteq
X$, and by taking the union $\bigcup_{i\in I}R_{i}\subseteq X$ of a collection
of subsets $(R_{i}\subseteq X)_{i\in I}$ of the same set. In particular,
$\mathsf{sub}$ has polynomials.

Moreover, there is a morphism of refinement systems from $\mathsf{tgt}$ to
$\mathsf{sub}$,

${{\mathrm{Set}}^{\to}}$${\mathrm{Subset}}$${\mathrm{Set}}$$\scriptstyle{\mathsf{tgt}}$$\scriptstyle{\mathop{\mathrm{im}}}$$\scriptstyle{\mathsf{sub}}$

given by the functor
$\mathop{\mathrm{im}}:{\mathrm{Set}}^{\to}\to\mathrm{Subset}$ which sends any
function $u:X\to Y$ to its image $u(X)\subseteq Y$, and every pair
$(f_{s},f_{t})$ of functions $f_{s}:X_{1}\times\dots\times X_{n}\to X$ and
$f_{t}:Y_{1}\times\dots\times Y_{n}\to Y$ defining an operation
$u_{1},\dots,u_{n}\to u$ of ${\mathrm{Set}}^{\to}$ to the function $f_{t}$,
which does indeed, by the naturality equation
$f_{t}\circ(u_{1},\dots,u_{n})=u\circ f_{s}$, satisfy that

$x_{1}\in u_{1}(X_{1}),\dots,x_{n}\in u_{n}(X_{n})$ implies
$f_{t}(x_{1},\dots,x_{n})\in u(X)$.

Observe that this morphism $\mathsf{tgt}\to\mathsf{sub}$ has a right adjoint

${{\mathrm{Set}}^{\to}}$${\mathrm{Subset}}$${\mathrm{Set}}$$\scriptstyle{\mathsf{tgt}}$$\scriptstyle{\mathop{\mathrm{im}}}$$\scriptstyle{\mathsf{sub}}$${\bot}$
(34)

given by the functor interpreting a subset $U\subseteq X$ as a monic function
$U\to X$.

######  Corollary 53.

The composite morphism

${\mathcal{F}\,\,\mathbb{S}}$${{\mathrm{Set}}^{\to}}$${\mathrm{Subset}}$${\mathcal{O}}$${\mathrm{Set}}$${\mathrm{Set}}$$\scriptstyle{p}$$\scriptstyle{\mathop{\widetilde{\mathrm{con}}_{p}}}$$\scriptstyle{\mathsf{tgt}}$$\scriptstyle{\mathop{\mathrm{im}}}$$\scriptstyle{\mathsf{sub}}$$\scriptstyle{\mathop{\mathrm{con}_{\mathcal{O}}}}$
(35)

generates an initial model of any bare gCFG $p$ in $\mathsf{sub}$.

######  Proof A.4.

Since postcomposition with the morphism
$\mathop{\mathrm{im}}:\mathsf{tgt}\to\mathsf{sub}$ induces a functor

$\mathrm{Mod}(p,\mathop{\mathrm{im}}):\mathrm{Mod}(p,\mathsf{tgt})\to\mathrm{Mod}(p,\mathsf{sub})$

which is a left adjoint, and as a left adjoint it preserves initial objects.

In the case of a classical context-free grammar $G$ with associated functor
$p:\mathcal{F}\,\,\mathbb{S}\to\mathcal{W}\,{\Sigma}$, the
$\mathsf{sub}$-language is precisely the traditional language
$\mathcal{L}_{G}^{\mathsf{sub}}=\mathcal{L}_{G}\subseteq\Sigma^{*}$ generated
by the grammar, and more generally for a gCFG with start symbol
$S\ThisStyle{\sqsubset}A$ one recovers the language of constants
$\mathcal{L}_{G}\subseteq\mathop{\mathrm{con}}A$ in the sense of Def. 1.8 as
the $\mathsf{sub}$-language. Equations such as (19) and (20) are automatically
satisfied as instances of the master equation (26), by virtue of the fact that
the initial model in $\mathsf{sub}:\mathrm{Subset}\to\mathrm{Set}$ is exact
(Prop. 48) and the concrete description of the pushforward and fiberwise
coproduct as image and union.

Both of these languages in $\mathsf{tgt}$ and $\mathsf{sub}$ can also be
adapted relative to a fixed interpretation of the base operad
$M:\mathcal{O}\to\mathrm{Set}$ by pushing forward the respective initial
models along the unique natural transformation
$!_{M}:\mathop{\mathrm{con}_{\mathcal{O}}}\Rightarrow M$. Abstractly, this may
be seen as a consequence of the fact that both $\mathsf{tgt}$ and
$\mathsf{sub}$ are bifibrations, so that any natural transformation
$\theta:L\Rightarrow M$ induces an adjunction

${\mathrm{Mod}_{L}(p,q)}$${\mathrm{Mod}_{M}(p,q)}$$\scriptstyle{\mathop{\theta_{*}}}$$\scriptstyle{\mathop{\theta^{*}}}$${\bot}$
(36)

between the respective categories of models (for $q=\mathsf{tgt}$ and
$\mathsf{sub}$), and as a left adjoint the pushforward functor
$\mathop{\theta_{*}}$ preserves initial objects. Concretely, in the case of
$\mathsf{tgt}$, the language relative to $M$ interprets a gCFG $G$ with start
symbol $S\ThisStyle{\sqsubset}A$ as the composite arrow

${\mathcal{L}_{G}^{M,\mathsf{tgt}}\quad:=\quad\mathop{\mathrm{con}_{\mathcal{F}\,\,\mathbb{S}}}{S}}$${\mathop{\mathrm{con}_{\mathcal{O}}}{A}}$${M(A)}$

mapping every closed derivation $\alpha:S$ in $\mathcal{F}\,\,\mathbb{S}$ to
the interpretation $M(c)$ of the constant $c=p(\alpha):A$ in $\mathcal{O}$
that it derives.

For one more example of a $q$-language relative to a base interpretation, let
us recall the notion of _Chomsky algebra_ introduced by Grathwohl, Henglein,
and Kozen [GHK17], defined as an idempotent semiring that is algebraically
closed in the sense that every finite system of polynomial inequalities over
the semiring has a least solution in the semiring. It is possible to associate
a polynomial refinement system to any idempotent semiring, as follows. Given
an arbitrary (not necessarily idempotent) semiring $(R,+,\cdot,0,1)$, one can
construct an operad $\mathcal{R}$ equipped with a functor
$\pi_{R}:\mathcal{R}\to\mathcal{W}\,{(R,\cdot,1)}$ into the operad of spliced
arrows over its underlying multiplicative monoid seen as a one-object
category. The operad $\mathcal{R}$ has elements of $R$ as colors, and
operations $x_{1},\dots,x_{n}\to y$ given by spliced elements
$a_{0}{-}a_{1}{-}\dots-a_{n}$ such that $a_{0}x_{1}a_{1}\dots x_{n}a_{n}\leq
y$, for the natural ordering defined by $x\leq y$ iff $\exists a.x+a=y$. The
functor $\pi_{R}$ always has pushforwards, given by spliced multiplication.
When $+$ is idempotent, $\pi_{R}$ will moreover have fiberwise coproducts,
corresponding to joins with respect to $\leq$, and hence yield a polynomial
refinement system.

Now, suppose given a gCFG $G=(\mathcal{O},\mathbb{S},S,p)$, a Chomsky algebra
$(R,+,\cdot,0,1)$, and a functor $M:\mathcal{O}\to\mathcal{W}\,{(R,\cdot,1)}$.
(Most commonly, i.e., for a classical CFG, $\mathcal{O}$ will be
$\mathcal{F}\,\,\mathbb{B}_{\Sigma}$ and $M$ will be derived from a function
$\Sigma\to R$ assigning every letter of the alphabet an element of the
semiring.) Any model of $G$ in $\pi_{R}$ with base interpretation $M$ is a
solution to a finite system of polynomial inequalities determined by the
production rules of $G$ and by the functor $M$. Hence there is an initial
model by the defining assumption on a Chomsky algebra, i.e.,
$\mathcal{L}_{G}^{M,\pi_{R}}$ exists.

To conclude this preliminary exploration of the concept of $q$-language, we
will now explain how some mild conditions on $q$ suffice to guarantee the
existence of initial models, as well as to establish abstract versions of both
the weak and strong translation principles. Although we are focused on
modelling gCFGs, much of the story makes sense at a greater level of
generality. Thus suppose given three functors of operads
$p_{1}:\mathcal{D}_{1}\to\mathcal{O}$, $p_{2}:\mathcal{D}_{2}\to\mathcal{O}$
and $T:\mathcal{D}_{1}\to\mathcal{D}_{2}$ defining a commutative diagram

${{\mathcal{D}_{1}}}$${{\mathcal{D}_{2}}}$${{\mathcal{O}}}$$\scriptstyle{T}$$\scriptstyle{p_{1}}$$\scriptstyle{p_{2}}$
(37)

in the category $\mathop{\mathsf{Oper}}$, which we summarize by writing
$T:p_{1}\to p_{2}$. For any fixed functor of operads
$M:\mathcal{O}\to\mathcal{B}$, precomposition with $T$ induces a functor of
categories

${\mathop{T^{*}}\quad:\quad\mathrm{Mod}_{M}(p_{2},q)}$${\mathrm{Mod}_{M}(p_{1},q)}$

which transports every model $(M,\tilde{M}):p_{2}\to q$ to the model
$(M,\tilde{M}\circ T):p_{1}\to q$. Now, our aim is to show that under certain
conditions on $q$, the functor $\mathop{T^{*}}$ has a left adjoint
$\mathop{T_{*}}$. Hence, we will be in a situation where every functor
$T:p_{1}\to p_{2}$ as above induces an adjunction

${\mathrm{Mod}_{M}(p_{1},q)}$${\mathrm{Mod}_{M}(p_{2},q)}$$\scriptstyle{\mathop{T_{*}}}$$\scriptstyle{\mathop{T^{*}}}$${\bot}$
(38)

between the corresponding categories of $q$-models relative to $M$, from which
we will be able to extract various important consequences.

A sufficient condition for the existence of this left adjoint is that $q$ has
pushforwards and has all (small) _fiberwise colimits,_ in the natural sense
generalizing fiberwise coproducts. Formally, we say that a functor
$q:\mathcal{E}\to\mathcal{B}$ has fiberwise colimits when any diagram
$D:J\to\mathcal{E}_{X}$ of unary operations lying in the fiber over some
object $X\in\mathcal{B}$ has a colimit
$(\mathop{\underline{\mathsf{colim}}}D,(in_{i}:D(i)\to\mathop{\underline{\mathsf{colim}}}{D})_{i\in
D})$ in the fiber category $\mathcal{E}_{X}$, and moreover the universal
property of this colimiting cocone extends to the total operad in the sense
that precomposition with the $in_{i}$ induces a bijection

$\mathcal{E}_{f}(\Theta,\mathop{\underline{\mathsf{colim}}}{D},\Theta^{\prime};S)\cong\lim\mathcal{E}_{f}(\Theta,D(-),\Theta^{\prime};S)$

for every compatible operation $f$ of $\mathcal{B}$. (Note that if $q$ is an
opfibration, then it has fiberwise colimits just in case every fiber category
$\mathcal{E}_{X}$ is cocomplete and all of the pushforward functors
$\mathop{f_{*}}:\mathcal{E}_{X_{1}}\times\dots\times\mathcal{E}_{X_{n}}\to\mathcal{E}_{X}$
are cocontinuous.)

######  Proposition 54.

Assume that $q:\mathcal{E}\to\mathcal{B}$ has pushforwards and fiberwise
colimits. Let $p_{1}$, $p_{2}$, $T$, and $M$ be as above. Then the pullback
functor $\mathop{T^{*}}:\mathrm{Mod}_{M}(p_{2},q)\to\mathrm{Mod}_{M}(p_{1},q)$
has a left adjoint
$\mathop{T_{*}}:\mathrm{Mod}_{M}(p_{1},q)\to\mathrm{Mod}_{M}(p_{2},q)$.

Before proving the proposition by showing how to construct the left adjoint,
let us describe a few of its consequences.

_Existence of $q$-languages for all gCFGs._ Suppose given any gCFG
$G=(\mathcal{O},\mathbb{S},S,p)$ and a base interpretation
$M:\mathcal{O}\to\mathcal{B}$. Start by constructing an initial model
$\tilde{M}$ of the underlying “discrete” grammar
$|G|=(\mathcal{O},|\mathbb{S}|,S,p\circ incl)$, where
$incl:\mathcal{F}\,\,|\mathbb{S}|\to\mathcal{F}\,\,\mathbb{S}$ is the
inclusion functor we described earlier. (Viewed as a grammar, $|G|$ has the
same non-terminals and start symbol as $G$, but no production rules.) To
construct the initial model of $|G|$ relative to $M$, it suffices to take
$\tilde{M}$ to map every non-terminal $R\ThisStyle{\sqsubset^{p}}A$ to the
initial object $0_{M\,A}\in\mathcal{E}_{M\,A}$ of the appropriate fiber. Then
we push $\tilde{M}$ forward along $incl$. Since left adjoints preserve initial
objects, $\mathop{incl_{*}}\tilde{M}$ will be an initial model of $p$, and we
have $\mathcal{L}_{G}^{M,q}:=\mathop{incl_{*}}\tilde{M}\,S$.

_Translation principles._ Suppose given a pair of gCFGs
$G_{1}=(\mathcal{O},\mathbb{S}_{1},S_{1},p_{1})$ and
$G_{2}=(\mathcal{O},\mathbb{S}_{2},S_{2},p_{2})$ over the same operad,
together with a translation $T:G_{1}\to G_{2}$ in the sense of Definition 1.4.
Fix a base interpretation $M:\mathcal{O}\to\mathcal{B}$. By the preceding, we
know that there exist functors
$\tilde{M}_{1}:\mathcal{F}\,\,\mathbb{S}_{1}\to\mathcal{E}$ and
$\tilde{M}_{2}:\mathcal{F}\,\,\mathbb{S}_{2}\to\mathcal{E}$ such that
$\tilde{M}_{1}$ and $\tilde{M}_{2}$ are initial objects in
$\mathrm{Mod}_{M}(p_{1},q)$ and $\mathrm{Mod}_{M}(p_{2},q)$ respectively.
Initiality of $\tilde{M}_{1}$ implies that there exists a unique morphism of
models $\theta:\tilde{M}_{1}\Rightarrow\mathop{T^{*}}\tilde{M}_{2}$, as
depicted below:

${\mathcal{F}\,\,\mathbb{S}_{2}}$${\mathcal{F}\,\,\mathbb{S}_{1}}$${\mathcal{E}}$${\mathcal{O}}$${\mathcal{B}}$$\scriptstyle{p_{2}}$$\scriptstyle{\tilde{M}_{2}}$$\scriptstyle{p_{1}}$$\scriptstyle{T}$$\scriptstyle{\tilde{M}_{1}}$$\scriptstyle{q}$$\scriptstyle{M}$$\scriptstyle{\theta}$
(39)

Instantiating this natural isomorphism at $S_{1}$ and applying the assumption
that $T$ preserves the start symbol, we immediately obtain a morphism

${\mathcal{L}_{G_{1}}^{M,q}\equiv\tilde{M}_{1}(S_{1})}$${\tilde{M}_{2}(T\,S_{1})=\tilde{M}_{2}(S_{2})\equiv\mathcal{L}_{G_{2}}^{M,q}}$$\scriptstyle{\theta_{S_{1}}}$
(40)

in the fiber category $\mathcal{E}_{M\,A}$, where
$p_{1}(S_{1})=p_{2}(S_{2})=A$. This may be seen as a categorification of the
weak translation principle, reducing to
$\mathcal{L}_{G_{1}}\subseteq\mathcal{L}_{G_{2}}$ in the case that
$q=\mathsf{sub}$ and $M=\mathop{\mathrm{con}_{\mathcal{O}}}$. Moreover, we
know (again since pushforward preserves initial objects) that $\tilde{M}_{2}$
is isomorphic to the pushforward of $\tilde{M}_{1}$ along $T:p_{1}\to p_{2}$,
and that $\theta$ is equal to the composition of this isomorphism
$\mathop{T_{*}}\tilde{M}_{1}\cong\tilde{M}_{2}$ with the unit
$\eta:\tilde{M}_{1}\Rightarrow\mathop{T^{*}}\mathop{T_{*}}\tilde{M}_{1}$ of
the adjunction (38), as depicted below:

${\mathcal{F}\,\,\mathbb{S}_{2}}$${\mathcal{F}\,\,\mathbb{S}_{1}}$${\mathcal{E}}$${\mathcal{O}}$${\mathcal{B}}$$\scriptstyle{p_{2}}$$\scriptstyle{\mathop{T_{*}}\tilde{M}_{1}}$$\scriptstyle{p_{1}}$$\scriptstyle{T}$$\scriptstyle{\tilde{M}_{1}}$$\scriptstyle{q}$$\scriptstyle{M}$$\scriptstyle{\eta}$
(41)

The last piece of the puzzle will be to show that when the functor $T$ is
fully faithful then $\eta$ is invertible, although this relies on an explicit
formula for the pushforward functor $\mathop{T_{*}}\tilde{M}_{1}$. From
invertibility of $\eta$, we derive an isomorphism of $q$-languages

${\mathcal{L}_{G_{1}}^{M,q}\equiv\tilde{M}_{1}(S_{1})}$${\mathop{T^{*}}\mathop{T_{*}}\tilde{M}_{1}(S_{1})\cong\tilde{M}_{2}(S_{2})\equiv\mathcal{L}_{G_{2}}^{M,q}}$$\scriptstyle{\eta_{S_{1}}\atop\sim}$
(42)

which may be seen as a categorification of the strong translation
principle.888Indeed, in Proposition 5 we already tried to state the strong
translation principle in a proof-relevant way, by mentioning that the grammars
generate “isomorphic sets of parse trees for the arrows in the language”.
Formally, this is really an instance of the strong translation principle for
$q$-languages, with $q=\mathsf{tgt}$!

Diagram (41) is suggestive of a Kan extension, and indeed the computation that
we describe below of the pushforward model $\mathop{T_{*}}\tilde{M}_{1}$ may
be seen as a kind of fibered and operadic generalization of the usual
construction of the left Kan extension
$\mathop{\mathrm{Lan}_{F}}{G}:\mathcal{C}_{2}\to\mathcal{E}$ of a functor of
categories $G:\mathcal{C}_{1}\to\mathcal{E}$ along another functor of
categories $F:\mathcal{C}_{1}\to\mathcal{C}_{2}$, as a pointwise colimit in
$\mathcal{E}$. The strong translation principle may then be seen as a
generalization of the fact that if $F$ is fully faithful, then the unit 2-cell
$\eta:G\Rightarrow\mathop{\mathrm{Lan}_{F}}{G}\circ F$ of such a pointwise
left Kan extension is invertible [Mac98, Corollary X.3.3, p.239].

######  Proof A.5 (Proof of Proposition 54.).

We suppose given an arbitrary commutative triangle of functors of operads
$T:p_{1}\to p_{2}$ as in (37) above, together with a target functor
$q:\mathcal{E}\to\mathcal{B}$ that we assume to have pushforwards and
fiberwise colimits, and a fixed base interpretation functor
$M:\mathcal{O}\to\mathcal{B}$. We also suppose given an arbitrary (not
necessarily initial) model of $p_{1}$ in $q$ relative to $M$, corresponding to
a functor $\tilde{M}:\mathcal{D}_{1}\to\mathcal{E}$ such that
$q\circ\tilde{M}=M\circ p_{1}$. Our aim is to construct a functor
$\mathop{T_{*}}\tilde{M}:\mathcal{D}_{2}\to\mathcal{E}$ defining a model of
$p_{2}$ in $q$ relative to $M$, equipped with a universal morphism of models
$\eta:\tilde{M}\Rightarrow\mathop{T^{*}}\mathop{T_{*}}\tilde{M}$, as depicted
below:

${\mathcal{D}_{2}}$${\mathcal{D}_{1}}$${\mathcal{E}}$${\mathcal{O}}$${\mathcal{B}}$$\scriptstyle{p_{2}}$$\scriptstyle{\mathop{T_{*}}\tilde{M}}$$\scriptstyle{p_{1}}$$\scriptstyle{T}$$\scriptstyle{\tilde{M}}$$\scriptstyle{q}$$\scriptstyle{M}$$\scriptstyle{\eta}$
(43)

To define $\mathop{T_{*}}\tilde{M}$, we map each color
$R\ThisStyle{\sqsubset^{p_{2}}}A$ of $\mathcal{D}_{2}$ to the fiberwise
colimit

$\mathop{T_{*}}\tilde{M}\,R\quad:=\quad\mathop{\underline{\mathsf{colim}}}{D_{R}^{\tilde{M}}}$
(44)

of a certain diagram

$D_{R}^{\tilde{M}}\quad:\quad T/R\longrightarrow\mathcal{E}_{M\,A}$

defined as follows. The (relative) “operadic slice” category $T/R$ has objects
given by tuples

$(R_{1},\dots,R_{n};\alpha)$

consisting of a sequence of colors $R_{1},\dots,R_{n}$ of $\mathcal{D}_{1}$
and an operation $\alpha:TR_{1},\dots,TR_{n}\to R$ of $\mathcal{D}_{2}$, and
arrows

$(\gamma_{1},\dots,\gamma_{k}):(R_{1},\dots,R_{n};\alpha)\longrightarrow(S_{1},\dots,S_{k};\beta)$

given by a sequence of operations $\gamma_{1}:\Gamma_{1}\to
S_{1},\dots,\gamma_{k}:\Gamma_{k}\to S_{k}$ of $\mathcal{D}_{1}$ such that
$\alpha=\beta\circ(T\gamma_{1},\dots,T\gamma_{k})$ (which implies that
$\Gamma_{1},\dots,\Gamma_{k}$ is a composition of $R_{1},\dots,R_{n}$ into $k$
parts). The functor $D_{R}^{\tilde{M}}$ is defined on objects by the
pushforward formula

$D_{R}^{\tilde{M}}(R_{1},\dots,R_{n};\alpha)\quad:=\quad
M{g}(\tilde{M}{R_{1}},\dots,\tilde{M}{R_{n}})$ (45)

where $g=p_{2}(\alpha)$ is the underlying image of $\alpha$ in $\mathcal{O}$.
(This pushforward is well-defined and gives an object in the fiber
$\mathcal{E}_{M\,A}$, by the assumption that $\alpha:TR_{1},\dots,TR_{n}\to R$
and that $p_{1}=p_{2}\circ T$ and $q\circ\tilde{M}=M\circ p_{1}$.) It extends
to the arrows of $T/R$ by applying the action of $\tilde{M}$ on operations of
$\mathcal{D}_{1}$, as well as the laws of pushforwards. Finally,
$\mathop{T_{*}}\tilde{M}$ extends to a functor $\mathcal{D}_{2}\to\mathcal{E}$
by the functoriality of the slicing construction $T/-$ and the fact that
pushforwards preserve fiberwise colimits.

Now, the natural transformation $\eta$ is given by taking

${\eta_{R}\quad:=\quad\tilde{M}R\cong
Mid_{A}(\tilde{M}R)}$${\mathop{\underline{\mathsf{colim}}}{D_{R}^{\tilde{M}}}}$
(46)

to be the canonical injection into the colimit associated to the object
$(R,id_{TR})$ of $T/R$, composed with a canonical isomorphism of the form (24)
(since $Mid_{A}=id_{MA}$). Universality says that any model
$\tilde{L}:p_{2}\to q$ over $M$ equipped with a morphism of models
$\theta:\tilde{M}\Rightarrow\mathop{T^{*}}\tilde{L}$ factors uniquely via
$\eta$ and a morphism of models
$\theta^{\prime}:\mathop{T_{*}}\tilde{M}\Rightarrow\tilde{L}$. The latter
corresponds to a natural family of arrows

$\theta_{R}^{\prime}\quad:\quad\mathop{\underline{\mathsf{colim}}}{D_{R}^{\tilde{M}}}\Longrightarrow\tilde{L}\,R$

in $\mathcal{E}_{M\,A}$ for every color $R\ThisStyle{\sqsubset^{p_{2}}}A$ of
$\mathcal{D}_{2}$, the definition of which is entirely forced by the universal
property of the colimit, the definition of the diagram $D_{R}^{\tilde{M}}$,
and the input morphism $\theta:\tilde{M}\Rightarrow\mathop{T^{*}}L$.

We now make two remarks by inspection of the formula for the pushforward model
$\mathop{T_{*}}\tilde{M}$. First, when the functor
$T:\mathcal{D}_{1}\to\mathcal{D}_{2}$ is fully faithful, the relative slice
category $T/TR$ is isomorphic to the slice category $\mathcal{D}_{1}/R$ for
every color $R$ of $\mathcal{D}_{1}$. In particular, $(R,id_{TR})$ is a
terminal object of $T/TR$ when $T$ is fully faithful. From this follows that
the unit $\eta_{R}$ defined by (46) is invertible, and as a consequence we get
the strong translation principle (42).

Second, although we assumed that $q$ has all fiberwise colimits, clearly the
cardinalities of the indexing categories $T/R$ of the colimit diagrams are
bounded to an extent by the cardinalities of $\mathcal{D}_{1}$ and
$\mathcal{D}_{2}$. In particular, it suffices for $q$ to have _countable_
fiberwise colimits to be able to define the pushforward

${\mathop{T_{*}}\quad:\quad\mathrm{Mod}_{M}(p_{1},q)}$${\mathrm{Mod}_{M}(p_{2},q)}$

induced by a translation $T:G_{1}\to G_{2}$ between any pair of gCFGs, since
the respective operads $\mathcal{D}_{1}=\mathcal{F}\,\,\mathbb{S}_{1}$ and
$\mathcal{D}_{2}=\mathcal{F}\,\,\mathbb{S}_{2}$ are freely generated from
finite species.

We summarize the situation below.

######  Corollary 55.

Let $q:\mathcal{E}\to\mathcal{B}$ be a functor with pushforwards and countable
fiberwise colimits. Then every gCFG $G$ over an operad $\mathcal{O}$ generates
a $q$-language $\mathcal{L}_{G}^{M,q}$ relative to any base interpretation
$M:\mathcal{O}\to\mathcal{B}$. Moreover, $q$-languages enjoy both the weak and
the strong translation principles, as expressed by the morphism (40) and the
isomorphism (42).

Of course it remains to establish the expected closure properties for
$q$-gCFLs (cf. Proposition 9), and to show that the class of $q$-gCFLs
interacts as expected with an appropriately formulated class of $q$-regular
languages (cf. Corollary 35), which we leave as (unsolved!) exercises for the
reader. We hope to have demonstrated that there is some interest in this
slightly more abstract way of thinking about the languages generated by
context-free grammars, complementary to the more concrete approach taken in
the main body of the paper.

###### Contents

  1. 1 Context-free languages of arrows in a category
    1. 1.1 Preliminaries on free operads and species
    2. 1.2 The operad of spliced arrows of a category
    3. 1.3 Context-free grammars over a category
    4. 1.4 Properties of a context-free grammar and its associated language
    5. 1.5 A fibrational view of parsing as a lifting problem
    6. 1.6 An inductive formula and a sequent calculus for displayed free operads
    7. 1.7 Application to parsing
    8. 1.8 Generalized context-free grammars
    9. 1.9 Related work
  2. 2 Finite state automata over categories and operads
    1. 2.1 Non-deterministic word automata as finitary ULF functors over categories
    2. 2.2 From word automata to tree automata and beyond
    3. 2.3 Additional properties of ULF and finitary functors
    4. 2.4 Closure properties of regular languages
    5. 2.5 Related work
  3. 3 The Chomsky-Schützenberger Representation Theorem
    1. 3.1 Pulling back context-free grammars along finite state automata
    2. 3.2 The contour category of an operad and the contour / splicing adjunction
    3. 3.3 The universal context-free grammar of a pointed species, and its associated tree contour language
    4. 3.4 Representation theorem
    5. 3.5 Related work
  4. 4 Conclusion
  5. A gCFLs as initial models of gCFGs