6

# Dynamic Tracing: a graphical language for rewriting protocols

Kristopher Brown
Topos Institute
<EMAIL_ADDRESS>
& David I. Spivak
Topos Institute
<EMAIL_ADDRESS>
###### Abstract

The category $\mathbf{Set}_{*}$ of sets and partial functions is well-known to
be traced monoidal, meaning that a partial function $S+U\rightharpoonup T+U$
can be coherently transformed into a partial function $S\rightharpoonup T$.
This transformation is generally described in terms of an implicit procedure
that must be run. We make this procedure explicit by enriching the traced
category in $\mathbf{Cat}^{\sharp}$, the symmetric monoidal category of
categories and cofunctors: each hom-category has such procedures as objects,
and advancement through the procedures as arrows. We also generalize to traced
Kleisli categories beyond $\mathbf{Set}_{*}$, providing a conjectural trace
operator for the Kleisli category of any polynomial monad of the form $t+1$.
The main motivation for this work is to give a formal and graphical syntax for
performing sophisticated computations powered by graph rewriting, which is
itself a graphical language for data transformation.

_Keywords_ Double pushout rewriting $\cdot$ category theory $\cdot$ graph
rewriting

##  1 Motivation

Explicitly constructed programs are the standard means of specifying data
transformation. However, by forgoing the full expressivity of a general
programming language, one can work within a restricted syntax—a _domain-
specific language_ —that has desirable properties. For example, flowcharts are
often used as an informal syntax for software projects, where each box is
associated with a subroutine that transforms data that flows on input wires
into data that flows on output wires. Category theory makes this assignment of
semantics precise: the syntax of directed wiring diagrams can formally be
given a semantics in any symmetric monoidal category. There are advantages of
this two-dimensional syntax over one-dimensional expression trees in a general
purpose language, including transparent visualization, operadic substitution,
and algebraic manipulation. Furthermore, when represented as a combinatorial
object, the diagram itself is a particularly efficient normal form for a large
number of syntax trees which it is equivalent to [18].

The field of graph transformation uses the syntax of spans in an adhesive
category, interpreting them as rewrite rules. The semantics of deletion,
copying, merging, and adding data can be attributed to these spans in various
formalisms, notably DPO [7], SPO [13], and SqPO [6] rewriting. If these sorts
of operations are all one needs, it is advantageous to work with this syntax
rather than general expression trees, as its rules are more easily visualized
and subject to static analysis.

Despite these virtues, there has been difficulty in applying graph
transformation in engineering practice [2, 27]. The cited reviews discuss
various strategies for computation via graph rewriting. A straightforward
method is unordered graph rewriting, where rewrite rules are applied in an
arbitrary order, possibly with constraints; however, many applications require
the expressivity of executing sequences of atomic rewrites in a systematic,
domain-specific way, e.g. looping over a set of matches. Some earlier
diagrammatic languages for this are based on directed graphs [5, 8], where
vertices are rewrite rules and edges are $\mathbb{B}$-valued, indicating where
to go next if the current rule either does match or doesn’t match. There are
also more expressive languages which propose a BNF grammar for graph
programs[20, 19]. The control flow of such programs are implicit in the
semantics given to constructors like while rather than explicit (e.g. the
looping of a diagram). Current abstractions for programming with graph
rewriting make it difficult for engineers to collaborate due to
incompatibilities between software implementations or between the ontologies
presupposed by rewrite rules. Furthermore, fine-grained control over _which_
match is used in a rewrite is not emphasized.

We will demonstrate how the structure of a rich class of data transformations
can be given the structure of a symmetric monoidal category with a conjectural
trace operator, which licenses the use of wiring diagrams with feedback loops
as a graphical syntax. After describing this class abstractly, we demonstrate
how this formalism guides the user interface and implementation of software
designed to construct elaborate computations built up out of rewrite rules.

In Section 2 we lead up to the construction of a category $\mathbf{DK}_{t}$,
parameterized by a polynomial monad $t$, that will be sufficient for our
rewriting application. In Section 3, we show it is a cocartesian monoidal
category enriched in $\mathbf{Cat}^{\sharp}$. We also offer a conjectural
trace operator for monads meeting a certain criterion. In Section 4, we
produce a domain-specific language (DSL), with semantics in $\mathbf{DK}_{t}$,
for constructing sophisticated programs that manipulate data via rewrite
rules. We conclude with a summary and future work in Section 5.

## Notation

We assume familiarity with categories, functors, and enriched category theory.
Many technical details related to $\mathbf{Poly}$ and its many monoidal
structures ($+,\times,\otimes,\mathbin{\triangleleft}$) can be referenced in
[25]; we elide these to instead focus on providing intuitions for these
constructions in Section 2. In contrast, Section 3 requires a strong technical
understanding of $\mathbf{Poly}$. We will use the notation $[-,-]$ to refer to
the internal hom in a category, while $(-,-)$ will be used for (co)pairing
morphisms in a category with (co)products. We use $\sum$ to denote the
disjoint union of sets. We often denote the identity on an object simply by
the object name, e.g. we use $A$ to denote $\mathrm{id}_{A}$.

##  2 Background

In this section, we incrementally improve frameworks for modeling dynamical
systems of the sort we need for rewriting by proposing a sequence of
categories: $\mathbf{Meal}$, $\mathbf{Meal}/\sim$, $\mathbf{DynMeal}$, and
finally, $\mathbf{DK}_{t}$. Each formalism should allow us to view a large
system as the composition of smaller ones, where at any level of granularity
we can consider local systems as enclosed boxes, which can be entered and
exited and which evolve as we interact with them.

###  2.1 Mealy machines

We first consider the category $\mathbf{Meal}$ of Mealy machines:

$\displaystyle\operatorname{Ob}(\mathbf{Meal})$
$\displaystyle:=\operatorname{Ob}(\mathbf{Set})$
$\displaystyle\operatorname{Hom}_{\mathbf{Meal}}(A,B)$
$\displaystyle:=\left\\{\left(S:\mathbf{Set},s_{0}:S,\phi\colon A\times S\to
S\times B\right)\right\\}$

A map could be called a _dynamic function_. It includes a set $S$ of states
and a particular state $s_{0}$. Further, given any state $s:S$, it provides
both a function $A\to B$ and, for any input $a:A$, an updated state; all this
is encoded in $\phi(-,s)\colon A\to S\times B$. Thus we can think of a
morphism in $\mathbf{Meal}$ as a function $A\to B$ that is updated that every
time it receives an input. An example morphism in a toy model of chess pieces
evading traps is given in Figure 1a-b.

Figure 1: Suppose we play a game like chess where certain pieces may be in
various conditions: Unaware, Alert, and Captured. a. A morphism
$\mathit{Trap}:\operatorname{Hom}_{\mathbf{Meal}}(\\{U,A\\},\\{U,A,C\\})$
represents a system where one’s opponent may have set a trap to capture a
piece: this is a dynamical system that accepts a piece (Unaware or Alert) and
outputs an Unaware, Alert, or Captured piece. $\mathit{Trap}$ has two possible
states: either there is a trap ($T$) or no trap($N$) set, with the system
starting in state $T$. b. $\mathit{Trap}$ requires a function
$S\times\\{U,A\\}\to S\times\\{U,A,C\\}$, which is visualized by showing the
dynamics in both possible states. In state $T$, unaware pieces fall for the
trap and are captured, whereas alert pieces stay alert (and the state changes
to $N$). In state $N$, all inputs exit as unaware, though a $U$ input triggers
the state to change to $T$. c. A family of morphisms in $\mathbf{Meal}$ of the
form $\operatorname{Hom}_{\mathbf{Meal}}(X+X,X)$, for any set $X$. We will
visually depict this as a dot with multiple incoming wires. d. A family of
morphisms in $\mathbf{Meal}$ of the form
$\operatorname{Hom}_{\mathbf{Meal}}(\varnothing,X)$, for any set $X$. We will
visually depict this as a dot with one outgoing wire. e. A composite dynamical
system $\mathit{Trap}_{2}$ depicting pieces passing through two
$\mathit{Trap}$ systems: Alert pieces exiting the first subsystem skip the
second one. This diagram formally depicts the sequential composition of five
morphisms, which are distinguished by the dotted vertical lines:
$\mathit{Trap}\mathbin{\fatsemi}(U+\square_{A}+A+\nabla_{C})\mathbin{\fatsemi}(\mathit{Trap}+A+C)\mathbin{\fatsemi}(U+A+\sigma_{C,A}+C)\mathbin{\fatsemi}(U+\nabla_{A}+\triangledown
C)$. The state space of the composite system is
$\\{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}T},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N}\\}\times\\{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}T},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N}\\}$,
with initial state
$({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}T},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}T})$.

We claim $\mathbf{Meal}$ is a symmetric monoidal category, with monoidal unit
$\varnothing$ and the object $A\otimes B$ given by disjoint union of sets. For
tensor and composition of morphisms, we define111 We are elide the symmetry
$B\times S\cong S\times B$ in our notation ‘$\phi\times\psi$‘.

$\displaystyle(S,s_{0},\phi)\otimes(T,t_{0},\psi)$
$\displaystyle\coloneqq(S\times T,(s_{0},t_{0}),\phi\times\psi)$
$\displaystyle(S,s_{0},\phi)\mathbin{\fatsemi}(T,t_{0},\psi)$
$\displaystyle\coloneqq(S\times T,(s_{0},t_{0}),(\phi\times
T)\mathbin{\fatsemi}(S\times\psi))$

