Braids, Twists, Trace and Duality in Combinatory Algebras
Masahito Hasegawa

Research Institute for Mathematical Sciences, Kyoto University

Serge Lechenne

École Normale Supériere Paris-Saclay

National Institute for Informatics

We investigate a class of combinatory algebras, called ribbon combinatory algebras, in which we can interpret both the braided untyped linear lambda calculus
and framed oriented tangles.  Any reflexive object in a ribbon category gives rise to
a ribbon combinatory algebra. Conversely, From a ribbon combinatory algebra, we
can construct a ribbon category with a reflexive object, from which the combinatory
algebra can be recovered. To show this, and also to give the equational characterisation of ribbon combinatory algebras, we make use of the internal PRO
construction developed in Hasegawa's recent work.
Interestingly, we can characterise ribbon combinatory algebras in two different ways: as balanced combinatory algebras
with a trace combinator, and as balanced combinatory algebras with duality.

2024 Copyright held by the authors.
This is the authors' version of the work to appear in Proc. 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '24).
The definitive version will be available from <https://doi.org/10.1145/3661814.3662098>.]

§ INTRODUCTION

Since the 1980s, there has been a huge amount of research focusing on the
graphical formulations of the lambda calculus and related systems,
both from theoretical and practical sides. Major themes include
term graphs and graph reductions <cit.>, proof nets <cit.>, and Geometry of Interaction <cit.>.
Most of them are combinatorial, in the sense that they concern the graph-theoretic
formalism and techniques. On the other hand, the geometric perspective
has been less studied. For instance, one could ask: how can we implement such graphical structures in the three-dimensional space? Do they form meaningful geometric entities?

As an example, let us consider the combinator $\CC=\lambda fxy.f\,y\,x$,
that can be represented, under the rooted trivalent graph interpretation developed in <cit.> as

(55,0)$\lambda fxy.fy\,x$
(-15,15)$\lambda xy.fy\,x$
(-37,60)$\lambda y.fy\,x$

where the lambda abstraction and application are expressed by the nodes (7,5)[c]$\lamnode$ and (7,5)[c]$\appnode$ respectively
(see the pictures below left),
which obey the $\beta$-rule (below right).

(45,10)(0,0)$\lambda x.M$

In the three-dimensional space, the graph of $\CC$ can have several implementations which are topologically different. For example:

This three dimensional nature of $\CC$ was formalised by Hasegawa <cit.>
as braided terms of a new lambda calculus, called a braided lambda calculus. In that work,
variables are realised as wires, and permutations/exchanges of variables are
realised by appropriate braids <cit.>. Two terms are identified modulo
the $\beta\eta$-equality which includes continuous deformations of such wires.
Thus terms are regarded as entities of low-dimensional topology.

In the subsequent work <cit.>, Hasegawa developed a general approach to combinatory algebras,
where it is shown that any planar, linear, braided and classical combinatory algebra validating the $\beta\eta$-theory of the corresponding
lambda calculus gives rise to an internally defined monoidal category equipped with a reflexive object, and the combinatory algebra
induced by the reflexive object is isomorphic to the original combinatory algebra. The key idea is the notion of arity, which determines the
structure of the monoidal category in a canonical way. Now combinators get a geometric reading via the string diagram of the internally
defined monoidal categories, which subsumes the case of the braided lambda calculus.
Furthermore, as noted in <cit.>,
we could have a non-standard combinator $\Tr$
with the following graph,
which does not correspond to the usual lambda term:

$\Tr$, if combined with braided terms, can be used for creating knots:
$\beta$-reductions on $\Tr\,(\Tr\,(\CC^+)^3)$ produce a trefoil knot.

Here, the application of the non-standard combinator $\Tr$ implements a (partial) braid closure, or more generally an abstract trace <cit.>.

Following these results, in this paper, we make a further step towards the geometric reading of terms / combinators by investigating
the structure of ribbon categories in combinatory algebras. Ribbon categories <cit.>, also known as tortile categories <cit.>,
are monoidal categories with braids, twists and duality which can model the framed tangles (ribbons) <cit.>, just in the same way that cartesian closed
categories can model the simply typed lambda calculus <cit.>. In <cit.> Hasegawa considered braids and symmetry. In this paper, we deal with
twist, trace and duality.

As a result, we get a situation in which tangles and lambda terms/combinators can be freely mixed, which has not been studied before.
Our results are theoretical and we do not claim that they have some practical application (at least immediately). Nevertheless,
we think that this approach exhibits the less-known geometric perspectives of combinatory logic which deserve further study, and they
might lead to
some practical applications (e.g., low-level physical implementation models such as topological quantum computation <cit.>).
Also, we shall point out that some of the key ideas were already present in Curry's pioneering work <cit.>; it seems that Curry had a
clear geometric reading of combinators in mind, which we believe is not very far from ours.

In addition, in the presence of braids, twists and trace/duality, we find that combinatory algebras offer a much simpler formalism
than lambda calculi in which we cannot avoid quite complicated substitution mechanisms as observed in <cit.>.

The rest of this paper is organised as follows.
In Section <ref>, we recall monoidal categories and related structures to be used throughout this work.
In Section <ref>, we study how monoidal categories can be derived from combinatory algebras, following Hasegawa's approach. Section <ref> is devoted to the study of reflexive objects in ribbon categories.
Using the results of Section <ref> and <ref>, we introduce ribbon combinatory algebras in Section <ref>.
In Section <ref> we compare a ribbon category with a reflexive object and the internal PROB of the ribbon combinatory algebra
derived from the reflexive object. In Section <ref> we discuss related work, including Curry's classical work.
We conclude this paper with a summary and some future work in Section <ref>.

§ MONOIDAL CATEGORIES

In most cases, we write $f;g$ for the composition of arrows $f\colon A\rightarrow B$
and $g\colon B\rightarrow C$ in a category. On the other hand, we write
$a\circ b$ for the composition $\BB\,a\,b$ in combinatory algebras and their internal PROs (Section <ref>).
Note that, in an internal PRO, $a\colon l\rightarrow m$ and $b\colon m\rightarrow n$ imply
$a\circ b\colon l\rightarrow n$
(Lemma <ref>), which is $a;b$ in the other cases and is the opposite of
the conventional use of the symbol $\circ$.

§.§ Monoidal categories

A monoidal category (also called tensor category) <cit.>
is a category $\mathbb{C}$ equipped with a functor
$\otimes\colon {\mathbb{C}}\times{\mathbb{C}}\rightarrow{\mathbb{C}}$ (tensor product),
an object $I\in{\mathbb{C}}$ (tensor unit) and natural
(A\otimes B)\otimes C\stackrel{\sim}{\rightarrow}A\otimes(B\otimes C)$,
$l_A\colon I\otimes A\stackrel{\sim}{\rightarrow}A$ and
$r_A\colon A\otimes I\stackrel{\sim}{\rightarrow}A$
subject to the standard coherence axioms.
It is said to be strict if $a,l,r$ are
identity morphisms. Whenever convenient, we will pretend as if our monoidal categories are strict;
the coherence theorem <cit.> ensures that nothing goes wrong in doing so.

In the sequel, we will make use of the string diagrams: the graphical presentation of
morphisms in monoidal categories <cit.>. A morphism
$  f\colon A_1\otimes A_2\otimes\dots\otimes A_m\rightarrow
B_1\otimes B_2\otimes\dots\otimes B_n$ in a monoidal category
will be drawn as (to be read from left to right):

07040 (-20,70)(0,0)$A_m$
03040 (-20,30)(0,0)$A_2$ (-20,45)$\vdots$
01040 (-20,10)(0,0)$A_1$
907040 (145,70)(0,0)$B_n$
903040 (145,30)(0,0)$B_2$ (145,45)$\vdots$
901040 (145,10)(0,0)$B_1$

The composition and tensor of morphisms are depicted as follows.

2002020 (200,23)$A$
2502020 (255,23)$B$
3002020 (310,23)$C$
(260,-28)(0,0) $f;g\colon A\rightarrow C$

1502520 (150,30)$A_1$
2002520 (210,30)$B_1$
1506520 (150,70)$A_2$
2006520 (210,70)$B_2$
(185,-10)(0,0) $f_1\otimes f_2\colon A_1\otimes A_2\rightarrow B_1\otimes B_2$

A PRO, meaning a "PROduct category", is a strict monoidal category generated by
a single object. We identify objects of a PRO with natural numbers $\mathbb{N}$; the tensor product of objects $m$ and $n$
is the addition $m+n$, while the tensor unit $I$ is $0$. Thus a PRO $\mathbb{C}$ can be defined
as an $\mathbb{N}^2$-indexed family $\mathbb{C}(m,n)$ with the following constructs

* the identity $\id_n\in\mathbb{C}(n,n)$

* the composition $f;g\in\mathbb{C}(l,n)$ for $f\in\mathbb{C}(l,m)$, $g\in\mathbb{C}(m,n)$

* the tensor $f_1+f_2\in\mathbb{C}(m_1+m_2,n_1+n_2)$ for $f_i\in\mathbb{C}(m_i,n_i)$

which are subject to the following axioms.

\begin{array}{lr}
\multicolumn{2}{l}{\id_m;f=f=f;\id_n\hspace{2mm}(f\in\mathbb{C}(m,n))}\\
\multicolumn{2}{l}{(f;g);h = f;(g;h)\hspace{2mm}(f\in\mathbb{C}(l,m),~g\in\mathbb{C}(m,n),~h\in\mathbb{C}(n,p))}\\
f+\id_0 = f = \id_0+f \\
(f_1+f_2)+f_3=f_1+(f_2+f_3) \\
\id_m+\id_n = \id_{m+n}\\
(f_1+f_2);(g_1+g_2) = (f_1;g_1)+(f_2;g_2) & (f_i\in\mathbb{C}(l_i,m_i),~g_i\in\mathbb{C}(m_i,n_i))
\end{array}

From these axioms, we have the interchange law

for $f\in\mathbb{C}(m,n)$ and $g\in\mathbf{C}(m',n')$.
Indeed, instead of $f+g$ for arrows $f$ and $g$, we may use $f+m$ $(=f+\id_m)$ and $m+f$ $(=\id_m+f)$ as primitive constructs,
with slightly simplified axioms $f+0=f=0+f$, $(m+f)+m'=m+(f+m')$, $(m+m')+f=m+(m'+f)$, $(f+m)+m'=f+(m+m')$
and the interchange law
for defining PROs.
$f+g$ is then defined either as $(f+m');(n+g)$ or $(m+g);(f+n')$.
This alternative characterisation will be useful in developing PROs in combinatory algebras.

§.§ Braids and twists

A braid <cit.> in a monoidal category is a natural isomorphism
$ \sigma_{A,B}\colon A\otimes B\stackrel{\cong}{\rightarrow} B\otimes A$
such that both $\sigma$ and $\sigma^{-1}$
satisfy the following “bilinearity” or “Hexagon Axiom"
(the case for $\sigma^{-1}$ is omitted):

(50,60)(1,0)25 (62.5,65)(0,0)$a_{A,B,C}$
(125,60)(1,0)25 (137.5,65)(0,0)$\sigma_{A,B\otimes C}$

(50,20)(1,0)25 (62.5,15)(0,0)$a_{B,A,C}$
(125,20)(1,0)25 (137.5,15)(0,0)$B\otimes \sigma_{A,C}$

(25,52.5)(0,-1)25 (9,40)(0,0)$\sigma_{A,B}\otimes C$
(175,52.5)(0,-1)25 (187,40)(0,0)$a_{B,C,A}$

(25,60)(0,0)$(A\otimes B)\otimes C$
(100,60)(0,0)$A\otimes (B\otimes C)$
(175,60)(0,0)$(B\otimes C)\otimes A$

(25,20)(0,0)$(B\otimes A)\otimes C$
(100,20)(0,0)$B\otimes (A\otimes C)$
(175,20)(0,0)$B\otimes (C\otimes A)$

A braided monoidal category is a monoidal category equipped with a braid.

A twist or balance <cit.> for a braided monoidal category is a natural isomorphism
$\theta_A\colon A\stackrel{\cong}{\rightarrow}A$ satisfying
$\theta_{A\otimes B}=\sigma_{A,B};(\theta_B\otimes\theta_A);\sigma_{B,A}$.
A balanced monoidal category is a braided monoidal category with a twist.

The braids and twists will be depicted in the string diagrams (oriented from left to right)
as follows (cf. <cit.>).

