This is a tutorial text giving an advanced introduction to the diagrammatic syntax of monoidal (and Cartesian) closed categories in the style of “functorial boxes”.
This syntax can be efficiently represented as a data structure which we call hierarchical hypergraphs, the systematic rewriting of which represents a way of deriving abstract machines for higher-order programming languages directly from their operational semantics.
To arrive at this main intended application we pay attention in particular to the diagrammatic language of adjunctions and explicit strictifications.
Finally, we present new proof techniques made possible by a quasi-canonical presentation of terms in monoidal closed categories called foliations which are useful in the case of complicated program transformations such as automatic differentiation and closure conversion.

Dan R. Ghica and Fabio Zanasi, 2023

§ INTRODUCTION

The representation of syntax of programming languages, and even more so of natural languages, requires complex data structures.
When writing programs, specifications of programs, or syntactic models of programming langauges, such as operational semantics or abstract machines, it is customary to deploy syntax in its serialised form: a linear sequence of symbols which we call text or, to use more technical vocabulary, terms.
Terms are, however, an awkward data structure for algorithmic purposes.
Hence, compilers and other programming language tools never work on terms directly but immediately convert them, through processes known as lexing and parsing, into more useful data structures.
The most common, if not the most sophisticated, is called the abstract syntax tree (AST).

It is generally admitted that ASTs, although an improvement on terms, are far from the ideal data structure for representing syntax.
Various graph-based alternatives have been proposed, with some of them implemented in production compilers.
Such data structures fall under the general label of intermediate representation (IR).
We propose an improved representation called hierarchical hypergraphs (HH), which have uniquely helpful theoretical and algorithmic properties.

The design space for data structures to represent syntax is large.
Sound methodology requires that an IR is best derived in a principled way, from more general mathematical concepts, as informed by pragmatic considerations where needed.
Our mathematical starting point is string diagrams (SD), a two-dimensional syntax for monoidal categories.

A clarification is required: unfortunately, in the literature string diagrams are often conflated with their concrete, combinatorial representations as graphs.
We find it profitable to maintain the distinction and to insist on the former being syntax, albeit two-dimensional or planar.
Most mathematical syntax is one-dimensional, or linear, so one may reasonable wonder whether there are any advantages to two-dimensional syntax.
Or, perhaps, it is preserved merely out of deference to tradition.

One-dimensional syntax can absorb quotienting by associativity, thus reducing unpleasant use of parantheses.
We need not distinguish between $a\cdot(b\cdot c)$ and $(a\cdot b)\cdot c$ when the operation $\cdot$ is associative.
This is why we are entitled to simply write $a\cdot b\cdot c$.
If $\cdot$ is a common operation we can even represent it by simple concatenation, so that

\[
abc = a(bc) = (ab)c.
\]

If the operation is simply concatenation it would make sense to represent the unit of the operation, should it exist, by empty space (␣), as empty space is the unit of concatenation, which would give the following unit rules:

\[
\]

This is, of course, not common practice, but if used it would also allow unit rules to be absorbed into linear notation.

Two dimensional notation can be useful in absorbing quotienting by further equations.
Consider for instance fractions writen two-dimensionally

\[
a \div b = \frac a b.
\]

Written in planar form, certain unobvious linear equations are simply absorbed by the notation:

\[
(a\div c)(b\div d)=\frac a c \frac b d = \frac{ab}{cd}=(ab)\div (cd).
\]

This suggests a criterion to compare notations:
A notation is better if it absorbes more equations, by which we mean that instead of using an explicit equation to identify two terms they become syntactically equal in the improved notation.

Planar notation has an additional advantage over linear notations in that it can make certain notational invariants obvious.
Consider for example matrices, written most commonly in two dimensional syntax:

\[
M =
\begin{pmatrix}
a & b & c\\
u & v & w\\
x & y & z
\end{pmatrix}.
\]

For formal reasoning (in proof assistants) or algorithmic processing (in computer libraries) two-dimensional syntax is not possible so matrices are linearised as vectors-of-vectors, with $M$ above writen either as list of columns

\[
M = \bigl(
(a, u, x), (b, v, y), (c, w, z)
\bigr),
\]

or as list of rows.
The key invariant that all columns (or rows, respectively) have the same size is no longer enforced by the notation: in the planar notation it is impossible to write a matrix with mismatched rows or columns.

This suggests an additional criterion for comparing notations:
A superior notation absorbs more invariants, so that malformed terms cannot be written as such.

The planar notation for matrices also absorbes equational properties, for instance the fact that the transpose is an involution.

To conclude this brief detour into two-dimensional syntax, hopefully it can be now accepted that moving from linear to planar has certain non-trivial advantages.
However, moving from syntactic to combinatorial graph-like representations will have further, deeper advantages which we will explore in the rest of this tutorial.
Yet, neither terms, nor diagrams, nor graphs completely supersede each other.
They are all useful forms of syntax, fit for different purposes.

The ultimate aim of this tutorial is to persuade the reader to accept a new and multifaceted vision of syntax which we (rather grandly) call syntactic trinitarianism: terms, diagrams, graphs.
They are all ultimately interchangeable representations of an abstract, Platonic if you like, ideal of syntax, each serving distinct roles:

Terms. Despite the obvious appeal of graphical syntaxes, in particular to beginners, term syntax remains the workhorse of formal writing, be it programming, mathematics, or logic.
The serial sequence of symbols, easily grouped by the brain into tokens, wrapping around the end of the page, decorated with whitespace and font variations remains the tried-and-tested repository for formal text.
Our facility as humans with this representation arguably goes back to language itself evolving first as a spoken form of communication: a serial sequence of auditory symbols, decorated with pitch and tone, modulated by volume and speed.
Programs ranging from student projects of tens of lines to software infrastructure such as operating systems or compilers of millions of lines of code can be written, understood (to some extent), and evolved using this format.
For all its shortcomings term syntax is here to stay.

Graphs. Algorithms do not work very well on terms.
They are an awkward data structure.
But graphs are efficient, allowing a far greater diversity of structure compared to the list-like terms.
They can represent sharing and they can allow fast access from one region to the other by following edges.
However, the more expressive structure comes at a conceptual cost.
When modifying graphs, maintaining the right invariants is difficult.
Writing algorithms and reasoning about properties of graphs is harder since they lack inductive structure.
Even coming up with the right graph structure for a problem is difficult since the design space can be broad and not obviously constrained.

Diagrams. The conceptual bridge between terms and graphs are diagrams.
A new development, with roots in theoretical physics and category theory, string diagrams are ideally suited to this purpose.
They are syntactic in the sense that they can be generated by grammars, but they are two-dimensional rather than linear, much like the standard notation for matrices is a two-dimensional syntax.
The two-dimensional syntax, if written in a certain way, makes the graph representation intuitive and its formalisation unsurprising.

The particular concept that bridges diagrams and graphs is that of foliation, to which we dedicate Section <ref>.
A foliation of a diagram is obtained by representing it first as a graph, then representing the graph back into a diagram of a particular form, which we can thing of as a quasi-normal form.
These are not true normal forms because they are not unique, yet they are useful in greatly simplifying the structure of diagrams, ultimately allowing the formulation of inductive algorithms on essentially non-inductive data structures.
These algorithms are not efficient, but they can be reasoned about using convenient inductive methods.
Moreover, these algorithms, which are essentially executable specifications, can be further refined into graph-algorithms which are efficient.

The presentation assumes some basic understanding of the relevant categorical concepts, particulary in order to motivate the entire project.
Some understanding of basics of programming language theory, such as operational semantics and abstract machines, as well as basic compiler developments should further enhance the appreciation of the material.
Despite the theoretical underpinnings, the presentation here should lead to a practical understanding of hierarchical graphs as a realistic and useful data structure for representing syntax in compilers, interpreters, and program analysis tools.[An open-source implementation of this framework is under development. ]

The style of presentation is neither purely theoretical nor purely practical, but a kind of `technology transfer'.
Readers with a background in category theory should be able to find genuine practical applications which hopefully will inform their work and allow them to converse and collaborate with compiler writers.
Readers with a background in compiler development should find themselves alerted to the possiblities of using category theory not only as a semantic framework, not only as a type-theoretic framework, but also as a syntactic framework.
Finally, this work is intended to be read as a tutorial rather than a comprehensive survey or a reference handbook.
To minimise distractions we will save all references and discussions for special sub-sections.

The structure of the presentation is linear and the reader is advised to proceed section-by-section.
We start with a general introduction to string diagrams in Section <ref> in which we pay attention to some constructions which are generally disregarded in the standard literature, in particular adjunctions and strictification, but are essential for dealing with closed monoidal structure.
Building closely on this we introduce, in Section <ref>, string diagrams for closed monoidal categories and Cartesian closed categories, with an immediate application to the syntax and equational theory of the lambda calculus.
The connection between the two dimensional syntax of string diagrams and the graph rewriting intuitions are made precise in Section <ref>.
Section <ref> will turn to the operational semantics of the lambda calculus, pure but also extended with operations into more practical programming languages.
Finally, in Section <ref> we give three non-trivial applications of string diagrams: type inference, closure conversion, and reverse automated differentiation.
They will arguably provide some evidence that string diagrams lead to clearer and more insightful versions of some known algorithms that, in their terms-based formulation, are considered sometimes exceedingly complicated.

§.§ Related work

We will only mention some related work in terms of syntax and intermediate representations.
There is much more related work which we shall not mention here as it will be discussed in more detail in the following sections.

The earliest and one of the most influential approaches to making syntax a data structure with better algorithmic properties is de Bruijn `nameless dummies', known widely as `de Bruijn indices' <cit.>.
In this notation variable names are replaced by natural numbers, assigned using a deterministic schema that takes into account the depth of the binder.
This notation is widely used in formalisations of the lambda calculus, but it has the drawback that variables need to be re-indexed following applications.
This is a symptom of it being non-compositional, as the integer assignment schema is global for the term.

For representations of syntax two alternative approaches are significant.
The first one has been promoted by Pitts, Gabbay, Urban, Cheney and others and is based on so-called `nominal techniques' <cit.>.
The key goal here is to reconcile quotienting by alpha equivalence with recursive definitions and inductive proofs.
This goal is achieved by introducing names as a data structure equipped with only two operations: one local, testing for equality, and one global, generating a fresh name.
Because names are indistinguishable save for their identity they are dubbed `atoms'.
An essential consequence of this is that nominal data structures are `equivariant', which means that two elements are indistinguishable if the underlying atoms are systematically changed.

Graph-based representations are also implicitly equivariant, since graph isomorphism subsumes equivariance for the actual identity of nodes and edges.
However, nominal techniques give a nice syntactic model of binding which does not appear in the graph representation, where it does not seem to be required.
Instead of the standard structural induction or recursion that nominal representations support, the string-diagram representation offers a new approach, of induction or recursion on `foliations'.

A different approach to syntax is `higher-order abstract syntax' (HOAS) <cit.>.
It is a way of incorporating notions of binding in an abstract syntax tree when using a meta-language that itself supports binding.
This is helpful for encoding programming langauges into, for example, proof checkers, but it is not ideal as a data structure to be used, as is our aim, as an intermediate represenatation in a compiler.
HOAS and de Bruijn notations complement each other, and can be used together <cit.>.

The approach to intermediate representation in compilers is quite different from using de Bruijn or HOAS notations, which indicates a rift between theory and practice.
There is also a sometimes manifested confusion between `intermediate representation' and `intermediate language', which we shall clarify before we proceed.
The former is a (programming) language not intended for a human programmer.
It is either an aggressive desugaring of the object language, as is the case for example with OCaml's FLambda intermediate langauge <cit.>, or is an abstraction of the details of assembly, as is the case with LLVM <cit.>.
In both cases, the intermediate language has a much simplified syntax, which makes specifications less cumbersome.

In contrast, an intermediate representation (IR) is a data structure, the simplest of which is the abstract syntax tree (AST).
The AST is quite simple, for example missing any concept of direct sharing, and relying either on copying or on auxiliary data structures such as symbol tables.
The graph representation unifies all this in a single, convenient data structure.
Graph-based IRs have been used before with some success in commercial compilers <cit.>, sometimes under the name of sea-of-nodes representation <cit.>, but they have rarely given the required importance.
For instance, it is relatively common for intermediate languages to be formalised in mechanical proof assistants <cit.> but we are unaware of efforts to mechanise the theory of graph-based IRs, as data structures.
Although we do not present it here, an effort of formalising the graph representation of string diagrams is ongoing.
Note that there exists an important distiction must be made between IRs and other graph-based representations which are used in compilers, such as control-flow graphs (CFGs) and single-static assignment (SSA), or register allocation algorithms.

Finally, a special acknowledgement is required for `interaction nets', a diagrammatic representation of programming language which uses graph rewriting to give an operational semantics <cit.>.
The only difference, which is nevertheless essential, between interaction nets and our string diagrams is that the former are flat and the latter are hierarchical.
We will see later on why the flat structure is problematic when it comes to representing the binding structure common in programming languages.

§ STRING DIAGRAMS

We assume a familiarity of the reader with basic concepts of category theory and string diagrams, therefore in this first section we will move quickly through the material, emphasising only those aspects which are specific to the current presentation.
For readers who require a more introductory presentation to category theory there are numerous tutorial presentations to start from, many of them aimed at computer scientists <cit.>.
Particularly relevant and useful are tutorial introductions to string diagrams <cit.>.

§.§ Categories and their graphical language

A (small) category $\category C$ consists of

* a set of objects $\mathit{obj}(\category C)$

* a set of morphisms $hom(\category C)$ such that for each morphism $f$ there exist unique objects $A$ and $B$, respectively called the source and target of $f$,  written $f:A\to B$.

* a composition operation $\circ$ on morphisms such that

closure for all morphisms if $f:A\to B$ and $g: B\to C$ then $g\circ f:A\to C$ is a morphism

associativity for all morphisms $f:A\to B$, $g: B\to C$, $h:C\to D$,

\[ h\circ(g\circ f) = (h\circ g)\circ f \]

identity for all objects $A$ there exists a morphism $\id_A:A\to A$ such that

\[ \id_B\circ f = f \circ \id_A = f\]

for any $f:A\to B$.

We may freely generate a category $\category C$ from a signature $(\Sigma_0,\Sigma_1)$ consisting of a set $\Sigma_0$ of generating objects and a set $\Sigma_1$ of generating morphisms with sources and targets in $\Sigma_0$. First, $\Sigma$-terms are defined inductively as follows:

* All morphisms $f \colon A \to B$ in $\Sigma_1$ and identities $\id_A \colon A \to A$ are $\Sigma$-terms.

* If $f \colon A \to B$, $g \colon B \to C$ are $\Sigma$-terms, then $g\circ f:A\to C$ is a $\Sigma$-term.

The category $\category C$ freely generated by $(\Sigma_0,\Sigma_1)$ is defined as having objects $\mathit{obj}(\category C) = \Sigma_0$ and morphisms  $hom(\category C)$ the $\Sigma$-terms quotiented by associativity and identity equations as above.

Morphisms are sometimes called maps or arrows.
The name of the morphism is sometimes stacked onto the arrow:

\[
A\stackrel f \to B \defeq f:A\to B.
\]

If $A,B\in \mathit{obj}(\category C)$ are fixed we write the set of all $f:A\to B$ as $hom_{\category C}(A,B)$.
Composition is sometimes defined using a reverse-order operator

\[
f \semic g\defeq g\circ f,
\]

as it follows more naturally the left-to-right order of the arrow itself, i.e.

\[
(A\stackrel f \to B)\semic (B\stackrel g\to C) = A\stackrel {f\semic g}\longrightarrow C.
\]

The notation above is often streamlined into

\[
A\stackrel f \to B\stackrel g\to C = A\stackrel {f \semic g}\longrightarrow C,
\]

usually rendered as a so-called commutative diagram:

\[
\xymatrix{
A \ar[dr]_{f \semic g} \ar[r]^f & B \ar[d]^g \\
& C }
\]

Render the equations for associativity and identity as commutative diagrams.

Because composition is associative, it is acceptable to elide the brackets when writing up more complex compositions, for example

\[
(f \semic g) \semic (h \semic (i \semic j)) = f \semic g \semic h \semic i \semic j.
\]

More specifically, if using the unbracketed form $f \semic g \semic h \semic i \semic j$ it does not matter how we insert brackets, because all bracketings will result in expressions which are equal even though syntactically distinct.
So the unbracketed expression represents an equivalence class of syntactic terms quotiented by associativity.
This is a very common syntactic trick in mathematics for associative operations that we used automatically, without reflecting on it.
But the idea of using notational convention to quotient classes of syntactic objects (terms) by their semantics is an attractive one as it inexorably leads to simpler, more abstract, notation.
In this situation we say that the equivalence is absorbed by the notation.
The question is: can we generalise this idea to other syntactic structures?
Using string diagrams, to be introduced momentarily, the answer is a clear `yes'.