Because $\mathbf{Meal}$ is a symmetric monoidal category, there is a ready-
made graphical language for visualizing serial and parallel compositions of
its morphisms. The icons of this language are wires, each labeled with a set,
boxes with input and output ports, also each labeled with a set, and
braidings; these are described in detail in [21, §3.1, 3.5]. In brief, data
flows from left to right on wires, which are objects. The vertical dimension
represents the tensoring $\otimes$ of objects and morphisms. We visualize an
element of $\operatorname{Hom}_{\mathbf{Meal}}(A,B)$ as a box with $|A|$ input
ports and $|B|$ output ports. A diagrammatic example of a nontrivial
composition of morphisms is provided in Figure 1e.

We are ultimately working towards a traced monoidal category with coproducts;
however, coproducts do not generally exist in $\mathbf{Meal}$. The natural
choice for a copairing of morphisms
$(S,s_{0},\phi):\operatorname{Hom}_{\mathbf{Meal}}(A,Z)$ and
$(S^{\prime},s^{\prime}_{0},\psi):\operatorname{Hom}_{\mathbf{Meal}}(B,Z)$ is
to place the boxes in parallel and merge their outputs, i.e.
$(S,s_{0},\phi)\otimes(S,s_{0},\phi)\mathbin{\fatsemi}\nabla_{Z}$, where
$\nabla_{Z}\colon Z+Z\to Z$ is the codiagonal. This would have the correct
behavior, in a sense that will be made precise in the following section.
However, the required coproduct equalities (e.g.
$\iota_{1}\mathbin{\fatsemi}(\phi,\psi)=\phi$) do not hold in general because
the state spaces are not equal, i.e. $S\times S^{\prime}\cong^{?}S$.

###  2.2 Quotienting by behavioral equivalence

We now talk about behaviors as proper objects of study, rather than merely
induced by Mealy machines. Although the set of behaviors of an Mealy machine
with input $A$ and output $B$ can be succinctly characterized as the
underlying set of the final coalgebra on $X\mapsto B^{A}X^{A}$, a set we will
eventually denote by
$\mathfrak{c}\langle[A\mathcal{y},B\mathcal{y}]\rangle(1)$, we will more
naturally be able to generalize our results by viewing behavior through the
lens of polynomial functors; indeed, this is where the above notation comes
from: $[A\mathcal{y},B\mathcal{y}]$ is an internal hom in $\mathbf{Poly}$ and
$\mathfrak{c}\langle-\rangle$ is the cofree comonoid construction on
$\mathbf{Poly}$.

Polynomial functors are formally sums of representable functors
$\mathbf{Set}\to\mathbf{Set}$, i.e. functors of the form
$\mathcal{y}^{A}:=\operatorname{Hom}_{\mathbf{Set}}(A,-):\mathbf{Set}\to\mathbf{Set}$,
sending any set $X$ to $X^{A}$. The sum is indexed by a set $I$ such that the
polynomial can be denoted $p:=\sum_{i:I}\mathcal{y}^{A_{i}}$. Note that $I$ is
canonically isomorphic to $p(1)$. The elements of $p(1)$ are called positions,
while for each position $i:p(1)$ there is a set of directions $A_{i}$. We
denote $A_{i}$ by $p[i]$, so we may write
$p\cong\sum_{i:p(1)}\mathcal{y}^{p[i]}$. Polynomial functors can be thought of
as system interfaces, and a few ways to represent them are shown below.