\begin{array}{cccccc}
\sigma_{X,Y}
\sigma_{X,Y}^{-1}
\theta_X
\theta_X^{-1}
\\
\\
\begin{picture}(60,20)(-10,0)
\thicklines
\braid{10}{0}{5}{10}
\put(5,0){\makebox(0,0){\scriptsize$X$}}
\put(5,20){\makebox(0,0){\scriptsize$Y$}}
\put(35,0){\makebox(0,0){\scriptsize$Y$}}
\put(35,20){\makebox(0,0){\scriptsize$X$}}
\end{picture}
\begin{picture}(60,20)(-10,0)
\thicklines
\braidInv{10}{0}{5}{10}
\put(5,0){\makebox(0,0){\scriptsize$Y$}}
\put(5,20){\makebox(0,0){\scriptsize$X$}}
\put(35,0){\makebox(0,0){\scriptsize$X$}}
\put(35,20){\makebox(0,0){\scriptsize$Y$}}
\end{picture}
\begin{picture}(60,20)(-10,0)
\thicklines
\twist{10}{10}
\put(5,10){\makebox(0,0){\scriptsize$X$}}
\put(35,10){\makebox(0,0){\scriptsize$X$}}
\end{picture}
\begin{picture}(60,20)(-10,0)
\thicklines
\twistInv{10}{10}
\put(5,10){\makebox(0,0){\scriptsize$X$}}
\put(35,10){\makebox(0,0){\scriptsize$X$}}
\end{picture}
\\
\end{array}

A braid $\sigma$ is called a symmetry when it satisfies $\sigma_{X,Y}^{-1}=\sigma_{Y,X}$ for all $X$ and $Y$,
which will be depicted as
A symmetric monoidal category is a monoidal category equipped with a symmetry.
Note that a balanced monoidal category is symmetric exactly when its twist is the identity.

PROPs and PROBs
A PROP, meaning a "PROduct and Permutation category", is a PRO equipped with a symmetry,
thus a strict symmetric monoidal category generated by
a single object. In a PROP, its symmetry $\sigma$ is determined by its $(1,1)$-component $\sigma_{1,1}\colon 2\rightarrow 2$
as the Hexagon axiom implies $\sigma_{l,m+n}=(\sigma_{l,m}+n);(m+\sigma_{l,n})$ and
$\sigma_{m+n,1}=(m+\sigma_{n,1});(\sigma_{m,1}+n)$. We may define a PROP as a PRO equipped with $\sigma\colon 2\rightarrow 2$
such that the Coxter relations $\sigma;\sigma=\id_2$ and $(1+\sigma);(\sigma+1);(1+\sigma)=(\sigma+1);(1+\sigma);(\sigma+1)$

hold and $\sigma_{m,n}\colon m+n\rightarrow n+m$ induced by $\sigma=\sigma_{1,1}$ satisfies the naturality $(f+g);\sigma_{n,n'}=\sigma_{m,m'};(g+f)$.

Similarly, a PROB is a PRO equipped with a braid, i.e., a strict braided monoidal category with a single generating object.
It can be defined as a PRO equipped with $\sigma^+,\sigma^-\colon 2\rightarrow 2$
subject to the Coxter relations (or Reidemeister move II and III) $\sigma^\pm;\sigma^\mp=\id_2$ and

and the naturality of $\sigma_{m,n}\colon m+n\rightarrow n+m$ determined from $\sigma_{1,1}=\sigma^+$.

In addition, we can talk about balanced PROB: it is a PROB equipped with $\theta^+,\theta^-\colon 1\rightarrow 1$
satisfying $\theta^\pm;\theta^\mp=\id_1$ and the naturality of $\theta_m\colon m\rightarrow m$ determined by
$\theta_1=\theta^+$ and

§.§ Duality and trace

In a monoidal category, a  dual pairing between two objects
$A$ and $B$ is a pair of morphisms $\eta\colon I\rightarrow A\otimes B$, called unit,
and $\varepsilon\colon B\otimes A\rightarrow I$, called counit,
depicted in the string diagrams
as follows

\renewcommand{\arraystretch}{.5}
\begin{array}{cccccc}
\eta
\varepsilon
\\
\\
\begin{picture}(40,20)(5,0)
\thicklines
\arcLR{20}{0}{-10}{10}
\lineseg{20}{20}{30}{20}
\lineseg{20}{0}{30}{0}
\put(35,0){\makebox(0,0){\scriptsize$A$}}
\put(35,20){\makebox(0,0){\scriptsize$B$}}
\end{picture}
\begin{picture}(40,20)(-5,0)
\thicklines
\arcLR{20}{0}{10}{10}
\lineseg{20}{20}{10}{20}
\lineseg{20}{0}{10}{0}
\put(0,20){\makebox(0,0){\scriptsize$A$}}
\put(0,0){\makebox(0,0){\scriptsize$B$}}
\end{picture}
\\
\\
\end{array}

which are subject to the snake equations:

In such a dual pairing, $B$ is called the left dual of $A$ while $A$ is the right dual of $B$.
For any object, its left (or right) dual, if exists, is unique up to isomorphism.
A left autonomous category is a monoidal category $\mathbb{C}$ in which
every object $X$ has a (chosen) left dual $X^*$ with unit $\eta_X\colon I\rightarrow X\otimes X^*$ and counit $\varepsilon_X\colon X^*\otimes X\rightarrow I$.
The map $X\mapsto X^*$ extends to a contravariant functor $(\_)^*\colon \mathbb{C}^\mathrm{op}\rightarrow\mathbb{C}$.
A symmetric left autonomous category is called a compact closed category <cit.>.

Ribbon categories.

A ribbon category <cit.>, also called a tortile monoidal category <cit.>, is a balanced monoidal category which is left autonomous and satisfies $(\theta_X)^*=\theta_{X^*}$.
Ribbon categories are of great importance in low-dimensional topology and representation theory of quantum groups,
since the free ribbon category is equivalent to the category of (oriented framed) tangles <cit.>, and many useful ribbon categories
are obtained as categories of representations of quantum groups <cit.>.
Compact closed categories are ribbon categories whose braid is symmetric and whose twist is the identity.

A (right) trace on a balanced monoidal category $\mathbb{C}$ is a family of maps
$\mathit{Tr}^X_{A,B}\colon \mathbb{C}(A\otimes X,B\otimes X)\rightarrow\mathbb{C}(A,B)$
subject to a few coherence axioms <cit.>. A traced monoidal category is a balanced
monoidal category equipped with a trace.

If $\mathbb{C}$ is a ribbon category,
it has a unique trace <cit.> given by

\mathit{Tr}^X_{A,B}(f)=
(f\otimes X^*);

Hence a ribbon category is also a traced monoidal category.
While not all traced monoidal categories are ribbon,
any traced monoidal category can be embedded in
a ribbon category <cit.>. Specifically, given a traced monoidal
category $\mathbb{C}$, one can construct a ribbon category $\mathbf{Int}\mathbb{C}$
with a fully faithful structure-preserving functor from $\mathbb{C}$ to $\mathbf{Int}\mathbb{C}$.
So traced monoidal categories can be characterised as the monoidal full subcategories of ribbon categories.

§.§ Closed structure and reflexive objects

We say a monoidal category $\mathbb{C}$ is closed when the functor $(\_)\otimes A\colon \mathbb{C}\rightarrow\mathbb{C}$ has a right adjoint
$A\multimap(\_)\colon \mathbb{C}\rightarrow\mathbb{C}$, hence $\mathbb{C}(X\otimes A,B)\cong\mathbb{C}(X,A\multimap B)$.
In particular, left autonomous categories and ribbon categories are closed with $A\multimap B= B\otimes A^*$.

In a
monoidal category $\mathbb{C}$
(which does not have to be closed), we say an object $A$ is (strictly) reflexive when the
functor $\mathbb{C}(\_\otimes A,A)$ is represented by $A$ itself, thus there exists a natural isomorphism
$\mathsf{cur}\colon \mathbb{C}(\_\otimes A,A)\stackrel{\cong}{\rightarrow}\mathbb{C}(\_,A)$. When $\mathbb{C}$ is closed,
$A$ is a reflexive object if and only if $A$ is isomorphic to $A\multimap A$.
Using a reflexive object, we can model the abstraction and application in the untyped lambda calculus as follows.
For $f\colon X\otimes A\rightarrow A$, its currying $\mathsf{cur}(f)\colon X\rightarrow A$ amounts to the lambda abstraction. For the application,
we have $\mathsf{app}=\mathsf{cur}^{-1}(\mathit{id}_A)\colon A\otimes A\rightarrow A$. Then the $\beta$-rule  $(\mathsf{cur}(f)\otimes X);\mathsf{app}=f$
holds for $\mathsf{cur}^{-1}(\mathsf{cur}(f))=f$ and the naturality of $\mathsf{cur}$.
The $\eta$-rule is immediate as $\mathsf{cur}(\mathsf{cur}^{-1}(g))=g$.
Alternatively, a reflexive object can be defined as an object $A$ equipped with a morphism $\mathsf{app}\colon A\otimes A\rightarrow A$
such that, for any $f\colon X\otimes A\rightarrow A$, there exists a unique $\mathsf{cur}(f)\colon X\rightarrow A$ satisfying
$(\mathsf{cur}(f)\otimes A);\mathsf{app}=f$. Note that the naturality $h;\mathsf{cur}(f)=\mathsf{cur}((h\otimes A);f)$ ($h\colon X\rightarrow Y$, $f\colon Y\otimes A\rightarrow A$)
follows from the uniqueness of the currying.

(In the literature, it is more common to define a reflexive object to be an object $A$ such that  $A\multimap A$ is a retract of $A$,
which can model the $\beta$-theory of the lambda calculus.
In this paper, we focus on the extensional (i.e., $\beta\eta$) cases, and by a reflexive object we mean a strict one as defined above.)

Reflexive PROs

We are particularly interested in PROs in which $1$ is a reflexive object, which gives a neat setting to discuss the untyped lambda calculus
and combinatory algebras.
We call such a PRO a reflexive PRO. Thus a reflexive PRO is a PRO equipped with $\mathsf{app}\colon 2\rightarrow 1$ and
a unique $\mathsf{cur}(f)\colon n\rightarrow 1$ satisfying $(\mathsf{cur}(f)+1);\mathsf{app}=f$ for $f\colon n+1\rightarrow 1$.
In particular, for any $f\colon n\rightarrow 1$, $\mathsf{cur}^n(f)\colon 0\rightarrow 1$ is a unique element such that
$(\mathsf{cur}^n(f)+n);(\mathsf{app}+(n-1));\dots;(\mathsf{app}+1);\mathsf{app}=f$ holds.

In this paper ribbon categories with a reflexive object will play a central role.
For a concrete nontrivial (non-symmetric) example of such a ribbon category, we refer to <cit.>.
A combinatory algebra arising from such an example will be described in Example <ref>.

§ MONOIDAL STRUCTURES IN COMBINATORY ALGEBRAS

Hasegawa <cit.> has shown that a combinatory algebra arises from a reflexive object in a monoidal category if
and only if it has a monoidal category with a reflexive object internally defined in the combinatory algebra itself. The basic idea
follows from the standard practice  of encoding tuples of terms $M_1,\dots, M_n$ by $\lambda f.f\,M_1\,\dots\,M_n$ in the lambda calculus
we use a combinator corresponding to the closed lambda term of the form

$$\lambda fx_1\dots x_m.f\,M_1\,\dots M_n$$

as a
morphism with $m$ inputs and $n$ outputs, where the variable $f$, expressing the evaluation context or the continuation of the
process, is not free in $M_i$'s. Intuitively, such a combinator takes a continuation $f$ and inputs $x_1,\dots x_m$,
and returns the outputs $M_1,\dots,M_n$ to the continuation.
We say that such a combinator $a$ is of arity $m\rightarrow n$ and express this as $a\colon m\rightarrow n$.
While not all combinators have arity (e.g., the combinator corresponding to $\lambda xy.y\,x$),
several standard combinators do have arity, including
$\BB=\lambda fxy.f\,(x\,y)\colon 2\rightarrow 1$, $\II=\lambda f.f\colon 0\rightarrow 0$, $\CC=\lambda fxy.f\,y\,x\colon 2\rightarrow 2$,
$\SS=\lambda fxy.f\,y\,(x\,y)\colon 2\rightarrow 2$, $\KK=\lambda fx.f\colon 1\rightarrow 0$, and $\WW=\lambda fx.f\,x\,x\colon 1\rightarrow 2$.
Also, for any combinator $a$ (which may not have an arity), $\lambda f.f\,a$ is of arity $0\rightarrow 1$.
We can depict these combinators with arity using string diagrams as follows:

(30,30)(0,0)$\BB\colon 2\rightarrow 1$

(30,30)(0,0)$\CC\colon 2\rightarrow 2$

The central findings of <cit.> are

* algebraic characterisation of arities:  a combinator $a$ with arity $m\rightarrow n$
can be characterised as the one satisfying an equation expressing that the following interchange law

holds for any $b$;

* internal PRO: combinators with arity form a strict monoidal category generated by a single object $1$ (the internal PRO);

* reflexive object: $1$ is a reflexive object in the internal PRO, with the application $\BB\colon 2\rightarrow 1$; and

* internal representation: the combinatory algebra derived from the reflexive object is isomorphic to the original combinatory algebra,

