Dieses Kapitel untersucht die Ausweitung kontextfreier Sprachen auf monoide Kategorien, aufbauend auf den etablierten algebraischen Strukturen von Monoiden und Kategorien. Es stellt das Konzept der String-Diagramme vor, die als grafische Syntax für monoidale Kategorien dienen, und untersucht ihre Rolle in der formalen Sprachtheorie. Der Text vertieft sich in den algebraischen Rahmen monoider Kategorien und hebt deren intuitive und vollständige grafische Darstellung hervor. Es stellt eine neuartige Klasse kontextfreier monoidaler Sprachen vor, die traditionelle kontextfreie Sprachen verallgemeinern und verschiedene erweiterte Begriffe aus der Informatik-Literatur erfassen. Das Kapitel diskutiert auch die Beziehung zwischen kontextfreien Sprachen in Kategorien und monoiden Kategorien und liefert ein Darstellungstheorem, das verschiedene Verallgemeinerungen kontextfreier Sprachen vereint. Anhand detaillierter Beispiele und strenger Beweise bietet das Kapitel eine umfassende Untersuchung des Zusammenspiels zwischen grafischer Syntax und formalen Sprachen im Kontext monoider Kategorien und leistet damit einen bedeutenden Beitrag auf dem Gebiet der Sprachtheorie und Kategorientheorie.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
We introduce context-free languages of morphisms in monoidal categories, extending recent work on the categorification of context-free languages, and regular languages of string diagrams. Context-free languages of string diagrams include classical context-free languages of words, trees, and hypergraphs, when instantiated over appropriate monoidal categories. We prove a representation theorem for context-free languages of string diagrams: every such language arises as the image under a monoidal functor of a regular language of string diagrams.
1 Introduction
Monoids are the classical algebraic home of formal languages, and a long line of research beginning in the 60s has sought to extend the tools and concepts of language theory to other algebraic structures, such as trees [24, 44], traces [14], hypergraphs [12, 26, 45], models of algebraic theories [20, 49], algebras for monads [3, 4], and categories [2, 50].
Categories are “monoids with many objects”, and passing from the theory of context-free languages in monoids to the theory of context-free languages in categories has been the subject of recent work by Melliès and Zeilberger [35, 36]. This novel structural point of view suggests a natural generalization to categories with additional structure. Here, we pursue this idea for monoidal categories. On the one hand, strict monoidal categories are two-dimensional monoids, and so a natural step from their one-dimensional counterpart. On the other hand, they have a natural graphical syntax, string diagrams, providing a fresh approach to languages of graphs.
Anzeige
A vast literature has explored language theory in various algebras of graphs, culminating in the celebrated results of Courcelle [12]. Our point of departure is the claim that many graphical notions can be naturally viewed as morphisms in monoidal categories; that is, monoidal categories provide a suitable algebraic framework for graphical formal languages. This manuscript pursues this idea in the context of recent work in the foundations of language theory which takes a structural approach to context-freeness. Ultimately, this line of work seeks to unify the various generalizations of context-free languages, and identify reusable tools for reasoning about them.
1.1 Languages of string diagrams
Monoidal categories have an intuitive, sound and complete graphical syntax: string diagrams. String diagrams resemble graphical languages commonly found in engineering and science, and indeed, they allow us to reason about Markov kernels [23], linear algebra [6], or quantum processes [1]. In computer science, they provide foundations for visual programming [29, 31].
The use of string diagrams as a syntax in these various domains suggests the need for a corresponding theory of string diagrams as a formal language. This is one aim of recent work on languages of string diagrams or monoidal languages, such as that elaborated by Sobociński and the first author [17, 18], who introduced the class of regular monoidal languages. A monoidal language in this sense is simply a subset of morphisms in a strict monoidal category, just as a classical formal language is a subset of a monoid. In this work, we introduce a natural class of context-free monoidal languages, which capture various extended notions of context-free language found in the computer science literature.
1.2 Context-free languages over categories
Our main point of reference in this paper is the recent work of Melliès and Zeilberger [35, 36]. This work is a thoroughgoing refashioning of the theory of context-free languages from a “fibrational” point of view. Melliès and Zeilberger demonstrate that it is natural and fruitful to consider context-free languages over arbitrary categories. They introduce an adjunction between splicing (introducing gaps or contexts in terms) and contouring (linearizing derivation trees), and use it to give a novel conceptual proof of the Chomsky-Schützenberger representation theorem: every context-free language is the image of the intersection of a regular language and the language of balanced parentheses [9].
Anzeige
Melliès and Zeilberger provide an ample supply of examples of context-free languages in categories, such as context-free languages of runs over an automaton, languages with an explicit end-of-input marker, multiple context-free grammars [46] and a grammar of series-parallel graphs. However, it is less clear how notions such as context-free grammars of trees and hypergraphs fit into this framework. In this paper, we show how this can be accomplished by adapting the machinery of Melliès and Zeilberger to the wider setting of monoidal categories and their string diagrams. This generalization is non-trivial, and sheds light on the intriguing differences between languages of string diagrams and classical languages. In particular, our two-dimensional version of the Chomsky-Schützenberger representation theorem says that every context-free language of string diagrams is the image under a monoidal functor of a regular language of string diagrams: no intersection of context-free and regular languages is necessary.
Related work Bruggink and König have investigated recognizable languages of morphisms in a category using a notion of automaton functor [8], which is similar to our notion of non-deterministic monoidal automaton. Similar ideas have also been investigated by Colcombet and Petrisan [11]. Griffing has also introduced a notion of recognizable set of morphisms in a category [25]. These works deal with languages over categories, rather than monoidal categories.
The representation of context-free grammars as certain morphisms of multigraphs was introduced by Walters in a short paper [51]. A similar type-theoretical version of this idea was also introduced by De Groote [13]. As discussed more extensively above, this idea was taken up and substantially refined by Melliès and Zeilberger, first in a conference paper [35] and later in an extended version [36].
A different notion of context-free families of string diagrams has been introduced by Zamdzhiev [52]. There, string diagrams are defined combinatorially as string graphs, and context-free families are then generated by B-edNCE graph grammars [45]. Though similar, the resulting notion is not directly comparable to ours. Here, we use the native algebra of monoidal categories and their multicategories of contexts to define and investigate languages.
Finally, Heindel’s abstract [27] claims a proof of a Chomsky-Schützenberger theorem for morphisms in symmetric monoidal categories, but the work described in this abstract was never published. Our development is quite different from that outlined in Heindel’s abstract. We prove a stronger representation theorem that does not require an intersection of languages; we work without the assumption of symmetry; and we generalize the categorical machinery of Melliès and Zeilberger.
Contributions We introduce context-free languages of string diagrams (Definition 4.12) and show that they include a wide variety of examples in the computer science literature including context-free languages of trees and hypergraphs. We introduce the category of raw optics (Definition 5.1) over a monoidal category, and its left adjoint, the optical contour (Definition 5.5, Theorem 5.6). We use this machinery to prove a representation theorem for context-free monoidal languages (Theorem 6.6), relating them to previous work on regular monoidal languages.
2 Preliminaries
In this paper, we define context-free grammars as particular morphisms of multigraphs. This point of view, while perhaps unfamiliar, is simple and powerful. It suggests natural generalizations of context-free grammars, such as we will pursue in the main body of the paper, and new conceptual tools for reasoning about them. This idea is not original to us; its roots go back to Walters [51], with recent refinement and extension by Melliès and Zeilberger [35, 36].
2.1 Context-free languages in free monoids and other categories
We introduce the definition of context-free grammars as morphisms of certain multigraphs. Multigraphs (or species in the work of Melliès and Zeilberger [36]) are a kind of graph in which edges have a list of sources and single target. It is often helpful to think of a multigraph as a signature, specifying a set of typed operations. Note that this is a different use of the term multigraph from that specifying graphs allowing multiple parallel edges.
Definition 2.1
A multigraphM is a set S of sorts, and sets \(M(X_1,...,X_n;Y)\) of generating operations (or multimorphisms), for each pair of a list of sorts \(X_1,...,X_n\) and a sort Y. A multigraph is finite if sorts and operations are finite sets. A morphism of multigraphs is given by a function f on sorts and functions \(M(X_1,...,X_n;Y) \rightarrow M(fX_1, ..., fX_n; fY)\) between sets of operations.
Multigraphs freely generate multicategories, also known as operads (though this term sometimes refers only to the single-sorted, symmetric case). See Leinster [34] for a comprehensive reference on multicategories. The free multicategory \(\mathcal {F}_{\triangledown }{M}\) over a multigraph M has as multimorphisms \(\mathcal {F}_{\triangledown }{M}(X_1, ..., X_n; Y)\) the “trees” rooted at Y, with open leaves \(X_1, ..., X_n\), that one can build by “plugging together” operations in M. We call closed trees, i.e. nullary multimorphisms \(d \in \mathcal {F}_{\triangledown }{M}(; Y)\), derivations. Every multicategory \(\mathbb {M}\) has an underlying multigraph, denoted \(|{\mathbb {M}}|\), given by forgetting identities and composition.
Every rule in a context-free grammar is of the form \(R \rightarrow w_1R_1...R_{n-1}w_{n}\), where \(R,R_i\) are non-terminals, and \(w_i\) are (possibly empty) words over an alphabet \(\varSigma \). The insight of Melliès and Zeilberger [36] is that this data may be arranged as an operation \(R_1,...,R_n \rightarrow R\) in a multigraph over an n-ary operation \(w_1-...-w_n\) called a spliced word: a word with n gaps, as in Figure 1. We introduce the multicategory of spliced arrows in a category.
Definition 2.2
(Melliès and Zeilberger [36]). The multicategory of spliced arrows, \(\mathscr {W}{\mathbb {C}}\), over a category \(\mathbb {C}\), contains, as objects, pairs of objects of \(\mathbb {C}\), denoted as \({\begin{array}{c} A \\ B \end{array}}\). Its multimorphisms are morphisms of the original category, but with n “gaps” or “holes”, into which other morphisms (with holes) may be spliced. More precisely, the multimorphisms of \(\mathscr {W}{\mathbb {C}}\) are given by:
By convention, nullary multimorphisms are morphisms of \(\mathbb {C}\), that is \(\mathscr {W}{\mathbb {C}}(;{\begin{array}{c} X \\ Y \end{array}}) := \mathbb {C}(X;Y)\). The identity is given by a pair of identities of the original category, multicategorical composition is derived from the composition of the original category.
Fig. 1.
(Left) Generic form of a context-free rule. (Right) Context-free rules as a morphism of multigraphs into spliced arrows; here, spliced arrows in a monoid.
We can now present a context-free grammar in terms of a morphism of multigraphs from a multigraph of non-terminals to the underlying multigraph of spliced arrows, as in Figure 1.
Definition 2.3
(Melliès and Zeilberger [36]). A context-free grammar of morphisms in a category \(\mathbb {C}\) is a morphism of multigraphs \(G \rightarrow |\mathscr {W}{\mathbb {C}}|\) and a sort S in G (the start symbol).
By the free-forgetful adjunction between multicategories and multigraphs, morphisms \(\phi : G \rightarrow |\mathscr {W}{\mathbb {C}}|\) and morphisms of multicategories (or multifunctors) \(\widehat{\phi } : \mathcal {F}_{\triangledown }{G} \rightarrow \mathscr {W}{\mathbb {C}}\) are in bijection. This allows for a slick definition of the language of a grammar.
Definition 2.4
(Melliès and Zeilberger [36]). Let \(\mathcal {G} = (\phi : G \rightarrow |\mathscr {W}{\mathbb {C}}|, S)\) be a context-free grammar of morphisms in \(\mathbb {C}\). The language of \(\mathcal {G}\) is given by the image of the set of derivations \(\mathcal {F}_{\triangledown }{G}(;S)\) under the multifunctor \(\widehat{\phi }\).
When \(\mathbb {C}\) is a finitely generated free monoid considered as a one-object category, then context-free grammars over \(\mathbb {C}\) correspond precisely to the classical context-free grammars.
An important realization of Melliès and Zeilberger is that the operation of forming the multicategory of spliced arrows in \(\mathbb {C}\) has a left adjoint. That is, every multicategory gives rise to a category called the contour of \(\mathbb {M}\), and this contouring operation is left adjoint to splicing. We refer to their paper for more details [36, Section 3.2]. Contours give a conceptual replacement for Dyck languages in the classical theory of context-free languages: they linearize derivation trees.
In Section 5, we define a new contour of multicategories which we call the optical contour; we shall use it to prove a representation theorem for languages of string diagrams (Theorem 6.6), inspired by generalized Chomsky-Schützenberger representation theorem proved by Melliès and Zeilberger.
2.2 Monoidal categories, their string diagrams and languages
In this paper, we will mostly be concerned with monoidal categories presented by generators and equations between the string diagrams built from these generators. Generators are given by polygraphs.
Definition 2.5
A polygraph\(\varGamma \) is a set \(S_\varGamma \) of sorts, and sets \(\varGamma (X_1\otimes ...\otimes X_n; Y_1\otimes ...\otimes Y_m)\) of generators for every pair of lists \(X_i, Y_j\) of sorts. A polygraph is finite if sorts and generators are finite sets. A morphism of polygraphs is a function f on sorts and functions \(\varGamma (X_1\otimes ...\otimes X_n; Y_1\otimes ...\otimes Y_m) \rightarrow \varGamma (fX_1\otimes ...\otimes fX_n; fY_1\otimes ...\otimes fY_m)\) between generators.
Fig. 2.
The free strict monoidal category over a polygraph \(\varGamma \) has set of objects \(S_\varGamma ^{*}\) and morphisms string diagrams given inductively over the generators of \(\varGamma \) as above quotiented by the equivalence relation generated by planar isotopy of diagrams, keeping left and right boundaries fixed. The leftmost rule denotes the empty diagram. We use colours to indicate sorts.
For a generator \(\gamma \) of arity \(X_1\otimes ...\otimes X_n\) and coarity \(Y_1\otimes ...\otimes Y_m\) we write \(\gamma : X_1 \otimes ... \otimes X_n \rightarrow Y_1 \otimes ... \otimes Y_m\). When S is single-sorted, we use natural numbers for the arities and coarities; this case will cover most of the examples in the following. We depict generators as boxes with strings on the left and right for their arities and coarities (Figure 2).
Proposition 2.6
String diagrams with generators in a polygraph construct a monoidal category (Figure 2). The monoidal category of string diagrams over a polygraph is the free strict monoidal category over the polygraph [30, 47]. Every monoidal category is equivalent to a strict one. In particular, string diagrams are sound and complete for monoidal categories.
We shall need to impose equations between string diagrams, such as in defining symmetric monoidal categories, cartesian monoidal categories and hypergraph categories. To this end, we introduce the following notion of presentation.
Definition 2.7
A finite presentation of a strict monoidal category consists of a finite polygraph of generators, \(\mathcal {P}\), and a finite polygraph of equations, \(\mathcal {E}\), with projections for the two sides of each equation, \(l,r : \mathcal {E} \rightarrow |{\mathcal {F}_{\otimes }{\mathcal {P}}}|\). The strict monoidal category presented by \((\mathcal {P},\mathcal {E},l,r)\), is defined as the free strict monoidal category generated by \(\mathcal {P}\) and quotiented by the equations in \(\mathcal {E}\); in other words, the equalizer of the two projections \(l^{*}, r^{*} : \mathcal {F}_{\otimes }{\mathcal {E}} \rightarrow \mathcal {F}_{\otimes }{\mathcal {P}}\).
For the soundness and completeness of string diagrams, see Joyal and Street [30]. For a survey of string diagrams for monoidal categories, see Selinger [47].
Definition 2.8
A monoidal language or language of string diagrams is a subset of morphisms in a strict monoidal category.
3 Regular Monoidal Languages
Before introducing context-free monoidal languages, we introduce the regular case, which shall play an important role in Section 6. Regular monoidal languages were introduced by Sobociński and the first author [17, 18], following earlier work of Bossut and Heindel [7, 28]. They are defined by a simple automaton model, reminiscent of tree automata. In a regular monoidal language, the alphabet is given by a finite polygraph.
Definition 3.1
A non-deterministic monoidal automaton comprises: a finite polygraph \(\varGamma \) (the alphabet); a finite set of states Q; for each generator \(\gamma : n \rightarrow m\) in \(\varGamma \), a transition function \(\varDelta _\gamma : Q^n \rightarrow \mathscr {P}(Q^m)\); and initial and final state vectors \(i, f \in Q^{*}\).
Example 3.2
Classical non-deterministic finite state automata arise as monoidal automata over single-sorted polygraphs in which every generator has arity and coarity 1. Bottom-up regular tree automata [24] arise precisely from monoidal automata over single-sorted polygraphs in which every generator has coarity 1 and arbitrary arity, with initial state the empty word and final state a singleton.
A finite state automaton over an alphabet \(\varSigma \) accepts elements of the free monoid \(\varSigma ^{*}\). A monoidal automaton over a polygraph \(\varGamma \) accepts morphisms in the free monoidal category \(\mathcal {F}_{\otimes }{\varGamma }\) over \(\varGamma \). Let us see some examples before giving the formal definition of the accepted language. We depict the transitions of a monoidal automaton as elements of a polygraph with strings labelled by states, and generators labelled by the corresponding element of \(\varGamma \).
Example 3.3
Consider the following polygraph containing generators (left, below) for an opening and closing parenthesis, and the monoidal automaton over this polygraph with \(Q = \{S,M\}\), \(i = f = S\), and transitions shown below, centre. An accepting run over this automaton is shown below, right. The string diagram accepted by this run is what we obtain by erasing the states from this picture.
It is clear that the language accepted by this automaton is exactly the “balanced parentheses”, but note that this is not a language of words, since we use an extra string to keep track of opening and closing parentheses. This principle will play an important role in our representation theorem in Section 6. Roughly speaking, this extra wire arises from the optical contour of a string language of balanced parentheses.
Example 3.4
In the field of DNA computing, Rothemund, Papadakis and Winfree demonstrated self-assembly of Sierpiński triangles from DNA tiles [43]. Sobociński and the first author [17] showed how to recast the tile model as a regular monoidal language over a polygraph containing two tile generators (white and grey), along with start and end generators, as in Figure 3. Note that the start (end) generators have arity (coarity) 0, and hence effect a transition from (to) the empty word of states.
Fig. 3.
Transitions for the Sierpiński monoidal automaton (left) and an element of the language (right). The initial and final states are the empty word.
Transitions of a non-deterministic monoidal automaton over \(\varGamma \) extend inductively to string diagrams in \(\mathcal {F}_{\otimes }{\varGamma }\), giving functions \(\hat{\delta }_{n,m} : Q^n \times \mathcal {F}_{\otimes }{\varGamma }(n,m) \rightarrow \mathscr {P}(Q^m)\).
Definition 3.5
A string diagram \(s : n \rightarrow m\) in the free monoidal category \(\mathcal {F}_{\otimes }{\varGamma }\) over a polygraph \(\varGamma \) is in the language of a non-deterministic monoidal automaton \((\{\varDelta _\gamma \}_{\gamma \in \varGamma }, i, f)\) if and only if the run over s reaches the final state, \(f \in \hat{\delta }_{n,m}(i, s)\).
Definition 3.6
A monoidal language L is a regular monoidal language if and only if there exists a non-deterministic monoidal automaton accepting L.
The data of a monoidal automaton is equivalent to a morphism of finite polygraphs, which we call a regular monoidal grammar, following Walters’ [51] use of the term grammar when data is presented as fibered over an alphabet, and automata when the alphabet indexes transitions as in Definition 3.1. We shall use this convenient presentation in the following.
Definition 3.7
A regular monoidal grammar is a morphism of finite polygraphs \(\psi : \mathbb {Q} \rightarrow \varGamma \), equipped with finite initial and final sorts \(i,f \in S_\mathbb {Q}^{*}\). The morphisms in \(\mathcal {F}_{\otimes }{\mathbb {Q}}(i,f)\) are derivations in the grammar, and their image under the free monoidal functor \(\mathcal {F}_{\otimes }{\psi }\) is the language of the grammar; a subset of morphisms in \(\mathcal {F}_{\otimes }{\varGamma }\).
Proposition 3.8
For every non-deterministic monoidal automaton there is a regular monoidal grammar with the same language, and vice-versa.
Proof
(Sketch). From the transitions \(\varDelta _\gamma \subseteq Q^n \times Q^m\) of a monoidal automaton, we can build a polygraph \(\mathbb {Q}\) by taking a generator \(\gamma _i : q_1 \otimes ... \otimes q_n \rightarrow q'_1 \otimes ... \otimes q'_m\) for each \(((q_1, ..., q_n), (q'_1, ..., q'_m)) \in \varDelta _\gamma \). The morphism of polygraphs \(\psi : \mathbb {Q} \rightarrow \varGamma \) simply maps \(\gamma _i\) to \(\gamma \). The reverse is analogous.
Not every monoidal language is a regular monoidal language. The following is an example.
Proposition 3.9
Let \(\varGamma \) be the polygraph containing two generators: one for “over-braiding”
and one for “under-braiding”
. The language of unbraids on two strings over \(\varGamma \), i.e. diagrams equivalent under planar isotopy to untangled strings, is not a regular monoidal language.
Proof
(Sketch). We can use the pumping lemma for regular monoidal languages [19, Lemma 5.1], with \(k=2\). The argument is analogous to that for classical languages of balanced parentheses: every over-braiding or under-braiding must be eventually balanced with its opposite.
In the next section, we introduce context-free monoidal languages and we shall see that unbraids fall in this class. In Section 6, we prove a surprising representation theorem: every context-free monoidal language is the image under a monoidal functor of a regular monoidal language.
Remark 3.10
As defined, regular monoidal languages are subsets of free strict monoidal categories: we shall need only this case in order to prove our main theorem. Context-free monoidal languages will be defined over arbitrary strict monoidal categories, so this raises the question of extending the regular case to monoidal categories that are not free. We suggest this can be done by a generalization of Melliès and Zeilberger’s definition of finite-state automata over a category as finitary unique lifting of factorizations functors [36, Section 2].
4 Context-Free Monoidal Languages
We now turn our attention to context-free grammars over monoidal categories. The multicategory of spliced arrows is defined for any category. However, for categories equipped with a monoidal structure, it is natural to consider more general kinds of holes than allowed by the spliced arrows construction (Figure 4). Rather than tuples of disjoint pieces, we should allow the possibility that a hole can be surrounded by strings. The necessity of considering these more general holes is forced upon us by various examples that could not be captured using spliced arrows (e.g. Examples 4.14 and 4.15). Proofs omitted from this section may be found in the full version [15].
4.1 The symmetric multicategory of diagram contexts
Context-free monoidal grammars should contain productions from a variable to an incomplete diagram containing multiple variables or “holes”. This section constructs diagram contexts over an arbitrary polygraph. Diagram contexts represent the incomplete derivation of a monoidal term: as such, they consist of string diagrams over which we add “holes”. We shall notate these holes in string diagrams as pink boxes (e.g. Figure 4).
Fig. 4.
(Left) A spliced arrow is a tuple of morphisms. (Right) In a monoidal category, there is the possibility of more general holes, which do not split a morphism into disjoint pieces.
Substituting another diagram context inside a hole induces a symmetric multicategorical structure on the diagrams: symmetry means that we do not distinguish the specific order in which the holes appear. This allows us to avoid declaring a particular ordering of holes when defining a context-free monoidal grammar. We could achieve this by introducing a rule that allows us to permute contexts. However, this breaks the correspondence between terms and derivations. Instead, we shall use shufflings, inspired by the work of Shulman [48].
Definition 4.1
A shuffling of two lists, \(\varPsi \in \textrm{Shuf}(\varGamma ,\varDelta )\) is any list \(\varPsi \) that contains the elements of both \(\varGamma \) and \(\varDelta \) in any order but preserving the relative orders of \(\varGamma \) and \(\varDelta \).
For instance, if
and
, a shuffling is
, but not
. The theory of diagram contexts will introduce a shuffling every time it mixes two contexts: this way, if a term was derived by combining two contexts, we can always reorder these contexts however we want. For instance, the term
was derived from composing the axioms
and
; by choosing a different shuffling, we can also derive the term
. Let us now formally introduce the theory.
Definition 4.2
The theory of diagram contexts
over a polygraph, \(\mathcal {P}\), is described by the following logic. This logic contains objects (\(A,B,C,... \in \mathcal {P}_{obj}^{*}\)) that consist of lists of types of the polygraph, \(X,Y,Z,... \in \mathcal {P}_{obj}\); it also contains contexts \((\varGamma ,\varDelta ,\varPsi ,...)\) that consist of lists of pairs of objects. Apart from the single variables (x, y, z, ..) and the generators of the polygraph (f, g, h, ...); we consider fully formed terms \((t_1,t_2,...)\).
denotes the concatenation of lists. Every term in a given context has a unique derivation. We consider terms up to \(\alpha \)-equivalence and we impose the following equations over the terms whenever they are constructed over the same context:
Proposition 4.3
The multicategory of derivable sequents in the theory of diagram contexts is symmetric. In logical terms, exchange is admissible in the theory of diagram contexts: whenever we can prove that a diagram context exists under certain context \(\varGamma \), we can prove that it exists under a permutation of \(\varGamma \).
Proposition 4.4
Derivable sequents in the theory of diagram contexts over a polygraph \(\mathcal {P}\) form the free strict monoidal category over the polygraph extended with special “hole” generators, \(\mathcal {P} + \{ h_{A,B} : A \rightarrow B \mid A , B \mid \mathcal {P}_{obj}^{*} \}\). Derivable sequents over the empty context form the free strict monoidal category over the polygraph \(\mathcal {P}\). Moreover, there exists a symmetric multifunctor
interpreting each monoidal term as its derivable sequent.
Remark 4.5
Various notions of “holes in a monoidal category” exist in the literature, under names such as optics, contexts, or wiring diagrams [38, 40]. Hefford and the authors [16, 41] gave a universal characterization of the produoidal category of optics over a monoidal category. This produoidal structure is useful for describing decompositions of diagrams. The above logic generates a multicategory similar to the operad of directed, acyclic wiring diagrams introduced by Patterson, Spivak and Vagner [38]; whose operations are generic morphism shapes, rather than holes in a specific monoidal category.
Definition 4.6
A symmetric multigraph is a multigraph G equipped with bijections \(\sigma ^{*} : G(X_1, ..., X_n; Y) \cong G(X_{\sigma (1)}, ..., X_{\sigma (n)}; Y)\) for every list \(X_1,...,X_n\) of sorts and every permutation \(\sigma \), satisfying
and \(\textsf{id} ^{*} = \textsf{id} \). A morphism of symmetric multigraphs is a morphism of multigraphs which commutes with the bijections.
Definition 4.7
Every multigraph, M, freely induces a symmetric multigraph, \(\textsf{clique}(M)\), with the same objects and, for each \(f \mid M(X_1,...,X_n;Y)\), a clique of elements
connected by symmetries, meaning that \(\sigma ^{*}(f_{\tau }) = f_{\sigma \cdot \tau }\). This is the left adjoint to the inclusion of symmetric multigraphs into multigraphs.
Remark 4.8
Given any symmetric multigraph G, finding a multigraph M whose clique recovers it, \(\textsf{clique}(M) = G\), amounts to choosing a representative for each one of the cliques of the multigraph. Any symmetric multigraph can be (non-uniquely) recovered in this way: for each multimorphism \(f \mid G(X_1,...,X_n;Y)\), we can consider its orbit under the action of the symmetric group, \(\textsf{orb}(f) = \{\sigma ^{*}(f) \mid \sigma \in S_n\}\) – the orbits of different elements may coincide, but each element does have one – and picking an element \(g_o\) for each orbit, \(o \mid \{\textsf{orb}(f) \mid f \mid G\}\), recovers a multigraph giving rise to the original symmetric multigraph.
Definition 4.9
The theory of diagram contexts over a finitely presented monoidal category, \((\mathcal {P},\mathcal {E},l,r)\) (Definition 2.7), is the theory of diagram contexts over its generators, quotiented by its equations; in other words, it is the equalizer of the two projections of each equation, interpreted as derivable sequents
.
Proposition 4.10
The formation of diagram contexts in a monoidal category or polygraph extends to functors
and
, which moreover commute with the free multicategory \(\mathcal {F}_{\triangledown } \) and free monoidal category functors \(\mathcal {F}_{\otimes } \).
At this point, the reader may doubt that the formation of diagram contexts has a left adjoint similar to the contour functor for spliced arrows. Indeed, in order to recover a left adjoint, we shall need to introduce another multicategory of diagrams which we call raw optics. This technical device will allow us to prove our main theorem (Theorem 6.6). However, let us first see the definition of context-free monoidal grammar, and some examples.
4.2 Context-Free Monoidal Grammars
We now have the ingredients for our central definition. A context-free monoidal grammar specifies a language of string diagrams by a collection of rewrites between diagram contexts, where the non-terminals of a context-free grammar are now (labelled) holes in a diagram (e.g. Figure 8). Our definition is entirely analogous to Definition 2.3, but using our new symmetric multicategory of diagram contexts in a monoidal category, instead of spliced arrows.
Definition 4.11
A context-free monoidal grammar over a strict monoidal category \((\mathbb {C},\otimes ,I)\) is a morphism of symmetric multigraphs
, into the underlying multigraph of diagram contexts in \(\mathbb {C}\), where \(\mathcal {G}\) is finite, and a start sort \(S \in \mathcal {G}\).
We shall use the notation \(S \sqsubset {\begin{array}{c} A \\ B \end{array}}\) to indicate that \(\varPsi (S) = {\begin{array}{c} A \\ B \end{array}}\), following the convention in the literature [36]. A morphism of symmetric multigraphs
defining a grammar uniquely determines, via the free-forgetful adjunction, a symmetric multifunctor
, mapping (closed) derivations to morphisms of \(\mathbb {C}\). The language of a grammar is then defined analogously to Definition 2.4:
Definition 4.12
Let
be a context-free monoidal grammar. The language of \(\varPsi \) is the set of morphisms in \(\mathbb {C}(A;B)\) given by the image under \(\hat{\varPsi }\) of the set of derivations \(\mathcal {F}_{\triangledown }{\mathcal {G}}(;S)\). A set of morphisms L in \(\mathbb {C}\) is a context-free monoidal language if and only if there exists a context-free monoidal grammar whose language is L.
Example 4.13
(Classical context-free languages). Every context-free monoidal grammar of the following form is equivalent to a classical context-free grammar of words. Let \(\varGamma \) be a single-sorted finite polygraph whose generators are all of arity and coarity 1. Then context-free monoidal grammars over \(\mathcal {F}_{\otimes }{\varGamma }\) with a start symbol \(\phi (S) \sqsubset {\begin{array}{c} 1 \\ 1 \end{array}}\) are context-free grammars of words over \(\varGamma \). Figure 5 gives the classical example of balanced parentheses. Similarly, every context-free grammar of words may be encoded as a context-free monoidal grammar in this way.
Fig. 5.
Balanced parentheses as a context-free monoidal grammar.
Example 4.14
(Context-free tree grammars).Context-free tree grammars [24, 44] are defined over ranked alphabets of terminals and non-terminals, which amount to polygraphs in which the generators have arbitrary arity (the rank) and coarity 1. Productions have the form \(A(x_1, ..., x_m) \rightarrow t\) where the left hand side is a non-terminal of rank m whose frontier is labelled by the variables \(x_i\) in order, and whose right hand side is a tree t built from terminals and non-terminals, and whose frontier is labelled by variables from the set \(\{x_1, ..., x_m\}\). Note that t may use the variables non-linearly.
For example, let S be a non-terminal with arity 0, A a non-terminal with arity 2, f a terminal of arity 2, and x a terminal of arity 0 (a leaf). Then a possible rule over these generators is \(A(x_1, x_2) \rightarrow f(x_1 , A(x_1,x_2))\), where \(x_1\) appears non-linearly. In order to allow such non-linear use of variables in a context-free monoidal grammar, we can consider the free cartesian category over \(\varGamma \). In terms of string diagrams, this amounts to introducing new generators for copying (
) and deleting variables (
).
Let \(\varGamma \) be a polygraph in which generators have arbitrary arity, and coarity 1, as above. Context-free monoidal grammars over the free cartesian category on \(\varGamma \), with a start symbol \(S \sqsubset {\begin{array}{c} 0 \\ 1 \end{array}}\) are context-free tree grammars. In Figure 6 we extend the above data to a full example. Note that by allowing start symbols \(S \sqsubset {\begin{array}{c} 0 \\ n \end{array}}\), we can produce forests of n trees.
Fig. 6.
Example of a context-free tree grammar as a context-free monoidal grammar. The string diagrams at the bottom are equal in the free cartesian category over the polygraph of terminals.
Fig. 7.
A hypergraph grammar for simple control flow graphs with branching and looping, as a context-free monoidal grammar. Based on Habel [26, Example 3.3].
Example 4.15
(Hyperedge-replacement grammars). Hyperedge-replacement (HR) grammars are a kind of context-free graph grammar [12]. We consider HR grammars in normal form in the sense of Habel [26, Theorem 4.1]. A production \(N \rightarrow R\) of an HR grammar has N a non-terminal with arity and coarity, and R a hypergraph with the same arity and coarity1, whose hyperedges are labelled by some finite set of terminals and non-terminals. Just as trees are morphisms in free cartesian monoidal categories (Example 4.14), hypergraphs are the morphisms of monoidal categories equipped with extra structure, known as hypergraph categories [5, 22, 42]. Generators in a polygraph are exactly directed hyperedges. The extra structure in a hypergraph category, amounts to a combinatorial encoding of patterns of wiring between nodes.
Let \(\varGamma \) be a polygraph of terminal hyperedges, G a multigraph of non-terminal rules, and \(S \in G\) a start symbol. Then context-free monoidal grammars \((G \rightarrow |{\textsf {Hyp}[\varGamma ]}|, S)\) over the free hypergraph category on \(\varGamma \) are exactly hyperedge replacement grammars over \(\varGamma \) (e.g. Figure 7). A hole in a morphism in \(\textsf {Hyp}[\varGamma ]\) is a placeholder for an (n, m) hyperedge, the grammar labels these holes by non-terminals, and composition corresponds to hyperedge replacement.
Fig. 8.
A context-free monoidal grammar of unbraids, with start symbol S.
Example 4.16
(Unbraids). We return to the language of unbraids suggested in Proposition 3.9. Take the grammar over the over- and under-braiding polygraph depicted in Figure 8, with start symbol \(S \sqsubset {\begin{array}{c} 2 \\ 2 \end{array}}\). The language of this grammar consists of unbraids on two strings.
Let us record some basic closure properties of context-free monoidal languages.
Proposition 4.17
Context-free monoidal languages over \(\mathbb {C}\) with start symbol \(S \sqsubset {\begin{array}{c} X \\ Y \end{array}}\) are closed under union. The underlying morphism is given by the copairing, and start symbols can be unified by introducing a fresh symbol and productions where necessary, as in the classical case. Context-free monoidal languages are also closed under images of strict monoidal functors: the underlying morphism is given by postcomposition.
5 Optical Contour of a Multicategory
An important realization of Melliès and Zeilberger is that the formation of spliced arrows in a category has a left adjoint, which they call the contour of a multicategory [36, Section 3.2]. This adjunction is a key conceptual tool in their generalized version of the Chomsky-Schützenberger representation theorem, and is closely linked to the notion of item in LR parsing [36]. In this section, we present a similar adjunction for the monoidal setting. However, it is not clear that the formation of diagram contexts has a left adjoint. We must therefore first conduct a dissection of diagram contexts into raw optics.
5.1 The multicategory of raw optics
A raw optic is a tuple of morphisms obtained by cutting a diagram context into a sequence of disjoint pieces. The term optics refers to a notion closely related to diagram contexts, which are defined exactly as a quotient of raw optics [10, 39]. In Section 5 we shall see that raw optics has a left adjoint, the optical contour, and this will be enough to prove our representation theorem (Theorem 6.6).
Definition 5.1
The multicategory of raw optics over a strict monoidal category \(\mathbb {C}\), denoted \(\textsf{ROpt}[\mathbb {C}]\), is defined to have, as objects, pairs \({\begin{array}{c} A \\ B \end{array}}\) of objects of \(\mathbb {C}\), and, as its set of multimorphisms, \(\textsf{ROpt}[\mathbb {C}]({\begin{array}{c} A_1 \\ B_1 \end{array}}, ..., {\begin{array}{c} A_n \\ B_n \end{array}}; {\begin{array}{c} S \\ T \end{array}})\), the following set, where we write AB for \(A \otimes B\),
As a special case, \(\textsf{ROpt}[\mathbb {C}](;{\begin{array}{c} S \\ T \end{array}}) := \mathbb {C}(S;T)\). In other words, a multimorphism, from \({\begin{array}{c} A_1 \\ B_1 \end{array}}, ..., {\begin{array}{c} A_n \\ B_n \end{array}}\) to \({\begin{array}{c} S \\ T \end{array}}\), consists of two families of objects, \(M_1,\ldots ,M_n\) and \(N_1,...,N_n\), and a family of functions, \((f_0, ..., f_n)\), with types \(f_0 : S \rightarrow M_1 \otimes A_1 \otimes N_1\); with \(f_i : M_i \otimes B_i \otimes N_i \rightarrow M_{i+1} \otimes A_{i+1} \otimes N_{i+1};\) for each \(1 \le i \le n-1\); and \(f_n : M_n \otimes B_n \otimes N_n \rightarrow T\). In the special nullary case, we have a single morphism \(f_0 : S \rightarrow T\).
Identities are given by pairs \((\textsf{id}_{A}, \textsf{id}_{B})\). Given two raw optics \(f = (f_0, ..., f_n)\) and \(g = (g_0, ..., g_m)\), their composition is defined by
Fig. 9.
Two raw optics (left, centre) in \(\textsf{ROpt}[\mathbb {C}]({\begin{array}{c} A \\ B \end{array}};{\begin{array}{c} S \\ T \end{array}})\) which quotient to the same diagram context. Note that a raw optic is not the same as a spliced arrow: the types M, N must match.
Every raw optic can be glued into a diagram context, as illustrated in Figure 9. More precisely, we have the following result.
Proposition 5.2
There is an identity on objects multifunctor
mapping each raw optic to its corresponding diagram context. Equivalently, there is an identity on objects symmetric multifunctor
; this symmetric multifunctor is full.
Proposition 5.3
The construction of raw optics extends to a functor \(\textsf{ROpt} : \textsf {MonCat}\rightarrow \textsf {MultiCat}\) between the categories of strict monoidal categories and strict monoidal functors, and multicategories and multifunctors.
Remark 5.4
We could have defined context-free monoidal grammars as morphisms into raw optics, rather than diagram contexts, but this would require an arbitrary choice of raw optic for each rule, as in Figure 9. In particular, this would force us to choose a particular ordering of the holes, since raw optics do not form a symmetric multicategory. On the other hand, that such a choice exists will be needed to prove our representation theorem (Section 6).
5.2 Optical contour
We now introduce the left adjoint to the formation of raw optics, which we call the optical contour of a multicategory. The difference from the contour of Section 2 is that additional objects \(M_i, N_i\) are introduced which keep track of strings that might surround holes. This gives rise to a strict monoidal category.
Fig. 10.
A multimorphism \(p \in \mathbb {M}(A,B;Y)\) and its three sectors given by optical contour: \((p,0) : Y^L \rightarrow M_1\otimes A^L\otimes N_1, (p,1) : M_1\otimes A^R\otimes N_1 \rightarrow M_2\otimes B^L\otimes N_2, (p,2) : M_2\otimes B^R\otimes N_2 \rightarrow Y^R\).
Definition 5.5
Let \(\mathbb {M}\) be a multicategory. Its optical contour, \(\mathcal {C}\mathbb {M}\), is the strict monoidal category presented by a polygraph whose generators are given by taking contours of multimorphisms in \(\mathbb {M}\). Each multimorphism gives rise to a set of generators for the monoidal category \(\mathcal {C}\mathbb {M}\) – its set of sectors, as in Figure 10.
Explicitly, for each object \(A \in \mathbb {M}\), the optical contour \(\mathcal {C}\mathbb {M}\) contains a left polarized, \(A^L\), and a right polarized, \(A^R\), version of the object. Additionally, for each multimorphism \(f \in \mathbb {M}(X_1, ..., X_n; Y)\), there exists a family of objects \(M_1^f, ..., M_n^f, N_1^f, ..., N_n^f\), whose superscripts we omit when they are clear from context. The morphisms are given by the following generators. For each \(f \in \mathbb {M}(X_1, ..., X_n; Y)\), we consider the following \(n+1\) generators:
In particular, for a nullary multimorphism \(f \in \mathbb {M}(;Y)\), we consider a generator \((f,0) : Y^L \rightarrow Y^R\). Further, we ask for the following equations which ensure that the optical contour preserves identities and composition: for all \(x \in \mathbb {M}\), \((\textsf{id}_{X}, 0) = \textsf{id}_{X^L}, (\textsf{id}_{X}, 1) = \textsf{id}_{X^R}\) with \(M_1^{\textsf{id}_{X}} = N_1^{\textsf{id}_{X}} = I\); and given any \(f \in \mathbb {M}(X_1, ..., X_n; Y_i)\) and \(g \in \mathbb {M}(Y_1, ..., Y_m; Z)\),
In particular, when \(f \in \mathbb {M}(;Y_i)\) is nullary,
.
Theorem 5.6
Optical contour is left adjoint to raw optics; there exists an adjunction \((\mathcal {C} \dashv \textsf{ROpt}) : \textsf {MonCat}\rightarrow \textsf {MultiCat}.\)
6 A Monoidal Representation Theorem
The Chomsky-Schützenberger representation theorem says that every context-free language can be obtained as the image under a homomorphism of the intersection of a Dyck language and a regular language [9]. Melliès and Zeilberger [35] use their splicing-contour adjunction to give a novel proof of this theorem for context-free languages in categories: the classical version is recovered when the category is a free monoid. The role of the Dyck language, providing linearizations of derivation trees, is taken over by contours of derivations.
Monoidal categories provide a more striking case: the Dyck language is not needed because the information that parentheses encode can be carried instead by tensor products. In this section, we show that a regular monoidal language of optical contours is sufficient to reconstruct the original language. Theorem 6.6 states that every context-free monoidal language is the image under a monoidal functor of a regular monoidal language.
Our strategy will be to first choose a factoring of a grammar into raw optics, then use the optical contour/raw optics adjunction to produce the required monoidal functor. We must first establish that such a factoring exists. Omitted proofs may be found in the full version [15].
Lemma 6.1
Any morphism of symmetric multigraphs underlying a context-free monoidal grammar,
, factors (non-uniquely) through the quotienting of raw optics (Proposition 5.2); meaning that there exists some multigraph \(G'\) satisfying \(G = \textsf{clique}(G')\), and some morphism \({\phi }_r :G' \rightarrow |{\textsf{ROpt}[\mathbb {C}]}|\), such that
.
Call the factor \({\phi }_r : G' \rightarrow |{\textsf{ROpt}[\mathbb {C}]}|\) a raw representative of \(\phi \). It amounts to choosing a fixed ordering of the holes in a diagram context for each rule in the grammar, and a particular splicing into a raw optic.
Lemma 6.2
Let \(\mathcal {G} = (\phi , S)\) be a context-free monoidal grammar. Then the language of any raw representative \({\phi }_r\) of \(\phi \) (with start symbol S) equals the language of \(\mathcal {G}\). That is, \({\phi }_r[\mathcal {F}_{\triangledown }{G'}(;S)] = \phi [\mathcal {F}_{\triangledown }{G}(;S)]\).
Lemma 6.3
A raw representative \({\phi }_r : G' \rightarrow |{\textsf{ROpt}[\mathbb {C}]}|\) uniquely determines a strict monoidal functor \(I_\phi : \mathcal {F}_{\otimes }{(\mathcal {C}{G'})} \rightarrow \mathbb {C}\).
We shall see that this monoidal functor maps the following regular monoidal language over \(\mathcal {C}{G}\) to the language of the original context-free monoidal grammar.
Definition 6.4
Let
be a context-free monoidal grammar, and \({\phi }_r\) a raw representative with domain \(G'\). Define a regular representative of \(\mathcal {G}\) to be the regular monoidal grammar \(\mathcal {R} = (\textsf{id} : \mathcal {C}{G'} \rightarrow \mathcal {C}{G'}, S^L, S^R)\) over optical contours of \(G'\) whose morphism of polygraphs is the identity.
Lemma 6.5
Given a multigraph G, there is a bijection between derivations rooted at a sort S and optical contours from \(S^L\) to \(S^R\), i.e.
The language of a context-free monoidal grammar
equals the image of a regular representative under the monoidal functor \(I_\phi \) of Lemma 6.3.
Theorem 6.6 is at first quite surprising, since in comparison with the usual Chomsky-Schützenberger theorem and its generalization [36], one might expect to see an intersection of a regular monoidal language and a context-free monoidal language. Instead, this theorem tells us that regular monoidal languages are powerful enough to encode context-free monoidal languages, even while the latter is strictly more expressive than the former. Just as a context-free grammar suffices to specify a programming language which may encode instructions for arbitrary computations, regular monoidal languages can specify arbitrary context-free monoidal languages, with a monoidal functor effecting the “compilation”.
7 Conclusion
There are still many avenues to explore in this structural approach to context-free languages. One obvious direction is to investigate a notion of pushdown automaton for context-free monoidal languages. In fact, it still remains to be elaborated how pushdown automata emerge for context-free languages over plain categories. Following the general principle of parsing as a lifting problem [36], and the duality of grammars (fibered) and automata (indexed) may provide some clue to characterizing such automata by a universal property.
The study of languages and the dependence relations that diagram contexts naturally present may be useful to the study of complexity in monoidal categories, such as the notion of “monoidal width” proposed by Di Lavore and Sobociński [32, 33]. Conversely, measures of monoidal complexity may inform the cost of parsing different terms.
Finally, different types of string diagram exist for a variety of widely applied categorical structures beyond monoidal categories, such as double categories [37]. There are many opportunities to extend the general principle elaborated here to a notion of context-free language in these structures.
Acknowledgements
Matt Earnshaw was supported by Estonian Research Council grant PRG1210. Mario Román was partly supported by the Air Force Office of Scientific Research (AFOSR) award number FA9550-21-1-0038 and partly supported by the Advanced Research + Invention Agency (ARIA) Safeguarded AI Programme.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
It is clear that the language accepted by this automaton is exactly the “balanced parentheses”, but note that this is not a language of words, since we use an extra string to keep track of opening and closing parentheses. This principle will play an important role in our representation theorem in Section 6. Roughly speaking, this extra wire arises from the optical contour of a string language of balanced parentheses.
and one for “under-braiding”
. The language of unbraids on two strings over \(\varGamma \), i.e. diagrams equivalent under planar isotopy to untangled strings, is not a regular monoidal language.
and
, a shuffling is
, but not
. The theory of diagram contexts will introduce a shuffling every time it mixes two contexts: this way, if a term was derived by combining two contexts, we can always reorder these contexts however we want. For instance, the term
was derived from composing the axioms
and
; by choosing a different shuffling, we can also derive the term
. Let us now formally introduce the theory.
over a polygraph, \(\mathcal {P}\), is described by the following logic. This logic contains objects (\(A,B,C,... \in \mathcal {P}_{obj}^{*}\)) that consist of lists of types of the polygraph, \(X,Y,Z,... \in \mathcal {P}_{obj}\); it also contains contexts \((\varGamma ,\varDelta ,\varPsi ,...)\) that consist of lists of pairs of objects. Apart from the single variables (x, y, z, ..) and the generators of the polygraph (f, g, h, ...); we consider fully formed terms \((t_1,t_2,...)\). 
denotes the concatenation of lists. Every term in a given context has a unique derivation. We consider terms up to \(\alpha \)-equivalence and we impose the following equations over the terms whenever they are constructed over the same context:
and \(\textsf{id} ^{*} = \textsf{id} \). A morphism of symmetric multigraphs is a morphism of multigraphs which commutes with the bijections.
.
and
, which moreover commute with the free multicategory \(\mathcal {F}_{\triangledown } \) and free monoidal category functors \(\mathcal {F}_{\otimes } \).
, into the underlying multigraph of diagram contexts in \(\mathbb {C}\), where \(\mathcal {G}\) is finite, and a start sort \(S \in \mathcal {G}\).
defining a grammar uniquely determines, via the free-forgetful adjunction, a symmetric multifunctor
, mapping (closed) derivations to morphisms of \(\mathbb {C}\). The language of a grammar is then defined analogously to Definition 2.4:
be a context-free monoidal grammar. The language of \(\varPsi \) is the set of morphisms in \(\mathbb {C}(A;B)\) given by the image under \(\hat{\varPsi }\) of the set of derivations \(\mathcal {F}_{\triangledown }{\mathcal {G}}(;S)\). A set of morphisms L in \(\mathbb {C}\) is a context-free monoidal language if and only if there exists a context-free monoidal grammar whose language is L.
) and deleting variables (
).
mapping each raw optic to its corresponding diagram context. Equivalently, there is an identity on objects symmetric multifunctor
; this symmetric multifunctor is full.
.
, factors (non-uniquely) through the quotienting of raw optics (Proposition 5.2); meaning that there exists some multigraph \(G'\) satisfying \(G = \textsf{clique}(G')\), and some morphism \({\phi }_r :G' \rightarrow |{\textsf{ROpt}[\mathbb {C}]}|\), such that
.
be a context-free monoidal grammar, and \({\phi }_r\) a raw representative with domain \(G'\). Define a regular representative of \(\mathcal {G}\) to be the regular monoidal grammar \(\mathcal {R} = (\textsf{id} : \mathcal {C}{G'} \rightarrow \mathcal {C}{G'}, S^L, S^R)\) over optical contours of \(G'\) whose morphism of polygraphs is the identity.
equals the image of a regular representative under the monoidal functor \(I_\phi \) of Lemma 6.3.