$\begin{array}[]{ccccccc}\textbf{Interface}&&\textbf{Algebraic}&&\textbf{Bundle}&&\textbf{Corolla
forest}\\\
\begin{array}[]{l}\\{\text{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}Listen}}\\}\mathcal{y}^{\\{L,R\\}}\\\
+\
\text{\\{{\color[rgb]{0.0,0.5,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.5,0.3}Left},
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}Right}\\}}\mathcal{y}^{\text{\\{Move\\}}}\\\
+\
\text{\\{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}Stop}\\}}\mathcal{y}^{\\{\\}}\end{array}&&\mathcal{y}^{2}+2\mathcal{y}+1&&\leavevmode\hbox
to66.7pt{\vbox to45.21pt{\pgfpicture\makeatletter\hbox{\hskip
2.56pt\lower-6.95522pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.72638pt}{-2.22221pt}\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{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}$\bullet$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.22638pt}{22.76228pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.72638pt}{20.54007pt}\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{{$\bullet$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.72638pt}{29.07599pt}\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{{$\bullet$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} ; ;
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.95276pt}{-2.22221pt}\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{{\color[rgb]{0.0,0.5,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.5,0.3}$\bullet$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{28.45276pt}{22.76228pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.95276pt}{20.54007pt}\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{{$\bullet$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} ; ;
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{40.17914pt}{-2.22221pt}\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{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}$\bullet$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{42.67914pt}{22.76228pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{40.17914pt}{20.54007pt}\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{{$\bullet$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} ; ;
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{54.40552pt}{-2.22221pt}\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{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}$\bullet$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{56.90552pt}{22.76228pt}\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{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} ; ; {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{58.93852pt}{6.75522pt}\pgfsys@lineto{12.19337pt}{6.75522pt}\pgfsys@curveto{9.43192pt}{6.75522pt}{7.19337pt}{4.51668pt}{7.19337pt}{1.75522pt}\pgfsys@lineto{7.19337pt}{-1.75522pt}\pgfsys@curveto{7.19337pt}{-4.51668pt}{9.43192pt}{-6.75522pt}{12.19337pt}{-6.75522pt}\pgfsys@lineto{58.93852pt}{-6.75522pt}\pgfsys@curveto{61.69998pt}{-6.75522pt}{63.93852pt}{-4.51668pt}{63.93852pt}{-1.75522pt}\pgfsys@lineto{63.93852pt}{1.75522pt}\pgfsys@curveto{63.93852pt}{4.51668pt}{61.69998pt}{6.75522pt}{58.93852pt}{6.75522pt}\pgfsys@closepath\pgfsys@moveto{7.19337pt}{-6.75522pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{8.19337pt}{0.0pt}\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{\minipage[t]{54.74515pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{56.43852pt}{38.0534pt}\pgfsys@lineto{12.19337pt}{38.0534pt}\pgfsys@curveto{9.43192pt}{38.0534pt}{7.19337pt}{35.81487pt}{7.19337pt}{33.0534pt}\pgfsys@lineto{7.19337pt}{23.22928pt}\pgfsys@curveto{7.19337pt}{20.46782pt}{9.43192pt}{18.22928pt}{12.19337pt}{18.22928pt}\pgfsys@lineto{56.43852pt}{18.22928pt}\pgfsys@curveto{59.19998pt}{18.22928pt}{61.43852pt}{20.46782pt}{61.43852pt}{23.22928pt}\pgfsys@lineto{61.43852pt}{33.0534pt}\pgfsys@curveto{61.43852pt}{35.81487pt}{59.19998pt}{38.0534pt}{56.43852pt}{38.0534pt}\pgfsys@closepath\pgfsys@moveto{7.19337pt}{18.22928pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{8.19337pt}{28.14136pt}\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{\minipage[t]{52.24515pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{ {}{}{}}{}{
{}{}{}}{}} {}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }{}{{ {\pgfsys@beginscope
\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{} {}{}{} {}{}{}
\pgfsys@moveto{-2.56pt}{3.12257pt}\pgfsys@curveto{-2.0923pt}{1.24901pt}{-1.05006pt}{0.3643pt}{0.0pt}{0.0pt}\pgfsys@curveto{-1.05006pt}{-0.3643pt}{-2.0923pt}{-1.24901pt}{-2.56pt}{-3.12257pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{34.31595pt}{18.02928pt}\pgfsys@lineto{34.31595pt}{7.7552pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{34.31595pt}{7.35521pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{24.88269pt}{10.33948pt}\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{{$\pi$}}
}}\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}}&&\leavevmode\hbox
to77.67pt{\vbox to16.83pt{\pgfpicture\makeatletter\hbox{\hskip
8.50842pt\lower-2.39998pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.61108pt}{-2.22221pt}\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{{${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bullet}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{{}}
{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{{ {\pgfsys@beginscope
\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{} {}{}{} {}{}{}
\pgfsys@moveto{-2.07999pt}{2.39998pt}\pgfsys@curveto{-1.69998pt}{0.95998pt}{-0.85318pt}{0.28pt}{0.0pt}{0.0pt}\pgfsys@curveto{-0.85318pt}{-0.28pt}{-1.69998pt}{-0.95998pt}{-2.07999pt}{-2.39998pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}{}{}{{}}\pgfsys@moveto{-0.31644pt}{0.63336pt}\pgfsys@lineto{-6.93431pt}{13.86862pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.44724}{0.89442}{-0.89442}{-0.44724}{-7.02374pt}{14.04749pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{0.31644pt}{0.63336pt}\pgfsys@lineto{6.93431pt}{13.86862pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.44724}{0.89442}{-0.89442}{0.44724}{7.02374pt}{14.04749pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} { {}{}{}}{}{}{{{{}{}{}}}}{{}}{{{
{}{}{}}}}{}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{18.23746pt}{-2.22221pt}\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{{${\color[rgb]{0.0,0.5,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.5,0.3}\bullet}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{21.84854pt}{0.42221pt}\pgfsys@lineto{21.84854pt}{13.82639pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{21.84854pt}{14.02638pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} { {}{}{}}{}{}{{{{}{}{}}}}{{}}{{{
{}{}{}}}}{}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{40.086pt}{-2.22221pt}\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{{${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\bullet}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{43.69708pt}{0.42221pt}\pgfsys@lineto{43.69708pt}{13.82639pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{43.69708pt}{14.02638pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {
{}{}{}}{}{}{{{{}{}{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{61.93454pt}{-2.22221pt}\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{{${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\bullet}$}}
}}\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}}\end{array}$

Figure 2: Various representations of a polynomial functor that characterizes
an interface which can do three things: it can listen (and receive a boolean
value), it can move (left or right), or it can stop.

Polynomial comonads can be identified with categories [1] and cofunctors, a
category we denote $\mathbf{Cat}^{\sharp}$. The cofree comonad functor
$\mathfrak{c}\langle-\rangle\colon\mathbf{Poly}\to\mathbf{Cat}^{\sharp}$ can
be thought of as sending a polynomial $p$ to a category whose objects are
possible behavior trees of a system with interface $p$. These are potentially
infinite trees and are obtained by starting with a root and stacking one-step
behaviors, as seen in the corolla forest representation of the polynomial. To
provide intuition for what these behavior trees look like, Figure 3 shows a
tree corresponding to the Mealy machine of Figure 1a-b as well as a tree for
the above example interface. This allows us to define the category,
$\mathbf{Meal}/\sim$:

$\displaystyle\operatorname{Ob}(\mathbf{Meal}/\sim)$
$\displaystyle:=\operatorname{Ob}(\mathbf{Set})$ (1)
$\displaystyle\operatorname{Hom}_{\mathbf{Meal}/\sim}(A,B)$
$\displaystyle:=\operatorname{Ob}\mathfrak{c}\langle[A\mathcal{y},B\mathcal{y}]\rangle$

$Ⓣ$$Ⓣ$$Ⓣ$$U$ $Ⓝ$$A$$U$ $Ⓝ$$Ⓣ$$U$ $Ⓝ$$A$$A$

$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\mathit{Move}$$L$
$\bullet$$\bullet$$\mathit{Move}$$R$$\mathit{Move}$$L$
$\bullet$$\bullet$$\bullet$$\bullet$$\mathit{Move}$$L$
$\bullet$$\bullet$$\mathit{Move}$$R$$\mathit{Move}$$R$

Figure 3: Left. An object of
$\mathfrak{c}\langle[\\{U,A\\}\mathcal{y},\\{U,A,C\\}\mathcal{y}]\rangle$
which is the behavior of $\mathit{Trap}$ from Figure 1b. Note that
$[2\mathcal{y},3\mathcal{y}]\cong 3^{2}\mathcal{y}^{2}$, i.e. it is an
interface that receives one of three possible inputs and can be configured in
any possible function $2\to 3$. We label two of these eight possible functions
as $T$ and $N$. Right. One possible behavior for the interface of Figure 2,
i.e. an object of the category
$\mathfrak{c}\langle\mathcal{y}^{2}+2\mathcal{y}+1\rangle$. The machine starts
in listening state, and upon receiving the input $L$ (respectively $R$) it
moves left (resp. right). The machine repeats this once more and then stops.

An important feature is not explicitly modeled. We have
$\operatorname{Hom}(A,B)$ being a mere set of behaviors, but we need to make
use of a rich structure that this set of behaviors has when evolving the
system over time: the way the system changes as new inputs are received.
Enriching our category, i.e. replacing each set of morphisms by a category,
will allow us to characterize how the morphisms change as inputs are received.

###  2.3 Modeling the system evolution in time

Recall that $\mathfrak{c}\langle p\rangle$ sends a polynomial $p$ to a
category. Until now we have only considered the objects of that category. The
morphism $\mathit{tree}_{1}\to\mathit{tree}_{2}$ is given by a path in
$\mathit{tree}_{1}$, starting from the root and ending at a copy of
$\mathit{tree}_{2}$ (see Figure 4). This is crucial for explicitly modeling
how a sequence of inputs leads to a new dynamical system. We define
$\mathbf{DynMeal}$ to have the same objects as $\mathbf{Meal}$ but to be
enriched in $\mathbf{Cat}^{\sharp}$ rather than $\mathbf{Set}$, such that the
hom-object
$\operatorname{Hom}_{\mathbf{DynMeal}}(A,B):=\mathfrak{c}\langle[Ay,By]\rangle$.

$\bullet$$\bullet$$\bullet$$\bullet$$L$
$\bullet$$\bullet$$\bullet$$\mathit{Move}$$\mathit{Move}$$R$$L$
$\bullet$$\bullet$$\mathit{Move}$$R$$\mathit{Move}$

$\overset{\mathit{Move};L}{\longrightarrow}$

$\bullet$$\bullet$$L$
$\bullet$$\bullet$$\bullet$$\mathit{Move}$$\mathit{Move}$$R$

Figure 4: A morphism between two objects in
$\mathfrak{c}\langle\mathcal{y}^{2}+2\mathcal{y}+1\rangle$, with the data of
the morphism represented by thick arrows, i.e. $\mathit{Move}$, then $L$.

The category $\mathbf{Cat}^{\sharp}$ is that of
$\mathbin{\triangleleft}$-comonoids in $\mathbf{Poly}$, which is equivalent to
the category of categories and _co_ functors as proven in [1, 14]. A cofunctor
has a map in the forward direction on objects but a map on morphisms in the
reverse direction. This means, for a composite system $\phi\cdot\psi$, we can
construct a composite behavior tree given behavior trees for $\phi$ and
$\psi$, but the way $\phi$ and $\psi$ evolve over time is dictated by how
$\phi\cdot\psi$ evolves over time, for example, see Figure 5. Every comonoid
in $\mathbf{Poly}$ has an underlying polynomial, and the associated functor
$U$ has a right adjoint $\mathfrak{c}\langle-\rangle$:

${\mathbf{Poly}}$${\mathbf{Cat}^{\sharp}}$$\scriptstyle{\mathfrak{c}\langle-\rangle}$${\top}$$\scriptstyle{U}$
(2)

${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}TT}}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}TT}$$U$
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}T}}$$A$
TT$C$

$\Longrightarrow$

TT$U$ N$A$

TT$U$ N$A$

$:\operatorname{Hom}\mathfrak{c}\langle[\\{U,A,C\\}\mathcal{y},\\{U,A,C\\}\mathcal{y}]\rangle$

$:\operatorname{Hom}\mathfrak{c}\langle[\\{U,A\\}\mathcal{y},\\{U,A,C\\}\mathcal{y}]\rangle$

Figure 5: Example of the change in behavior of the composite system
$\mathit{Trap}_{2}$ (Figure 1e) in response to an input $A$. Just like in
Figure 3, where
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}T}$ and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N}$
represented elements of $3^{2}$, the labels
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}TT}$ and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}N}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}T}$
refer to elements of $3^{3}$, induced by where $\mathit{Trap}_{2}$ sends its
inputs data of the wiring diagram of $\mathit{Trap}_{2}$ instructs how to
convert this $A$-interaction into interactions for its $\mathit{Trap}$
subcomponents. Note that the second $\mathit{Trap}$ subcomponent is not
updated at all for an $A$ input, i.e. its update is an identity morphism in
$\mathfrak{c}\langle[\\{U,A\\}\mathcal{y},\\{U,A,C\\}\mathcal{y}]\rangle$.

There is a strong connection between this story and that of coalgebras. For
any polynomial $p$, the set of $\mathfrak{c}\langle p\rangle$ objects is
isomorphic to the underlying set of the final coalgebra on $X\mapsto
B^{A}X^{A}$. The category of functors $\mathfrak{c}\langle
p\rangle\to\mathbf{Set}$ is equivalent to the category of $p$-coalgebras. Each
behavior tree in $\mathfrak{c}\langle p\rangle$ is sent to the set of states
with that behavior.

The enriched structure of $\mathbf{DynMeal}$ now makes explicit how our
behavior trees change in response to inputs. The last improvement to be made
is one of expressivity, e.g. adding the possibility of entering an environment
and failing to ever exit it, considering lists of possible outcomes, and
considering probability distributions of possible outcomes.

###  2.4 Adding monadic effects

The expressivity captured so far can be vastly generalized by incorporating a
polynomial monad $(t,\eta,\mu)$ on $\mathbf{Set}$ into our morphisms.
Particular monads of interest are

$\mathrm{Maybe}=\mathcal{y}+1,\qquad\mathrm{Writer}_{M}=M\mathcal{y},\qquad\mathrm{List}=\sum_{N:\mathbb{N}}\mathcal{y}^{N},\qquad\text{and
}\mathrm{Dist}=\sum_{N:\mathbb{N}}\Delta_{N}\mathcal{y}^{N}$ (3)

where $M$ is a monoid and ${\Delta_{N}=\\{P:N\to[0,1]\ |\ 1=\sum P(i)\\}}$.
Our work so far has been general to polynomials, not merely interfaces of the
form $Ay\to By$, so monadic effects can be incorporated into our category by
considering the Hom object of an interface $A\to B$ to be
$\mathfrak{c}\langle[Ay,t\mathbin{\triangleleft}By]\rangle$.

######  Definition 1 (Dynamic Kleisli category).

Given a polynomial monad $t$, we define a category enriched in
$\mathbf{Cat}^{\sharp}$, denoted $\mathbf{DK}_{t}$, as follows:

$\displaystyle\operatorname{Ob}(\mathbf{DK}_{t})$
$\displaystyle:=\operatorname{Ob}(\mathbf{Set})$
$\displaystyle\operatorname{Hom}_{\mathbf{DK}_{t}}(A,B)$
$\displaystyle:=\mathfrak{c}\langle[Ay,t\mathbin{\triangleleft}By]\rangle$

##  3 $\mathbf{DK}_{t}$ as a traced monoidal category

Throughout this section we assume that $(t,\eta,\mu)$ is a Cartesian
polynomial monad. This is sufficient to show that $\mathbf{DK}_{t}$ is a
cocartesian monoidal $\mathbf{Cat}^{\sharp}$-enriched category. In Section 3.1
we will show it is a $\mathbf{Cat}^{\sharp}$-enriched category, and in Section
3.2 we will show it has coproducts.

In fact, we would like $\mathbf{DK}_{t}$ to be traced monoidal, meaning that
there are morphisms

$\mathrm{Tr}^{U}_{A,B}\colon\operatorname{Hom}_{\mathbf{DK}_{t}}(A\otimes
U,B\otimes U)\to\operatorname{Hom}_{\mathbf{DK}_{t}}(A,B)$ (4)

satisfying various compatibility conditions. Traced monoidal categories have a
graphical syntax that includes loops

$f$$\textnormal{Tr}(f)$$\scriptstyle U$$\scriptstyle A$$\scriptstyle B$

(see also [21]). This notion was defined for $\mathbf{Set}$-enriched
categories in [11], and the definition can be extended to the $V$-enriched
setting by asking that the trace map (4) be a map in $V$. In Section 3.3, we
will propose a trace map for $\mathbf{DK}_{t}$, whenever $t$ is exceptional in
the sense of Definition 2.

###  3.1 $\mathbf{Cat}^{\sharp}$-enriched category structure on
$\mathbf{DK}_{t}$

In this section we suppose a good deal more familiarity with $\mathbf{Poly}$.
The proposed $\mathbf{Cat}^{\sharp}$-enriched category structure on
$\mathbf{DK}_{t}$ was given in Definition 1; our first goal in this section is
to prove that it satisfies the correct properties. In Section 3.2 we will show
that it is monoidal.

For any lax monoidal functor $\mathcal{V}\to\mathcal{W}$, there is an induced
functor $\mathcal{V}\text{-}\mathbf{Cat}\to\mathcal{W}\text{-}\mathbf{Cat}$.
For all monoidal categories $(\mathcal{V},I,\otimes)$, the functor
$\mathcal{V}(I,-)\colon\mathcal{V}\to\mathbf{Set}$ is lax monoidal, and we
call the induced functor $V\text{-}\mathbf{Cat}\to\mathbf{Cat}$ as the
underying category functor. We say that a category $\mathcal{C}$ is enriched
in $\mathcal{V}$ when there is a $\mathcal{V}$-category for which
$\mathcal{C}$ is the underlying category. Our second goal in this section is
to show that the usual Kleisli category $\mathbf{Set}_{t}$ is enriched in
$(\mathbf{Cat}^{\sharp},\mathcal{y},\otimes)$.

Our strategy for the first goal is to show that $\mathbf{Set}_{t}$ is enriched
in $(\mathbf{Poly},\mathcal{y},\otimes)$.

######  Theorem 1.

Let $(t,\eta,\mu)$ be a polynomial monad. The Kleisli category
$\mathbf{Set}_{t}$ is enriched in $(\mathbf{Poly},\mathcal{y},\otimes)$.

###### Proof.

For sets $A,B:\mathbf{Set}$, define the polynomial

$h^{t}_{A,B}\coloneqq[A\mathcal{y},t\mathbin{\triangleleft}B\mathcal{y}].$ (5)

Maps of the form $\mathcal{y}\to h^{t}_{A,B}$ are in bijection with polymomial
maps $A\mathcal{y}\to t\mathbin{\triangleleft}B\mathcal{y}$. Note that these
are in bijection with functions $A\to t\mathbin{\triangleleft}B$, which are
exactly the Kleisli morphisms, i.e. we have

$\mathbf{Poly}(\mathcal{y},h^{t}{A,B})\cong\mathbf{Set}_{t}(A,B).$ (6)

So it suffices to define an identity and a unital and associative composition
law for the hom-objects $h^{t}_{A,B}:\mathbf{Poly}$.

For the identity on $A$ we use

$A\mathcal{y}\cong\mathcal{y}\mathbin{\triangleleft}A\mathcal{y}\xrightarrow{\eta\mathbin{\triangleleft}A\mathcal{y}}t\mathbin{\triangleleft}A\mathcal{y}.$

Maps of the form $h^{t}_{A,B}\otimes h^{t}_{B,C}\to h^{t}_{A,C}$ are in
bijection with maps
$A\mathcal{y}\otimes[A\mathcal{y},t\mathbin{\triangleleft}B\mathcal{y}]\otimes[B\mathcal{y},t\mathbin{\triangleleft}C\mathcal{y}]\to
C\mathcal{y}$, so beginning with the evaluation map
$A\mathcal{y}\mathbin{\triangleleft}[A\mathcal{y},t\mathbin{\triangleleft}B\mathcal{y}]\to
t\mathbin{\triangleleft}B\mathcal{y}$, it suffices to find a map
$(t\mathbin{\triangleleft}B\mathcal{y})\otimes[B\mathcal{y},t\mathbin{\triangleleft}C\mathcal{y}]\to
C\mathcal{y}$. Since $\mathbf{Poly}$ is duoidal, we have the desired map:

$(t\mathbin{\triangleleft}B\mathcal{y})\otimes(\mathcal{y}\mathbin{\triangleleft}[B\mathcal{y},t\mathbin{\triangleleft}C\mathcal{y}])\xrightarrow{\textnormal{duoid}}(t\otimes\mathcal{y})\mathbin{\triangleleft}(B\mathcal{y}\otimes[B\mathcal{y},t\mathbin{\triangleleft}C\mathcal{y}])\xrightarrow{\textnormal{eval}}t\mathbin{\triangleleft}t\mathbin{\triangleleft}C\mathcal{y}\xrightarrow{\mu}t\mathbin{\triangleleft}C.$

It is easy to check that these definitions are associative and unital. ∎

######  Corollary 1.

Let $(t,\eta,\mu)$ be a polynomial monad. The Kleisli category
$\mathbf{Set}_{t}$ is enriched in
$(\mathbf{Cat}^{\sharp},\mathcal{y},\otimes)$.

###### Proof.

For sets $A,B$, let $h^{t}_{A,B}:\mathbf{Poly}$ be as in (5). Since the
functor
$\mathfrak{c}\langle-\rangle\colon\mathbf{Poly}\to\mathbf{Cat}^{\sharp}$ is
lax monoidal, we can define hom-objects

$\mathbf{DK}_{t}(A,B)\coloneqq\mathfrak{c}\langle
h^{t}_{A,B}\rangle=\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}B\mathcal{y}]\rangle$

giving rise to a $\mathbf{Cat}^{\sharp}$-category. To see that its underlying
category is $\mathbf{Set}_{t}$, we use Eqs. 6 and 2

$\mathbf{Cat}^{\sharp}(\mathcal{y},\mathfrak{c}\langle
h^{t}_{A,B}\rangle)\cong\mathbf{Poly}(\mathcal{y},h^{t}_{A,B})\cong\mathbf{Set}_{t}(A,B),$

completing the proof. ∎

As a $\mathbf{Cat}^{\sharp}$-category, $\mathbf{DK}_{t}$ not only has an
underlying ordinary category, induced by the lax monoidal functor
$\mathbf{Cat}^{\sharp}(\mathcal{y},-)\colon\mathbf{Cat}^{\sharp}\to\mathbf{Set}$,
but another corresponding ordinary category as well, induced by the lax
monoidal functor
$\operatorname{Ob}\colon\mathbf{Cat}^{\sharp}\to\mathbf{Set}$. There is a
natural transformation between these two:

${(\mathbf{\mathbf{Cat}^{\sharp}},\mathcal{y},\otimes)}$${(\mathbf{Set},1,\times)}$$\scriptstyle{\mathbf{Cat}^{\sharp}(\mathcal{y},-)}$$\scriptstyle{\operatorname{Ob}}$

By Definition (1), we recover $\mathbf{Meal}/\sim$ from $\mathbf{DK}_{t}$ by
locally applying $\operatorname{Ob}$, as in the following.

######  Proposition 1.

The functor
$\mathbf{Cat}^{\sharp}\text{-}\mathbf{Cat}\to\mathbf{Set}\text{-}\mathbf{Cat}$
induced by $\operatorname{Ob}\colon\mathbf{Cat}^{\sharp}\to\mathbf{Set}$ sends
$\mathbf{DK}_{t}\mapsto\mathbf{Meal}/\sim$.

###  3.2 Coproduct monoidal structure on $\mathbf{DK}_{t}$

We next show that the $\mathbf{Cat}^{\sharp}$-category $\mathbf{DK}_{t}$ has
coproducts, as defined in [12, §3.8] and explicated in [23].

We need to show that for any two sets $A,B:\mathbf{Set}$, there are morphisms

$i\colon\mathcal{y}\to\mathfrak{c}\langle
h^{t}_{A,A+B}\rangle\qquad\text{and}\qquad
j\colon\mathcal{y}\to\mathfrak{c}\langle h^{t}_{B,A+B}\rangle$

such that for each $C:\mathbf{Set}$, each $v:\mathbf{Cat}^{\sharp}$ and each
pair of maps $f\colon v\to\mathfrak{c}\langle h^{t}_{A,C}\rangle$ and $g\colon
v\to\mathfrak{c}\langle h^{t}_{B,C}\rangle$, there is a unique morphism
$(f,g)\colon v\to\mathfrak{c}\langle h^{t}_{A+B,C}\rangle$ such that the
following diagrams commute

${\mathcal{y}\otimes v}$${\mathfrak{c}\langle
h^{t}_{A,A+B}\rangle\otimes\mathfrak{c}\langle
h^{t}_{A+B,C}\rangle}$${v}$${\mathfrak{c}\langle
h^{t}_{A,C}\rangle}$$\scriptstyle{\cong}$$\scriptstyle{i\otimes(f,g)}$$\scriptstyle{f}$
${\mathcal{y}\otimes v}$${\mathfrak{c}\langle
h^{t}_{B,A+B}\rangle\otimes\mathfrak{c}\langle
h^{t}_{A+B,C}\rangle}$${v}$${\mathfrak{c}\langle
h^{t}_{B,C}\rangle}$$\scriptstyle{\cong}$$\scriptstyle{j\otimes(f,g)}$$\scriptstyle{g}$
(7)

######  Theorem 2.

For any polynomial monad $(t,\eta,\mu)$, the $\mathbf{Cat}^{\sharp}$-category
$\mathbf{DK}_{t}$ has coproducts.

###### Proof.

For any $p,q,x:\mathbf{Poly}$, the inclusions $p\to p+q\leftarrow q$ induce an
isomorphism

$[p+q,x]\xrightarrow{\cong}[p,x]\times[q,x]$

in $\mathbf{Poly}$, so in particular we have

$h^{t}_{(A+B),C}\cong h^{t}_{A,C}\times h^{t}_{B,C}.$

By (2), maps $v\to\mathfrak{c}\langle p\rangle$ in $\mathbf{Cat}^{\sharp}$ are
in bijection with maps $v\to p$ of polynomials. Thus we can identify a pair of
$\mathbf{Cat}^{\sharp}$-maps $f\colon v\to\mathfrak{c}\langle
h^{t}_{A,C}\rangle$ and $g\colon v\to\mathfrak{c}\langle h^{t}_{B,C}\rangle$
with a single $\mathbf{Poly}$-map $(f,g)\colon v\to h^{t}_{A+B,C}$. The
commutativity of the diagrams from (7) follows easily. ∎

###  3.3 Proposed traced structure on $\mathbf{DK}_{t}$

In this section we propose a trace structure on $\mathbf{DK}_{t}$ for certain
polynomial monads $t$, which we call _exceptional_ because they are equipped
with an element $\xi\colon 1\to t$ that acts like an exception: if any
branches of a syntax tree throw an exception then so does the whole tree.

Defining the trace map requires even more background on $\mathbf{Poly}$ than
the previous sections. Whereas the $\mathbf{Cat}^{\sharp}$-category structure
on $\mathbf{DK}_{t}$, as defined in Sections 3.1 and 3.2 was induced by a
simpler, $\mathbf{Poly}$-category structure on $\mathbf{DK}_{t}$, the
application to rewriting and the trace structure both make use of the full
$\mathbf{Cat}^{\sharp}$-enrichment.

Our first goal is to define exceptional monads.

######  Lemma 1.

For any cartesian polynomial monad $(t,\eta,\mu)$, the polynomial $t+1$ also
carries the structure of a polynomial monad, and the coproduct inclusion $t\to
t+1$ is a morphism of monads.

###### Proof.

It suffices to show that for any $t$ there is a distributive law
$t\mathbin{\triangleleft}(\mathcal{y}+1)\to(\mathcal{y}+1)\mathbin{\triangleleft}t$
that commutes with the inclusion $\mathcal{y}\to\mathcal{y}+1$ on both sides.

In any category with a terminal object, a coproduct inclusion
$A\rightarrowtail B$, i.e. an isomorphism $A+A^{\prime}\cong B$ for some
$A^{\prime}$, induces a map

$B\xrightarrow{\cong}A+A^{\prime}\xrightarrow{A+!}A+1$

such that $A\to B\to A+1$ is the coproduct inclusion.

It is easy to show that every cartesian monomorphism in $\mathbf{Poly}$ is a
coproduct inclusion. Moreover, for any polynomial $p$, the map $p\cong
p\mathbin{\triangleleft}\mathcal{y}\to
p\mathbin{\triangleleft}(\mathcal{y}+1)$ is a cartesian monomorphism because
$\mathcal{y}\to\mathcal{y}+1$ is, and $\mathbin{\triangleleft}$ preserves
monomorphisms and cartesian maps in both variables. Thus we have a map
$p\mathbin{\triangleleft}(\mathcal{y}+1)\to
p+1\cong(\mathcal{y}+1)\mathbin{\triangleleft}p$, natural with respect to
cartesian maps $p\to p^{\prime}$. One can check that when $t$ is a cartesian
monad, this map is always a distributive law, completing the proof. ∎

######  Definition 2 (Exceptional monad).

Let $(t,\eta,\mu)$ be a cartesian polynomial monad. An _exception_ structure
on $t$ is a retraction $\xi\colon t+1\to t$ of the monad inclusion $t\to t+1$
from Lemma 1.

By Lemma 1, $t+1$ is an exceptional monad for any cartesian polynomial monad
$t$.

######  Remark 1.

In the multiplication $\mu\colon t\mathbin{\triangleleft}t\to t$ of an
exceptional monad, a position of the left-hand side consists of a position
$I:t(1)$ and, for every direction $i:t[I]$, a position $J_{i}:t(1)$. If either
$I$ or any of the the $J_{i}$ is the exceptional element $\xi$, then its image
under $\mu$ must be the exceptional element: an exception anywhere causes an
exception in the whole computation.

The notion of exceptional monad differs from that of _monad with zero_ [28]
even though in each case the monad $t$ is equipped with a constant $1\to t$.
For example, the $\mathrm{List}$ monad has a zero, namely the empty list, but
it is not exceptional because a list of lists can contain the empty list
without its concatenation being empty.

We next propose our trace map
$\mathrm{Tr}^{U}_{A,B}\colon\mathfrak{c}\langle[(A+U)\mathcal{y},t\mathbin{\triangleleft}(B+U)\mathcal{y}]\rangle\to\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}B\mathcal{y}]\rangle$.
In fact, it is more straightforward to define an _iteration_ map as in [21] of
the form

$\mathit{iter}^{A}_{B}\colon\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}(A+B)\mathcal{y}]\rangle\to\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}B\mathcal{y}]\rangle$
(8)

at which point we can define $\mathrm{Tr}^{U}_{A,B}$ to be given by the
composite

$\displaystyle\mathfrak{c}\langle[(A+U)\mathcal{y},t\mathbin{\triangleleft}(B+U)\mathcal{y}]\rangle$
$\displaystyle\to\mathfrak{c}\langle[(A+U)\mathcal{y},t\mathbin{\triangleleft}(A+U+B)\mathcal{y}]\rangle$
$\displaystyle\xrightarrow{\mathit{iter}^{A}_{B}}\mathfrak{c}\langle[(A+U)\mathcal{y},t\mathbin{\triangleleft}B\mathcal{y}]\rangle$
$\displaystyle\to\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}B\mathcal{y}]\rangle.$

To get there, we need to be more explicit about the cofree comonad
construction and the free monad construction on a polynomial $p$.

The free monad $\mathfrak{m}\langle p\rangle$ on a pointed polynomial
$\mathcal{y}\to p$ is constructed in two steps. For any finitary pointed
polynomial $q$—one for which each $q[J]$ is a finite set—the free monad on $q$
can be constructed in one step, namely as the colimit:

$\mathfrak{m}\langle q\rangle\coloneqq\operatorname*{colim}(\cdots\leftarrow
q^{\mathbin{\triangleleft}n+1}\xleftarrow{g_{n}}q^{\mathbin{\triangleleft}n}\leftarrow\cdots\leftarrow
q)$

where the maps $g_{n}\colon q^{\mathbin{\triangleleft}n}\to
q^{\mathbin{\triangleleft}n+1}$ are defined inductively by
$p^{\mathbin{\triangleleft}n}\cong\mathcal{y}\mathbin{\triangleleft}p^{\mathbin{\triangleleft}n}\to
p\mathbin{\triangleleft}p^{\mathbin{\triangleleft}n}=p^{\mathbin{\triangleleft}n+1}$.
An arbitrary polynomial $p$ can be written as the filtered limit of its
vertical projections $p\to p^{j}$ onto finitary polynomials: that is, for each
sum-component $I:p(1)$, just replace $p[I]$ by an arbitrary finite subset of
it, and take the limit of all such things under component-wise projection.
That limit is isomorphic to $p$, and we write $p\cong\lim_{j:J_{p}}p^{(j)}$.
By construction, each of these $p^{(j)}$ is finitary, so let
$\mathfrak{m}\langle p^{(j)}\rangle\coloneqq\mathfrak{m}\langle
p^{(j)}\rangle$ denote the free monad on it, constructed as above. Then
finally we construct the free monad $\mathfrak{m}\langle p\rangle$ on $p$ as
their filtered limit:

$\mathfrak{m}\langle p\rangle\coloneqq\lim_{j:J_{p}}\mathfrak{m}\langle
p^{(j)}\rangle.$

The cofree comonoid $\mathfrak{c}\langle p\rangle$ on $p:\mathbf{Poly}$ is
constructed in just one step. It is carried by the limit

$\mathfrak{c}\langle p\rangle\coloneqq\lim(\cdots\to
p^{(n+1)}\xrightarrow{f^{(n)}}p^{(n)}\to\cdots\to
p^{(1)}\xrightarrow{f^{(0)}}p^{(0)})$

where the $p^{(k)}$ are defined inductively as follows:

$\displaystyle p^{(0)}$ $\displaystyle\coloneqq\mathcal{y}$ $\displaystyle
p^{(k+1)}$
$\displaystyle\coloneqq(p\mathbin{\triangleleft}p^{(k)})\times\mathcal{y}$ and
the maps $f^{(k)}\colon p^{(k+1)}\to p^{(k)}$ are defined inductively as
follows: $\displaystyle p^{(0)}=p\times\mathcal{y}$
$\displaystyle\xrightarrow{f^{(0)}\coloneqq\textnormal{proj}}\mathcal{y}=p^{(0)}$
$\displaystyle p^{(k+1)}=(p\mathbin{\triangleleft}p^{(k+1)})\times\mathcal{y}$
$\displaystyle\xrightarrow{f^{(k+1)}\coloneqq(p\mathbin{\triangleleft}f^{(k)})\times\mathcal{y}}(p\mathbin{\triangleleft}p^{(k)})\times\mathcal{y}=p^{(k+1)}$

######  Proposition 2.

Let $\mathcal{y}\to p$ be a cartesian map of polynomials, and let
$\mathfrak{m}\langle p\rangle$ be the free monad on it; let
$\mathfrak{c}\langle p\rangle$ be the cofree comonad on $p$. There is a
natural cartesian monomorphism

$\mathfrak{m}\langle p\rangle\to\mathfrak{c}\langle
p\rangle\mathbin{\triangleleft}(\mathcal{y}+1).$

###### Proof.

For any $q:\mathbf{Poly}$, the functor $-\mathbin{\triangleleft}q$ commutes
with limits. Since $\mathfrak{c}\langle-\rangle$ is a right adjoint, it also
commutes with limits. Since the limit of cartesian monomorphisms is a
cartesian monomorphism, we may assume $p$ is finitary and it suffices to
produce compatible cartesian monomorphism $\varphi_{i}\colon
p^{\mathbin{\triangleleft}i}\to p^{(i)}\mathbin{\triangleleft}(\mathcal{y}+1)$
for each $i:\mathbb{N}$. We take $\varphi_{0}$ to be the cartesian
monomorphism $\mathcal{y}\to\mathcal{y}+1$. Suppose given $\varphi_{i}$. To
define
$p^{\mathbin{\triangleleft}i+1}\to(p\mathbin{\triangleleft}p^{(i)})\mathcal{y}\mathbin{\triangleleft}(\mathcal{y}+1)$,
it suffices to give two maps, $p^{\mathbin{\triangleleft}i+1}\to
p\mathbin{\triangleleft}p^{(i)}\mathbin{\triangleleft}(\mathcal{y}+1)$ and
$p^{\mathbin{\triangleleft}i+1}\to\mathcal{y}+1$. For the latter, use
$p_{(i+1)}\to 1\to\mathcal{y}+1$. It remains to give a cartesian monomorphism
$p^{\mathbin{\triangleleft}i+1}\to
p\mathbin{\triangleleft}p^{(i)}\mathbin{\triangleleft}(\mathcal{y}+1)$, which
we obtain by induction
$p\mathbin{\triangleleft}p^{\mathbin{\triangleleft}i}\xrightarrow{p\mathbin{\triangleleft}\varphi_{i}}p\mathbin{\triangleleft}p^{(i)}\to
p\mathbin{\triangleleft}p^{(i)}\mathbin{\triangleleft}(\mathcal{y}+1)$. ∎

######  Lemma 2.

In $\mathbf{Poly}$, any cartesian monomorphism $p\to q$ is a coproduct
inclusion.

###### Proof.

Suppose $\varphi\colon p\to q$ is a cartesian monomorphism. Since $p\mapsto
p(1)$ is a right adjoint, $\varphi(1)\colon p(1)\to q(1)$ is an injection; let
$J^{\prime}\coloneqq q(1)-p(1)$ be its compliment. Then we have the desired
isomorphism

$q\cong p+\sum_{j:J^{\prime}}\mathcal{y}^{q[j]}.$

∎

######  Proposition 3.

For any pointed polynomial $\mathcal{y}\to p$ there is a map
$\mathfrak{c}\langle
p\rangle\mathbin{\triangleleft}(\mathcal{y}+1)\to\mathfrak{m}\langle
p\rangle+1$.

###### Proof.

By Proposition 2 we have a cartesian monomorphism $\mathfrak{m}\langle
p\rangle\to\mathfrak{c}\langle p\rangle\mathbin{\triangleleft}\mathcal{y}+1$,
which is a coproduct inclusion by Lemma 2. For any coproduct $p\to q$
inclusion in a category with terminal object, we have a map $q\cong
p+p^{\prime}\to p+1$, completing the proof. ∎

Let’s return to our goal of producing an $\mathit{iter}$ map as in (8). By
(2), it suffices to define a polynomial map of the form
$\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}(A+B)\mathcal{y}]\rangle\to[A\mathcal{y},t\mathbin{\triangleleft}B\mathcal{y}]$,
or equivalently one of the form
$A\mathcal{y}\otimes\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}(A+B)\mathcal{y}]\rangle\to
t\mathbin{\triangleleft}B\mathcal{y}$. Given the exceptional structure
$\xi\colon t+1\to t$ on $t$ and the fact that any monad $t$ carries an algebra
structure $\mathfrak{m}\langle t\rangle\to t$, it suffices by Proposition 3 to
find a map
$A\mathcal{y}\otimes\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}(A+B)\mathcal{y}]\rangle\to\mathfrak{c}\langle
t\rangle\mathbin{\triangleleft}(\mathcal{y}+1)\mathbin{\triangleleft}B\mathcal{y}$.