provided the combinatory algebra validates the $\beta\eta$-theory of the lambda calculus (i.e., they are Curry algebras).
They immediately imply a version of Scott's theorem <cit.>: any such combinatory algebra arises
via a reflexive object in a monoidal category.
Also, we can systematically derive axioms for such combinatory algebras from these results: axioms directly follow from those of PROs
and reflexive objects.
Below we first recall the most basic case of the combinatory algebras corresponding to the planar lambda calculus;
as shown in <cit.>, cases with symmetry (the linear lambda calculus), braids (the braided lambda calculus),
copying and discarding (the lambda calculus) are covered by adding appropriate constructs to the planar case.
In the remaining part of this section, We shall explain how we can introduce and axiomatise braids, symmetry and twists in combinatory algebras.
The main contribution of the present paper is then to show that this story can be carried out for the case with duality, i.e., ribbon categories,
which will be done in the following sections.

§.§ Combinatory algebras

Let us recall some basics on applicative structures and combinatory algebras
<cit.> which will be used in the rest of this paper.
A applicative structure $(\calA,\cdot)$ is a set $\calA$ equipped with
a binary map $(\_)\cdot(\_):\calA\times \calA\rightarrow \calA$ called application.
As is customary, applications are assumed to be left associative, and the infix $\cdot$ is often omitted.
Thus $a\,b\,c$ means $(a\cdot b)\cdot c$ while $a\,(b\,c)$ is $a\cdot(b\cdot c)$.
In the literature, a combinatory algebra often refers to an $\SK$-algebra, which is an applicative structure
equipped with elements $\SS$ and $\KK$ satisfying $\SS\,a\,b\,c=(a\,c)\,(b\,c)$ and $\KK\,a\,b=a$.
However, combinatory algebras can also be characterised more conceptually by the combinatory completeness <cit.>.
For an applicative structure $\calA$, let $\calA[x_1,\dots,x_n]$ be the set of expressions (polynomials)
generated by elements of $\calA$
and indeterminates $x_1,\dots,x_n$ and application $\cdot$.
We say $\calA$ is combinatory complete if, for any $p\in\calA[x_1,\dots,x_n,x]$, there exists
$\lambda^*x.p\in\calA[x_1,\dots,x_n]$ such that $(\lambda^*x.p)\cdot x=p$ holds; and then a combinatory algebra can be defined
as a combinatory complete applicative structure. It is well-known that these two definitions of combinatory algebras coincide:
combinatory completeness implies existence of $\SS$ and $\KK$, while it is standard to define $\lambda^*x.p$ using $\SS$ and $\KK$

In this paper, we will deal with more general classes of combinatory algebras than those recalled above.
By focusing on combinatory completeness concerning linear polynomials (in which each indeterminate is used exactly once),
we have the linear variant of combinatory algebras, which are $\BCI$-algebras with elements $\BB$, $\CC$ and $\II$
satisfying $\BB\,a\,b\,c=a\,(b\,c)$, $\CC\,a\,b\,c=a\,c\,b$ and $\II\,a=a$. Similarly, by further restricting our attention to
planar polynomials (in which each indeterminate is used exactly once in the prescribed order),
we have a planar variant of combinatory algebras, which will be recalled below.
Hasegawa <cit.> argues that the notion of operads (one-object multicategories) gives a uniform foundation handling
these variations and more (the braided case in particular).

§.§ Planar combinatory algebras and their internal PROs

The planar lambda calculus <cit.> is an untyped linear lambda calculus in which no exchange of variables is allowed.
Its terms are generated by the following rules for variables, lambda abstractions and applications:

\frac{}{x\vdash x}
\hspace{15mm}
\frac{\Gamma,x\vdash M}{\Gamma\vdash \lambda x.M}
\hspace{15mm}
\frac{\Gamma\vdash M \hspace{3mm}\Gamma'\vdash N}{\Gamma,\Gamma'\vdash M\,N}

Planar terms are closed under $\beta\eta$-conversions. The most important planar terms include
$\BB=\lambda fxy.f\,(x\,y)$, $\II=\lambda f.f$ and $M^\bullet=\lambda f.f\,M$ for closed planar $M$.
On the other hand, $\CC=\lambda fxy.f\,y\,x$ is not planar.

Tomita <cit.> introduced $\BIdot$-algebras as the combinatory algebras corresponding to the planar lambda calculus.

A $\BIdot$-algebra is an applicative structure $\calA$ with elements $\BB$, $\II$ and $a^\bullet$ for $a\in\calA$, satisfying
$\II\,a=a$ and

Tomita has shown that a $\BIdot$-algebras is planar combinatory complete:
for a planar term $p$ with its rightmost variable $x$, there is $\lambda^*x.p$ satisfying $(\lambda^*x.p)\,x=p$.
$\lambda^*x.p$ which can be given by

\begin{array}{rcll}
\lambda^*x.x &=& \II\\
\lambda^*x.p\,q &=& \BB\,q^\bullet\,(\lambda^*x.p) & (x~\mathrm{free~in}~p)\\
\lambda^*x.p\,q &=& \BB\,p\,(\lambda^*x.q) & (x~\mathrm{free~in}~q).
\end{array}

$\BIdot$-algebras are central in Tomita's theory of non-symmetric realizability: the assemblies of a
$\BIdot$-algebra form a closed multicategory <cit.> which models the implicational fragment of the
non-commutative multiplicative intuitionistic linear logic.

Extensionality axioms and the internal PRO

As is well-known, combinatory completeness alone is not sufficient for interpreting the $\beta\eta$-theory of the
lambda calculus in combinatory algebras, and the same is the case for the planar lambda calculus and $\BIdot$-algebras.
Hasegawa <cit.> identified additional extensionality axioms for $\BIdot$-algebras making them sound and complete for
the planar lambda calculus with $\beta\eta$-theory.
(This notion of extensionality differs from the standard terminology <cit.> where an applicative structure
$A$ is said to be extensional when $a\,x=b\,x$ implies $a=b$ for all elements $x$ of $\calA$.
Our extensionality agrees with the notion of Curry-algebras; see <cit.> for relevant discussions.)

A $\BIdot$-algebra is extensional when it satisfies the following axioms,
where $a\circ b$ is an abbreviation for $\BB\,a\,b$.

\begin{array}{rcll}
\BB\,\II &=& \II & (BI)\\
(a\,b)^\bullet &=& b^\bullet\circ(a^\bullet\circ\BB) & (\bullet\mathit{app})\\
\BB^\bullet\circ (\BB\circ(\BB\circ\BB)) &=& (\BB\,\BB)\circ\BB & (\mathit{arity}_\BB)\\
\II^\bullet \circ \BB &=& \BB\,\II & (\mathit{arity}_\II)\\
a^{\bullet\bullet}\circ\BB &=& (\BB\,a^\bullet)\circ\BB & (\mathit{arity}_{a^\bullet})\\
\end{array}

It is routine to check that reflexive objects in monoidal categories give extensional $\BIdot$-algebras:

Suppose that $A$ is a reflexive object in a monoidal category $\mathbb{C}$.
Then $\mathbb{C}(I,A)$ is an extensional $\BIdot$-algebra with
$a\cdot b=(a\otimes b);\mathsf{app}$,
$\BB=\mathsf{cur}(\mathsf{cur}(\mathsf{cur}((A\otimes\mathsf{app});\mathsf{app})))$, $\II=\mathsf{cur}(\id_A)$ and
$a^\bullet=\mathsf{cur}((A\otimes a);\mathsf{app})$.

We will soon see that all extensional $\BIdot$-algebras arise in this way (Cor. <ref>).

In an extensional $\BIdot$-algebra, $(a\circ b)\circ c=a\circ(b\circ c)$ and $a\circ\II=a=\II\circ a$ hold.
Moreover, $\BB\,\II=\II$ and $\BB\,(a\circ b)=(\BB\,a)\circ(\BB\,b)$ hold.

$\BB\,(a\circ b)=((\BB\,\BB)\circ\BB)\,a\,b=
(\BB^\bullet\circ(\BB\circ(\BB\circ \BB)))\,a\,b=(\BB\,a)\circ(\BB\,b)$.
$(a\circ b)\circ c = \BB\,(a\circ b)\,c=((\BB\,a)\circ(\BB\,b))\,c=a\circ(b\circ c)$.

For an element $a$ of a $\BIdot$-algebra, let $a^0=\II$ and $a^{n+1}=a\circ a^n$.

An element $a$ of an extensional $\BIdot$-algebra is said to be of arity $m\rightarrow n$
(notation: $a\colon m\rightarrow n$)
when it satisfies

a^\bullet\circ\BB^{m+1}\,=\,(\BB\,a)\circ\BB^n \hspace{1cm} (\mathit{arity}_a).

In the combinatory algebra of closed terms of the $\lambda_{\beta\eta}$-calculus, a term is of arity $m\rightarrow n$
if and only if
it equals a term of the form $\lambda fx_1\dots x_m.f\,M_1\dots M_n$ with no free $f$ in $M_i$'s <cit.>.

In an extensional $\BIdot$-algebra, the following results hold.

* For $a\colon m\rightarrow n$ and $b$, $(\BB^m\,b)\circ a = a\circ (\BB^n\,b)$ holds.

* $\BB\colon 2\rightarrow 1$,
$\II\colon 0\rightarrow0$
$a^\bullet\colon 0\rightarrow 1$ for any $a\in\calA$.

* If $a\colon m\rightarrow n$, then
$\BB\,a\colon m+1\rightarrow n+1$.

* If $a\colon l\rightarrow m$
and $b\colon m\rightarrow n$, then
$a\circ b\colon l\rightarrow n$.

* If $a\colon m\rightarrow n$, then
$a\colon m+1\rightarrow n+1$.

* $a\colon m\rightarrow 1$ iff $a=(a\,\II)^\bullet\circ\BB^m$.

* $(\BB^m\,b)\circ a = (a^\bullet\circ \BB^{m+1})\,b= ((\BB\,a)\circ\BB^n)\,b= a\circ (\BB^n\,b)$.

* Immediate from the axioms of extensionality.

* $(\BB\,a)^\bullet\circ\BB^{m+2}=a^\bullet\circ\BB^\bullet\circ\BB^{m+3}=
a^\bullet\circ(\BB\,\BB)\circ\BB^{m+1}=\BB\circ a^\bullet\circ\BB^{m+1}=\BB\circ(\BB\,a)\circ\BB^n=(\BB\,a)\circ\BB^{n+1}$.

* $(a\circ b)^\bullet\circ\BB^{l+1}=b^\bullet\circ(\BB\,a)^\bullet\circ\BB^{l+2}=
= (\BB\,a)\circ b^\bullet\circ\BB^{m+1}
= (\BB\,a)\circ(\BB\,b)\circ\BB^n
= (\BB\,(a\circ b))\circ\BB^n$.

* Immediate.

* If $a\colon m\rightarrow 1$, then
$(a\,\II)^\bullet\circ \BB^m=\II^\bullet\circ a^\bullet\circ\BB^{m+1}=\II^\bullet\circ(\BB\,a)\circ\BB=a\circ\II^\bullet\circ\BB=a\circ\II=a$.
Conversely, if $a=(a\,\II)^\bullet\circ\BB^m$, $a\colon m\rightarrow 1$ because $(a\,\II)^\bullet\colon m\rightarrow m+1$ and $\BB^m\colon m+1\rightarrow 1$.

From Lemma <ref> and <ref> and discussions on PRO in Section <ref> we have:

Given an extensional $\BIdot$-algebra $\calA$, the following data determine a PRO $\IA$.

* $\IA(m,n)=\{a\in\calA~|~a\colon m\rightarrow n\}$.

* For $a\colon l\rightarrow m$ and $b\colon m\rightarrow n$, $a;b=a\circ b\colon l\rightarrow n$.

* $\id_m=\II\colon m\rightarrow m$.

* For $a\colon m\rightarrow n$, $l+a=\BB^l\,a\colon l+m\rightarrow l+n$.

* For $a\colon m\rightarrow n$, $a+l=a\colon m+l\rightarrow n+l$.

Note the asymmetry between $n+(\_)$ and $(\_)+n$; the former is given by applying $\BB$ $n$-times, while the latter
we do not need to do anything because of the extensionality.
To help with the intuition, it might be useful to look at the case of the closed term model of the $\lambda_{\beta\eta}$-calculus
where we have,
for $a=\lambda fx_1\dots x_m.f\,M_1\dots M_n\colon m\rightarrow n$,

\begin{array}{rll}
{\red 1\,+\,}a
\lambda f{\red x_0}x_1\dots x_m.f\,{\red x_0}\,M_1\dots M_n\\
(\lambda fxy.f\,(x\,y))\,(\lambda fx_1\dots x_m.f\,M_1\dots M_n)\\
\\
a{\red \,+\,1}
\lambda fx_1\dots x_m{\red x_{m+1}}.f\,M_1\dots M_n\,{\red x_{m+1}}\\
\lambda fx_1\dots x_m.f\,M_1\dots M_n\\
\end{array}