The graphical language of a category $\category C$ is

Objects $A$ are represented as labelled wires
\[ \input{pics/id.pdf_tex} \]

Morphisms $f:A\to B$ are represented as boxes
\[ \input{pics/obj.pdf_tex} \]

Identities $\id_A:A\to A$ are represented as labelled wires
\[ \hfill \input{pics/id.pdf_tex} \]

Composition $f \semic g$ is represented as
\[ \input{pics/comp.pdf_tex} \]

We call terms of the graphical language string diagrams.

The graphical language is a bracket-free syntax so it presumes associativity of composition by construction.
As we shall see soon, it is possible to use the equivalent of brackets (boxes) in the graphical language for disambiguation.
However, it remains our goal to avoid this as much as possible.
Reducing the need for brackets or boxes is one of the hallmarks of good syntax.

The identity equations are absorbed into the graphical language.
Note the following ambiguity regarding this string diagram,

\[
\input{pics/obj.pdf_tex}
\]

which could be interpreted as $id_A \semic f$ or $f \semic id_B$.

\[
id_A \semic f=f \semic  id_B.
\]

Similarly, the string diagram

\[
\input{pics/id.pdf_tex}
\]

can be interpreted as $id_A$ or $id_A \semic id_A$ or $id_A \semic id_A \semic id_A$ and so on, all of which are equal.

The astute reader might rightfully complain that, actually

\begin{align*}
id_A &=\input{pics/id.pdf_tex} \\
id_A \semic id_A &=\input{pics/id2.pdf_tex}\\
id_A \semic id_A \semic  id_A &=\input{pics/id3.pdf_tex}.
\end{align*}

And that is a valid objection which can be raised against a sleight of hand we have performed.
We did not specify how the string diagrams are to be represented concretely.
The answer is going to be, at this stage, informal.
Formalising the graphical language as a combinatorial object is possible, and it will capture the intuition that they are graph-like objects with well defined (albeit hidden) interfaces to the right and to the left of the diagram, anchoring what appears like `dangling' wires.
As graphs, these objects will be quotiented by an appropriately defined notion of isomorphism, which renders the length and other attributes of the wires irrelevant, focussing on connectivity only.
This is why the three wires of increasing length above are all equal in the interpretation, as they can be formalised as isomorphic graph-like structures.
We consider these formal details mostly as a sanity check, in the sense that they precisely described the desired intuitions, so we postpone them until Section <ref>.

§.§ Functors and boxes

This section will introduce some more basic definitions and notations, to be illustrated with interesting examples later on.

Let $\category C$ and $\category D$ be two categories.
We define a map $F:\category C \to \category D$ between these categories as a map on objects together with a map on morphisms such that source and target objects are preserved:

\[
F(f:A\to B) = Ff:FA\to FB.
\]

In the graphical language maps $F:\category C \to \category D$ are represented as $F$-labelled boxes:

\[
F(f:A\to B) := \input{pics/map.pdf_tex}
\]

The box serves the same role, in the two-dimensional landscape of string diagrams, that brackets serve in the one-dimensional world of terms.
But, unlike a bracket, the box acts on the object: as the wire crosses the boundary of the box the objects on either side may be different.
This can be emphasised by the use of further graphical conventions, such as use of distinct colours; this distinction is sometimes worth making.
However, in general we leave this an implicit caveat.

A map $F:\category C \to \category D$ is a functor if it preserves composition and identity, i.e.

\begin{align*}
F(id_A:A\to A) &= id_{FA}: FA\to FA \\
F(A\stackrel f\to B \stackrel g\to C) &= FA\stackrel {Ff}\to FB \stackrel {Fg}\to FC.
\end{align*}

In the graphical language functoriality is expressed as the following equalities of string diagrams:

\[
\input{pics/fid.pdf_tex}
\]

If clear from context we may elide some of the annotations in order to prevent clutter.
For instance, if $\category C$ and $\category D$ are singletons (a single object) we can write the functoriality diagrams for some fixed map between them as:

\[
\input{pics/fidlite.pdf_tex}
\]

The notion of map of categories generalises in an obvious way to maps from two categories, i.e. $F:\category C_1\times \category C_2\to \category D$.
The graphical language representation of $F(f_1, f_2)$ is

\[
\input{pics/map2.pdf_tex}
\]

Maps of two categories which are also functors are called bifunctors.

Using different colours for the inside and outside of the box, indicating the two different categories, can also add an extra visual indicator helpful for error-checking, as we shall see in the next section.

§.§.§ Natural transformations

Climbing further up the ladder of abstraction, natural transformations can be seen as maps between functors.
They are collections of morphisms indexed by objects in the source category, which are `uniform' over the target category.
The uniformity property is defined below.

If $F,G$ are functors from $\category C$ to $\category D$ then a natural transformation $\eta:F\Rightarrow G$ between them is an object-indexed family of morphisms such that:

* For each object $X$ in $\mathcal C$ there exists a morphism $\eta_X: FX\to GX$ in $\category D$.

* For each morphism $f:X\to Y$ in $\mathcal C$