We produce the desired map again by induction. The right-hand side is the
limit

$\mathfrak{c}\langle
t\rangle\mathbin{\triangleleft}(\mathcal{y}+1)\mathbin{\triangleleft}B\mathcal{y}\cong\lim(t^{(i)}\mathbin{\triangleleft}(\mathcal{y}+1)\mathbin{\triangleleft}B\mathcal{y}).$

When $i=0$, we use
$A\mathcal{y}\otimes\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}(A+B)\mathcal{y}]\rangle\to
1\to
t^{(0)}\mathbin{\triangleleft}(\mathcal{y}+1)\mathbin{\triangleleft}B\mathcal{y}$.
Suppose given a map $\varphi_{i}\colon
A\mathcal{y}\otimes\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}(A+B)\mathcal{y}]\rangle\to
t^{(i)}\mathbin{\triangleleft}(\mathcal{y}+1)\mathbin{\triangleleft}B\mathcal{y}$.
Define

$\displaystyle
A\mathcal{y}\otimes\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}(A+B)\mathcal{y}]\rangle$
$\displaystyle\to\mathcal{y}\times(A\mathcal{y}\otimes([A\mathcal{y},t\mathbin{\triangleleft}(A+B)\mathcal{y}]\mathbin{\triangleleft}\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}(A+B)\mathcal{y}]\rangle)$
$\displaystyle\to\mathcal{y}\times(t\mathbin{\triangleleft}(A+B)\mathcal{y}\mathbin{\triangleleft}\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}(A+B)\mathcal{y}]\rangle)$
$\displaystyle\to\mathcal{y}\times(t\mathbin{\triangleleft}((A\mathcal{y}\mathbin{\triangleleft}\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}(A+B)\mathcal{y}]\rangle)+B\mathcal{y}))$
$\displaystyle\xrightarrow{\cong}\mathcal{y}\times(t\mathbin{\triangleleft}((A\mathcal{y}\otimes\mathfrak{c}\langle[A\mathcal{y},t\mathbin{\triangleleft}(A+B)\mathcal{y}]\rangle)+B\mathcal{y}))$
$\displaystyle\to\mathcal{y}\times(t\mathbin{\triangleleft}((t^{(i)}\mathbin{\triangleleft}(\mathcal{y}+1)\mathbin{\triangleleft}B\mathcal{y})+B\mathcal{y}))$
$\displaystyle\to\mathcal{y}\times(t\mathbin{\triangleleft}t^{(i)}\mathbin{\triangleleft}(\mathcal{y}+1)\mathbin{\triangleleft}B\mathcal{y})$
$\displaystyle\to(\mathcal{y}\times(t\mathbin{\triangleleft}t^{(i)}))\mathbin{\triangleleft}(\mathcal{y}+1)\mathbin{\triangleleft}B\mathcal{y})$
$\displaystyle\xrightarrow{\cong}t^{(i+1)}\mathbin{\triangleleft}(\mathcal{y}+1)\mathbin{\triangleleft}B\mathcal{y}$