This difference between left-tensor and right-tensor in internal PROs cannot be ignored even
in the braided or symmetric cases. In particular,
we will later discuss left traces on internal PROBs which are much easier to describe than right traces because of this asymmetry.

Another possible source of confusion would be that $\BB$ plays multiple important roles in this story: it gives the composition $a\circ b=\BB\,a\,b$,
the left-tensor $1+a=\BB\,a$, as well as an element of arity $2\rightarrow1$ serving as the application.
This complexity is already present in the calculus of $\BB$ studied by Ikebuchi and Nakano <cit.>.

$\IA$ defined as above is reflexive, with $\mathsf{app}=\BB\colon 2\rightarrow 1$
and $\mathsf{cur}(a)=(a\,\II)^\bullet\circ\BB^m\colon m\rightarrow 1$ for $a\colon m+1\rightarrow 1$.
Moreover, $\IA(0,1)=\{a\in\calA~|~a\colon 0\rightarrow 1\}=\{a^\bullet~|~a\in\calA\}=\calA^\bullet$ has a $\BIdot$-algebra structure
with $a\cdot_{\calA^\bullet} b=b\circ a\circ \BB$, $\BB_{\calA^\bullet}=\BB^\bullet$,
$\II_{\calA^\bullet}=\II^\bullet$, and $a^{\bullet_{\calA^\bullet}}=a^\bullet$.
This $\BIdot$-algebra is isomorphic to $\calA$, with isomorphisms $a\mapsto a^\bullet\colon \calA\stackrel{\cong}{\rightarrow}\calA^\bullet$ and
$a\mapsto a\,\II\colon \calA^\bullet\stackrel{\cong}{\rightarrow}\calA$.

Every extensional $\BIdot$-algebra is isomorphic to one arising from a reflexive object in a monoidal category.

A pleasant consequence of having the internal PRO is that we can use the string diagrams of monoidal categories for expressing and
reasoning about combinators with arity. This makes the lengthy and dry equational reasoning on combinators
much easier and more accessible. Let us draw

for $\BB\colon 2\rightarrow 1$ and

for $a^\bullet\colon 0\rightarrow 1$.
For example, the arity axioms can be drawn (keeping in mind that adding a lower wire amounts to applying $\BB$ while nothing to do for adding an upper wire)
as follows.

Thus they have very natural graphical meaning, from which it is immediate to see that $\calA^\bullet$ forms a $\BIdot$-algebra.

It is natural to ask if every reflexive PRO arises as the internal PRO of an extensional $\BIdot$-algebra.
The answer is no; a simple counterexample is as follows.

Let $\mathbb{C}$ be the PRO
such that $\mathbb{C}(0,0)=\{0,1\}$ and $\mathbb{C}(m,n)=\{0\}$ for $m+n>0$,
with composition and tensor of $f$ and $g$ given by the multiplication
$f\cdot g$, and $\id_0=1$ while $\id_m=0$ for $m>0$. Thus $\mathbb{C}$ is trivial except $\mathbb{C}(0,0)$. It is reflexive
as $\mathbb{C}(m+1,1)=\calC(m,1)=\{0\}$.
$\calA=\mathbb{C}(0,1)$ is the trivial $\BIdot$-algebra, and its
internal PRO $\IA$ is the trivial PRO ($\IA(m,n)=\{0\}$ for any $m$ and $n$).
(In this example, $\mathbb{C}(0,0)$ can be replaced by any commutative monoid with an absorbing element $0$. Hence there are infinitely many reflexive PROs giving rise to the trivial $\BIdot$-algebra.)

§.§ Adding braids and symmetry

We have seen that, for an extensional $\BIdot$-algebra $\calA$, $\IA$ is a reflexive PRO. Now suppose that
$\IA$ has a braid, i.e., it is a reflexive PROB. Following the discussion on PROBs
(Section <ref>), we need
elements $\CC^+$ and $\CC^-$ which are of arity $2\rightarrow 2$ and satisfy the Coxter relations

\begin{array}{rcll}
\CC^\pm\circ\CC^\mp &=& \BB\,(\BB\,\II)\\
(\BB\,\CC^\pm)\circ\CC^\pm\circ(\BB\,\CC^\pm) &=& \CC^\pm\circ(\BB\,\CC^\pm)\circ\CC^\pm
\end{array}

such that the
family of elements $\bsigma_{m,n}\colon m+n\rightarrow n+m$ given by

\begin{array}{rclrcl}
\bsigma_{0,1} &=& \II & \hspace{5mm}
\bsigma_{m+1,1} &=&
(\BB\,\bsigma_{m,1})\circ\CC^+ \\
\bsigma_{m,0} &=& \II &
\bsigma_{m,n+1} &=&
\bsigma_{m,1}\circ(\BB\,\bsigma_{m,n}).
\end{array}

is natural in $m$ and $n$. It turns out that naturality follows from just the following instances:

\begin{array}{rcll}
(1+\BB)\circ\bsigma_{1,1}^{\pm1} &=& \bsigma_{1,2}^{\pm1}\circ (\BB+1) \\
(1+a^\bullet)\circ\bsigma_{1,1}^{\pm1} &=& a^\bullet+1
\end{array}

or equivalently

\begin{array}{rcll}
(\BB\,\BB)\circ\CC^\pm &=& \CC^\pm\circ(\BB\,\CC^\pm)\circ\BB \\
(\BB\,a^\bullet)\circ\CC^\pm &=& a^\bullet
\end{array}

By drawing

for $\CC~+$ and $\CC^-$ respectively,
these naturality with respect to $\BB$ and $a^\bullet$ can be depicted as follows.

(37.5,50)(0,0)$\CC^+\circ (\BB\,\CC^+)\circ\BB$

(37.5,50)(0,0)$\CC^-\circ (\BB\,\CC^-)\circ\BB$

Note the naturality with respect to $a^\bullet$ implies $\CC^\pm\,a\,b\,c=a\,c\,b$ as well as $\CC^\pm\,\II\,a=a^\bullet$
and more generally $\CC^\pm\,b\,a=a^\bullet\circ b$.
So it is possible to axiomatise algebras with braid without using $(\_)^\bullet$ as a primitive construct.
The equation $a^\bullet\circ\BB^{m+1}=(\BB\,a)\circ\BB^n$ for characterising the arity $m\rightarrow n$
(Definition <ref>) can be
replaced by

in the braided setting. As a result, we obtain extensional $\BCpmI$-algebras <cit.>:

An extensional $\BCpmI$-algebra is an applicative structure
with elements $\BB$, $\CC^+$, $\CC^-$ and $\II$ satisfying the following axioms.

\begin{array}{rcll}
\BB\,a\,b\,c &=& a\,(b\,c) & (B)\\
\CC^\star\,a\,b\,c &=& a\,c\,b & (C)\\
\II\,a &=& a & (I)\\
\CC^+\,a\,b &=& \CC^-\,a\,b & (C2)\\
\BB\,\II &=& \II  & (\lambda)\\
\CC^\star\,\BB\,\II &=& \BB\,\II & (\rho)\\
(\CC^\star\,\BB\,\BB)\circ(\BB\circ\BB) &=& (\BB\,\BB)\circ\BB  & (\alpha)\\
\CC^\pm\circ\CC^\mp &=& \BB\,(\BB\,\II) & (\cox_1)\\
(\CC^\star\,\BB\,\CC^\pm)\circ(\BB\circ\BB) &=& (\BB\,\CC^\pm)\circ(\BB\circ\BB)  & (\cox_2)\\
(\BB\,\CC^\pm)\circ(\CC^\pm\circ(\BB\,\CC^\pm)) &=&
\CC^\pm\circ((\BB\,\CC^\pm)\circ\CC^\pm) & (\cox_3)~~~\\
(\BB\,\BB)\circ\CC^\pm &=& \CC^\pm\circ((\BB\,\CC^\pm)\circ\BB) &(bc)\\
\end{array}

The double signs $\pm$ and $\mp$ in an equation should be taken
as appropriately linked, while $\star$ indicates an arbitrary choice of $+$ or $-$.
(As we have $(C2)$, assuming just an instance of $\star$ suffices.)

Suppose that $A$ is a reflexive object in a braided monoidal category $\mathbb{C}$.
Then $\mathbb{C}(I,A)$ is an extensional $\BCpmI$-algebra with (in addition to the constructs from Proposition <ref>)

$$\CC^\pm=\mathsf{cur}(\mathsf{cur}(\mathsf{cur}((A\otimes\sigma_{A,A}^{\pm1});(\mathsf{app}\otimes A);\mathsf{app}))).$$

For an extensional $\BCpmI$-algebra $\calA$, its internal PRO $\IA$ is braided (i.e., a PROB) with the braid $\bsigma$.
$\IA$ is reflexive, and $\IA(0,1)=\calA^\bullet$ forms an extensional $\BCpmI$-algebra
which is isomorphic to $\calA$.

The most non-trivial point is the naturality of $\bsigma$. Naturality with respect to elements of arity $m\rightarrow 1$ easily follows from that with respect to $\BB$ and $a^\bullet$
as they can be expressed as $a^\bullet\circ\BB^m$ for some $a$. Naturality for general $h\colon m\rightarrow n$
is reduced to that w.r.t. $(\BB\,h)\circ\BB^n\colon m+1\rightarrow 1$.

Every extensional $\BCpmI$-algebra is isomorphic to one arising from a reflexive object in a braided monoidal category.

Similarly, we can characterise extensional $\BCI$-algebras as extensional $\BCpmI$-algebras in which $\CC^+$ agrees with $\CC^-$.
For the resulting axiomatisation, we refer to <cit.>. The internal PRO $\IA$
of an extensional $\BCI$-algebra $\calA$ is symmetric (i.e., a PROP),
and its reflexive object $1$ induces an extensional $\BCI$-algebra $\calA^\bullet$  which is isomorphic to $\calA$.

§.§ Adding twists

Now we shall add a twist to the internal PROB $\IA$ of an extensional $\BCpmI$-algebra $\calA$
following the discussions on balanced PROB in Section <ref>.

An extensional $\BCpmI$-algebra is balanced
when it has elements $\btheta^+$ and $\btheta^-$ satisfying
the following axioms.

\begin{array}{rcll}
(\BB\,\btheta^\pm)\circ\BB &=& (\CC^\star\,\BB\,\btheta^\pm)\circ\BB &
\btheta^\pm\circ\btheta^\mp &=& \BB\,\II & (\theta_2)\\
\CC^\star\,\btheta^\star\,a&=& \CC^\star\,\II\,a & (\theta_3)\\
\BB\circ\btheta^\pm &=&
\btheta^\pm\circ\CC^\pm\circ\btheta^\pm\circ\CC^\pm\circ\BB & (\theta_4)\\
\end{array}

$(\theta_1)$ says $\btheta^+$ and $\btheta^-$ are of arity $1\rightarrow 1$.
$(\theta_2)$ says $\btheta^+$ and $\btheta^-$ are inverse to each other.
$(\theta_3)$ implies $a^\bullet\circ\btheta^\pm=a^\bullet$
(naturality of the twist for $a^\bullet$).
It also implies
$(\theta_4)$ is the naturality of the twist for $\BB$.
By drawing

for $\btheta^+$ and $\btheta^-$, $(\theta_4)$ is depicted as follows.

Suppose that $A$ is a reflexive object in a balanced monoidal category $\mathbb{C}$.
Then $\mathbb{C}(I,A)$ is a balanced extensional $\BCpmI$-algebra with (in addition to the constructs from Prop. <ref> and <ref>)

Note that an extensional $\BCI$-algebra is an extensional balanced
with $\CC^+=\CC^-$ and $\btheta^+=\btheta^-=\II$.

Similarly to the case of braids, the naturality of $\btheta^\pm$ for $\BB$ and $a^\bullet$ is sufficient to
ensure the naturality of the induced twist. Thus the internal PROB is balanced:

The internal PROB of a balanced extensional $\BCpmI$-algebra
is balanced with the twist $\btheta_m\colon m\rightarrow m$ determined by
$\btheta_0=\II$, $\btheta_1=\btheta^+$ and

Every balanced extensional $\BCpmI$-algebra is isomorphic to one arising from a reflexive object in a balanced monoidal category.

§ RIBBON CATEGORIES WITH A REFLEXIVE OBJECT

Starting with combinatory algebras which give rise to reflexive PROs, we have enriched our algebras with braids
and twists.
The next step is to add trace and/or duality. But before doing that, it is useful to look at the situation from the categorical side.
Specifically, we consider ribbon categories with a reflexive object and figure out what the combinatory algebra arising from the
reflexive object looks like. Most interestingly, we will see that these combinatory algebras have an element whose application
sends elements of arity $1+m\rightarrow 1+n$ to its (left) trace of arity $m\rightarrow n$.