\[
\xymatrix{
X\ar[d]_f & FX\ar[d]_{Ff} \ar[r]^{\eta_X} & GX\ar[d]_{Gf} \\
Y & FY\ar[r]_{\eta_Y} & GY
\]

The morphism $\eta_X$ is called the component of $\eta$ at $X$.
It is usual, and convenient, to add the morphism $f:X\to Y$ to the commuting diagram as an annotation.
If the components of a natural transformation are isomorphisms then the natural transformation is called a natural isomorphism.
In this case, we write $\eta_X : FX \simeq GX.$

Natural transformations are, from the point of view of string diagrams, just collections of morphisms so no new graphical notation needs to be introduced.
But the commuting diagram for components can be represented graphically as:

\[
\input{pics/nat.pdf_tex}
\]

Above we left out all the information that can be inferred from the diagram context, to reduce clutter.
To further reduce clutter we may indicate the functor using colour-coding or by decorating the border of the box, e.g.

\[
\input{pics/natlite.pdf_tex}
\]

and removing more information that can be inferred from the context of the diagram ($X$ and $Y$ can be recovered from $f:X\to Y$ etc.)

The graphical notation, we can argue, is already starting to pay dividends by now.
String diagrams more directly suggest that naturality is a generalisation of commutativity, using functoriality and indexing as a clever way to make the source and the target of the map $f$ match with those of a well chosen component of the natural transformation.
Furthermore, as we shall see shortly, when calculating with string diagrams it will be easier to identify formula `redexes', i.e. spots in a formula where an equation can be applied.

§.§.§ Adjunctions

Two functors that stand in a certain relation to each other are said to be adjoint.
Adjoint functors are common in mathematics and computer science.
We shall not present examples at this moment, just introduce definitions and properties, with examples to follow later.

Adjunctions can be characterised in several ways, but we will emphasise the definition most suitable to a nice rendering in the graphical language of string diagrams, namely the so-called unit-counit adjunction.

A unit-counit adjunction between two categories $\category C$ and $\category D$ consists of two functors $F:\category D\to \category C$ and $G:\category C\to\category D$ and two natural transformations $\epsilon:F\circ G\Rightarrow \id_{\category C}$ and $\eta:\id_{\category D}\Rightarrow G\circ F$ respectively called the counit and the unit of the adjunction such that for each object $A$ in $\category C$ and $X$ in $\category D$:

\begin{gather*}
F\eta_{X} \semic  \epsilon_{FX} = \id_{FX}\\
\eta_{GA} \semic  G\epsilon_A = \id_{GA}.
\end{gather*}

If two functors are adjoint, as defined above, we say that $F$ is the left adjoint and $G$ the right adjoint, written $F\dashv G$.

Using string diagrams, the two diagram equations become quite suggestive in a graphical rendering:

\[
\input{pics/adj.pdf_tex}
\]

To make the diagrams even more suggestive we can represent the unit and the counit as opposite facing half-circles.
To avoid ambiguity, if necessary, they can be annotated with the indexing object.
We use different colours to indicate morphisms in the two categories, and colour the functor boxes in the same colour as their codomain.
With these further conventions the two string diagram equations become simply:

\[
\input{pics/adjlite.pdf_tex}
\]

The colours (purple and orange) are used to identify what category the identity belongs to, and also the two functors by tagging them with the colour of their codomain category.
All elided information (object labels, etc.) can be unambiguously inferred.

Homset adjunctions

The unit-counit presentation of adjunctions is arguably the best when using string diagrams.
On the basis of this definition we can also show the equivalence of the alternative homset formulation of adjunctions.

An adjunction between categories $\category C$ and $\category D$ consists of two functors $F:\category D\to \category C$ and $G:\category C\to\category D$ such that for all objects $A$ in $\category D$ and $V$ in $\category C$ there exists a family of bijections, natural in $A$ and $V$, between morphisms sets

\[
hom_{\category C}(FA, V)\cong hom_{\category D}(A, GV).
\]

Naturality here means that there are natural isomorphisms between the pair of functors ${\mathcal {C}}(F-,V):{\mathcal {D}}\to \mathrm {Set} $ and ${\mathcal {D}}(-,GV):{\mathcal {D}}\to \mathrm {Set}$ for a fixed $V$ in $\mathcal {C}$, and also the pair of functors ${ {\mathcal {C}}(FA,-):{\mathcal {C}}\to \mathrm {Set} } $ and ${\mathcal {D}}(A,G-):{\mathcal {C}}\to \mathrm {Set} $ for a fixed $A$ in $\mathcal {D}$.

We can now show that Definition <ref> is implied by Definition <ref>. The two maps, which will turn out to be inverses, are:

\[
\input{pics/homset.pdf_tex}
\]

where the orange box, decorated with a small outline mark, is the $G$ functor and the purple box, decorated with a small solid mark, the $F$ functor.

This is how we show the first direction of these maps being inverses.

\[
\input{pics/hom-inv.pdf_tex}
\]

Show the other direction of the property of homset functions being inverses.

The reader is encouraged to repeat the same exercise in the conventional term language of category theory or using conventional commuting diagrams in order to experience the relative convenience of the diagrammatic notation.
For calculations with functors (which are not endofunctors) the use of colour serve as an additional `type-checking' mechanism, which adds an extra layer of notational comfort.

§.§ Monoidal categories

A bifunctor of particular importance in many areas of mathematics, physics, and computer science is the monoidal tensor, $\otimes:\category C\times \category C\to \category C$ as it can be used to model the construction of aggregate data types out of simpler data types.
The monoidal tensor is associative up to isomorphism, indicating the fact that data can be aggregated in ways that are different yet retrievable one form another in a canonical way.
This property holds both for product types and for sum types, both of which are instances of monoidal tensor.
If the tensor is associative on the nose, i.e. the isomorphisms are identities, it is said to be strict.
Once we introduce strict monoidal tensors in a category, the graphical language of string diagrams truly starts to achieve its full potential.

A monoidal category is a category $\category C$ equipped with the following structure:

Tensor A bifunctor $\otimes:\category C\times \category C\to \category C$

Unit An object $I$, also called identity

Associators A family of object-indexed natural isomorphisms (associators)

\[ \alpha_{A,B,C} : A\otimes(B\otimes C)\simeq (A\otimes B)\otimes C \]

Unitors Two families of object-indexed natural isomorphisms (left and right unitors)

\begin{align*}
\lambda_A:I\otimes A\simeq A \\
\rho_A:A\otimes I \simeq A,
\end{align*}

such that the following coherence conditions hold for all objects $A,B,C$:

\begin{gather*}
\xymatrix{
A\otimes(B\otimes (C\otimes D)) \ar[r]^{\alpha_{A,B,C\otimes D}}\ar[d]_{\id_A\otimes\alpha_{B,C,D}} & (A\otimes B)\otimes (C\otimes D) \ar[r]^{\alpha_{A\otimes B,C,D}} & ((A\otimes B)\otimes C)\otimes D\\
A\otimes((B\otimes C)\otimes D) \ar[rr]_{\alpha_{A,B\otimes C,D}}                     & & (A\otimes (B\otimes C))\otimes D \ar[u]_{\alpha_{A,B,C}\otimes \id_D}
} \\
\xymatrix{
A\otimes(I\otimes B) \ar[rr]^{\alpha_{A,I,B}}\ar[dr]_{\id_A\otimes \lambda_B} & & (A\otimes I)\otimes B \ar[dl]^{\rho_A\otimes \id_B}\\
& A\otimes B
\end{gather*}

The first coherence is usually called the pentagon diagram and the second the triangle diagram, due to their respective shapes.

It is quite common to have composition higher priority than tensor, so $f\otimes g\circ h$ can only be bracketed as $f\otimes (g\circ h)$.
However, for most of the examples here it is more conveient that the tensor should be stronger than composition, so

\[
f\otimes g \semic h = (f\otimes g) \semic  h.
\]

The naturality of the associator isomorphism means that the following string diagram equation holds, where the box represents the $\otimes$ bifunctor:

\[
\input{pics/assoc.pdf_tex}
\]

The notation improves greatly if the tensor is strict, that is the associators $\alpha$ are identities.
In this case the equation becomes:

\[
\input{pics/assocstr.pdf_tex}
\]

We are now in a situation similar to that of the associativity of composition, in which

\[
(f \semic g) \semic h=f \semic (g \semic h)=f \semic g \semic h.
\]

We recall that boxing is the two-dimensional counterpart of bracketing, so the diagram above expresses the property that the two possible boxings are equal.
We are justified then to quotient out the boxes altogether and to absorb this equation into a new notational convention, representing the strictly associative tensor simply as:

\[
\input{pics/assocstrq.pdf_tex}
\]

Removing boxes of functors which are associative on the nose is the two-dimensional version of removing brackets of associative operations in the one-dimensional notation for terms.

A similar situation arises in the case of the unitors, where the naturality conditions, diagrammatically, are:

\[
\input{pics/unitors.pdf_tex}
\]

On the right-hand-side of the diagram the functor is the identity functor.

In the strict case the unitors are also identities, so the two diagrams become:

\[
\input{pics/unitorsstr.pdf_tex}
\]

which only makes sense if the unit identity is deleted altogehter.

Just like the identity morphism can be represented graphically in a way that makes it absorbed by composition, so the identity for the unit $\id_I$ can be absorbed into the tensor by representing it as just empty space.

\[
\input{pics/unitorsstr2.pdf_tex}
\]

In the above, the dotted box is simply an attempt to highlight the presence of empty space; it has no further meaning.

We have now defined the core diagrammatic notation of strict monoidal categories.
To summarise, it is a syntax of labelled boxes and wires in which the boxes are the morphisms and the wires the objects.
Morphisms are composed by connecting wires serially, while the monoidal tensor is a parallel stacking of diagrams.
The identity of the unit of the tensor can be elided by representing it as empty space.

In a strict monoidal category objects are essentially lists with the unit $I$ the empty list.
We introduce notations to define lists and basic operations on lists, which are handy for working with morphisms in strict monoidal categories.

List of objects: $[A_1, A_2, \ldots,A_k]$

Empty:  $[\ ]$

Concatenation:  $[A_1,\ldots,A_k]+\!\!+[B_1,\ldots,B_j]=[A_1, \ldots,A_k,B_1, \ldots,B_j]$.

This notation will come in handy occasionally. For instance, we may use it to freely obtain strict monoidal categories starting from a signature, similarly to the case of plain categories (Definition <ref>).

A monoidal signature is a pair $(\Sigma_0,\Sigma_1)$ where $\Sigma_0$ is a class of generating objects and $\Sigma_1$ a pair of generating morphisms with sources and targets lists of objects in $\Sigma_0$. Monoidal $\Sigma$-terms are defined inductively as follows:

* All morphisms $f \colon L_1 \to L_2$ in $\Sigma_1$, the identity $id_{[]} \colon [] \to []$, and identities $\id_{[A]} \colon [A] \to [A]$ for all $A \in \Sigma_0$, are $\Sigma$-terms.

* If $f \colon L_1 \to L_2$, $g \colon L_2 \to L_3$ are $\Sigma$-terms, then $f ; g \colon L_1 \to L_3$ is a $\Sigma$-term.

* If $f \colon L_1 \to L_2$, $g \colon L_3 \to L_4$ are $\Sigma$-terms, then $f \otimes g \colon (L_1 +\!\!+ L_3) \to (L_2 +\!\!+ L_4)$ is a $\Sigma$-term.

The strict monoidal category $\category C$ freely generated by $(\Sigma_0,\Sigma_1)$ is defined as having objects $\mathit{obj}(\category C) = \Sigma_0^{\star}$ (i.e., lists of objects in $\Sigma_0$) and morphisms  $hom(\category C)$ the $\Sigma$-terms quotiented by the equations of strict monoidal categories, where $[]$ acts as the identity for $\otimes$, plus the following:

\[ \id_{L_1 +\!\!+ L_2} = \id_{L_1} \otimes \id_{L_2}. \]

A common situation is for a strict monoidal category to be freely generated by a signature $(\Sigma_0,\Sigma_1)$ where $\Sigma_0$ consists of a single object, denoted by $\bullet$.
We call such strict monoidal categories single sorted.
In this case the generated objects are

\begin{align*}
\overline 0 = [\ ] &= I \\
\overline 1 = [\bullet] &= \bullet \\
\overline 2 = [\bullet, \bullet] &= \bullet \otimes \bullet \\
\overline 3 = [\bullet, \bullet, \bullet] &= (\bullet \otimes \bullet)\otimes \bullet = \bullet\otimes(\bullet\otimes\bullet) \\
\end{align*}

Every object in the strict monoidal category is fully characterised by its size so it can be written as $\overline n$ for $n$ some natural number.

Suppose that a single-sorted strict monoidal category has
morphisms generated by $\mathsf t:\overline 0\to\overline 1, \mathsf f:\overline 0\to\overline 1$, and ${\land},{\lor}:\overline 2\to \overline 1$.
Since the category is constructed as strict, generators of type $\overline 2\to \overline 1$ are represented as having two wires on the left and one wire on the right.
Concretely, a term such as

\[
\mathsf t\otimes(\mathsf f\otimes \mathsf t) \semic ((\id\otimes \mathsf f \semic {\land})\otimes{\lor}) \semic {\lor}
\]

corresponds to the diagram:

\[
\input{pics/exred.pdf_tex}
\]

Some of the equations of strict monoidal categories become trivialised by the being fully absorbed into the graphical notation.
For instance, consider the functoriality of the tensor:

\[
(f\otimes g) \semic (f'\otimes g') = (f \semic f')\otimes (g \semic g')
\]

for any $f,f',g,g'$ so that the compositions are well defined.
This is trivial since both sides of the equation correspond to the diagram

\[
\input{pics/functens.pdf_tex}
\]

Show that the following equations hold by constructing the string diagrams of all the expressions involved:

\begin{equation*}
(f \semic \id)\otimes(\id \semic g) = f\otimes g = (\id \semic f)\otimes(g \semic \id).
\end{equation*}

We refer the reader back to Example <ref>.
Let us equip the category with equations consistent with the standard interpretation of Boolean logic, i.e. $t\otimes t \semic  \land = t$, $t\otimes f \semic \land = f$ etc.
The concrete term used in the example reduces to a single Boolean value.
A possible step-by-step calculation in the one-dimensional (term) syntax involves repeated applications of naturality to re-associate the term so that the equation of boolean connectors can be applied.
On the other hand, the two-dimensional (string diagram) makes these redexes obvious.
The reader is invited to fill in the details, which are edifying.

§.§ Strictification and string diagrams

The simplified representation of the functorial box for the tensor makes calculation with string diagram for strict monoidal categories particularly pleasant.
However, many interesting categories are not strict.
The motivating examples of data types in programming languages (product, sum) are not strict.
In a programming language tuples $(a,(b,c))$ and $((a,b),c)$ and $(a,b,c)$ are never considered equal, even though canonical isomorphisms between them are straightforward.
Tupling, when non-strict, is a convenient mechanism for abstraction.
For instance, consider a type of headers ($H$), a type of payloads $P$, from which we can construct a type of messages $M=H\otimes P$, from which we can construct a type of error-correcting messages $E=M\otimes C$, where $C$ is a checksum applied to a message of type $M$.
But we could have, on the other hand, a type of error-correcting payloads $E'=P\otimes C$ where the checksum is applied to the message $M$ only, from which we can construct messages $M'=H\otimes E'$.
The first data-type is $(H\otimes P)\otimes E$, the second $H\otimes (P\otimes E)$, and they should not be taken as equal even if isomorphic.

As our overall intent is to define string diagrams for programming languages, we can not usually assume the tensor to be strict.
But without strictness, the functorial box for the tensor loses its simplifying properties and consequently the graphical notation loses its elegance.
This may seem as an insurmountable obstacle, but there exists a principled way out using strictification.
As we shall see, this construction introduces a deliberately strict version of a monoidal tensor in a way that result in a new category which is equivalent to the original.
The diagramatic presentation should give a clearer account of what is going on.

This construction

is interesting and powerful, and has been interpreted in various ways.
The broadest, and rather misleading, common interpretation is that “in a free monoidal category all diagrams made of unitors and associators commute.”

Given a monoidal category $(\category C, \otimes, I)$ we define
$\overline{\category C}$ as the strict monoidal category freely generated by:

* Objects $\overline A$ for each object $A$

* Morphisms $\overline f:\overline A\to\overline B$ for each morphism $f:A\to B$ in $\category C$.

* De-strictifying generators:

\begin{align*}
\phi &: [\ ]\to \overline I & & \input{pics/phi.pdf_tex}\\
\psi_{A, B} &: [\overline A, \overline B]\to \overline{A\otimes B} & & \input{pics/psi.pdf_tex}
\end{align*}

* Strictifying generators:

\begin{align*}
\phi^* &: \overline I \to [\ ] & & \input{pics/phistar.pdf_tex}\\
\psi_{A,B}^* &: \overline{A\otimes B}\to [\overline A, \overline B] & & \input{pics/psistar.pdf_tex}
\end{align*}

subject to the equations in Figure <ref>.

\[
\input{pics/strictification.pdf_tex}
\]

Strictification equations (Definition <ref>)

Since the category $\overline{\category C}$ is strict monoidal we are entitled to use the strict string diagrams without ambiguity.
In Figure <ref> and elsewhere we omit the labels on the generator boxes since they can be unambiguously identified by shape and number and position of wires.

This is a functorial construction, yielding a (monoidal) equivalence between
$\category C$ and $\overline{\category C}$.
The details involved in formulating the following precisely are outside the scope of this tutorial survey, so we will only state this property informally:

The category $\overline{\category C}$ is essentially equivalent to $\category C$.
Every construction in the former category is essentially the same as in the latter.

The second sentence above may seem puzzling, since the use of strictifiers and de-strictifiers appears to greatly complicate the diagrammatic language.
We will show, with a simple example, that it is not the case, and shine a light, at the same time, on the implications of strictification as a syntactic device, allowing the rigorous use of string diagrams for non-strict tensors.

Recall example <ref> in which an equation, namely

\[
(f\otimes g) \semic (f'\otimes g') = (f \semic f')\otimes (g \semic g'),
\]

is shown to hold by constructing the string diagram expression of both side and noticing that it is the same, when the tensor is strict.
Let us conduct the same exercise in a non-strict diagram.

The two diagrams are:

\[
\input{pics/functensns.pdf_tex}
\]

Showing only the part of the diagram that differs, the first diagram can be reduced to the second using the first, then fourth, then first again (twice) equations from Figure <ref>:

\[
\input{pics/firstfourth.pdf_tex}
\]

The important idea in the proof of the property in Remark <ref> is that any construction in the non-strict category can be expressed by a diagram that has the following general shape:

\[
\input{pics/drawing.pdf_tex}
\]

strictification: A prefix diagram ($\sigma^*$) which is a tree of strictifiers, flattening the tensors,

diagram: The actual diagram $f$ as if constructed in the strict setting,

de-strictification: A suffix diagram ($\tau$) specifying the association of the tensors.

So we can define string diagrams as if they were performed in a strict category, without loss of generality.
However, we can still use the non-strict tensor whenever convenient to pack structure into the wires for the purpose of abstraction.
An example will be given in the next section (Example <ref>).
More concretely speaking:

A morphism $f:A\otimes B\to C$ can be drawn without ambiguity in three equivalent ways:

\[
\input{pics/threeways.pdf_tex}
\]

Using diagrammatic reasoning and the equations of strictification prove some of the expected properties of $\overline{\category C}$, e.g. $\overline {\alpha} \semic \overline{\alpha^{-1}} = \id$.

The exercise above should make the point that diagrammatic reasoning is not a panacea, and simple equational reasoning is sometimes more handy than diagrammatic reasoning.
Diagrammatic reasoning is just another arrow in your quiver, to be fired at the appropriate targets.

[Sorting network]
A sorting network is a freely generated strict monoidal category, where the objects represent a fixed-size integer data type and there is one generator morphism $s_2:2\to 2$, a two-input sorter, plus a family of generator morphisms $k_i:0\to 1$ corresponding to constant integers  $i\in\mathbb N$, so that

\begin{align*}
(k_i\otimes k_j) \semic s_2 &= k_i\otimes k_j &\text{if }i\geq j\\
(k_i\otimes k_j) \semic s_2 &= k_j\otimes k_i &\text{if }i\le j.
\end{align*}

Larger sorting networks are constructed recursively.
Two common ones are insertion sort in which the first $n$ wires are sorted then the remaining value is inserted, and bubble sort in which the largest value is propagated to the bottom, then the remaining $n$ values are sorted.
The insert-sort network is defined by the following two recursive definitions, with base case $max_2=s_2$:

\[
\input{pics/sorting.pdf_tex}
\]

* Construct $s_4$ and simplify according to the strictification equations.

* Define the bubble-sorter, according to the informal specification above.

* Prove that the bubble-sorter and the insert-sorter are always equal.

* Define an efficient sorter, e.g. a bitonic sorter <cit.>.

§.§ Symmetric monoidal categories

Remember that we gave the tensor ($\otimes$)  higher precedence than composition ($ \semic $), so we shall continue to do that in the sequel.

A symmetric monoidal category is a monoidal category $(\category C, \otimes, I)$ such that, for every pair $A, B$ of objects in $\category C$, there is an isomorphism $\sigma_{A,B}:A\otimes B\to B\otimes A$, called symmetry, that is natural in both $A$ and $B$ and such that

\begin{align*}
\sigma_{A,I} \semic \lambda_A & =\rho_A \\
\sigma_{A,B}\otimes \id_C \semic \alpha_{B,A,C} \semic \id_B\otimes \sigma_{A,C} &=\alpha_{A,B,C} \semic \sigma_{A,B\otimes C} \semic \alpha_{B,C,A} \\
\sigma_{A,B} \semic \sigma_{B \semic A}&=\id_{A\otimes B}.
\end{align*}

As discussed in the previous section, it is simpler to work in a strict setting and add strictifier and de-strictifier morphisms globally only if non-strict tensoring is required.

In a strict monoidal category the symmetry equations are:

\begin{align*}
\sigma_{A,I}&=\id_A\\
\sigma_{A,B}\otimes \id_C \semic \id_B\otimes \sigma_{A,C} &=\sigma_{A,B\otimes C}\\
\sigma_{A,B} \semic \sigma_{B \semic A}&=\id_{A\otimes B}.
\end{align*}

The string diagram language needs no extension, so the two equations above, along with the naturality equations are given in Figure <ref>.

\[
\input{pics/symmetryo.pdf_tex}
\]

Symmetry equations

Symmetry is an important property of many instances of the monoidal tensor (e.g. Cartesian product) and reasoning with the symmetry equations above is ubiquitous.
A particularly clever development in the design of string diagram languages is to introduce special graphical notation for symmetry so that these equations become absorbed into the graphical notation.
This is done by imagining symmetry $\sigma_{A,B}$ as a swapping of the wires for $A$ and $B$.
With this new and improved graphical notation, the same equations become as in Figure <ref>, and they are absorbed into graphical equivalence by allowing wires to bend and cross and boxes to slide along them.
These are informal considerations, but a suitable mathematical concept of graph can be expressed rigorously, and the rigorously defined notion of isomorphism of such graphs corresponds precisely to the intuition at work here.

\[
\input{pics/symmetryg.pdf_tex}
\]

Symmetry equations absorbed into the graphical notation

The first equation of symmetry shows that $\sigma_{A,B\otimes C}$ can be constructed out of the simpler $\sigma_{A,B}$ and $\sigma_{B,C}$.
Attempting to formally generalise this axiom to showing how general symmetries can be constructed from the basic symmetry in a single sorted strict monoidal category is an interesting exercise which shows the usefulness of strictification in an already strict category!

The following family of mutually recursive axioms show how $\sigma_{\overline m,\overline n}$ can be constructed from $\sigma_{\overline 1, \overline 1}$ in a symmetric single sorted strict symmetric monoidal category.
These categories are a common setting for string diagrams, called PROPs (from PROducts and Permutations).

\[
\input{pics/sigmamn.pdf_tex}
\]

Even in a strict monoidal category it is convenient to have a way to unpack a composite wire into its components, and to pack it again.
Without such a facility composite symmetries are usually specified using ellipses in the diagrammatic notation, which injects an unpleasant element of informality.

We construct $\sigma_{2,2}$ according to the definition in Example <ref>.
Unfolding the definition produces the diagram

\[
\input{pics/sigma22.pdf_tex}
\]

in which the dotted boxes indicate instances of $\sigma_{2,1}$.
Using the strictification axioms the matching pair of a de-strictifier and a strictifier can be eliminated, resulting in:

\[
\input{pics/sigma22b.pdf_tex}
\]

Find two different constructions for $\sigma_{2,2}$, then prove that the two definitions are equal in the equational theory of the PROP.

Prove that for any $m,n$, it is the case that $\sigma_{m,n}$ constructed as above is indeed the symmetry of the PROP.

Analogously to monoidal categories, we may freely generate symmetric strict monoidal categories from a signature $(\Sigma_0,\Sigma_1)$. In short, what changes with respect to Definition <ref> is that the inductive definition of $\Sigma$-term includes an additional clause for symmetries:

* If $A$ and $B$ are in $\Sigma_0$, then the `symmetry' $\sigma_{[A],[B]} \colon [A,B] \to [B,A]$ is a $\Sigma$-term.

and the morphisms of the freely generated category are $\Sigma$-terms quotiented as in Definition <ref> plus a family of equations saying that arbitrary symmetries are constructed from symmetries only involving generating objects, analogously to what is shown in Example <ref>.

\[
\star\star\star\star\star
\]

This concludes the presentation of the core language of string diagrams, for symmetric monoidal categories, on which much of the more elaborate graphical syntaxes rely.
The pedagogical trajectory we followed is rather different from the one the reader will find in most of the literature, with an emphasis on functorial boxes and non-strict tensoring.
The hope is that this perspective has some pedagogical value, in itself and as a complement of the presentations found in the literature, in understanding the core graphical language of string diagrams.
Our unusual emphasis on functorial boxes and non-strict tensoring was pedagogically motivated, but these constructs will turn out to be important in their own right.

§.§ Foliations

As compared to the term notation the diagrammatic notation was seen to have several advantages.
It is more abstract, as several terms correspond to the same diagram;
it is automatically quotiented by systematic renaming of variables ($\alpha$-equivalence);
it can more easily identify redexes, which allows the derivation of more efficient abstract machines through the fine-grained control of copying and sharing.

In this section we shall see how the diagrammatic presentation can help derive a quasi-normal form for terms which leads to simpler inductive algorithms and proofs of correctness for certain classes of algorithms on graph-like data structures.
To give concrete examples we will use a generic syntax for an OCaml-like functional language (call-by-value, algebraic data types, pattern matching).
The techniques we illustrate here are part of the folklore of string diagram research but a deliberate and focussed, rather than incidental, presentation can be considered to be new.

Let us begin with a common situation where a non-tree-like data structure is algorithmically justified, and examine the issues and the proposed approaches.
In functional languages, tree-like data structures are ubiquitous since they can be expressed as an algebraic data type.
Consider for example the type of binary trees with (integer) data stored in the nodes:

language=Haskell, basicstyle=, keywordstyle=, identifierstyle=

type tree = Node int tree tree | Empty

A standard function on trees would be map, which applies a function $f$ to each node while preserving the overall tree shape:

map f (Node n t t') = Node (f n) (map f t) (map f t')
map f Empty         = Empty

The function is inductive (or structurally recursive on the data structure) so that termination is guaranteed.
For instance, this is the effect of mapping the function $\lambda x.x+1$ on some tree, represented graphically in the usual way:

\[
\input{pics/mapf.pdf_tex}
\]

Note that this particular tree has a certain amount of duplication.
A common space-saving algorithmic device in this situation is to use directed acyclic graphs (DAGs) to represent sharing of common substructures.
The tree above can have several optimised DAG representations, with the minimal one shown below:

\[
\input{pics/dagmin.pdf_tex}
\]

Note that the DAG has exactly the same paths as the tree it efficiently represents.

The problem we now face is that DAGs are not an inductive data structure.
Efficient algorithms on DAGs can be written functionally, but they are rather sophisticated (attribute grammars and higher-order abstract syntax are two ways of doing it).

Here we will present a concrete solution to this problem based on string diagrams, then we will give a more general framework for such algorithms.
Consider a freely generated PROP with signature morphisms $node_k : 2\to 1 $ for $k\in\Int$ and $emp:0\to 1$.
Both the tree and the DAG used in the examples below can be represented int this category as string diagrams (if we tilt the graphs to the right to fit our graphical conventions).

To save on notation overload we introduce the following auxiliary notation:

\[
f^{(k)}=f\otimes\cdots\otimes f\qquad (k\text{ times})
\]

As terms, they are

\begin{align*}
\text{Tree}& : emp^{(8)} \semic node_3^{(4)} \semic node_2^{(2)} \semic node_1\\
\text{DAG}& : emp^{(2)} \semic node_3 \semic node_2 \semic node_1
\end{align*}

noting that these representations are not unique.

Find alternative representations for the tree and the DAG used in the example.

The key observation here is that we wrote morphisms in a form (sequentially composed tensors of signature elements and basic structural morphism) that can always be represented as a list of lists:

\begin{multline*}
\text{tree:} \bigr[[emp \semic emp \semic emp \semic emp \semic emp \semic emp \semic emp \semic emp] \semic \\
[node_3 \semic node_3 \semic node_3 \semic node_3] \semic
[node_2 \semic node_2] \semic
\end{multline*}

\[
\text{DAG:} \bigl[
[emp \semic emp] \semic [node_3] \semic [node_2] \semic [node_1]
\bigr]
\]

The inner lists are aggregated by tensor ($\otimes$) and the outer list by composition ($ \semic $).
We call this presentation of the morphism a foliation.

Of course, a morphism can be presented in a different form, which does not fit this shape, for instance this tree:

\[
(((emp\otimes emp) \semic node_1)\otimes((emp\otimes emp) \semic node_2) \semic node_3
\]

Its foliation is

\[
emp^{(4)} \semic (node_1\otimes node_2) \semic node_3.
\]

The advantage of this representation is that now we can write a general inductive map function for DAGs presented as foliations, remembering that the language of a freely generated PROP also includes identity ($id$) and symmetry ($sym$).
However, since a map function preserves the shape of the DAG, it simply preserve these structural morphisms.

map' f (emp    :: xs) = emp :: (map' f xs)
map' f (node k :: xs) = node (f k) :: (map' f xs)
map' f (id     :: xs) = id :: (map' f xs)
map' f (sym    :: xs) = sym :: (map' f xs)
map' f []             = []

map f xs :: xss = (map' f xs) :: (map f xss)
map f []        = []

If List.map is the usual map on lists, the DAG.map above can be written more compactly as

lift f (node k) = node (f k)
lift f x        = x

Dag.map f = List.map (List.map (lift f))

Or, with a function composition operator defined as

f ; g x = g(f x)

Dag.map = lift ; List.map ; List.map

Let us consider some other common functions on such binary graphs and DAGs.
Map preserves the shape of a DAG, and functions that transform the shape in a uniform way are also easy to implement.
Mirroring a binary tree, as an inductive data type is:

flip Node n t t' = Node n (flip t') (flip t)
flip Empty       = Empty

On DAG foliations, we simply reverse every list in the foliation:

DAG.flip = List.reverse ; List.map

where List.reverse is the usual list reversing function.
Also functions that modify a DAG locally, by replacing a node with another DAG are easy to implement;
they are left as an exercise.

Functions that ignore the shape of the DAG are also trivial, as the DAG can be flattened into a list.
The structural elements (identities and symmetries) can be filtered out if needed.
Finding an element $n$ in a DAG can simply done by searching for it in the flattened list of lists:

Dag.find n = List.concat ; List.find (node n)

Find the minimum element of a DAG presented as a foliation.

However, not all algorithms are naturally suited when a DAG is presented as a foliation.
The following is difficult, but not impossible.
Define a datatype of expressions (integers, addition, multiplication) as a tree and write a simple evaluator.
Consider the types of expressions with shared sub-expressions as a DAG and write an evaluator on foliations.

Manty algorithms which are standard on graph representations seem harder to write efficiently or naturally on foliations, for example traversals with a prescribed order (e.g. prefix, infix, postfix), searching for sub-graphs, or computing isomorphisms.
Applying the operational semantics is a perfect example of algorithm apparently unsuitable for foliations, which would benefit from the greater flexibility of the graph representation.
Note here that the unsuitability is not in terms of expressiveness but in terms of efficiency: the token can be represented as a node in the graph and the rewriting rules can be represented in a suitable way.
However, the traversal of the identities may require several steps in the list-like notation, instead of the single step in the conventional graph notation.
In general, any edge may be represented by a number of identities and symmetries in the list-like notation, which is likely to be inefficient in time and space.

Simple inductive algorithms on foliations are not to be seen as practical from the point of view of computation.
The best way to think of them is as simple inductive (and executable) specifications on DAGs which are easier to formalise and use in proofs than working with DAGs as a native data structure.
This feature particularly comes in handy in defining and proving complex program transformations such as (reverse) automatic differentiation or closure conversion.
However, the computational overhead of computing in terms of foliation rather than on a direct implementation of graph using pointers has not been studied.

§.§ Properties of foliations

The following theorem is category theory folklore:

Any morphism $f$ in a freely generated (strict) monoidal category can be presented as

\[
f = \bigotimes_{i_0}f_{1,i_0} \semic \cdots \semic \bigotimes_{i_n}f_{1,i_n}
\]

where $f_{j,k}$ are elements of the signature or structural morphisms (identities, symmetries if the category is symmetric, etc.).

This theorem is the corollary of a stricter version:

Any morphism $f$ in a freely generated (strict) monoidal category can be presented as

\[
f = id_{A_1}\otimes f_{1}\otimes id_{A_1'} \semic \cdots \semic id_{A_n}\otimes f_{n}\otimes id_{A_n'}
\]

where $f_k$ are elements of the signature or structural morphisms (identities, symmetries if the category is symmetric, etc.).

We sketch the proof below.

First we write $f$ as a string diagram, and we consider its concrete graph representation, which we topologically sort.
We take the smallest node in the graph and call it $f_1$.
Since this is a topological sort $f_1$ is not connected on the left to any other node but directly to the input interface.
The interface itself is a list and we take the type of the edges below the input edges of $f_1$ to be $A_1$ and those above to be $A_1'$.
Note that edges do not cross (in braided or symmetric categories the braiding or the symmetry are non-identity morphisms).
We have obtained the first term of the foliation, $id_{A_1}\otimes f_{1}\otimes id_{A_1'}$.
Repeat the procedure for the smaller graph obtained by removing $f_1$ and its incoming edges, and adding its outgoing edges to the input interface.
Continue until the graph is empty.
The result is the foliation. Proving that this foliation is equal to $f$ is a tedious but simple exercise.

Note that since the topological sort is not unique, the foliation is also not unique.

§.§ Further reading and related work

Besides the survey mentioned in the beginning of the section <cit.> a conceptual and high level understanding of string diagrams in the context of physics, logic, topology and computer science can be gleaned from <cit.>.
The particular style of presentation we rely on, that of `functorial boxes' is due to <cit.>—although we have to point out that, somewhat curiously, this paper stops short of applying the technique to adjunctions, which is where we found it most useful.
These three papers together provide the best foundations for understanding the philosophy, motivation, and some of the technical details in this section.
They were also an important source of inspiration for the first author in gaining a personal appreciation of the beauty and power of string diagrams.
Also inspirational, although, as it will be seen in the next section, without an immediate technical connection, is <cit.>, which is a culmination of a series of papers starting with <cit.> which have firmly established diagrammatic methods as a serious and useful syntax for monoidal categories and their applications.

The diagrammatic notation presented here is not the only kind of string diagrams out there.
Unrelated, other than in spirit, are string diagram calculi using two <cit.> and higher dimensional structures <cit.>.
This should alert the reader to the fact that the term `string diagram' is rather broad and may cause some confusion.

One important possible confusion worth explicating is the conflation of the term `string diagram' as a two-dimensional syntax with its graph representation, as a combinatorial mathematical object or concrete data structure.
The distinction between the two is worth making, as the rest of this tutorial will hopefully show.
The second author's research work on rewriting techniques used to formalise the equational theory of string diagrams represented as graphs insists on this distinction, as seen for example in <cit.>.

For monoidal categories we need to mention the original papers which introduce a graphical notation in the style of string diagrams <cit.>.
Since these general monoidal categories are not presumed to be symmetric the notion of equivalence is not isomorphism but `homotopy', i.e. smooth deformations of the substrate in which the diagrams are embedded.
Symmetry is also considered in the original papers, with the interesting observation that isomorphism can be reduced to isotopy by increasing the number of dimensions of the substrate, i.e. the isomorphism of a 2-dimensional structure can be seen as isotopy in a 3-dimensional space.

The original papers, and virtually the entire literature that follows, operate in the context of strict monoidal categories.
The issue of non-strict categories is rather summarily dismissed: “In principle, most results obtained with the hypothesis that a tensor category is strict can be reformulated and proved without this condition.” (p. 59, loc. cit.).
Mathematically this is perhaps true, but the details are clearly worth spelling out if we are to seriously consider string diagrams as a formal syntax.
This careful specification of strictification for string diagrams is done in <cit.>.

§ HIERARCHICAL STRING DIAGRAMS AND THE $\LAMBDA$-CALCULUS

A symmetric closed monoidal category (SCMC) is the essential mathematical structure for the interpretation of higher-order computation.
It is the foundation on which models of lambda calculi are constructed.

A symmetric monoidal category $\category C$ is closed if for all objects $X$ the tensor product functor $F_X(A)=X\otimes A: \category  C\to\category C$ has a right adjoint functor $G_X(A)$, usually written as $X\multimap A$:

\[
X\otimes A \quad \dashv \quad X\multimap -.
\]

Objects $A\multimap B$ are called exponential objects and are sometimes also written as $B^A$.

We use the functorial boxes and adjunction notations to represent all the equations entailed by this definition, first noting that the functor $F_X$ can be represented explicitly:

\[
\input{pics/fclosed.pdf_tex}
\]

The equations are shown in Figure <ref>: note that in order to express these equations rigorously, in particular the last one, the availability of explicit strictification and de-strictification comes in handy.
The co-unit of the adjunction is usually called eval (evaluation) so, for the sake of symmetry, we will call the unit co-eval.

\[
\input{pics/adjclosed.pdf_tex}
\]

Naturality of unit and co-unit

\[
\input{pics/adjclosed2.pdf_tex}
\]

Unit and co-unit equations

Symmetric closed monoidal adjunction equations

As we shall see both in models of lambda calculi and in the lemma below, a construction that proves to be useful is the following.

For any morphism $f:X\otimes A\to Y$ we define its abstraction as the morphism $\Lambda_X(f):A\to X\multimap Y$, denoted graphically as below:

\[
\input{pics/lambda.pdf_tex}
\]

Note that the rounded box with a wire attached to the edge is merely a graphical convention, and the abstraction box only has a precise meaning as expanded according to its definition.
Most importantly, it is not a functorial box.

A useful property of abstraction is that it can `swallow' other abstractions it is sequenced with:

\[
f;\Lambda(g) = \Lambda\bigl((f\otimes id);g\bigr).
\]

\[
\input{pics/sbstlam0.pdf_tex}
\]

The following is the defining property of SCMCs.

In a SCMC $\mathcal C$

\[ hom_{\category C}(X\otimes Y,Z)\simeq hom_{\category C}(X, Y\multimap Z)\]

\[ X\otimes Y\multimap Z\simeq X\multimap (Y\multimap Z).\]

The two isomorphisms are:

\[
\input{pics/curryuncurry.pdf_tex}
\]

The proof that the first morphism composed to the second is the identity is sketched in Figure <ref>.
The steps are:

* the initial morphism composition,

*  apply Lemma <ref>,

* elaborate the definition of abstraction,

* naturality of unit,

* naturality of unit,

* unit-counit cancellation,

* unit-counit cancellation,

* symmetry cancellation,

* strictification-destrictification cancellation,

* unit and co-unit cancellation.

The diagrammatic redexes involved in a particular step are highlighted in red.

The details of verifying all the other details that these are indeed natural isomorphisms are left as an exercise.

\[
\input{pics/curryproofnew.pdf_tex}
\]

Proof of identity of composition

The notion of a category freely generated from a signature, as seen for monoidal and symmetric monoidal strict monoidal categories in Section <ref>, can be adapted to the case of SCMCs. A difference is that, in order to properly express the conditions of closedness, we need a more fine grained representation for the objects: because of the presence of the operator $\multimap$, objects cannot be abstractly represented as lists of generators.

A closed monoidal signature is a pair $(\Sigma_0,\Sigma_1)$ where $\Sigma_0$ is a set of generating objects and $\Sigma_1$ a pair of generating morphisms with sources and targets elements of the set $\mathit{obj}_{\Sigma_0}$, defined inductively as follows:

* A designated object $I$ (the unit) and each object in $\Sigma_0$ is in $\mathit{obj}_{\Sigma_0}$.

* If $A_1$, $A_2$ are in $\mathit{obj}_{\Sigma_0}$, then $A_1 \otimes A_2$ and $A_1 \multimap A_2$ are in  $\mathit{obj}_{\Sigma_0}$.

The closed monoidal $\Sigma$-terms are defined inductively as follows:

* All morphisms $f \colon A_1 \to A_2$ in $\Sigma_1$ are $\Sigma$-terms.

* If $A$ and $B$ are in $\mathit{obj}_{\Sigma_0}$, then the identity $\id_{A} \colon A \to A$ and symmetry $\sigma_{A,B} \colon {A \otimes B} \to B \otimes A$ are $\Sigma$-terms.

* If $f \colon A_1 \to A_2$, $g \colon A_2 \to A_3$ are $\Sigma$-terms, then $f ; g \colon A_1 \to A_3$ is a $\Sigma$-term.

* If $f \colon A_1 \to A_2$, $g \colon A_3 \to A_4$ are $\Sigma$-terms, then $f \otimes g \colon A_1 \otimes A_3 \to A_2 \otimes A_4$ is a $\Sigma$-term.

* If $X$ and $A$ are in $\mathit{obj}_{\Sigma_0}$, then the `evaluation' map $eval_{X,A} \colon ((X \multimap A) \otimes X) \to A$ is a $\Sigma$-term, represented graphically in the same way as the unit of the adjunction.

* If $h \colon X \otimes A \to Y$ is a $\Sigma$-term, then its `abstraction' $\Lambda_X(h) \colon A \to (X \multimap Y)$ is a $\Sigma$-term, represented graphically as in Definition <ref>.

The closed monoidal category $\category C$ freely generated by $(\Sigma_0,\Sigma_1)$ is defined as having objects $\mathit{obj}(\category C) = \mathit{obj}_{\Sigma_0}$ and morphisms  $hom(\category C)$ the $\Sigma$-terms quotiented by:

* the equations of symmetric monoidal categories, where $\otimes$ acts as the monoidal product, and $I$ acts as the identity for $\otimes$;

* the following three equations, describing the behaviour of evaluation and abstraction (where we adopt the notation of Definition <ref> for $\Lambda_X(h)$):

\[
\input{pics/abstreval.pdf_tex}
\]

Observe that the last equation is the same equation proven in Lemma <ref>.

Considering SCMCs were introduced as SMCs with an adjunction, it is not completely obvious why the category $\category C$ obtained in Definition <ref> would meet the requirements of being monoidal closed. It is a pleasant exercise in diagrammatic reasoning to verify this fact.

Let $\category C$ be freely generated from a signature $(\Sigma_0,\Sigma_1)$ as in Definition <ref>. Then $\category C$ is a symmetric monoidal closed category.

First, we define the right adjoint functor $G_X(A)$ to the tensor product functor $F_X(A) = X \otimes A \colon C \to C$, as follows. On objects, we set $G_X(A)$ to be $X \multimap A$. On a morphism $f \colon A \to B$ we define it as

\begin{equation}\label{def:GXadj}
\input{pics/freesmc1.pdf_tex}
\end{equation}

We claim $G_X$ is right adjoint to $F_X$. To show this, we define the unit $\eta_B \colon ((X \multimap B) \otimes X) \to B$ of the adjunction as $eval_{X,B}$, and the counit $\epsilon_B \colon B \to (X \multimap (X \otimes B))$ as

\begin{equation}\label{def:counitAdj}
\input{pics/freesmc2.pdf_tex}
\end{equation}

It now remains to verify the four equations of Figure <ref>. In the derivations below, remember that the label $X \multimap$ in the functorial boxes appearing in the equations of Figure <ref> stands for the right adjoint $G_X$, and thus those boxes are defined according to (<ref>). The diagrammatic reasoning is in Figure <ref>.

\[
\input{pics/freesmc3.pdf_tex}
\]

Proof of monoidal closure

We may also show the converse implication, namely that any SCMC exhibits the structures defined by the construction of Definition <ref>. The reader may verify it via the following exercise.

Let $\category C$ be an SCMC. Consider objects $X, A, Y$ in $\category C$, and a morphism $h \colon X \otimes A \to Y$. Define an evaluation map $eval_{X,A} \colon ((X \multimap A ) \otimes X) \to A$ and abstraction $\Lambda_X(h) \colon A \to (X \multimap Y)$ satisfying the equations in Definition <ref>.

In contrast with the case of monoidal and symmetric monoidal categories, we constructed the free SCMC as a non-strict monoidal category. Intuitively, this is due to the fact that, in order to properly define the monoidal closed structure, we need wires in string diagrams of a SCMC to be labeled with arbitrary objects, rather than just the generating ones. This is particularly evident both in Definition <ref>, where we need to be able to abstract over any object $X$ that may be tensored with $A$, and in the definition (<ref>) of the counit. Because we need both wires for, say, $X$ and $A$, and for $X \otimes A$, we also need (de)strictifiers to switch from one representation to the other, as it happens for instance in (<ref>). It is thus essential to not impose strictness in the construction of Definition <ref>. This is also coherent with our motivating examples of SCMCs (to be explored in Section <ref> below) which are usually non-strict.

We conclude this section by pointing out that also the concept of foliation, introduced in Section <ref> for  monoidal categories, can be extended to a monoidal closed category, in the obvious way:

Any morphism $f$ in a freely generated monoidal closed category can be presented as

\[
f = \bigotimes_{i_0}f_{1,i_0} \semic \cdots \semic \bigotimes_{i_n}f_{1,i_n}
\]

where $f_{j,k}$ are

* elements of the signature

* structural morphisms (identities, symmetries, etc.)

* $\Lambda(f')$ for some morphism $f'$ which is also a hierarchical foliation.

The proof is similar to that of Theorem <ref> except that the graph-label of each hierarchical box is foliated beginning with the deepest one.
This is sound since the depth of nexting of $\Lambda()$ is finite.

Note that the proof of the foliation theorem(s) also works as a proof of definability, showing that any well-formed hierarchical graph can be converted into a term.
Starting with an arbitrary morphism in a (closed) monoidal category, therefore we can represent it as a string diagram, the retrieve an equal foliated morphism.
So foliations, in particular maximally sequential ones, can be seen as a quasi-canonical form of morphisms in such categories, and generating them a form of normalisation by evaluation.

We remark that, in obtaining the foliated form, the string diagram notation and its graph concrete representation are essential.
An algorithm for deriving a foliation out of a morphism using terms seems extremely difficult to formulate directly.

§.§ Cartesian product and Cartesian closed categories

We introduce a family of natural transformations called copying and deletion respectively, written as $\delta_A : A \to A \otimes A $ and $\omega_A : A \to I $, respectively.
Because deletion and copying play such an important role in a Cartesian category we employ graphical syntax for them, with the caveat that this graphical syntax is merely meant to prevent clutter but, unlike e.g. symmetry, does not absorb any equations.
The naturality equations are graphically rendered as:

\[
\input{pics/copydel.pdf_tex}
\]

Cartesian product is not strict but to avoid clutter we present the diagrammatic equations as if it is.
This imprecision can be easily corrected using explicit strictification and de-strictification as seen in Section <ref>.

A symmetric monoidal tensor is a (Cartesian) product if for each object $A$ in the category the following monoidal natural transformations exist:

\begin{align*}
\omega_A &: A \to I  & \text{(deletion)}\\
\delta_A &: A \to A \otimes A & \text{(copying)}
\end{align*}

such that

\begin{align*}
\omega_{A\otimes B} &= \omega_A\otimes\omega_B \\
\delta_{A\otimes B} &= \delta_A\otimes\delta_B  \semic
\id_A\sigma_{A,B}\otimes \id_B
\end{align*}

\[
\delta \semic \id\otimes \omega = \delta \semic \omega\otimes\id = \id
\]

Graphically, this is

\[
\input{pics/prodeq.pdf_tex}
\]

If a symmetric monoidal category is Cartesian it is customary to write the tensor as $A\times B$.
If it is also closed it is customary to write the exponentiation as $A\Rightarrow B$;  the composite morphisms $\pi_1:=\id\otimes\omega$ and $\pi_2:=\omega\otimes \id$ are called the first and second projections, respectively.
Such a category is said to be a Cartesian closed category (CCC)
Finally, it is usual to introduce notation for

\[
A\xrightarrow{\langle f,g\rangle}B\times C := A\xrightarrow{\delta_A}A\times A\xrightarrow{f\otimes g} B\times C,
\]

called the pairing of $f$ and $g$.

Further syntactic conventions

The principle of absorbing equations into the notation can be pushed farther.
It is convenient to generalise the notation for binary to $n$-ary copying:

\[
\input{pics/narycopy.pdf_tex}
\]

It can be easily shown that because of the laws of the Cartesian product any tree constructed of copying, deletion, and symmetry can be given a normal form, e.g.

\[
\input{pics/narycopy2.pdf_tex}
\]

A more formal construction of $n$-ary copying, in the style of Exercise <ref> is left as an exercise to the reader.

In general any term in a monoid or, as in the case of copying a co-monoid, can be reduced to this dot-like notation.
As a more advance graphical device, which we will not employ in the sequel, the presence or absence of commutativity (or co-commutativity, respectively) can be made graphically perspicuous by making it impossible to discern the order of incoming (or out-going) wires.
Thus, an $n$-ary addition operation ($+$), which is commutative, would be represented differently from an $n$-ary list constructor ($::$), which is not, as seen below (for $n=5$):

\[
\input{pics/plusvcons.pdf_tex}
\]

Universal products

The formulation of a Cartesian category in Definition <ref> is not the usual one found in category theory literature.
It is more common to define it using a universal property:

Given a category $\category C$ and two objects $A_1,A_2$, then their product $A_1\times A_2$ is an object equipped with morphisms (projections) $p_i:A_1\times A_2\to A_i$ for $i=1,2$ such that it is universal with this property, i.e. given any other object $X$ with morphisms $f_i:X\to A_i$ for $i=1,2$ there exists a unique morphism (pairing) $\langle f_1,f_2\rangle: X\to A_1\times A_2$ such that $f_i=\langle f_1, f_2\rangle \semic p_i$.

This definition generalises to arbitrary sets $i\in I$.

We can show that Definition <ref> implies that Definition <ref> also holds.
The projections and the pairing are:

\[
\input{pics/pairing.pdf_tex}
\]

The equation governing the interaction between the first projection and pairing is

\[
\input{pics/eqpairing.pdf_tex}
\]

The equation for the second projection is the obvious counterpart.

The proof of uniqueness is slightly more interesting.
Suppose there is a map $u$ satisfying the same equational properties as pairing, i.e.

\[
\input{pics/uniqpair.pdf_tex}
\]

The equation $u=\langle f_1,f_2\rangle$ follows from copy-delete interaction, naturality of copy, and the hypothesis:

\[
\input{pics/uniqpair2.pdf_tex}
\]

Product as adjunction

Mathematical concepts can be defined in many ways, something which is particularly true of category theory.
So let us define product in a third way, this time using adjunctions!

First consider the category $\mathcal C\times\mathcal C$ which is constructed so that its objects are pairs of objects of $\mathcal C$ and its morphisms are pairs of morphisms of $\mathcal C$, which we shall write as $(A,B)$ and $(f,g)$, respectively.

Note that this is a new category, but one which we can relate to $\mathcal C$ using an obvious diagonal functor that pairs objects, and respectively morphisms with themselves, $\Delta:\mathcal C\rightarrow \mathcal C\times\mathcal C$.
We can show that the functor ${-}\times{-} : \mathcal C\times\mathcal C\rightarrow \mathcal C$ is adjoint to the diagonal, $\Delta\dashv{-}\times{-}$.
To do that, we define

\[
\input{pics/pairingeta.pdf_tex}
\]

\[
\input{pics/pairingepsilon.pdf_tex}
\]

The details of checking that the above define an adjunction are routine and are left as an exercise to the reader.

§.§ The simply-typed lambda calculus

§.§.§ Term syntax

The simply-typed lambda calculus (STLC) is at the core of the design of the functional fragment of most modern programming languages.
The types $T$ are constructed from a fixed set of base types, for instance natural numbers ($N$), and exponentiation $T\to T$.
Terms $u$ are constructed from variables $x$,  abstraction $\lambda x{:}T.u$, and application $u\, u$.
This is the pure fragment of the calculus, that can be extended with constants $c$, resulting in the applied STLC.
For now we focus on the pure fragment.
If the type is unimportant we may omit it from a term and just write $\lambda x.u$.

An important syntactic operation is that of substituting a term $v$ for a variable $x$ in some other term $u$, written as $u[x/v]$.
For instance

\[
(\lambda x.f\, x)[f/\lambda y.y] = \lambda x.(\lambda y.y)\, x.
\]

This operation is not mere textual replacement, and must be defined carefully in order to avoid variable capture:
A $\lambda x.u$ term defines $x$ locally, in a definite scope $u$;  $x$ is said to be bound.
Otherwise, a variable is said to be free, such as $f$ in the example above.
Moreover, repeated definitions are allowed, so variables can overshadow other variables.
For instance, the term $\lambda x.(\lambda \underline x.\underline x)\, x$, shows four occurrences of the string $x$, functioning sometimes as a binder and sometimes as a bound variable.
The correct matchups between binders and bound variables are identified using underlining.

The set of free variables $\mathcal F(-)$ of a lambda term is defined inductively on its syntax as

\begin{align*}
\mathcal F(x) = \{ x\}
\quad
\mathcal F(u\,u') = \mathcal F(u)\cup\mathcal F(u')
\quad
\mathcal F(\lambda x{:}T.u) = \mathcal F(u)\setminus\{x\}.
\end{align*}

To see why substitution is not merely textual replacement, consider the following invalid substitution:

\[
(\lambda x.f\, x)[f/x] \not= \lambda x.x\, x.
\]

The status of the occurrence of the substituted variable changes from free $f$ to captured $x$ in the resulting term.
The operation of substitution is, however, always well defined because bound variables can be systematically renamed in any lambda term so, the correct application of substitution is:

\[
(\lambda x.f\, x)[f/x] = (\lambda y.f\, y)[f/x] = \lambda y.x\, y.
\]

The first equation is the renaming of $x$ to $y$, the next is the actual performing of the substitution.
To get there we define first transposition of variables, then $\alpha$-equivalence of terms up to renaming of bound variables.

The transposition of variables $x,y$ in $u$, written as $(x\,y)\cdot u$, is defined inductively on terms taken as text, swapping all occurrences ignoring the bindings.

\begin{align*}
(x\,y)\cdot x &= y\\
(x\,y)\cdot y &= x\\
(x\,y)\cdot z &= z &\text{if } x\neq z\neq y\\
(x\,y)\cdot (u\,u') &= \bigl((x\,y)\cdot u\bigr)\,\bigl((x\,y)\cdot u'\bigr)\\
(x\,y)\cdot (\lambda z.u) &= \lambda (x\,y)\cdot z. (x\,y)\cdot u.
\end{align*}

Using it, we can define

The relation of $\alpha$-equivalence between $\lambda$ terms, written as $u\equiv u'$, is defined as

\[
\frac{}{x\equiv x} \qquad
\frac{u_1\equiv u_1' \qquad u_2\equiv u_2'}{u_1\,u_2\equiv u_1'\,u_2'} \quad
\frac{(z\, x)\cdot u\equiv (z\, y)\cdot u' \quad x\neq z\neq y}{\lambda x{:}T.u\equiv\lambda y{:}T.u'}
\]

From now on we consider $\lambda$ terms quotiented by $\equiv$, so e.g. $\lambda x.x=\lambda y.y$.
We can now define (capture-avoiding) substitution, inductively on the syntax of $\lambda$ terms up to $\alpha$ equivalence:

\begin{align*}
x[x/u] & = u \\
y[x/u] & = y & x\neq y\\
(u_1\,u_2)[x/u] &= (u_1[x/u])\,(u_2[x/u])\\
(\lambda y{:}T.u')[x/u] &= \lambda y{:}T.u'[x/u] &  x\neq y \text{ and } y\not\in \mathcal F(u).
\end{align*}

On a superficial glance the definition seems ill-defined.
What if $x\neq y$ and $y\in\mathcal F(u)$?
What if $x=y$?
Are there cases missing from the definition of substitution?
But this is exactly the situation of the variable capture discussed earlier!
Using the mechanics of $\alpha$-equivalence $y$ can be simply replaced by a suitably named variable not bound in $u$, just as we replaced $x$ in $(\lambda x.f\, x)[f/x]$.

Prove that $(\lambda x{:}T.u)[x/u'] = \lambda x{:}T.u$.

Types are assigned to terms using judgements of the form

\[
\Gamma \vdash u:T
\]

where $\Gamma = x_1:T_1, \ldots, x_k:T_k$ is a variable type assignment.
The judgement above is interpreted as term $u$ has type $T$ if each $x_i$ has type $T_i$ as given by $\Gamma$.
The rules for deriving type judgements can be given in the style of natural deduction:

\begin{gather}
\Gamma_1, x:T,\Gamma_2\vdash x:T
\tag{var}\\[1.5ex]
\frac
{\Gamma_1,x:T,\Gamma_2\vdash u:T' }
{\Gamma_1,\Gamma_2\vdash \lambda x{:}T.u:T\to T'}
\tag{abs}\\[1.5ex]
\frac
{\Gamma\vdash u_1:T_1 \quad \Gamma\vdash u_2:T_1\to T_2}
{\Gamma\vdash u_2\,u_1:T_2}
\tag{app}
\end{gather}

§.§ Categorical and string diagram syntax

The STLC can be given a canonical interpretation in any Cartesian closed category $\category C$.
Types are interpreted as objects of the category ($\seval N=N$, $\seval{T\to T'}=\seval T\Rightarrow\seval{T'}$).
To reduce clutter we shall just write $T$ instead of $\seval T$, without ambiguity.

\begin{align*}
\seval{\Gamma}=\seval{\lst{x:T}}=\seval{x_1:T_1,\ldots,x_n:T_n} = T_1\otimes\cdots\otimes T_n=\bigotimes_nT_i.
\end{align*}

To avoid clutter we also write just $\Gamma$ instead of $\seval \Gamma$.
Interpretation is given to type judgements, inductively on its derivation, with types interpreted as objects and judgements as morphisms:

\[
\seval{\Gamma\vdash u:T'}:\Gamma\to T'.
\]

The definitions are usually given as:

\begin{align*}
\seval{x:T,\Gamma\vdash x:T} &= \id_T\otimes\omega_{\Gamma}\\
\seval{x:T,\Gamma\vdash \lambda x{:}T.u:T'} &= \Lambda_T\bigl(\seval{x:T,\Gamma\vdash u:T'}\bigr)\\
\seval{\Gamma\vdash u_2\,u_1: T_2} &= \langle\seval{\Gamma\vdash u_1:T_1}, \seval{\Gamma\vdash u_2:T_1\to T_2}\rangle \semic eval_{T_1,T_2}.
\end{align*}

These definitions, which can be encountered with various small variations in the literature, treat the product used in the interpretation of $\Gamma$ as if it is strict, by quietly reassociating (and even applying symmetry) its components.
This is necessary since variables are not necessarily in the first position in the environment.
This is not likely to lead to serious confusions, due to the strictification theorem.
Not unless, that is, there is a product type in the language as well.
But it is possible to make the definitions formal if working in the strictified category.
Of course, it is possible to make the definitions as formal in the non-strict category as well, but that is an even more tedious exercise, which we shall leave to the reader.

Let us change the definition of the interpretation of $\Gamma$ to a strict tensor

\[
\seval{\Gamma}=\seval{x_1:T_1,\ldots x_n:T_n}=[T_1,\ldots,T_n]=[\Gamma]
\]

and change the definition of interpretation accordingly to

\[
\seval{\Gamma\vdash u:T'}:[\Gamma]\to T'.
\]

We write $[\Gamma]$ to avoid ambiguity with the non-strict interpretation, written just $\Gamma$.

It is convenient to define

\begin{align*}
\psi_{\Gamma} : [\Gamma] \to \Gamma\qquad
\psi^*_{\Gamma} : \Gamma \to [\Gamma].
\end{align*}

As the strictifiers and destrictifiers of $\Gamma$, respectively.

The more precise definitions can be now stated.

\begin{align*}
\seval{\Gamma_1,x:T,\Gamma_2\vdash x:T} = [\Gamma_1,T,\Gamma_2]& \xrightarrow{\psi_{[\Gamma_1,T],[\Gamma_2]}}[\Gamma_1,T]\otimes[\Gamma_2]\\
&\xrightarrow{\psi_{[\Gamma_1],T}\otimes\id_{[\Gamma_2]}}[\Gamma_1]\otimes (T\otimes[\Gamma_2])\\
&\xrightarrow{\alpha_{[\Gamma_2],T,[\Gamma_2]}}[\Gamma_1]\otimes T\otimes[\Gamma_2]\\
&\xrightarrow{\omega_{[\Gamma_1]}\otimes id_T\otimes\omega_{[\Gamma_2]}} T \\[1.5ex]
\seval{\Gamma_1,x:T,\Gamma_2\vdash \lambda x{:}T.u:T'} &= [\Gamma_1,\Gamma_2]\xrightarrow{\Lambda_T(f)}T\Rightarrow T'\\
f = T\otimes[\Gamma_1]\otimes[\Gamma_2] & \xrightarrow{\sigma_{T,[\Gamma_1]}\otimes \id{[\Gamma_2]}}[\Gamma_1]\otimes T\otimes[\Gamma_2]\\
&\xrightarrow{\alpha^{-1}_{[\Gamma_2],T,[\Gamma_2]}}[\Gamma_1]\otimes (T\otimes[\Gamma_2])\\
& \xrightarrow{\psi^*_{[\Gamma_1,T],[\Gamma_2]}} [\Gamma_1,T,\Gamma_2] \\
& \xrightarrow{\seval{\Gamma_1,x:T,\Gamma_2\vdash u:T'}}T'\\[1.5ex]
\seval{\Gamma\vdash u_2\,u_1: T_2} = [\Gamma]&\xrightarrow{\langle\seval{\Gamma\vdash u_1:T_1}, \seval{\Gamma\vdash u_2:T_1\to T_2}\rangle}T_1\otimes (T_1\Rightarrow T_2)\\*
&\xrightarrow{\mathit{eval}_{T_1, T_2}} T_2.
\end{align*}

It is understandable why most presentation eschew the tedium of the structural manipulation of the type-assignment $\Gamma$, preferring to trade informality for readability.
With string diagrams, as we shall see, there is no price to pay for full rigour, as the bureaucracy of structural manipulation is for the most part absorbed into the notation.
The diagrammatic interpretation corresponding to the terms above is:

\[
%the pdf exported by inkscape has wrong margin because the text is framed badly:
\hspace{-15ex}
\input{pics/stlc.pdf_tex}\\
\]

The full calculation resulting in the simplified interpretations above is routine.
For instance, the full unsimplified diagram with all the strictifiers for the interpretation of abstraction is given in Figure <ref>.

Diagram of abstraction before simplifying strictification operators

By a slight, although unambiguous, overloading of the notation we will combine strictification and symmetry in a single box, to write abstraction as:

\[
\hspace{-25ex}
\input{pics/stlc2.pdf_tex}
\]

The object annotations on the composite box indicate that it can be uniquely reconstructed as

\[
\hspace{-15ex}
\input{pics/stlc3.pdf_tex}
\]

Consider the identity applied to itself $(\lambda x.x)(\lambda y.y)$.
Its string diagram representation is:
\input{pics/idid.pdf_tex}

Consider the term

\[
\lambda n{:}((o\to o)\to o \to o).\lambda f{:}o\to o.\lambda x:o .f (\,n f\, x)
\]

The diagram constructed from the earlier definitions is:

\[
\input{pics/fnfx.pdf_tex}
\]

The copying-deletion pairs introduced by the definition of application and variable, respectively can be simplified, resulting in:

\[
\input{pics/fnfx2.pdf_tex}
\]

§.§.§ Lambda calculus with product types

Extending the calculus with products is a simple exercise.
The language of types is extended with a new constructor, $T:=\cdots\mid T\times T$.
They term syntax is extended with the ability to construct pairs $(u_1,u_2)$, as well as a lambda abstraction on a pair, $\lambda(x,y).u$.
Note that this is a syntax that implies pattern matching on the argument.
Projections can be defined as a family of terms $\pi_i = \lambda(x_1{:}T_1,x_2{:}T_2).x_i:T_i$ with $i=1,2$.

The two new typing rules are:

\begin{gather*}
\frac{\Gamma\vdash u_i:T_i\quad i=1,2}{\Gamma\vdash{(u_1,u_2)}:T_1\times T_2}
\\[1.5ex]
\frac{\Gamma_1,x_1:T_1,
\Gamma_2,x_2:T_2,
\Gamma_3\vdash u:T_3}{\Gamma_1,\Gamma_2,\Gamma_3\vdash \lambda(x_1,x_2){:}T_1\times T_2.u:(T_1\times T_2)\to T_3}.
\end{gather*}

The diagrammatic syntax is:

\[
\input{pics/lambprod.pdf_tex}
\]

§.§.§ The un(i)typed lambda calculus

We can define lambda terms without typing information, i.e. untyped, and we call it UTLC for brevity.
However, in order to implement this calculus in a CCC types are essential, as they correspond to the category's objects.
So the interpretation will be uni-typed, assigning all objects a single type, interpreted by a single object $U$.

$U$ is a reflexive object in a CCC if it there are morphisms

\[
\xymatrix{
U \ar@<1ex>[r]^{\iota\quad} &  \ar@<1ex>[l]^{\rho\quad}
(U\Rightarrow U)
\]

such that

\[
\rho \semic \iota = \id_{U\Rightarrow U}.
\]

In this case we say that $U\Rightarrow U$ is a retract of $U$.

Let us use the following graphical syntax for the special morphisms $\iota$ and $\rho$:

\[
\input{pics/untypedlc.pdf_tex}
\]

Note that it is redundant to indicate the type of terms and variables in $\Gamma$, as they are always $U$.
With these, the interpretation of UTLC terms can be given as

\[
\hspace{-15ex}
\input{pics/utlc.pdf_tex}
\]

We can revisit Example <ref>.
Consider the identity applied to itself $(\lambda x.x)(\lambda y.y)$.
Its string diagram representation is, after cancelling out the retract, the same as before:

\[
\input{pics/idid2.pdf_tex}
\]

In the UTLC we can have more terms than in STLC, for example diverging terms, $(\lambda x.x\,x)\,(\lambda x.x\,x)$:

\[
\input{pics/omega.pdf_tex}
\]

§.§ The theory $\lambda$

We write the equality of two $\lambda$-calculus terms, typed or un(i)typed, as

\[
\Gamma \vdash u = v
\]

where $\Gamma \vdash u:T$ and $\Gamma \vdash v:T$ for some type $T$.

The equality of  consists of the usual equality axioms (reflexivity, symmetry, transitivity) plus  three congruences:

\[
\frac{\Gamma \vdash u=u'}{\Gamma \vdash u\,v=u'\,v}
\qquad
\frac{\Gamma \vdash v=v'}{\Gamma \vdash u\,v=u\,v'}
\qquad
\frac{\Gamma,x:U,\Gamma' \vdash u=u'}{\Gamma,\Gamma' \vdash \lambda x.u=\lambda x.u'}
\]

and a main rule, which makes the $\lambda$ calculus special, relating application and substitution:

\[
\Gamma \vdash (\lambda x.u)v = u[x/v],
\]

where $[-/-]$ is the capture-avoiding substitution defined earlier.
It is called the $\beta$ rule:

The calculus is often extended with an additional rule called $\eta$:

\[
\Gamma \vdash \lambda x.(u\,x)=u\qquad x\not\in \Gamma.
\]

The first set of inferences are called congruences because they immediately imply that if two terms are equivalent then they are so in any context, i.e. term-with-a-hole $\mathcal U[-]$:

\[
\frac{v=v'}{\mathcal U[v]=\mathcal U[v']}.
\]

The categorical and implicitly string-diagram syntax is constructed out of adjunctions which have their own equational properties.
Ideally, the theory $\lambda$ on the terms should coincide with the equational theory of the CCC as applied to the interpreted terms.

Before that, we will derive the interpretation of substitution in the CCC:

\begin{multline*}
\seval{\Gamma_1,\Gamma_2\vdash u[x/v]:T} = \\
\input{pics/sbst.pdf_tex}
\end{multline*}

The proof is by induction on the syntax of $u$, and we show the equations diagrammatically

* $u=x$, which implies $T=T'$, and $u[x/v]=x[x/v]=v$.

\[
\input{pics/sbstx.pdf_tex}
\]

$u=y$, $y\neq x$ which implies $u[x/v]=y[x/v]=y$.
The proof is in Figure <ref>.

\[
\input{pics/sbsty.pdf_tex}
\]

Proof of Lemma <ref>(<ref>)

* The case $u_1\,u_2$ is an immediate consequence of the naturality of copying, left as an exercise to the reader.

* The case $\lambda y.u$, $y\neq x$  which implies the right-hand-side is $(\lambda y.u)[x/v]=\lambda y.(u[x/v]$.
It follows from naturality of coeval and functoriality of the exponential, as shown in Figure <ref> (which is essentially the same as Lemma <ref>).

\[
\hspace{-20ex}
\input{pics/sbstlam.pdf_tex}
\]

Substitution in abstraction

For any $\Gamma\vdash u:T$, $\Gamma\vdash v:T$,
if $\Gamma \vdash u=v$ in the theory $\lambda$, then

\[\seval{\Gamma\vdash u:T}=\seval{\Gamma\vdash v:T}\]

in the CCC.

We use induction on the rules of the theory $\lambda$.
For the equality and congruence axioms the statement is obviously true.
The non-obvious rules are $\beta$ and $\eta$, which we derive graphically.

$\beta$ rule:
$(\lambda x.u)v=u[v/x]$, proof in Figure <ref>.

\[
\hspace{-20ex}
\input{pics/betaeq.pdf_tex}
\]

Proof of $\beta$ rule

$\eta$ rule: $\lambda x.ux = u$, with $x\not\in\mathcal F(u)$ is shown in Figure <ref>.

\[
\hspace{-20ex}
\input{pics/etaeq.pdf_tex}
\]

Proof of the $\eta$ law

§.§ The Geometry of Synthesis construction

In this section we will examine how Cartesian closed categories can be constructed out of more elemental categories, especially out of compact closed categories.
The latter are natural models of systems with a relational semantics, for instance electrical circuits, whereas the former are, as we have just seen, frameworks for models of programming languages.
“Compiling” conventional programming languages into circuits is a long standing area of engineering interest, generally called high level synthesis.
Indeed, this process can be achieved systematically by understanding how Cartesian closed categories can be constructed out of compact closed categories, a construction dubbed the Geometry of Synthesis <cit.>.
The name of the construction is a homage to a famous construction in semantics of linear logic proofs called the Geometry of Interaction, which shows how compact closed categories arise out of traced monoidal categories <cit.> and which can also be given an intuitively diagrammatic construction.

We will describe it briefly, starting with the diagram language of compact closed categories, which are (symmetric for this case) monoidal categories such that every object $A$ has:

* a dual $A^*$, unique up to canonical isomorphism;

* a unit $\eta_A:I\mapsto A^*\otimes A$

* a counit $\epsilon_A:A\otimes A^*\to A$

represented diagramatically as:

\[
\input{pics/compactcc.pdf_tex}
\]

such that the following equations hold, expressed directly in the diagrammatic language:

\[
\input{pics/compactcceq.pdf_tex}
\]

Using the machinery of the (symmetric) compact closed category, a monoidal closed category can be constructed in a standard way:

\[
\hspace{18ex} \input{pics/compcc2moncc.pdf_tex}
\]

Evaluation and the proof of correctness of evaluation (the $\beta$ law) are given below:

\[
\input{pics/compcc2moncceval.pdf_tex}
\]

The first equation relies on strictifier-destrictifier cancellation and symmetry.
The second equation is the `yanking' property of compact closed category in which the unit-counit pair cancel out, allowing the straightening of the wire.

However, this simple solution is not satisfactory because of a “no go” result of category theory, that in a compact closed category the product is automatically a co-product.
It is not important to dwell at this stage on what a co-product is, but having the two coincide is a degeneracy of the framework: in other words, there are now too many equations in the category, allowing certain constructions that should be distinct to be identified.
Therefore, this construction cannot be used to eliminate the need of a direct construction for a Cartesian closed category, as seen so far.

This construction is useful in the context of `high-level synthesis', with a caveat: the category cannot have unrestricted Cartesian product.
Restricting the scope of the product while maintaing the usefuleness of the language require certain type-system trickery inspired by bounded linear logic, which is beyond the scope of this tutorial <cit.>.

§.§ Abstract syntax graphs

This section is informal, intended to reconnect the readers, especially those less versed into category theoretical concepts, with more basic and more available intuitions.
As such, the section can be skipped without loss of continuity, especially by the reader confident in their mathematical intuitions.

It is common, especially in the area of compilers, to cling to the oversimplified view that syntax is represented by a tree.
In fact, syntax is a far more sophisticated data structure: a hierarchical graph.
In this section we shall see how the diagrams we used so far can be informally reconstructed as a data structure which enhances in a rather intuitive way the more commonly used yet often unsatisfactory `abstract syntax trees' (AST).

As an expression of algebraic expressions, abstract syntax trees are perfectly adequate.
Consider an expression such as $1+(2+3)$.
Its tree representation is conventionally written top-to-bottom like this:

\[
\input{pics/ast.pdf_tex}
\]

This syntax tree is `abstract' in the sense that not all the lexical tokens of the original are represented in the tree, namely the open and closed brackets in this example.

The representation becomes unsatisfactory when variables are introduced, as in the expression $x+(2+x)$.
The AST of this expression is:

\[
\input{pics/ast2.pdf_tex}
\]

The problem with this representation, as a data structure, is that it offers poor support to the most common operations performed on variables: substitution.
Replacing $x$ with, say, 0 requires searching the entire graph for occurrences of $x$.
By contrast, using string diagrams the same expression is represented such that only one logical occurrence of the variable $x$, the leftmost wire, is shared by two nodes in the expression:

\[
\input{pics/ast2sd.pdf_tex}
\]

To perform a substitution we no longer require to search the tree for occurrences of $x$, as there is only a single occurrence of the variable.
In fact, in any reasonable concrete implementation of string diagrams the left and right interface wires need to be explicitly recorded, which makes substitution possible in constant time, relative to the size of the overall string diagram.

Once binding syntax is introduced, the shortcomings of the AST become more perspicuous.
Consider the expression $\mathit{let}\ x=0\ in\ x+(2+x)$.
The AST form of the expression is:

\[
\input{pics/ast3.pdf_tex}
\]

Note that the binding occurrence of $x$ and the regular occurrence are not distinguished, and there is no easy way to connect them.
By contrast, the same expression, using a string diagram representation, is:

\[
\input{pics/ast3sd.pdf_tex}
\]

The overall structure is clearer, and it corresponds more closely to the meaning of the expression.
The problem of relating variable occurrences to the binder is solved be making variables into wires rather than boxes.
This distinction between variables and operations is useful in several ways, perhaps the most important being that the string diagram is automatically quotiented by alpha equivalence.

The convenience of this approach becomes more perspicuous in the case of variable shadowing, as in

\[
\mathit{let}\  x = 0\ in\ (\mathit{let}\  x = 1\ in\ x + 2) + x
\]

The AST is of course not ambiguous, but connecting variable occurrences to their binders is even more difficult:

\[
\input{pics/ast4.pdf_tex}
\]

This is why for purposes of mechanisation this representation of variables is usually avoided.
The more streamlined, if harder for human consumption, notation of deBruijn indices is the preferred alternative.
The string diagram representation of this expression is easy to read and it avoids all the pitfalls of variable shadowing:

\[
\input{pics/ast4sd.pdf_tex}
\]

The rather remarkable thing to note here is that this string diagram is equal to that of just $(1+2)+0$!
So the string diagram notation is significantly more abstract than `abstract' syntax trees, as not just alpha equivalence but also linear substitution are absorbed in the notation.

The version of string diagrams used up to this point can be called, in their concrete representation, `abstract syntax DAGs' (directed acyclic graphs).
The hierarchical aspect appears with the introduction of thunks.
Categorical considerations aside, thunks are have uses both semantically and syntactically.
Semantically they indicate to the evaluator that the evaluation of a piece of code must be postponed;  first, a thunk needs to be `forced', i.e. extracted from its protective bubble, by some other operations.
We have already seen how the if-then-else statement forces one of its argument thunks and how application forces the thunk that corresponds to the applied function.

Representing the nullary (i.e. which binds zero variables) thunks of the if-then-else statement explicitly may not seem justified enough.
But the small notational overhead of indicating the thunk explicitly is relevant for generic analyses that want to take the flow of control into account, as the presence of the thunk immediately indicates that the program can control and direct the evaluation.
But these are rather subtle and partly manufactured reasons;  the real reasons are conceptual, the consistency and integrity of the string diagram notation, as presented in the previous sections.

A more direct case can be made for the hierarchical notation in the case of thunks which also bind variables, as is the case with functions.
Taking the ubiquitous $\lambda$-abstraction, the same issues of binding and alpha equivalence discuss earlier will come into play again.
Notably, the binding structures above did not involve thunks.
Why do we need thunks for $\lambda$ and why is the hierarchical structure a reasonable evolution of the AST?

The most important thing is that thunks must be seen as undivided whole, in particular when it comes to their interaction with the Cartesian equations for copying and discarding.
Let us illustrate this with a simple non-example, in which we attempt, and fail, to represent thunks without resorting to hierarchical structure: $\lambda x.x+x$.
The conventional AST we have already agreed that it is not ideal, so we will use the variable conventions of string diagrams while treating the $\lambda$ as if it were an operation:

\[
\input{pics/astlam.pdf_tex}
\]

This is an approach similar to that taken in Interaction nets.

But this notation is clearly problematic both in the presence of copy and discard operation.
A term such as $\mathit{let}\ f=\lambda x.x\ in\ f\,f$ is represented in a way that applying the copying axioms results in an ill-formed string diagram which corresponds to no legal term:

\[
\input{pics/astlam2.pdf_tex}
\]

To overcome this problem interaction nets uses a different kind of node when $\lambda$ nodes are duplicated, with $C$ for copy and $\delta$ as the special node resulting from the copying of a $\lambda$, so the copying rule for abstraction is:

\[
\input{pics/astlam3b.pdf_tex}
\]

This, however, is not a satisfactory solution since it ruins the naturality of copying.
The hierarchical graph structure prevents this problem by treating a thunk as a single indivisible thing.
Indeed, a thunk is always a node, with the inner graph its label:

\[
\input{pics/astlamsd.pdf_tex}
\]

Consider the way in which applying the discard equation is not compatible with the naive representation of $\lambda$ nodes are operations.

Before we conclude, a note on expressing the the beta law or, more generally, the unit-counit cancellation in string diagrams.
The widely used string diagrams for strict monoidal compact closed categories absorb the cancellation rule for adjunctions.
Without going into the technical detail, the unit and the co-unit can be represented as `loops' so that their cancellation equations

\begin{gather*}
\id_A\otimes\eta  \semic  \epsilon\otimes\id_A = id_A \\
\eta\otimes\id_{A^*} \semic  \id_{A^*}\otimes\epsilon = id_{A^*}
\end{gather*}

have neat topological interpretations:

\[
\input{pics/compact-closed.pdf_tex}
\]

Such notations do not seem to be readily available for the unit-counit pair involved in the beta law.
A notable attempt has been made by Baez and Stay, who proposed a `bubble'-`claps' pair in their seminal `Rosetta Stone' paper.
However, their proposal was informal, a side issue to the main thrust of their paper, which focusses on the compact closed structure.
We will attempt to refine our notation here to make it more similar to bubble-clasp diagrams, but only for the sake of explanation.
In the sequel we will use the graphical syntactic sugar already introduced.

Currying in the Rosetta notation, vs. our notation is:

\[
\input{pics/rosetta-currying.pdf_tex}
\]

We can see that this notation is trying to maintain the strict monoidal convention that each wire is labelled by an object, so that composite wires can be decomposed in their constituents.
However, in the case of closed monoidal structure it is not a good idea to give direct access to both $X$ and $Y$ separately in $X\multimap Y$ unless additional graphical conventions are used to prevent nonsensical use of the clasp.

The Rosetta notation `peeks' inside the evaluation, which, so that the beta law is written as the following string diagram equation.

\[
\input{pics/rosetta-beta.pdf_tex}
\]

This is graphically more compelling as it establishes a visual parallel with the way compact closed categories cancel out the two adjunctions.
By using the clasp in a way similar to the strictifier-destrictifier morphisms, and by pairing it with an `anti-clasp' we can combine our notation with the Rosetta in a way that is perhaps graphically more informative without raising the possibility of ill-formed diagrams:

\[
\input{pics/rosetta-beta2.pdf_tex}
\]

However, the clasps and the anti-clasp now ruin somewhat the visual appeal.
But this is the price we may need to pay to avoid ill-formed diagrams.
The additional purchase of the clasps is not worth the additional clutter, so we will stick to the simpler notation.
The reader who disagrees may adopt it, with no cost in terms of rigour.

We conclude here this brief and informal section.
In it we have temporarily suspended our category-theory-driven approach and attempted to persuade the reader that string diagrams, and their concrete incarnation as hierarchical abstract syntax graphs (or more precisely abstract syntax DAGs) could be recovered as an evolution of the more conventional AST representation in which variables, binding, sharing, copying, and discarding are dealt with in such a way so that many useful properties are absorbed in the notation.

§ STRING DIAGRAM REWRITING

Even though we specified the above reduction rules as equations, they display a clear directionality. For instance, the $\beta$ rule may be seen as the process of applying a term $\lambda x u$ to a value $v$, resulting into the term $u[v/x]$. More formally, this amounts to orienting the equation $(\lambda x u) = u[v/x]$ into a rewrite rule $(\lambda x u)v \rew u[v/x]$. We may apply such a rule inside a $\lambda$-term $t$ when the left-hand side $(\lambda x u)v$ appears as a sub-term of $t$ — in this case say that $t$ contains a redex for the rewrite rule. Applying the rule then results into the substitution of $(\lambda x u)v$ with $u[v/x]$ inside $t$.

The rewriting theory of the $\lambda$-calculus is fundamental to describe the computational behaviour of $\lambda$-terms via an operational semantics — a perspective that we will pursue in Section <ref> below. The subject of this section is to illustrate how rewriting works when applied to string diagrams rather than terms.

§.§ Rewriting of String Diagrams in Symmetric Monoidal Categories

We first consider the case of string diagrams in a symmetric strict monoidal category, as introduced in Section <ref>. A naive attempt of transposing the above definitions to the context of string diagrammatic syntax poses immediate challenges. Consider the following example. Suppose we have a rewrite rule of string diagrams

\begin{equation}\label{eq:rewrule-stringdiag}
\raisebox{-.5cm}{\hbox{\input{pics/diagruleLHS.pdf_tex}}} \qquad \rew \qquad \raisebox{-.5cm}{\hbox{\input{pics/diagruleRHS.pdf_tex}}}
\end{equation}

which we want to apply inside a string diagram $t$ of the form

\begin{equation}\label{eq:rewcontext-stringdiag}
\end{equation}

`Morally', $t$ contains a redex for the rule. However, strictly speaking, we can isolate the left-hand side of the rule as a sub-term of $t$ only if we use naturality of the symmetry (Figure 3) to rearrange $t$ as follows:

\begin{equation}
\raisebox{-.7cm}{\hbox{\scalebox{.75}{\input{pics/diagrewlhs.pdf_tex}}}} \quad = \quad \raisebox{-.7cm}{\scalebox{.75}{\hbox{\input{pics/ruleappLHS.pdf_tex}}}}
\end{equation}

Note $t$ and $t'$ are equivalent string diagrams modulo the laws of symmetric monoidal categories. We now have a clear indication of how to apply the rewrite rule: simply replace in $t'$ the left-hand side of the rule with its right-hand side:

\begin{equation}\label{eq:rewstepstringdiag}
\raisebox{-.7cm}{\scalebox{.75}{\hbox{\input{pics/ruleappLHS.pdf_tex}}}} \quad \rew \quad \raisebox{-.7cm}{\scalebox{.75}{\hbox{\input{pics/ruleappRHS.pdf_tex}}}}
\end{equation}

This example suggests that the notion of redex becomes way subtler once moving from terms to string diagrams. A string diagram is an equivalence class of terms, and to find a redex in a string diagrams means to find at least one member of such an equivalence class which contains a redex in the traditional sense. More formally:

Consider a rewrite rule
$$\mathcal{R} \qquad = \qquad   \ \raisebox{-.2cm}{\hbox{\input{pics/diagl.pdf_tex}}} \rew  \ \raisebox{-.2cm}{\hbox{\input{pics/diagr.pdf_tex}}}.$$

We say that a string diagram   -.2cm has a redex for the  rule $\mathcal{R}$ if there exist string diagrams

$$ \ \raisebox{-.4cm}{\hbox{\input{pics/diaglc.pdf_tex}}}\quad \text{ and } \quad \raisebox{-.4cm}{\hbox{\input{pics/diagrc.pdf_tex}}}$$
such that

\begin{equation*}
\ \raisebox{-.2cm}{\hbox{\input{pics/diagf.pdf_tex}}} \quad = \quad \raisebox{-.5cm}{\hbox{\input{pics/rewcontextLHS.pdf_tex}}}
\end{equation*}

modulo the laws of symmetric monoidal categories. If $\ \raisebox{-.2cm}{\hbox{\input{pics/diagf.pdf_tex}}}$ has such a redex, then rewriting $\ \raisebox{-.2cm}{\hbox{\input{pics/diagf.pdf_tex}}}$ with $\mathcal{R}$ produces

\begin{equation*}
\ \raisebox{-.2cm}{\hbox{\input{pics/diagf.pdf_tex}}}  \quad  \rew\quad \raisebox{-.5cm}{\hbox{\input{pics/rewcontextRHS.pdf_tex}}}
\end{equation*}

Although mathematically correct, this definition of string diagram rewriting is unsatisfactory from a practical viewpoint. If we aim at studying the operational behaviour of programs using rewriting, finding a redex should be a computationally feasible task. When it amounts to finding a sub-term inside a $\lambda$-term, this is the case. However, imagine searching for a redex in a string diagram: one would need to explore the space of all equivalent terms represented by such diagram, trying to find one with a redex. This is typically an extremely expensive process to implement.

For this reason, we need to rely on an interpretation of string diagrams which is more efficient for the purpose of rewriting. The date structure which we use to interpret string diagrams is the one of a open hypergraph.

In a nutshell, open hypergraphs generalise standard (directed) graphs in two ways. First, edges are replaced with hyperedges: whereas an edge has just one ingoing and one outgoing node, a hyperedge may have multiple of them (or none), organised as lists. Second, the structures we consider are `open', in the sense that some of their nodes act as an interface, with which they may be combined together with other hypergraphs. Thanks to the interface, open hypergraphs may mirror sequential and parallel composition of string diagrams, and are thus adapted to interpret them.

An example showing our graphical representation of open hypergraphs is displayed in (<ref>) below. First, we proceed with the formal definition of these structures. Labels for nodes and hyperedges will come from a signature, as introduced in Section <ref> when discussing freely generated symmetric strict monoidal categories.

Fix a signature $\Sigma = (\Sigma_0,\Sigma_1)$ of objects $\Sigma_0$ and morphisms $\Sigma_1$.  A ($\Sigma$-labelled) hypergraph is a tuple $(N,E,v,l_n,l_e,)$ where

* $N$ is a set of nodes

* $E$ is a set of hyperedges

* $v \colon E \to N^{\star} \times N^{\star}$ is a function assigning to each hyperedge $e$ a list $\pi_1(v(e))$ of ingoing nodes and a list $\pi_2(v(e))$ of outogoing nodes

* $l_n \colon N \to \Sigma_0$ is a function labeling each node with a generating object in $\Sigma_0$

* $l_e \colon E \to \Sigma_1$ is a function labeling each hyperedge with a generating object in $\Sigma_0$, with the requirement that $l_e(e)$ must have arity $\pi_1(v(e))$ and coarity $\pi_2(v(e))$ in $\Sigma_0$.

Given $\Sigma$-labelled hypergraphs $G = (N,E,v,l_n,l_e,)$ and $G' = (N',E',v',{l'}_n,{l'}_e,)$, a hypergraph morphism $f \colon G \to G'$ consists of functions $f_N \colon N \to N'$ and $f_E \colon E \to E'$ respecting the labelling of nodes and hypergedges and the type of hyperdges. In other words, ${l'}_n(f_N(n)) = v(n)$, ${l'}_e(f_E(e)) = l_e(e)$, and $v'(f_E(e)) = (\hat{f}_N(\pi_1(v(e)),\hat{f}_N(\pi_2(v(e)) )$, where $\hat{f}_N \colon N^{\star} \to N^{\star}$ is the lifting of $f_N \colon N \to N'$, defined pointwise in the obvious way. Such a morphism is a monomorphism if $f_N$ and $f_E$ are both injective functions.

A ($\Sigma$-labelled) open hypergraph is a tuple $(L, G, R, f_L, f_R)$ where

* $G$ is a $\Sigma$-labelled hypergraph, called the carrier

* $L$ is a discrete[Recall that a graph is discrete when is has only nodes, and no (hyper)edges.] $\Sigma$-labelled hypergraph, called the left interface of $G$

* $R$ is a discrete $\Sigma$-labelled hypergraph, called the right interface of $G$

* $f_L \colon L \to G$ and $f_R \colon R \to G$ are hypergraph morphisms.

A open hypergraph morphism $h \colon (L,G,R, f_L, f_R) \to (L',G',R', f'_L, f'_R)$ consists of hypergraph morphisms $h_G \colon G \to G'$, $h_L \colon L \to L'$, $h_R \colon R \to R'$ commuting with the interface morphisms, i.e. such that $h_L  \semic  f'_L = f_L  \semic  h_G$ and $h_R  \semic  f'_R = f_R  \semic  h_G$.

Fix $\Sigma = (\{A,B,C\}, \{f \colon A \otimes B \to C\}, g \colon C \to B\})$. Here is an example of open $\Sigma$-hypergraph $(G,L,R, f_L, f_R)$, displayed both as a tuple (top) and in its graphical representation — in (<ref>) below.

\begin{gather*}
G = \left( \begin{matrix}
N = \{n_1,n_2,n_3,n_4\}, \ E = \{e_1,e_2\} \\
{\small v \colon e_1 \mapsto ([n_1,n_2],[n_3]), \ e_2 \mapsto ([n_3], [n_4])}\\
l_n \colon n_1 \mapsto A, \ n_2 \mapsto B,\  n_3 \mapsto C , \ n_4 \mapsto B \\
l_e \colon e_1 \mapsto f , \ e_2 \mapsto g
\end{matrix}\right)
\qquad
\begin{matrix}
f_L \colon m_1 \mapsto n_1, \ m_2 \mapsto n_2 \\ \\ f_R \colon p \mapsto n_4
\end{matrix}
\end{gather*}

\begin{gather*}
L = \left( \begin{matrix}
N = \{m_1, m_2\},  E = \emptyset \\
l_n \colon m_1 \mapsto A, \ m_2 \mapsto B
\end{matrix}\right)
\qquad
R = \left( \begin{matrix}
N = \{p\}, \ E = \emptyset \\
l_n \colon p \mapsto B
\end{matrix}\right)
\end{gather*}

\begin{equation}\label{ex:hyp}
\scalebox{0.9}{\tikzfig{exhyp}}
\end{equation}

Hyperdges are represented as boxes with round corners, labeled with the generating morphisms in $\Sigma$. Nodes are represented as black dots, labeled with the generating objects in $\Sigma$. The assignment function associating hyperedges to their ingoing and outgoing nodes is displayed with black lines. The left and right interface functions are displayed with red lines.  To emphasise the different role played by the three hypergraphs involved, we use a grey background for the carrier and a blue background for the left and right interfaces.

As mentioned, the presence of interfaces is essential to be able to compose open hypergraphs sequentially, mimicking the way string diagrams are composed. Given open hypergraphs $H_1 = (L_1, G_1, R_1, f_{L_1}, f_{R_1})$ and $H_2 = L_2, G_2, R_2, f_{L_2}, f_{R_2})$ such that $R_1 = L_2$, we can form a composite open hypergraph $H_1  \semic  H_2 = (L_1, G, R_2, f'_{L_1}, f_{R_2})$, where $G$ has been obtained by `gluing' together $G_1$ and $G_2$ along the common interface $R_1 = L_2$. For instance:

\begin{gather*}
H_1 = \scalebox{0.9}{\tikzfig{glueL}} \ \qquad H_2 = \scalebox{0.9}{\tikzfig{glueR}} \\
H_1  \semic  H_2 \ = \ \scalebox{0.9}{\tikzfig{exhyp}}
\end{gather*}

This operation can be defined in full generality using category theory. $\Sigma$-labelled hypergraphs form a category, in which open hypergraphs $H_1$ and $H_2$ as above can be identified with cospans $L_1 \xrightarrow{f_{L_1}} G_1 \xleftarrow{f_{R_1}} R_1$ and $L_2 \xrightarrow{f_{L_2}} G_2 \xleftarrow{f_{R_2}} R_2$ respectively. The composite open hypergraph $H_1 \semic H_2$ is then defined by the cospan $L_1 \xrightarrow{f_{L_1} \semic p_1} G \xleftarrow{f_{R_2} \semic p_2} R_2$ obtained via pushout along the shared interface $R_1 =L_2$:

\begin{eqnarray*}
\xymatrix{
L_1 \ar^{f_{L_1}}[dr] & & \ar_{f_{R_1}}[dl]  R_1 \ar^{f_{L_2}}[dr] & & \ar_{f_{R_2}}[dl] R_2\\
& H_1 \ar^{p_1}[dr]  & & \ar_{p_2}[dl] H_2 & \\
&& \pushoutcorner G &&
\end{eqnarray*}

Moreover, we can easily define a monoidal product operation between open hypergraphs of arbitrary interfaces, which pictorially amounts to stacking them vertically. For instance, with $H_1$ and $H_2$ as above, we have:

\begin{eqnarray*}
\qquad \qquad H_1  \otimes  H_2 & = & \vcenter{\scalebox{0.9}{\tikzfig{tnshyp}}}
\end{eqnarray*}

The reason to introduce open hyergraphs is that there is a well-behaved, natural interpretation of string diagrams into them. In a nutshell, each box (morphism) of a string diagram corresponds to a hyperedge, and each wire (object) corresponds to a node. Nodes on the interfaces correspond to the domain (left interface) and the codomain (right interface) of the string diagram. Sequential and parallel composition of string diagrams is interpreted as composition of open hypergraphs by $\semic$ and $\otimes$ respectively, as defined above.

Let $\Sigma$ be a signature. We define inductively an interpretation $\gint{ \cdot }$ mapping symmetric monoidal $\Sigma$-terms into $\Sigma$-labelled open hypergraphs as follows:

\begin{gather*}
{\input{pics/id.pdf_tex}} \ \mapsto \ \scalebox{0.9}{\tikzfig{idhyp}} \qquad\qquad \raisebox{-.5cm}{\hbox{\input{pics/symmetry.pdf_tex}}}
\ \mapsto \ \scalebox{0.9}{\tikzfig{symhyp}} \\[2em]
op \ \mapsto \ \scalebox{0.9}{\tikzfig{ophyp}} \\[2em]
\raisebox{-.2cm}{\hbox{\input{pics/seqcomp.pdf_tex}}} \mapsto \gint{f} \semic \gint{g} \qquad \raisebox{-.7cm}{\hbox{\input{pics/parcomp.pdf_tex}}} \mapsto \gint{f} \otimes \gint{g}
\end{gather*}

Note the interpretation is defined inductively on terms, but it is perfectly valid on string diagrams, because any two terms that are equal modulo the laws of symmetric monoidal categories are mapped to the same open hypergraph. In fact, even though we introduced this interpretation primarily for the purpose of implementing string diagram rewriting, it is of independent interest: we first introduced string diagrams as syntactic object, but we now have a formal justification to reason about them combinatorially, through the lenses of their hypergraph interpretation.

As it turns out, this interpretation is injective, but not surjective. There are open hypergraphs that are not in the image of any string diagrams. For instance:

\begin{equation}\label{eq:nonmonogamous}
\begin{gathered}
\scalebox{0.9}{\tikzfig{nonmog1}} \qquad \scalebox{0.9}{\tikzfig{nonmog2}} \\[1em]
\scalebox{0.9}{\tikzfig{nonmog3}}
\end{gathered}
\end{equation}

In these open hypergraphs, nodes deviate from their standard behaviour in the string diagram interpretation. In the first example, one node appears twice on the left interface. In the second example, one node does not appear on the right interface, even though it has no outgoing link to any hyperedge. In the third example, the same node is linked twice to the same hyperedge.

Drawing from these examples, we may give a general characterisation of precisely which open hypergraphs are in the image of the interpretation.

An open hypergraph
$(G, L, R, f_L, f_R)$ is monogamous if

* $f_L$ and $f_R$ are monomorphisms of hypergraphs

* for all nodes $n \in N$ of $G = (N,E,v,l_n,l_e)$:

* If $n$ is in the image of $f_L$, $n$ is not an outgoing node of any hyperedge, i.e. $n \not\in \pi_2(v(e))$ for all $e \in E$

* If $n$ is in the image of $f_R$, $n$ is not an ingoing node of any hyperedge, i.e. $n \not\in \pi_1(v(e))$ for all $e \in E$

* Otherwise, $n$ is not in the above images. In this case, $n$ must be an outoing node of exactly one hyperedge $e$ and an ingoing node of exactly one hyperedge $e'$.

Intuitively, monogamicity ensures that nodes on the left/right interface cannot be linked on the same side to a hyperedge, and nodes not on the interface are linked exactly to two hyperedges, one on their left and one on their right. For instance, the first open hypergraph in (<ref>) is not monogamous because its left interface morphism $f_L$ is not a monomorphism. The second is not monogamous because a node is not on any interface but it is linked to no hyperedge on its right. Finally, the third is not monogamous because a node is not on any interface but it is linked more than once to hyperedges on its left (the fact that it is linked to the same hyperedge twice or to different ones is immaterial to the criterion).

An open hypergraph is monogamous if and only if it is in the image of the interpretation $\gint{ \cdot }$.