We have now defined the purported $\mathit{iter}$ map and hence trace map, as
explained above.

######  Conjecture 1.

The purported trace on $\mathbf{DK}_{t}$ defined above satisfies the axioms of
a traced monoidal category.

While this conjecture has not been proven, it has influenced the development
of a working implementation in the open source AlgebraicRewriting.jl. This is
the subject of Section 4.

##  4 Application to rewriting and agent-based modeling

###  4.1 Attributed C-Sets

Our case study uses the AlgebraicJulia ecosystem [16] due to its support for
wiring diagram manipulation (Catlab.jl) as well as its graph rewriting
library, AlgebraicRewriting.jl [4]. The core data structure of AlgebraicJulia
is the ACSet, i.e. attributed $\mathcal{C}$-Set for some finitely-presented
category $\mathcal{C}$. ACSets offer a category-theoretic model of databases
which extends $\mathcal{C}$-Sets (i.e. copresheaves) to include
noncombinatorial data [17]. The database schema is given by a profunctor, i.e.
a functor $S:|S|\to 2$, which distinguishes objects in $|S|$ as representing
either tables or attribute types. Given an assignment $K:S_{1}\to\mathbf{Set}$
which provides concrete Julia types for attributes, the category
$\mathrm{ACSet}^{S}_{K}$ is bicomplete and a topos, and thus is an appropriate
setting for applying graph rewriting rules.