§.§ Reflexive objects in ribbon categories

Suppose that $A$ is an object of a ribbon category $\mathbb{C}$
with an isomorphism
$\varphi\colon A\otimes A^*\stackrel{\cong}{\rightarrow} A$,
i.e., $A$ is a reflexive object.
Define $\app\colon A\otimes A\rightarrow A$ and
$\lam\colon A\rightarrow A\otimes A$ by

\app~=~
A\otimes A\xrightarrow{\varphi^{-1}\otimes A}
A\otimes A^*\otimes A \xrightarrow{A\otimes\varepsilon}

\begin{array}{rcl}
\lam
A\otimes A\otimes A^* \xrightarrow{A\otimes A\otimes\theta^{-1}}
A\otimes A\otimes A^*
\xrightarrow{A\otimes\sigma^{-1}}
A\otimes A^*\otimes A \xrightarrow{\varphi\otimes A}
A\otimes A
\\
A\otimes A\otimes A^* \xrightarrow{A\otimes A\otimes\theta}
A\otimes A\otimes A^*
\xrightarrow{A\otimes\sigma}
A\otimes A^*\otimes A \xrightarrow{\varphi\otimes A}
A\otimes A
\end{array}

Using $\lam$ and trace, we can express the currying

\mathsf{cur}(f)=\mathit{Tr}^A_{X,A}(f;\lam)
=(X\otimes \eta_A);(f\otimes A^*);\varphi
\colon X\rightarrow A $$

for $f\colon X\otimes A\rightarrow A$.

The following equations hold.

* The $\beta$-equality:
$(\lam\otimes A);(A\otimes\sigma_{A,A}^{-1});(\app\otimes A)
=A\otimes\theta_A^{-1}\colon A\rightarrow A.$

* The $\eta$-equality:
$\mathit{Tr}^A_{A,A}(\app;\lam)=\mathit{id}_A\colon A\rightarrow A.$

The $\beta$-equality above corresponds to the $\beta$-rule of the trivalent graph representation of lambda terms
mentioned in the introduction.
Note that the usual $\beta\eta$-equalities

(\mathsf{cur}(f)\otimes A);\app=f
\hspace{8pt}(f\colon X\otimes A\rightarrow A)

\mathsf{cur}((g\otimes A);\app)=g
\hspace{8pt}(g\colon X\rightarrow A)

easily follow from Lemma <ref>.
A useful reformulation of the $\beta$-equality of Lemma <ref> is

For $f\colon A\otimes B\rightarrow A\otimes C$,

(\lam\otimes B);(A\otimes f);(\app\otimes C)=A\otimes\mathit{Tr}_L^A(f)\colon A\otimes B\rightarrow A\otimes C

where the left trace ${\mathit{Tr}_L}^X_{B,C}\colon \mathbb{C}(X\otimes B,X\otimes C)\rightarrow\mathbb{C}(B,C)$
is given by ${\mathit{Tr}_L}^X_{B,C}(f)=\mathit{Tr}^X_{B,C}( \sigma_{X,B}^{-1};f;\sigma_{C,X})$.

By letting $f$ be $\sigma^{-1}_{A,A}$ in Proposition <ref>, we recover the $\beta$-equality of
Lemma <ref>.
Proposition <ref> will be useful for defining the trace combinator below.
As an iterated version of this, we have:

For $f\colon A^{\otimes m}\otimes B\rightarrow A^{\otimes m}\otimes C$,

(\lam_m\otimes B);(A\otimes f);(\app_m\otimes C)=A\otimes\mathit{Tr}_L^{A^{\otimes m}}(f)\colon A\otimes B\rightarrow A\otimes C

where $\lam_m\colon A\rightarrow A^{\otimes (m+1)}$ is defined
by $\lam_0=\mathit{id}_A$ and $\lam_{m+1}=\lam_m;(\lam\otimes A^{\otimes m})$,
and $\app_n\colon A^{\otimes{n+1}}\rightarrow A$ by
$\app_0=\mathit{id}_A$ and $\app_{n+1}=(\app\otimes A^{\otimes n});\app_n$.

Remark on the trivial loop on a reflexive object.

$$\bigcirc=\mathit{Tr}^A(\mathit{id}_A)\colon I\rightarrow I$$

which we may call
the trivial loop on $A$ (or the dimension of $A$).
In general, $\bigcirc$ may not agree with $\id_I$ — for example, the PRO in Example <ref> is
actually compact closed, in which $\bigcirc=0$ while $\id_I=1$.
Since we assumed $A\otimes A^*\cong A$, (by noting that $X^{**}\cong X$ and $(X\otimes Y)^*\cong Y^*\otimes X^*$ hold in ribbon categories)
we have $A\cong A^*\cong A\otimes A$.
Explicitly, the isomorphism between $A$ and $A\otimes A$ can be
given as follows.

\mathit{Tr}^A_{A.A\otimes A}((A\otimes\lam);(\app\otimes\lam))
\colon A\rightarrow A\otimes A$$

\mathit{Tr}^A_{A\otimes A,A}((\lam\otimes\app);(A\otimes\app))
\colon A\otimes A\rightarrow A$$

From this, we have
\mathit{Tr}^A(\mathit{id}_A)
=\mathit{Tr}^{A\otimes A}(p^{-1};p)
=\mathit{Tr}^{A\otimes A}(\mathit{id}_{A\otimes A})
=\mathit{Tr}^A(\mathit{id}_A)\otimes \mathit{Tr}^A(\mathit{id}_A)
Thus the trivial loop $\bigcirc$ is idempotent
($\bigcirc=\bigcirc\otimes\bigcirc=\bigcirc;\bigcirc$) and
it does not make sense to count the number of
occurrences of $\bigcirc$. In Section <ref>, $\bigcirc$ will play an important role.

Duality on reflexive objects
In the sequel, we will write $\mathbb{C}|_A$ for the monoidal full subcategory of $\mathbb{C}$ whose objects are
tensor products of $A$. Since $A^*\cong A$, $\mathbb{C}|_A$ itself is a ribbon category.
The dual of $A$ is $A$ itself with unit and counit given by

\alpha=\mathit{Tr}^A_{I,A\otimes A}(\lam;(A\otimes\lam))\colon I\rightarrow A\otimes A

\beta=\mathit{Tr}^A_{A\otimes A,I}((A\otimes\app);\app)\colon A\otimes A\rightarrow I

804012040 1207014070

Then we have $(\alpha\otimes\id_A);(\id_A\otimes\beta)=(\id_A\otimes\alpha);(\beta\otimes \id_A)=\mathit{id}_A$.
The observation below is useful for simplifying calculation on duality:

The following equations hold.

\alpha=\alpha;(\id_A\otimes\theta^{\pm1}_A);\sigma^{\pm1}_{A,A}=\alpha;(\theta^{\pm1}_A\otimes\id_A);\sigma^{\pm1}_{A,A}

\beta=
\sigma^{\pm1}_{A,A};(\id_A\otimes\theta^{\pm1}_A);\beta=
\sigma^{\pm1}_{A,A};(\theta^{\pm1}_A\otimes\id_A);\beta

In particular, in the symmetric (i.e., compact closed) case, $\alpha=\alpha;\sigma_{A,A}$
and $\beta=\sigma_{A,A};\beta$ hold.

For the first equation

, see below:

The first step is by sliding and vanishing, and the second by tightening, superposing and yanking of the trace <cit.>. Other cases are similar.

§.§ The balanced extensional -algebra on a reflexive object

Let $\calA=\mathbb{C}(I,A)$ and define
the application $(\_)\cdot(\_)\colon \calA^2\rightarrow\calA$
by $f\cdot g = (f\otimes g);\app$.
Thanks to Prop. <ref>, we know that $\calA$ is a balanced extensional $\BCpmI$-algebra.
Spelling out its detail, we have:

$(\calA,\cdot)$ is a balanced extensional $\BCpmI$-algebra
with $\BB,\CC^+,\CC^-,\II,\btheta^+$ and $\btheta^-$ given in Figure <ref>.

In Figure <ref>, $F$ denotes the strict monoidal functor from  $\mathbb{C}|_A$ to the internal PROB $\IA$
$f\colon A^{\otimes m}\rightarrow A^{\otimes n}$
(emphasised with the greyed area in Figure <ref>)

\mathit{Tr}^A_{I,A}
\left(
A^{\otimes (m+1)}\xrightarrow{\!\lam\otimes f\!}
A^{\otimes (n+2)}\xrightarrow{\!A\otimes \app_n\!}
A\otimes A
\right)

of $\IA(m,n)$.
For instance, $f\colon A\otimes A\rightarrow A\otimes A$ is sent to

406010060 1206018060
804010040 1204014040

of $\IA(2,2)$. For $\sigma_{A,A}\colon A\otimes A\rightarrow A\otimes A$,
we have $F(\sigma_{A,A})=\CC^+\in\IA(2,2)$.
Similarly, $F(\sigma_{A,A}^{-1})=\CC^-\in\IA(2,2)$, $F(\app)=\BB\in\IA(2,1)$,
$F(a)=a^\bullet=\mathit{Tr}^A((\lam\otimes a);\app)\in\IA(0,1)$
for $a\colon I\rightarrow A$.
We shall note that these
can be seen as a reconstruction of the trivalent graph representations of combinators in <cit.>
in ribbon categories.

On the other hand, $F(\lam)\in\IA(1,2)$ does not correspond to any conventional combinator used in combinatory logic. This is the trace combinator to be discussed below.

(20,30)(0,0)$a\cdot b=(a\otimes b);\app$

(90,40)(0,0)$\BB=F(\app)\colon 2\rightarrow1$

804010040 1205014050

(20,20)(0,0)$\II=F(\mathit{id}_I)\colon 0\rightarrow0$

(20,40)(0,0)$\CC^+=F(\sigma_{A,A})\colon 2\rightarrow2$

406010060 1206018060
804010040 1204014040

(20,40)(0,0)$\CC^-=F(\sigma^{-1}_{A,A})\colon 2\rightarrow2$

406010060 1206018060
804010040 1204014040

(20,40)(0,0)$a^\bullet=F(a)\colon 0\rightarrow1$

(20,40)(0,0)$\btheta^+=F(\theta)\colon 0\rightarrow1$

(20,40)(0,0)$\btheta^-=F(\theta^{-1})\colon 0\rightarrow1$

(20,40)(0,0)$\Tr=F(\lam)\colon 1\rightarrow2$

(25,50)(0,0)$\balpha=F(\alpha)\colon 0\rightarrow2$

(25,50)(0,0)${\boldsymbol\beta}=F(\beta)\colon 2\rightarrow 0$

804012040 1207014070

[The ribbon combinatory algebra $\calA=\mathbb{C}(I,A)$]The ribbon combinatory algebra $\calA=\mathbb{C}(I,A)$
The ribbon combinatory algebra $\calA=\mathbb{C}(I,A)$

§.§ Combinators for duality and trace

Figure <ref> contains additional ingredients: $\balpha=F(\alpha)$, $\bbeta=F(\beta)$ and $\Tr=F(\lam)$.
Since $\alpha\colon I\rightarrow A\otimes A$ and $\beta\colon A\otimes A\rightarrow I$ form a duality in $\mathbb{C}|_A$ and
$F\colon \mathbb{C}|_A\rightarrow\IA$ strictly preserves the balanced monoidal structure,
$\balpha=F(\alpha)$ and $\bbeta=F(\beta)$ form a duality in $\IA$. So it is not surprising to see:

The internal PROB $\IA$ is a ribbon category with duality $\balpha\colon 0\rightarrow2$ and $\bbeta\colon 2\rightarrow0$.

Being a ribbon category, $\IA$ also has a unique trace <cit.>.
For $f\colon 1+m\rightarrow 1+n$, its left trace ${\mathit{Tr}_L}^1_{m,n}(f)\colon m\rightarrow n$ is $\balpha\circ(\BB\,f)\circ\bbeta$.
Thanks to combinatory completeness, this is equal to $(\lambda^* f.\balpha\circ(\BB\,f)\circ\bbeta)\,f=

\begin{array}{rcl}
\bbeta^\bullet\,(\BB\,(\BB\,\balpha\,(\BB\,f)))\\
\BB\,(\BB\,\balpha\,(\BB\,f))\,\bbeta\\
\balpha\circ(\BB\,f)\circ\bbeta.
\end{array}

Fortunately, this combinator $\bbeta^\bullet\circ\BB\circ(\BB\,\balpha)\circ\BB$ can be simplified as follows.

$\bbeta^\bullet\circ\BB\circ(\BB\,\balpha)\circ\BB= F(\lam)$ holds.

The left-hand side is, by unfolding the definition of each combinator, equal to
F((F(\beta)\otimes A);\app;(A\otimes\alpha);(\app\otimes A)).