Consider an ACSet $X$, equipped with a distinguished ‘focus’, i.e. morphism
$A\to X$. We will soon see applications where it makes sense to think of $A$
as the _shape_ of a particular agent in the state of the world $X$, where the
agent is picked out by the chosen morphism. Note that considering ACSets
without any agent is tantamount to picking the agent shape to be an empty
ACSet, 0, which is the initial object of $\mathrm{ACSet}^{S}_{K}$.

For example, consider the task of modeling wolves, sheep, and grass
distributed on a directed graph, where the wolves and sheep are facing
particular directions and have some integer number of energy units. Grass
grows on vertices and has an integer number of days until it is grown. The
schema in Figure 6 shows one way to model this.

Dir${E}$Wolf${V}$Sheep${{\mathbb{N}}}$$\scriptstyle{\mathit{tgt}}$$\scriptstyle{\mathit{src}}$$\scriptstyle{w_{\mathit{eng}}}$$\scriptstyle{w_{\mathit{pos}}}$$\scriptstyle{s_{\mathit{pos}}}$$\scriptstyle{s_{\mathit{eng}}}$grass$\scriptstyle{w_{\mathit{dir}}}$$\scriptstyle{s_{\mathit{dir}}}$$\scriptstyle{dir}$

Figure 6: Left An ACSet schema with six objects and morphisms as well as two
attribute types and six attributes (dotted edges). Center An example ACSet on
this schema Right The example, informally visualized with energy as integers,
sheep as blue boxes, and wolves as red boxes. If we wished to distinguish the
wolf as the ‘agent’, we would use an ACSet morphism into this example from an
ACSet with one wolf, zero edges, and one vertex, i.e. the _shape_ of a wolf.