\arraycolsep=3pt
\begin{array}{cll}
(F(\beta)\otimes A);\app;(A\otimes\alpha);(\app\otimes A)\\
(\mathsf{cur}(\lam;(\lam\otimes A);(A\otimes\beta))\otimes A);\app;(A\otimes\alpha);(\app\otimes A)\\
\lam;(\lam\otimes A);(A\otimes\beta);(A\otimes\alpha);(\app\otimes A)\\
\lam;(A\otimes{\mathit{Tr}_L}^1_{2,2}(\beta;\alpha))\\
\lam
\end{array}

by Lemma <ref> and Proposition <ref>.

Thus we have:

Let $\Tr\in\IA(1,2)$ be $F(\lam)$.
Then, for $a\in\IA(1+m,1+n)$, $\Tr\cdot a={\mathit{Tr}_L}^1_{m,n}(a)\in\IA(m,n)$ holds.

So the left trace allows a particularly simple description: just the application of $\Tr$.
On the other hand, we also have the right trace on $\IA$, which however is harder to describe because of the
asymmetry of the left-tensor and right-tensor in internal PROBs.

Somewhat surprisingly, we can recover the duality $\balpha$ and $\bbeta$ from the trace combinator $\Tr$ as
$\alpha$ and $\beta$ are defined by $\app$, $\lam$ and trace on $\mathbb{C}$.
We will discuss this for general balanced extensional $\BCpmI$-algebras in the next section.

§ RIBBON COMBINATORY ALGEBRAS

A traced extensional $\BCpmI$-algebra is a
balanced extensional $\BCpmI$-algebra with an element $\Tr$ satisfying the following axioms.

\begin{array}{rcll}
(\CC^\star\,\BB\,\Tr)\circ\BB &=& (\BB\,\Tr)\circ\BB^2 \!\!\!\!\!& \mathrm{(Left~ Tightening)}\\
(\BB\,\Tr)\circ(\CC^\star\,\BB\,\BB)\circ\BB &=& \BB\circ\Tr & \mathrm{(Right~ Tightening)}\!\!\\
\Tr\,\CC^\pm &=& \btheta^\pm
& \mathrm{(Yanking)}
\\
\!\!\Tr^2\circ(\CC^\star\,\BB\,\CC^-)\circ(\BB\,\CC^+) &=& \Tr^2 & \mathrm{(Exchange)}\\
\end{array}

(Left Tightening),
saying that $\Tr$ is of arity $1\rightarrow 2$, implies

a\circ(\Tr\,f)=((\CC^\star\,\BB\,\Tr)\circ\BB)\,a\,f=((\BB\,\Tr)\circ\BB^2)\,a\,f=\Tr\,((\BB\,a)\circ f).

Similarly, (Right Tightening) says

\Tr\,(f\circ(\BB\,b))=((\BB\,\Tr)\circ(\CC^\star\,\BB\,\BB)\circ\BB)\,f\,b = (\BB\circ\Tr)\,f\,b=(\Tr\,f)\circ b.

Thus they imply
$\Tr\,((\BB\,a)\circ f\circ (\BB\,b))=a\circ (\Tr\,f)\circ b$.

(Yanking) would not need any explanation. In the symmetric case, it is simply $\Tr\,\CC=\BB\,\II$.
Finally, (Exchange) says

$$\Tr\,(\Tr\,(\CC^+\circ f\circ \CC^-))=(\Tr^2\circ(\CC^\star\,\BB\,\CC^-)\circ(\BB\,\CC^+))\,f%=\Tr^2\,f

which is motivated by the axiomatisation of trace in <cit.>. We have

For a traced balanced extensional $\BCpmI$-algebra $\calA$, its internal PROB $\IA$
is a traced balanced monoidal category.

In fact, we will see that $\IA$ is not only traced but also ribbon.
First, we shall define the notion of duality on combinatory algebras:

A duality in an extensional $\BIdot$-algebra is a pair of elements $\balpha$ and $\bbeta$ satisfying
the following axioms.

\begin{array}{rcll}%\hline
\balpha^\bullet\circ\BB &=& (\BB\,\balpha)\circ\BB^2 & (\mathrm{Arity}_\alpha)\\
\bbeta^\bullet\circ\BB^3 &=& \BB\,\bbeta & (\mathrm{Arity}_\beta)\\
\balpha\circ(\BB\,\bbeta) &=& \BB\,\II & (\mathrm{Duality}_1)\\
(\BB\,\balpha)\circ\bbeta &=& \BB\,\II & (\mathrm{Duality}_2)\\
\end{array}

A ribbon extensional $\BCpmI$-algebra is a balanced extensional
$\BCpmI$-algebra with a duality satisfying the following axiom.

\begin{array}{rcll}
\balpha\circ\btheta^\pm &=& \balpha\circ(\BB\,\btheta^\pm) & (\mathrm{Duality}_\theta)
\end{array}

The axiom $(\mathrm{Arity}_\alpha)$ says $\balpha$ is of arity $0\rightarrow2$, while
$(\mathrm{Arity}_\beta)$ says $\bbeta$ is of arity $2\rightarrow0$.
$(\mathrm{Duality}_1)$ and $(\mathrm{Duality}_2)$
state they form a duality.
Finally, $(\mathrm{Duality}_\theta)$ ensures $\theta^*=\theta$ required for ribbon categories.

For a ribbon extensional $\BCpmI$-algebra $\calA$, its internal PROB $\IA$
is a ribbon category.

As we already observed for reflexive objects in ribbon categories, we can derive duality from the trace.
The key insight is that the trace combinator $\Tr$ can be used not only for defining trace but also
as the morphism $\lam\colon A\rightarrow A\otimes A$ in the previous section,
and the lambda-node (7,5)[c]$\lamnode$ in the trivalent graph representation in the introduction.

a traced balanced extensional $\BCpmI$-algebra has a duality given by

\begin{array}{rclcl}
\balpha &=&\Tr\,(\Tr\circ(\BB\,\Tr)\circ(\BB\,\CC^+)\circ\CC^+)&\colon &0\rightarrow2\\
\bbeta &=&\Tr\,(\CC^+\circ(\BB\,\CC^+)\circ(\BB\,\BB)\circ\BB)&\colon &2\rightarrow0
\end{array}

On the other hand, a ribbon extensional $\BCpmI$-algebra is traced with $\Tr=(\CC^+\,\BB\,\bbeta)\circ(\BB\,\balpha)\circ\BB$.
Thus we have:

A balanced extensional $\BCpmI$-algebra is traced if and only if it is ribbon.

In the sequel, by a ribbon combinatory algebra we mean a traced balanced extensional $\BCpmI$-algebra, or equivalently a
ribbon extensional $\BCpmI$-algebra.

We describe a ribbon combinatory algebra of infinite binary trees labelled by the elements of a group, which was originally
given as a model of the braided lambda calculus <cit.> in the ribbon category of crossed $G$-sets <cit.>. Fix a group $G=(G,\cdot,e,(\_)^{-1})$ and let
$\mathcal{D}=\{f\colon \{\mathsf{c},\mathsf{d}\}^*\rightarrow G~|~f(w)=f(\mathsf{c}w)\cdot f(\mathsf{d}w)^{-1}\}$.
Define $\multimap\colon \mathcal{D}^2\rightarrow \mathcal{D}$ by
$(f_1\imp f_2)(\varepsilon)=f_2(\varepsilon)\cdot f_1(\varepsilon)^{-1}$,
$(f_1\imp f_2)(\mathsf{d}w)=f_1(w)$ and
$(f_1\imp f_2)(\mathsf{c}w)=f_2(w)$.
There is a $G$-action $\bullet\colon G\times\mathcal{D}\rightarrow\mathcal{D}$ given by
$(g\bullet f)(w)=g\cdot f(w)\cdot g^{-1}$,
and a map $|\_|\colon \mathcal{D}\rightarrow G$ defined by $|f|=f(\varepsilon)$.
We say a subset $a$ of $\mathcal{D}$ is equivariant if, for any $f\in a$ and $g\in G$, $|f|=e$ and $g\bullet f\in a$ hold.
Let $\mathcal{A}$ be the set of equivariant subsets.
$\mathcal{A}$ is a ribbon combinatory algebra with

\begin{array}{lcl}
a\,b &=& \{y~|~\exists x~(x\imp y)\in a\,\&\, x\in b\}\\
\BB &=& \{(y\imp z)\imp((x\imp y)\imp(x\imp z))~|~x,y,z\in\mathcal{D}\}\\
\CC^+ &=& \{((|x|\bullet y)\imp (x\imp z))\imp(x\imp(y\imp z))~|~x,y,z\in\mathcal{D}\}\\
\CC^- &=& \{(y\imp ((|y|^{-1}\!\bullet x)\imp z))\imp(x\imp(y\imp z))~|~x,y,z\in\mathcal{D}\}\\
\II &=& \{x\imp x~|~x\in\mathcal{D}\}\\
\btheta^+ &=& \{((|x|\bullet x)\imp y)\imp(x\imp y)~|~x,y\in\mathcal{D}\}\\
\btheta^- &=& \{((|x|^{-1}\!\bullet x)\imp y)\imp(x\imp y)~|~x,y\in\mathcal{D}\}\\
\Tr &=& \{((x\imp y)\imp(x\imp z))\imp(y\imp z)~|~x,y,z\in\mathcal{D}\}\\
\end{array}

When $G$ is abelian, $\mathcal{A}$ is symmetric because $g\bullet f=f$ for any $g\in G$.

We conclude this section by showing that a ribbon combinatory algebra is symmetric (i.e., $\CC^+=\CC^-$ and $\btheta^+=\btheta^-=\II$)
iff $\btheta^+=\II$. Thus having a non-trivial twist is essential.

A ribbon combinatory algebra is symmetric whenever $\btheta^+=\II$ holds.

$\mathbf{p}=\Tr\circ(\BB\,\bbeta)\colon 2\rightarrow 1$ has an inverse $\mathbf{p}^{-1}=(\BB\,\balpha)\circ\BB\colon 1\rightarrow 2$.
The naturality of the twist implies $\mathbf{p}\circ\btheta_2=\btheta_1\circ\mathbf{p}$. On the other hand, $\btheta^+=\II$
implies $\btheta_2=\CC^+\circ\CC^+$ and $\btheta_1=\II$. Hence $\CC^+\circ\CC^+=\II$
by pre-composing $\mathbf{p}^{-1}$, and we have $\CC^+=\CC^-$.

§ RIBBON COMBINATORY ALGEBRAS VS RIBBON CATEGORIES

From the results of the previous sections, we have:

Every ribbon combinatory algebra is isomorphic to the one arising from a reflexive object in the ribbon category obtained as the internal PROB.

However, not every reflexive ribbon PROB arises as an internal PROB.
In general, given a ribbon category $\mathbb{C}$ with a reflexive object $A$, the internal PROB $\IA$ of the ribbon combinatory algebra
$\calA=\mathbb{C}(I,A)$ is not isomorphic to the ribbon PROB $\mathbb{C}|_A$, as the simple counterexample of Example <ref> shows.
Nevertheless, the presence of the structure-preserving functor $F\colon \mathbb{C}|_A\rightarrow\IA$ suggests
they are closely related; we shall look at this situation in more detail.

§.§ Almost full

We show that $F$ is almost full: the map $\mathbb{C}|_A(A^{\otimes m},A^{\otimes n})\rightarrow\IA(m,n)$ on morphisms
is surjective
except in the case of $m=n=0$.

First, the following partial result with codomain $1$ is easily derivable;
it is obtained essentially as a corollary to the equivalence between closed operads and extensional combinatory algebras
(which was stated as an adjunction <cit.> but later turned out to be an equivalence <cit.>).

For any $a\colon m\rightarrow 1$ in $\IA$, there exists  $f\colon A^{\otimes m}\rightarrow A$
in $\bbCA$ such that $a=Ff$ holds.

By Lemma <ref> (6),
any $a\colon m\rightarrow 1$ is equal to
$b^\bullet\circ\BB^m$ where $b=a\,\II\in\calA$. Let $f=(b\otimes A^{\otimes m});\app_m$. As $F(\app_m)=\BB^m$, we have
$Ff=Fb\circ F(\app_m)= b^\bullet\circ \BB^m=a$.

This result extends to the cases with non-zero domain or codomain:

For any $a\colon m\rightarrow 1+n$ in $\IA$, there exists  $f\colon A^{\otimes m}\rightarrow A^{\otimes (1+n)}$
in $\mathbb{C}|_A$ such that $a=Ff$ holds.

Let $f$ be

A^{\otimes m}\xrightarrow{(a\,\bbeta_n)\otimes A^{\otimes m}\otimes\alpha_n}
A^{\otimes (1+m+2n)}\xrightarrow{\app_{m+n}\otimes A^{\otimes n}}
A^{\otimes (1+ n)}