###  4.2 A DSL for graph rewriting programs

We use the theory of $\mathbf{DK}_{t}$ to implement a graph rewriting
programming language, with data manipulation specified by rewrite rules acting
upon ACSets (possibly with agents). These programs can be assembled from a
small number of primitive generators. In conjunction with Catlab’s general
infrastructure for manipulating wiring diagrams, these primitives function as
a powerful domain-specific language for agent-based modeling and programming
via graph rewriting.

The domain and codomain of our morphisms of interest consist of sets of
diagrams of the form in Figure 7, and coproducts thereof. Each such diagram,
which we will call a trajectory, is a sequence of ‘world states’ $X_{i}$ with
distinguished focuses $A_{i}\to X_{i}$. If the trajectory is represented by a
variable t::Traj in pseudocode, then let last(t) return $X_{n}$, length(t)
return $n$, and t[i] return $A_{i}\to X_{i}$. Let
postcompose(t::Traj,f::Hom(X,Xi),i::Int) compute the composite of f with the
partial maps from $i$ to $n$. This returns either a total morphism or nothing.
Let (t::Traj)+(b::Hom(A,Xn)) extend the trajectory with an identity partial
map. Because there are now infinite sets as the domains and codomains of our
morphisms, we adopt the following shorthand: when visualizing wiring diagrams,
a wire labeled by an ACSet $A_{n}$ represents the set of all trajectories
whose current agent is $A_{n}$. Stating a morphism is of type $A+B\rightarrow
C$ for ACSets $A,B,C$ indicates the domain is the coproduct of the set of
trajectories with current agent $A$ and the trajectories with current agent
$B$ and that the codomain is the set of trajectories with current agent $C$.

${{A_{1}}}$${{A_{2}}}$${{\cdots}}$${{A_{n}}}$${{X_{1}}}$${{X_{2}}}$${{\cdots}}$${{X_{n}}}$${\shortmid}$${\shortmid}$${\shortmid}$
Figure 7: A trajectory in the space of ACSets. $X_{1}$ and $X_{n}$
respectively represent the initial (resp. current) state of the world during
the simulation, and each successive world state is related to the previous via
a partial map (indicated by a ticked arrow). Each world state $X_{i}$ also has
a distinguished focus $A_{i}\to X_{i}$.

Some generating morphisms for rewriting programs are shown in Figures 8 and 9.
The semantics of the stateless generators is visually represented in Figure 8
and described here: Rewrite extends a trajectory with a partial map induced by
applying the rewrite rule (DPO, SPO, SqPO, and PBPO+ [15] semantics
supported). Rewrite rules must also have their pattern $L$ and replacement $R$
related to a specific input agent shape $A$ and output agent shape $B$,
respectively. The input agent shape imposes a strong constraint on valid
matches via a triangle which must commute. If, nevertheless, multiple matches
are valid, an arbitrary one is selected. If it is successfully rewritten, the
$B$ outport is exited, otherwise the $A$ outport is exited. Weaken extends a
trajectory without changing the state of the world $X_{n}$ by precomposing the
agent morphism. Strengthen extends a trajectory via pushout, which
simultaneously changes the agent shape and the state of the world. Init
switches the trajectory to a particular world state and agent, with no
relation to the previous world state. Fail can be given the semantics of
raising an exception. Alternatively, if the context is the $\mathrm{List}+1$
monad, it could silently produce an empty list.

The semantics of the ControlFlow box is to redirect an input to one of its
outports, possibly nondeterministically and possibly as a function of its
trajectory data. These morphisms are of the form
$\operatorname{Hom}_{\mathbf{DK}_{t}}(A,n\times A)$ for some set $n$ and have
a Mealy transition function which is pure, by which we mean it can be factored
into a map $\phi:S\times A\rightarrow S\times(n\times A)$ (such that
$\phi\mathbin{\fatsemi}\pi_{3}=\pi_{2}$) followed by the monad unit $\eta$.

${{S\times A}}$${{S\times(n\times A)}}$${{S\times t\triangleleft(n\times
A)}}$$\scriptstyle{\text{pure}\
\phi}$$\scriptstyle{\phi}$$\scriptstyle{S\times\eta\triangleleft(n\times A)}$

The semantics of the Query box is a Mealy machine with state space
$\mathrm{List}(\operatorname{Hom}_{\mathrm{ACSet}})\times\mathbb{N}$. The
first element is the list of queued ‘agents’ we have yet to process, and the
second element keeps track of what time step (in the trajectory) the Query box
was originally entered. The dynamics are given by two functions, an update
function $S\times A+C\to S$ and a readout function $S\times A+C\to A+B+0$.
Entering through the $A$ port at step $n$ has the significance of starting the
Query process anew; the internal state is overwritten to store $n$ and a list
of morphisms $B\to X_{n}$. Entering the $C$ port communicates that we have
finished one of the subagent’s subroutines - the agent is removed from the
box’s state and all other agents are pushed forward to the current timestep.
How the Query box is exited is firstly determined by whether or not there are
any remaining agents to process; if there are any, the $B$ port is exited with
a $B$ agent. If there are none, we try to exit with original $A$ agent. If
this agent is total when brought to the current state, we exit through the $A$
port, otherwise the $0$ port. In pseudocode, these functions are characterized
below:

⬇

1updateA(_, traj::Traj) = (homomorphisms(B,last(traj)), length(traj))

2updateC((bnext:bs,i), traj::Traj) =

3 ([b for b in bs if !isnothing(postcompose(traj,b,i))],i)

4updateC(([],i::Int),_) = error

5

6readout((bnext:bs,_), traj::Traj) = return (B,traj + bnext)

7readout(([],i::Int), traj::Traj) = case postcompose(traj,traj[i],i) of

8 nothing => return (0, traj + initial(last(traj)))

9 new_a_x => return (A, traj + new_a_x)

Figure 8: Primitive generating morphisms for graph rewriting programs which
have trivial dynamics, i.e. they are pure functions from input ports to output
ports, with exception to Fail, which can raise an exception. Figure 9:
Primitive generating morphisms for graph rewriting programs which have
nontrivial dynamics. Left. A generator for pure control flow. The value
$\mathbb{R}^{\geq 0}$ assigned to each outgoing wire is a weight to bias the
probability of exiting through that port. Right. A generator for running a
subroutine $B\to C$ for each $B$ agent in the the current world, $X_{i}$.

Although the ‘standard’ means of using a Query box is to connect a subroutine
from the $B$ outport to the $C$ inport, yielding a $A\to A+0$ interface, it
can be used in more flexible ways. For example, a procedure which applies the
rule $rw$ to a single (arbitrary) $A$ in the world state which satisfies
property $\phi$ is visualized in Figure 10.

Figure 10: A program $0\to 0$, in context of the $\mathrm{Maybe}$ monad. Its
input is a trajectory with an empty agent in its current time step. We then
loop over possible agents of shape $A$. As soon as one is found which both
satisfies property $\phi$ and is successfully rewritten, we replace our focus
$A$-shaped agent with the unique $0$-shaped agent and exit.

The above primitives were designed in order to be both easily interpretable
(e.g. control flow, focus shifting, and state changing are all separated
concerns) as well as expressive enough to reproduce popular agent-based
models. However, these primitives can be extended in a principled rather than
ad-hoc manner, due to the specification that new primitives must contain the
data of a morphism in $\mathbf{DK}_{t}$. Furthermore, these primitives can be
composed to libraries of operations at a higher level of abstraction for use
by a domain expert.

###  4.3 Implementation