where $\alpha_n\colon I\rightarrow A^{\otimes(2n)}$ is defined by
$\alpha_1=\alpha$ and $\alpha_{n+1}=\alpha;(A\otimes\alpha_n\otimes A)$.
Similarly define $\beta_n\colon A^{\otimes(2n)}\rightarrow I$, and
let $\balpha_n=F\alpha_n\colon 0\rightarrow 2n$ and $\bbeta_n=F\beta_n\colon 2n\rightarrow 0$.
Then $F((a\bbeta_n)\otimes A^{\otimes m}\otimes\alpha_n)$ is equal to

F(A^{\otimes m}\otimes\alpha_n)\circ F((a\bbeta_n)\otimes A^{\otimes(m+2n)})

while $F(\app_{m+n}\otimes A^{\otimes n})=\BB^{m+n}$,
and we have

\begin{array}{rcll}
\\
(\BB^m\,\balpha_n)\circ\bbeta_n^\bullet\circ a^\bullet\circ\BB^{1+m+n}
\\
(\BB^m\,\balpha_n)\circ\bbeta_n^\bullet\circ (\BB\,a)\circ\BB^{1+2n}
& (a\colon m\rightarrow n+1)
\\
(\BB^m\,\balpha_n)\circ a\circ\bbeta_n^\bullet\circ\BB^{1+2n}
& (\bbeta_n^\bullet\colon 0\rightarrow1)
\\
& (a\colon m\rightarrow n+1)
\\
a\circ(\BB^{n+1}\,\balpha_n)\circ (\BB\,\bbeta_n)
& (\bbeta_n\colon 2n\rightarrow 0)
\\
& \!\!\!\!\!((\BB u)\circ(\BB v)=\BB\,(u\circ v))
\\
& ((\BB^n\,\balpha_n)\circ\bbeta_n=\II)
\\
\end{array}

$a\colon m+1\rightarrow 0$ in $\IA$, there exists  $f\colon A^{\otimes (m+1)}\rightarrow I$
in $\bbCA$ such that $a=Ff$ holds.

$b=((\BB^m\,\balpha)\circ a)\,\II= (\BB^m\,\balpha)\,(a\,\II)$ and
$f=(b\otimes A^{\otimes{m+1}});\app_m;\beta$.
$Ff=b^\bullet\circ\BB^m\circ\bbeta=(\BB^m\,\balpha)\circ a\circ\bbeta=
(\BB^m\balpha)\circ(\BB^{m+1}\bbeta)\circ a =
(\BB^m\,(\balpha\circ\BB\,\bbeta))\circ a = a.

So just the case of $0\rightarrow0$ remains.
This seemingly harmless case turns out to be surprisingly difficult:

For any $a\colon 0\rightarrow 0$ in $\IA$,
there exists
$f\colon I\rightarrow I$ in $\bbCA$ such that
$\bigcirc; a=Ff$ holds, where $\bigcirc=\mathit{Tr}^A(\mathit{id}_A)\colon I\rightarrow I$.

Let $f=\mathit{Tr}^A((a\otimes A);\app)\colon I\rightarrow I$.
Since $a\colon 0\rightarrow 0$, $a^\bullet\circ\BB=\BB\,a$ holds. This implies

$$(A\otimes a\otimes A);(A\otimes\app);\app=(a\otimes\app);\app\colon A\otimes A\rightarrow A$$

in $\bbCA$. By pre-composing $\lam\colon A\rightarrow A\otimes A$ to both sides of the equation and by applying Proposition <ref>, we have