Our implementation is general over a finitary exceptional polynomial monad as
in Definition 2, using a codata structure for representing (potentially-
infinite) behavior trees. These trees can be provided directly for each
generator, although it is more convenient to programmatically generate them
from a Mealy machine representation. By switching from $t=\mathrm{Maybe}$ to
$\mathrm{List}+1$ or $\mathrm{Dist}+1$, we obtain nondeterministic or
probabilistic simulations. For many graph rewriting examples, we wish to
consider all possible matches, not merely an arbitrary match. A principled way
to do this is to use a Rewrite which produces a list of outputs, corresponding
to all possible matches. This is particularly important if a program is being
constructed to empirically test which graphs are reachable via a collection of
rewrite rules. Furthermore, if certain matches are more likely than others,
then a distribution on this output list can be incorporated into our programs.

One way in which we can take advantage of our formalism for rewriting programs
is functorial data migration [24]. Given a functor $S\to T$ between ACSet
schemas, a $\Sigma$ migration pushes $S$ ACSets forward to $T$ ACSets in a
universal way, while $\Delta$ migration migrates data the other direction. As
this is functorial, it is possible to apply these migrations to ACSet
morphisms, rewrite rules, and entire graph rewriting programs. Another key
advantage of working graphically is the various forms of composition of wiring
diagrams, which allow for concise operations for organization of morphisms
with $\otimes$ and as well as hierarchically constructing programs via
operadic substitution.

###  4.4 Example: discrete Lotka Volterra model

The first example agent-based model showcased by Netlogo [26] on their website
is a model of wolf-sheep predation. An analogue of this model using the
present framework is presented in Figure 11. Its construction leverages
$\Sigma$ and $\Delta$ data migrations, operadic substitution,
$t=\mathrm{Maybe}$, and the primitives Rewrite, Weaken, ControlFlow, and
Query. A pedagogical walkthrough of the model’s construction and running the
model is provided in an accompanying notebook. An example construction in
$\mathbf{DK}_{t}$ using the $\mathrm{Dist}$ monad can also be found in the
accompanying notebook.

Figure 11: A program performing a wolf-sheep simulation. $\mathit{Swap}$ here
represents a $\Delta$ migration which swaps wolves and sheep in the schema of
Figure 6, allowing for a shared implementation of actions that are common to
wolves and sheep. The agent shape $0$ is depicted as an unlabeled wire,
although wires sharing the same target port need not all be labeled, as they
must share the same agent for the program to be well-typed.

##  5 Conclusion and Future work

A general theory of dynamical tracing guided the development of a graph
rewriting DSL. Because this language is understood mathematically and
expressed as combinatorial data, rather than programming syntax, high level
rewrite procedures can be understood and serialized, independently from any
particular implementation (although an implementation in Julia was developed).
Abstract operations like data migration and various forms of composition
become natural to perform on these procedures due to their interpretation as
morphisms in $\mathbf{DK}_{t}$. Furthermore, the assimilation of Mealy
machines, system interfaces and behaviors, as well as monadic effects via
polynomial functors inspired an implementation that is both concise and
general.

There are dimensions along which this work can be extended. The formalism we
presented focuses on a dynamical system as something that is interacted with
by a single agent. It remains frozen as the agent interacts with other
systems, but this assumption could be relaxed as we consider multiple
simultaneous agents—i.e. parallel programming with graph transformation. The
notion of a trajectory presented here requires all ACSets involved to share
the same schema (as there are no morphisms between ACSets of different
schemas); this could be generalized to allow for multiscale modeling (data
transformation in both a high level, ‘macroscopic’ schema as well as a low
level ‘microscopic’ schema).

We plan to represent more existing agent-based models as well as develop new
ones in this formalism. Agent-based models are a preferred style of modeling
in any situation with emergent effects, such as physical phenomena (e.g. flow
and diffusion simulations) [3], human transportation networks [22], and
epidemiology [10]. Adding Catlab support for incremental graph matching [9]
will be important for rewriting programs to be competitive in performance with
established software like Netlogo and Kappa.

## References

  * [1] Ahman, D., Uustalu, T.: Directed containers as categories. Electronic Proceedings in Theoretical Computer Science 207, 89–98 (apr 2016). doi:10.4204/eptcs.207.5, https://doi.org/10.4204%2Feptcs.207.5
  * [2] Blostein, D., Fahmy, H., Grbavec, A.: Issues in the practical use of graph rewriting. In: Graph Grammars and Their Application to Computer Science: 5th International Workshop Williamsburg, VA, USA, November 13–18, 1994 Selected Papers 5. pp. 38–55. Springer (1996)
  * [3] Bonabeau, E.: Agent-based modeling: Methods and techniques for simulating human systems. Proceedings of the national academy of sciences 99(suppl_3), 7280–7287 (2002)
  * [4] Brown, K., Patterson, E., Fairbanks, J.P.: Double pushout rewriting of c-sets. CoRR abs/2111.03784 (2021), https://arxiv.org/abs/2111.03784
  * [5] Bunke, H.: Attributed programmed graph grammars and their application to schematic diagram interpretation. IEEE Transactions on Pattern Analysis and Machine Intelligence (6), 574–582 (1982)
  * [6] Corradini, A., Heindel, T., Hermann, F., König, B.: Sesqui-pushout rewriting. In: International Conference on Graph Transformation. pp. 30–45. Springer (2006)
  * [7] Ehrig, H., Pfender, M., Schneider, H.J.: Graph-grammars: An algebraic approach. In: 14th Annual Symposium on Switching and Automata Theory (swat 1973). pp. 167–180. IEEE (1973)
  * [8] Fahmy, H.: Reasoning in the presence of uncertainty via graph rewriting. (1996)
  * [9] Fan, W., Wang, X., Wu, Y.: Incremental graph pattern matching. ACM Transactions on Database Systems (TODS) 38(3), 1–47 (2013)
  * [10] Hunter, E., Mac Namee, B., Kelleher, J.D.: A taxonomy for agent-based models in human infectious disease epidemiology. Journal of Artificial Societies and Social Simulation 20(3) (2017)
  * [11] Joyal, A., Street, R., Verity, D.: Traced monoidal categories. In: Mathematical proceedings of the cambridge philosophical society. vol. 119, pp. 447–468. Cambridge University Press (1996)
  * [12] Kelly, M.: Basic concepts of enriched category theory, vol. 64. CUP Archive (1982)
  * [13] Löwe, M.: Algebraic approach to single-pushout graph transformation. Theoretical Computer Science 109(1-2), 181–224 (1993)
  * [14] Niu, N., Spivak, D.I.: Polynomial functors: A general theory of interaction
  * [15] Overbeek, R., Endrullis, J., Rosset, A.: Graph rewriting and relabeling with pbpo+. In: Graph Transformation: 14th International Conference, ICGT 2021, Held as Part of STAF 2021, Virtual Event, June 24–25, 2021, Proceedings. pp. 60–80. Springer (2021)
  * [16] Patterson, E., other contributors: Algebraicjulia/catlab.jl: v0.13.5 (Dec 2021). doi:10.5281/zenodo.5771194, https://doi.org/10.5281/zenodo.5771194
  * [17] Patterson, E., Lynch, O., Fairbanks, J.: Categorical Data Structures for Technical Computing. Compositionality 4 (Dec 2022). doi:10.32408/compositionality-4-5, https://doi.org/10.32408/compositionality-4-5
  * [18] Patterson, E., Spivak, D.I., Vagner, D.: Wiring diagrams as normal forms for computing in symmetric monoidal categories. Electronic Proceedings in Theoretical Computer Science 333, 49–64 (feb 2021). doi:10.4204/eptcs.333.4, https://doi.org/10.4204%2Feptcs.333.4
  * [19] Plump, D.: The design of gp 2. arXiv preprint arXiv:1204.5541 (2012)
  * [20] Schürr, A.: Progress: A vhl-language based on graph grammars. In: Graph Grammars and Their Application to Computer Science: 4th International Workshop Bremen, Germany, March 5–9, 1990 Proceedings 4. pp. 641–659. Springer (1991)
  * [21] Selinger, P.: A survey of graphical languages for monoidal categories. In: New Structures for Physics, pp. 289–355. Springer Berlin Heidelberg (2010). doi:10.1007/978-3-642-12821-9_4, https://doi.org/10.1007%2F978-3-642-12821-9_4
  * [22] Smith, L., Beckman, R., Baggerly, K.: Transims: Transportation analysis and simulation system. Tech. rep., Los Alamos National Lab.(LANL), Los Alamos, NM (United States) (1995)
  * [23] (https://math.stackexchange.com/users/666875/richard southwell), R.S.: What is a coproduct in an enriched category? Mathematics Stack Exchange, https://math.stackexchange.com/q/4353966, uRL:https://math.stackexchange.com/q/4353966 (version: 2022-01-11)
  * [24] Spivak, D.I.: Functorial data migration. Information and Computation 217, 31–51 (2012)
  * [25] Spivak, D.I.: A reference for categorical structures on $\mathbf{Poly}$ (2022). doi:10.48550/ARXIV.2202.00534, https://arxiv.org/abs/2202.00534
  * [26] Tisue, S., Wilensky, U.: Netlogo: A simple environment for modeling complexity. In: International conference on complex systems. vol. 21, pp. 16–21. Citeseer (2004)
  * [27] Voss, C., Petzold, F., Rudolph, S.: Graph transformation in engineering design: an overview of the last decade. AI EDAM 37, e5 (2023)
  * [28] Wisnesky, R.: Minimizing monad comprehensions. Tech. rep., Citeseer (2011)