$$A\otimes(\mathit{Tr}^A((a\otimes A);\app)=((a\otimes A);\app)\otimes(\mathit{Tr}^A(\id_A))\colon A\rightarrow A.$$

Hence $A\otimes f=((a\otimes A);\app)\otimes\bigcirc\colon A\rightarrow A$ holds.
By currying this, we have
$\mathsf{cur}(A\otimes f)=\mathsf{cur}(((a\otimes A);\app)\otimes\bigcirc)$.
The left-hand side is $Ff$, while the right-hand side is $\bigcirc;a$.

Therefore the idempotent element $\bigcirc$ is the obstacle in showing fullness,
and we only have the following partial result:

Suppose $\bigcirc=
\mathit{id}_I$.
Then $F$ is full.

§.§ Almost faithful

For $a\colon m\rightarrow n$, let $\overline{a}\colon A^{\otimes(m+1)}\rightarrow  A^{\otimes(n+1)}$

(\lam_n\otimes\theta_{A^{\otimes m}}^2);
(a\otimes\theta^{-1}_A\otimes A^{\otimes(n+ m)});
(\app\otimes \sigma^{-1}_{A^{\otimes m},A^{\otimes n}});
(\mathit{Tr}^A((A\otimes(\sigma^{-1}_{A,A^{\otimes m}};\sigma^{-1}_{A^{\otimes m},A}));(\app_m\otimes A);\sigma_{A,A})\otimes A^{\otimes n})

We show that $\overline{(\_)}$ serves as an "almost" inverse to $F$:

For any $f\colon A^{\otimes m}\rightarrow A^{\otimes n}$, $\overline{F(f)}=A\otimes f$ holds.

From Proposition <ref>, we can derive

\mathit{Tr}^A((A\otimes\lam_m);(\sigma^{-1}_{A,A});(A\otimes\app_n))
\colon A\rightarrow A

Using Corollary <ref> we have

Hence $\overline{F(f)}$ is equal to

By applying Corollary <ref> again and by some simplification,
this turns out to be equal to $A\otimes f$.

The map $\mathbb{C}|_A(A^{\otimes m},A^{\otimes n})\rightarrow\IA(m,n)$ on morphisms is bijective whenever $m\not=0$ or $n\not=0$.

Consider $f,g\colon A^{\otimes m}\rightarrow A^{\otimes n}$ with $m\not=0$ and assume $F(f)=F(g)$. Then
$A\otimes f=\overline{F(f)}=\overline{F(g)}=A\otimes g$, and
$f=(\theta_A^{-1}\otimes A^{m-1});\mathit{Tr}_L((\sigma_{A,A}\otimes A^{m-1});(A\otimes f))=
(\theta_A^{-1}\otimes A^{m-1});\mathit{Tr}_L((\sigma_{A,A}\otimes A^{m-1});(A\otimes g))=g$.
The case of $n\not=0$ is similar.

So again the case of $0\rightarrow0$ is the obstacle. Proposition <ref> implies

If the functor $A\otimes(\_)\colon \mathbb{C}|_A\rightarrow\mathbb{C}|_A$ is faithful,  $F$ is faithful.

When $\bigcirc=\mathit{Tr}^A(\mathit{id}_A)=\mathit{id}_I$,
$A\otimes(-)$ is faithful, as $A\otimes f=A\otimes g$ implies
f=\bigcirc\otimes f=\mathit{Tr}_L(A\otimes f)=\mathit{Tr}_L(A\otimes g)=\bigcirc\otimes g=g.
Hence we have, by Proposition <ref>
and <ref>,

Suppose $\bigcirc=\mathit{id}_I$.
Then $F$ is full and faithful, and gives an equivalence between
$\mathbb{C}|_A$ and $\IA$.

We do not know if $\bigcirc=\mathit{id}_I$ is a necessary condition for the equivalence.

§ RELATED WORK

§.§ Curry's Combinatory Logic

In 1931, Curry <cit.>
introduced the notion of order and degree for regular combinators, which are combinators corresponding to closed lambda terms of the form
$\lambda fx_1\dots x_m.f\,M_1\,\dots\,M_n$
with no lambda abstraction nor $f$ in $M_i$'s.
In his terminology, such a combinator is of order $m$ and degree $n$;
it is of arity $m\rightarrow n$ in our context.
In <cit.>, Curry has shown that a regular combinator $U$ is of order $m$ and degree $n$ if and only if it satisfies

which agrees with the definition of the arity $m\rightarrow n$
(Definition <ref>)

and also the characterisation

in Section <ref>,
because $\CC\,a\,b=b^\bullet\circ a$ holds in extensional $\BCI$-algebras.
Curry also has shown items 1 to 5 of Lemma <ref> for
regular combinators, thus he was aware of the compositional nature of the
arity (order and degree). Moreover, he has given an axiomatisation of combinatory logic <cit.>,
reproduced in Figure <ref> (except the standard axioms $\BB\,a\,b\,c=a\,(b\,c)$, $\CC\,a\,b\,c=a\,c\,b$, $\WW\,a\,b=a\,b\,b$ and $\KK\,a\,b=a$;
$\II$ was $\WW\,\KK$ in <cit.>),
which is very close to Hasegawa's axioms
of extensional $\mathbf{BCIWK}$-algebras in <cit.>.
The commutative axioms state the arity  $\BB\colon 2\rightarrow1$, $\CC\colon 2\rightarrow2$, $\WW\colon 1\rightarrow2$, $\KK\colon 1\rightarrow0$ and
$\II\colon 0\rightarrow0$. Axioms $\mathit(CC)_{1,2}$ are the Coxter relations of $\CC$, and $\mathit(BC)$,$\mathit(CW)$ and $\mathit{(CK)}$
are the naturality of $\CC$ with respect to $\BB$, $\WW$ and $\KK$.
$\mathit(WC)$, $\mathit(WW)$ and $\mathit(WK)$ say $(1,\WW,\KK)$ forms a commutative co-monoid, and
$\BB$ is a co-monoid homomorphism by $\mathit(BW)$ and $\mathit(BK)$.

\begin{array}{rcll}
\multicolumn{4}{l}{Commutative~Axioms~(Kommutative~Axiome)}\\
\CC\,(\BB^3)\,\BB &=& (\BB\,\BB)\circ\BB & (\mathit{Ax.~B.})\\
\CC\,(\BB^3)\,\CC &=& (\BB\,\CC)\circ\BB^2 & (\mathit{Ax.~C.})\\
\CC\,(\BB^2)\,\WW &=& (\BB\,\WW)\circ\BB^2 & (\mathit{Ax.~W.})\\
\CC\,(\BB^2)\,\KK &=& (\BB\,\KK)\circ\II & (\mathit{Ax.~K.})\\
\CC\,\BB\,\II &=& (\BB\,\II)\circ\II & (\mathit{Ax.~I.})\\
\multicolumn{4}{l}{Transmutative~Axioms~(Transmutative~Axiome)}\\
\BB\circ\CC &=& (\BB\,\CC)\circ\CC\circ(\BB\,\BB) & (\mathit{Ax.~(BC).})\\
\BB\circ\WW &=&
\multicolumn{2}{l}{(\BB\,\WW)\circ\WW\circ(\BB\,\CC)\circ(\BB^2\,\BB)\circ\BB}
\\
&&& (\mathit{Ax.~(BW).})\\
\BB\circ\KK &=& \KK\circ\KK & (\mathit{Ax.~(BK).})\\
\CC\circ\CC &=& \BB^2\,\II & (\mathit{Ax.~(CC)_1.})\\
(\BB\,\CC)\circ\CC\circ(\BB\,\CC) &=& \CC\circ(\BB\,\CC)\circ\CC & (\mathit{Ax.~(CC)_2.})\\
\CC\circ\WW &=& (\BB\,\WW)\circ\CC\circ(\BB\,\CC) & (\mathit{Ax.~(CW).})\\
\CC\circ\KK &=& \BB\,\KK & (\mathit{Ax.~(CK).})\\
\WW\circ\CC &=& \WW & (\mathit{Ax.~(WC).})\\
\WW\circ\WW &=& \WW\circ(\BB\,\WW) & (\mathit{Ax.~(WW).})\\
\WW\circ\KK &=& \BB\,\II & (\mathit{Ax.~(WK).})\\
\multicolumn{4}{l}{Other~Axiom~(Andere~Axiome)}\\
\BB\,\II &=& \II & (\mathit{Ax.~I_2.})
\end{array}

[Curry's axioms of combinatory logic]Curry's axioms of combinatory logic
Curry's axioms of combinatory logic

For instance, $\mathit(BW)$ can be depicted as follows (with $\WW=$

In a sense, Curry identified the PROP of regular combinators —
long before monoidal categories were invented.
It seems
that, throughout his early work on combinatory logic <cit.>, Curry had certain geometric intuition,
which we believe was not far from the string diagrams of internal PROs.
However, non-regular combinators such as $a^\bullet=\CC\,\II\,a=\lambda f.f\,a\colon 0\rightarrow1$ were not included in Curry's
study, and this is the crucial difference from Hasegawa's approach.

Unfortunately, Curry never used these notions of order and degree in his later work
(except the book <cit.> which contains slightly different definitions of order and degree used for unrelated purposes),
and we are not aware of any subsequent work developing Curry's early ideas further.

§.§ Semantics of lambda calculi and operads

Our work is closely related to Hyland's approach using semi-closed operads
as semantic models of the $\lambda_\beta$-calculus <cit.>,
though its emphasis was more on algebraic theory rather than geometric reading.
Hasegawa's approach using closed operads <cit.> is largely the same as ours using reflexive PROs;
the only difference is that <cit.> focuses on the internal operad $\IA(\_,1)$ rather than whole of the internal PRO $\IA$.
We looked at PROs more seriously because they are more suitable for studying trace and duality.
Although we considered only the extensional case in this paper, Hasegawa <cit.> recently generalised his approach to the non-extensional case,
which can be applied to ribbon combinatory algebras.

§.§ Knot theory and semantics

Classical results on braids <cit.> and quantum topology <cit.> are of great importance in our approach.
Also, studies on knotted graphs <cit.> are relevant to our study. For instance, as noted in <cit.>,
the Reidemeister Move IV for trivalent graphs

corresponds to the naturality of the braid with respect to $\BB\colon 2\rightarrow1$
(depicted in Sec. <ref>).

A braided version of relational semantics is developed in <cit.> using results from quantum topology,
from which the ribbon combinatory algebra in Example <ref> is derived.

§ SUMMARY AND FUTURE WORK

We have seen that a reflexive object in a ribbon category gives rise to
a ribbon combinatory algebra,
whose internal PROB is a ribbon category which is almost equivalent to
the appropriate subcategory of the original ribbon category.

This situation can be summarised as follows:

(100,43)(0,0)take the internal PROB
(100,17)(0,0)take the elements of $1$

where a reflexive ribbon PROB means a PROB $\mathbb{C}$
which is a ribbon category and $1$ is reflexive ($\mathbb{C}((\_)+1,1)\cong\mathbb{C}(-,1)$).

One might expect that this would form an equivalence of categories. However,
while $\IA(0,1)=\calA^\bullet\cong\calA$ holds for
a ribbon combinatory algebra $\calA$,  there is a nasty gap
between $\mathbb{C}$ and $\mathcal{I}_{\mathbb{C}(0,1)}$ for a ribbon PROB $\mathbb{C}$ as the functor
$F\colon \mathbb{C}\rightarrow\mathcal{I}_{\mathbb{C}(0,1)}$ does not have to give an equivalence. Nevertheless,
under a mild condition $\bigcirc=\mathit{id}_I$, $F$ indeed gives an equivalence
(Theorem <ref>).

We have given an axiomatisation of ribbon combinatory algebras in terms of the trace combinator $\Tr$, and shown that it is equivalent to
another axiomatisation using the combinators $\balpha$ and $\bbeta$ for the duality.
Thus, in the untyped (reflexive) extensional setting, to give a trace combinator is
to give a ribbon structure.

Future work
We have studied combinatory algebras whose internal
PROB (PROP) is ribbon (compact closed when symmetric).
A related question is
to characterise combinatory algebras whose internal PROB (PROP) is traced
(but not necessarily ribbon or compact closed).
For example, let $\mathbb{D}$ be a cartesian closed category with
a Conway fixed-point operator and a reflexive object $D$ — there are plenty of such cases found in domain theory, and a Conway operator
determines a trace <cit.>.
The global elements of $D$
form an extensional $\BCI$-algebra (in fact an extensional $\mathbf{SK}$-algebra). Its internal PROP is a cartesian category with a Conway operator, hence traced; but it is not compact closed.

Another important question is to give finer examples of ribbon combinatory algebras. The crossed $G$-set models
(Example <ref>) give ribbon combinatory algebras with non-trivial braids and twists, but they do not provide
interesting invariants of tangles. We expect to obtain better examples by applying techniques from knot theory.

For instance, the recent work relating knots and links to Thompson's group $F$ <cit.> might be relevant, as $F$ is the group of automorphisms on an object $A$  with an isomorphism
$A\otimes A\cong A$ in a monoidal category <cit.>.

The first author is supported by
keyJSPS KAKENHIurl
Grant No. key21K11753 and
The second author is supported by
hasuoJST ERATO HASUO Metamathematics for Systems Design Projecturl
(No. hasuoJPMJER1603).

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

authorpersonE. Artin. year1925.
Theorie der Zöpfe.
journalAbh. Math. Sem. Univ. Hamburg  volume4 (year1925), pages47–72.

authorpersonH.P. Barendregt. year1985.
booktitleThe Lambda Calculus - its Syntax and Semantics. seriesStudies in Logic and the Foundations of Mathematics, Vol. volume103.
publisherNorth-Holland, addressAmsterdam.

authorpersonH.B. Curry. year1930a.
Grundlagen der Kombinatorischen Logik, Tail I.
journalAmerican Journal of Mathematics volume52, number3 (year1930), pages509–536.

authorpersonH.B. Curry. year1930b.
Grundlagen der Kombinatorischen Logik, Tail II.
journalAmerican Journal of Mathematics volume52, number4 (year1930), pages789–834.

authorpersonH.B. Curry. year1931.
The universal quantifier in combinatory logic.
journalAnnals of Mathematics volume32, number1 (year1931), pages154–180.

authorpersonH.B. Curry. year2016.
booktitleFoundations of Combinatory Logic/Grundlagen der kombinatorischen Logik.
publisherCollege Publications, addressLondon.
English translation of <cit.> by F. Kamareddine and J.P. Seldin.

[Curry and Feys(1958)]
authorpersonH.B. Curry and personR. Feys. year1958.
booktitleCombinatory Logic. Vol. I.
publisherNorth-Holland, addressAmsterdam.

[Fiore and Leinster(2010)]
authorpersonM. Fiore and personT. Leinster. year2010.
An abstract characterization of Thompson's group $F$.
journalSemigroup Forum volume80, number2 (year2010), pages325–340.

authorpersonJ.-Y. Girard. year1987.
Linear logic.
journalTheoret. Comput. Sci. volume50, number1 (year1987), pages1–101.

[Haghverdi and Scott(2011)]
authorpersonE. Haghverdi and personP. Scott. year2011.
Geometry of interaction and the dynamics of proof reduction: a tutorial.
In booktitleNew Structures for Physics. seriesLecture Notes in Phys., Vol. volume813. publisherSpringer, addressHeidelberg, pages357–417.

authorpersonM. Hasegawa. year1999.
booktitleModels of Sharing Graphs: a Categorical Semantics of let and letrec.
publisherSpringer-Verlag, addressLondon.

authorpersonM. Hasegawa. year2009.
On traced monoidal closed categories.
journalMathematical Structures in Computer Science volume19, number2 (year2009), pages217–244.

authorpersonM. Hasegawa. year2012.
A quantum double construction in Rel.
journalMathematical Structures in Computer Science volume22, number4 (year2012), pages618–650.

authorpersonM. Hasegawa. year2021.
A braided lambda calculus. In booktitleProc. 2nd Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA 2020) (seriesElectronic Proceedings in Theoretical Computer Science, Vol. volume353). publisherOpen Publishing Association, addressWaterloo, pages94–108.

authorpersonM. Hasegawa. year2023a.
The internal operads of combinatory algebras. In booktitleProc. 38th International Conference on Mathematical Foundations of Programming Semantics (MFPS XXXVIII) (seriesElectronic Notes in Theoretical Informatics and Computer Science, Vol. volume1). publisherINRIA, addressLe Chesnay.

authorpersonM. Hasegawa. year2023b.
titlePlanar lambda algebras and semi-closed operads.

<https://www.kurims.kyoto-u.ac.jp/ hassei/papers/>

[Hindley and Seldin(2008)]
authorpersonJ.R. Hindley and personJ.P. Seldin. year2008.
booktitleLambda-Calculus and Combinators, an Introduction.
publisherCambridge University Press, addressCambridge.

authorpersonJ.M.E. Hyland. year2017.
Classical lambda calculus in modern dress.
journalMath. Structures Comput. Sci.  volume27 (year2017), pages762–781.

[Ikebuchi and Nakano(2020)]
authorpersonM. Ikebuchi and personK. Nakano. year2020.
On properties of B-terms.
journalLogical Methods in Computer Science volume16, number2 (year2020), pagesno. 8.

authorpersonV.F.R. Jones. year2017.
Some unitary representations of Thompson's groups $F$ and $T$.
journalJ. Comb. Algebra volume1, number1 (year2017), pages1–44.

authorpersonV.F.R. Jones. year2019.
On the construction of knots and links from Thompson's groups.
In booktitleKnots, Low-Dimensional Topology and Applications. seriesSpringer Proc. Math. Stat., Vol. volume284. publisherSpringer, addressCham, pages43–66.

[Joyal and Street(1991)]
authorpersonA. Joyal and personR. Street. year1991.
The geometry of tensor calculus, I.
journalAdvances in Mathematics volume88, number1 (year1991), pages55–112.

[Joyal and Street(1993)]
authorpersonA. Joyal and personR. Street. year1993.
Braided tensor categories.
journalAdv. Math. volume102, number1 (year1993), pages20–78.

[Joyal et al(1996)]
authorpersonA. Joyal, personR. Street, and personD. Verity. year1996.
Traced monoidal categories.
journalMath. Proc. Cambridge Phils. Soc.  volume119 (year1996), pages447–468.

[Kassel and Turaev(2008)]
authorpersonC. Kassel and personV.G. Turaev. year2008.
booktitleBraid Groups. seriesGraduate Texts in Mathematics, Vol. volume247.
publisherSpringer-Verlag, addressNew York.

authorpersonL.H. Kauffman. year1989.
Invariants of graphs in three-space.
journalTransactions of the American Mathematical Society volume311, number2 (year1989), pages697–710.

[Kelly and Laplaza(1980)]
authorpersonG.M. Kelly and personM.L. Laplaza. year1980.
Coherence for compact closed categories.
journalJ. Pure Appl. Algebra  volume19 (year1980), pages193–213.

authorpersonA. Kitaev. year2003.
Fault-tolerant quantum computation by anyons.
journalAnnals of Physics  volume303 (year2003), pages3–20.

[Lambek and Scott(1986)]
authorpersonJ. Lambek and personP.J. Scott. year1986.
booktitleIntroduction to Higher Order Categorical Logic. seriesCambridge Studies in Advanced Mathematics, Vol. volume7.
publisherCambridge University Press, addressCambridge.

authorpersonS. Mac Lane. year1971.
booktitleCategories for the Working Mathematician. seriesGraduate Texts in Mathematics, Vol. volume5.
publisherSpringer, addressNew York.

authorpersonD. Plump. year1999.
Term graph rewriting.
In booktitleHandbook of Graph Grammars and Computing by Graph Transformation Vol. 2, Applications, Languages and Tools. publisherWorld Scientific, addressRiver Edge, NJ, pages3–61.

authorpersonD.S. Scott. year1980.
Relating theories of the $\lambda $-calculus.
In booktitleTo H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. publisherAcademic Press, addressLondon-New York, pages403–450.

authorpersonP. Selinger. year2002.
The lambda calculus is algebraic.
journalJournal of Functional Programming  volume12 (year2002), pages549–566.

authorpersonP. Selinger. year2011.
A survey of graphical languages for monoidal categories.
In booktitleNew Structures for Physics. seriesLecture Notes in Phys., Vol. volume813. publisherSpringer, addressHeidelberg, pages289–355.

authorpersonM.C. Shum. year1994.
Tortile tensor categories.
journalJournal of Pure and Applied Algebra volume93, number1 (year1994), pages57–110.

authorpersonH. Tomita. year2021.
Realizability without symmetry. In booktitleProceedings of the 29th EACSL Annual Conference on Computer Science Logic (CSL2021) (seriesLIPIcs, Vol. volume183). publisherSchloss Dagstuhl – Leibniz-Zentrum für Informatik, addressWadern, pages38:1–38:16.

authorpersonV.G. Turaev. year1994.
booktitleQuantum Invariants of Knots and 3-Manifolds. seriesStudies in Mathematics, Vol. volume18.
publisherDe Gruyter, addressBerlin.

authorpersonZ. Wang. year2010.
booktitleTopological Quantum Computation. seriesCBMS Regional Conference Series in Mathematics, Vol. volume112.
publisherAmerican Mathematical Society, addressProvidence, RI.

authorpersonD.N. Yetter. year1989.
Category theoretic representations of knotted graphs in ${\bf S}^3$.
journalAdvances in Mathematics volume77, number2 (year1989), pages137–155.

authorpersonD.N. Yetter. year2001.
booktitleFunctorial Knot Theory. seriesSeries on Knots and Everything, Vol. volume26.
publisherWorld Scientific, addressRiver Edge, NJ.

authorpersonN. Zeilberger. year2016.
Linear lambda terms as invariants of rooted trivalent maps.
journalJ. Funct. Programming  volume26 (year2016), pagese21.

authorpersonN. Zeilberger. year2018.
A theory of linear typings as flows on 3-valent graphs. In booktitleProc. the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS2018). publisherACM, addressNew York, pages919–928.

[Zeilberger and Giorgetti(2015)]
authorpersonN. Zeilberger and personA. Giorgetti. year2015.
A correspondence between rooted planar maps and normal planar lambda terms.
journalLog. Methods Comput. Sci. volume11, number3 (year2015), pages1–39.

get arXiv to do 4 passes: Label(s) may have changed. Rerun