# Coherence by Normalization for Linear Multicategorical Structures

Federico Olimpieri

###### Abstract

We establish a formal correspondence between resource calculi an appropriate
linear multicategories. We consider the cases of (symmetric) representable,
symmetric closed and autonomous multicategories. For all these structures, we
prove that morphisms of the corresponding free constructions can be presented
by means of typed resource terms, up to a reduction relation and a structural
equivalence. Thanks to the linearity of the calculi, we can prove strong
normalization of the reduction by combinatorial methods, defining appropriate
decreasing measures. From this, we achieve a general coherence result:
morphisms that live in the free multicategorical structures are the same
whenever the normal forms of the associated terms are equal. As further
application, we obtain syntactic proofs of Mac Lane’s coherence theorems for
(symmetric) monoidal categories.

##  1 Introduction

The basis of the celebrated _Curry-Howard-Lambek correspondence_ is that
logical systems, typed $\lambda$-calculi and appropriate categorical
constructions are different presentations of the same mathematical structure.
An important consequence of the correspondence is that we can give
_syntactical presentations_ of categories, that can be exploited to prove
general results by means of elementary methods, such as induction. At the same
time, we can use categorical methods to obtain a more modular and clean design
of programming languages. The classic example is given by simply typed
$\lambda$-calculi and cartesian closed categories [20]. The idea is well-
known: morphisms in free cartesian closed categories over sets are identified
with equivalence classes of $\lambda$-terms up to $\beta\eta$-equality.
Another important setting is the _linear_ one, where we consider _monoidal_
categories instead of cartesian ones. In this case, _linear logic_ [10] enters
the scene: symmetric monoidal closed categories correspond to _linear_
$\lambda$-calculi. Computationally, this is a huge restriction, since linear
terms can neither copy nor delete their inputs during computation. A
refinement of this picture can be obtained by switching from categories to
_multicategories_ [19]. These structures were indeed first introduced by
Lambek to achieve a categorical framework formally closer to typed
calculi/proof systems. Morphisms of multicategories can have multiple sources
$f:a_{1},\dots,a_{n}\to a$, recalling the structure of a _type judgment_
$x_{1}:a_{1},\dots,x_{n}:a_{n}\vdash f:a.$

We are interested in establishing a Curry-Howard-Lambek style correspondence
for appropriate linear multicategories and then employ it to obtain _coherence
results_. When we deal with complex structures such as tensor products, it
becomes crucial to have a _decision process_ to establish whether two arrows
are equal. This is called a _coherence_ problem. The main example is Mac
Lane’s original result [22], which states that _all structural diagrams_ in
monoidal categories commute. If one considers more complex structures, the
class of commutative diagrams is normally more restrictive. In the case of
closed monoidal categories, Kelly and Mac Lane [16] associated _graphs_ to
structural morphisms, obtaining the following coherence result: two structural
arrows between appropriate objects111A restriction on the type of morphisms is
needed due to the presence of the monoidal unit. are equal whenever their
graph is the same. We aim to achieve coherence results for linear
multicategories, building on Lambek’s and Mints [26] intuition that coherence
problems can be rephrased in the language of proof theory and obtained by
exploiting appropriate notions of _normalization_ for proofs/terms [19]. We do
so by establishing a formal connection between _resource_ calculi and _linear_
multicategorical structures.

#### Main Results

We study free multicategorical constructions for (symmetric) representable and
closed structures. Representability consists of the multicategorical monoidal
structure [11]. We prove that free linear multicategories built on appropriate
signatures can be presented by means of typed resource calculi, where
morphisms correspond to equivalence classes of terms up to a certain
equivalence. We handle the tensor product via _pattern-matching_ , presented
as a syntactic _explicit substitution_. The definition of our type systems is
given in _natural deduction_ style: we have introduction and elimination rules
for each type constructor. Our work is conceptually inspired by an ‘ _adjoint
functors_ point-of-view’. A basic fact of the classic Curry-Howard-Lambek
correspondence is that $\beta\eta$-equality can be expressed by means of the
_unit_ ($\eta$) and the _counit_ ($\beta$) of the adjunction between products
and arrow types. We generalize this observation to the multicategorical
setting, thus introducing an appropriate reduction relation that corresponds
to the representable structure. Indeed, a fundamental aspect of our work
consists of the in depth study of resource terms rewriting. We introduce
confluent and strongly normalizing reductions, that express the appropriate
equalities. In order to do so, we exploit _action-at-distance_ to define our
operational semantics, that has proven to be a successful approach to calculi
with explicit substitution [17, 1, 2]. An important feature of this approach
is to distinguish the operational semantics, defined by action-at-distance,
from a notion of _structural equivalence_ , that deals with commutations of
explicit substitution with the other syntactic constructors. This approach
overcomes the classic difficulties of rewriting systems with explicit
substitution, allowing us to obtain confluence and strong normalization in an
elegant way. In this way, we get a general _coherence result_ : two structural
morphisms of linear multicategories are equal whenever the _normal forms_ of
their associated terms are equal. In the context of (symmetric) representable
multicategories, we apply this result to obtain a _syntactic proof_ of
stronger coherence theorems, that can be seen as multicategorical versions of
the classic MacLane coherence theorems for (symmetric) monoidal categories
[22]. The coherence theorem for representable multicategories was already
proved in [11]. We give an alternative type-theoretic proof for it. To our
knowledge, the other coherence results that we present are new. Moreover,
exploiting the equivalence between monoidal categories and representable
multicategories established by Hermida [11], we are able to obtain the
original Mac Lane’s results as corollaries of our coherence theorems.

#### Related Work

Building on Lambek’s original ideas, several researchers have advocated the
use of multicategories to model computational structures. Hyland [13] proposed
to rebuild the theory of pure $\lambda$-calculus by means of _cartesian
operads_ , that is one-object cartesian multicategories. The idea of seeing
resource calculi as multicategories was first employed by Mazza _et al._ [24,
23]. We build on their approach, showing that these calculi correspond to
appropriate _universal constructions_ , namely free linear multicategories.
The first resource calculus has been introduced by Boudol [6]. A similar
construction was also independently considered by Kfoury [18]. Resource terms
have gained special interest thanks to the definition by Ehrhard and Regnier
of the _Taylor expansion_ for $\lambda$-terms [8]. From this perspective, the
resource calculus is a _theory of approximation of programs_ and has been
successfully exploited to study the computational properties of
$\lambda$-terms [3, 32, 24, 28]. Our syntax is very close to the one of
_polyadic calculi_ or _rigid resource calculi_ [24, 31]. We need to extend the
standard operational semantics, adding an $\eta$-reduction and a reduction for
explicit substitution. Our $\eta$-reduction is built from an expansion rule
instead of a contraction, since $\eta$-expansion naturally fits the adjoint
point-of-view, corresponding the the unit of the considered adjunction. In
dealing with the technical rewriting issues, we follow [26, 15, 7], obtaining
a terminating $\eta$-reduction. As already discussed, we handle the explicit
substitution following Accattoli and Kesner methodology [17, 2, 1].

The calculi we present are also strongly related to _intuitionistic linear
logic_ [4]. It is well-known that resource calculi can be seen as fragments of
ILL [24, 23]. While ILL is presented via sequent calculus, we chose a natural
deduction setting, this latter being directly connected to the ‘adjoint
functors’ point-of-view. Accattoli and Kesner approach to explicit
substitution allows us to bypass the cumbersome commutation rules needed for
ILL rewriting. Moreover, resource calculi are closer to the multicategorical
definitions (their constructors being _unbiased_ [21], i.e., $k$-ary). Our
handling of symmetries is also more canonical and explicit. We use the
properties of _shuffle permutations_ , in a way similar to Hasegawa [27] and
Shulman [30], also inspired by our ongoing work on _bicategorical semantics_
[25]. In this way, the type system is _syntax directed_ and we are able to
prove that, given a term, there exists at most one type derivation for it. The
pioneering work of Mints [26] is very close to our perspective. Mints
introduced a linear $\lambda$-calculus to study the coherence problem of
closed category by the means of normalization. We build on that approach,
extending it to several different structures and to the multicategorical
setting.

Shulman’s type theory for (symmetric) monoidal categories [30] does not employ
explicit substitutions, being able to handle tensors in way similar to what
happens with standard product types. Our proposal differs considerably from
Shulman’s, both in purpose and in implementation. While Shulman’s goal is to
start from the categorical structure and define a ‘practical’ type theory to
make computations, ours consists of establishing a formal correspondence
between two _independent_ worlds: resource calculi and linear multicategories
and then employ it to prove results about the categorical structure.

_Graphical approaches_ to monoidal structures [29] have been widely developed.
Particularly interesting for our work are the Kelly-Mac Lane graphs [16], This
approach has been extended via linear logic, thanks to the notion of _proof-
net_ [5, 12]. However, the handling of monoidal units needs extra care from
this perspective, while the terms calculi approach can account for them
without any particular complication.

##  2 Preliminaries

We introduce some concepts, notations and conventions that we will use in the
rest of the paper.

#### Integers, Permutations and Lists

For $n\in\mathbb{N},$ we set $[n]=\\{1,\dots,n\\}$ and we denote by $S_{n}$
the symmetric group of order $n.$ The elements of $S_{n}$ are permutations,
that we identify with bijections $[n]\cong[n].$ Given $\sigma,\tau\in S_{n},$
we denote by $\sigma\circ\tau$ their composition. Given $\sigma\in
S_{n},\tau\in S_{m}$ we denote by $\sigma\oplus\tau:[n+m]\cong[n+m]$ the
evident induced permutation. We now introduce the notion of shuffle
permutation, that is crucial to obtain canonical type derivations for resource
terms with permutations (Proposition 4.2).

######  Definition 2.1 (Shuffles).

Let $n_{1},\dots,n_{k}\in\mathbb{N}$ with $n=\sum_{i=1}^{k}n_{i}.$ A
$(n_{1},\dots,n_{k})$-_shuffle_ is a bijection
$\sigma:\sum_{i=1}^{k}[n_{i}]\cong[n]$ such that the composite
$[n_{i}]\hookrightarrow\sum_{i=1}^{k}[n_{i}]\cong[n]$ is monotone for all
$i\in[k].$ We denote the set of all $(n_{1},\dots,n_{k})$-shuffles as
$\mathsf{shu}(n_{1},\dots,n_{k}).$

The relevant result on shuffles is the following, that induces canonical
decomposition of arbitrary permutations over sums of integers.

######  Lemma 2.2.

Every permutation $\sigma\in S_{\sum_{i=1}^{k}n_{i}}$ can be canonically
decomposed as $\tau_{0}\circ(\bigoplus_{i=1}^{k}\tau_{i})$ with
$\tau_{0}\in\mathsf{shu}(n_{1},\dots,n_{k})$ and $\tau_{i}\in S_{n_{i}}$ for
$i\in[k].$

Given a set $A$ and a list of its elements $\gamma=a_{1},\dots,a_{k}$ and
$\sigma\in S_{k}$ we set
${\gamma}\cdot{\sigma}=a_{\sigma(1)},\dots,a_{\sigma(k)}$ for the symmetric
group right action. We write $\mathsf{len}(\gamma)$ for its length. We denote
the _stabilisers_ for this action as $\mathsf{Stab}(\gamma)=\\{\sigma\in
S_{k}\mid{\gamma}\cdot{\sigma}=\gamma\\}.$ Given lists
$\gamma_{1},\dots,\gamma_{k},$ we set
$\mathsf{shu}(\gamma_{1},\dots,\gamma_{k})=\mathsf{shu}(\mathsf{len}(\gamma_{1}),\dots,\mathsf{len}(\gamma_{k})).$

#### Multicategories

Multicategories constitute the main object of our work. A multicategory is a
multigraph that comes equipped with an appropriate composition operation.

######  Definition 2.3.

A _multigraph_ $\mathcal{G}$ is given by the following data:

  * •

A collection of _nodes_ $\mathcal{G}_{0}\ni a,b,c\dots$

  * •

For every $a_{1},\dots,a_{n},b\in\mathcal{G}_{0},$ a collection of
_multiarrows_ $\mathcal{G}(a_{1},\dots,a_{n};b)\ni s,t,u\dots$

We denote by $\text{arr}(\mathcal{G})$ the set of all multiarrows of
$\mathcal{G}.$

######  Definition 2.4.

A _multicategory_ is a multigraph $\mathcal{G}$ equipped with the following
additional structure:

  * •

A _composition operation_
$-\circ\langle-,\dots,-\rangle:\mathcal{G}(a_{1},\dots,a_{n};b)\times\prod_{i=1}^{n}\mathcal{G}(\gamma_{i},a_{i})\to\mathcal{G}(\gamma_{1},\dots,\gamma_{n};a).$

  * •

_identities_ $id_{a}\in\mathcal{G}(a,a).$

The former data is subjected to evident associativity and identity axioms. We
call _objects_ the nodes of $\mathcal{G}$ and _morphisms_ its multiarrows.

A multicategory can be equipped with structure. We now introduce the notions
of _symmetric_ , _closed_ and _representable_ multicategories.

######  Definition 2.5.

A multicategory $\mathcal{M}$ is _symmetric_ if, for $\sigma\in S_{k}$ we have
a family of bijections
${-}\cdot{\sigma}:\mathcal{M}(\gamma,a_{1},\dots,a_{k};a)\cong\mathcal{M}(\gamma,a_{\sigma(1)},\dots,a_{\sigma(k)};a)$
that satisfies additional axioms [21].

######  Definition 2.6.

A (right) _closed_ structure for a multicategory $\mathcal{M}$ is given by a
family of objects $(a_{1}\otimes\dots\otimes a_{k})\multimap a\in\mathcal{M}$
and arrows
$ev_{a_{1},\dots,a_{k},a}:a_{1},\dots,a_{k},(a_{1}\otimes\dots\otimes
a_{k})\multimap a\to a$ , for $a_{1},\dots,a_{k},a\in\mathcal{M},$ such that
the maps

$ev\circ\langle-,id_{a_{1}},\dots,id_{a_{k}}\rangle:\mathcal{M}(\gamma;(a_{1}\otimes\dots\otimes
a_{k})\multimap a)\to\mathcal{M}(\gamma,a_{1},\dots,a_{k};a)$

induce a bijection, multinatural in $\gamma$ and natural in $a.$ We write
$\lambda(-)$ to denote the inverses to these maps.

######  Definition 2.7.

A _representable_ structure for a multicategory $\mathcal{M}$ is given by a
family of objects $(a_{1}\otimes\dots\otimes a_{k})\in\mathcal{M}$ and arrows
$\mathsf{re}_{a_{1},\dots,a_{k}}:a_{1},\dots,a_{k}\to(a_{1}\otimes\dots\otimes
a_{k})$, for $a_{1},\dots,a_{k}\in\mathcal{M},$ such that he maps

$-\circ\langle
id_{\gamma},\mathsf{re},id_{\delta}\rangle:\mathcal{M}(\gamma,(a_{1}\otimes\dots\otimes
a_{k}),\delta;a)\to\mathcal{M}(\gamma,a_{1},\dots,a_{k},\delta;a)$

induce a bijection, multinatural in $\gamma,\delta$ and natural in $a.$ We
write $\mathsf{let}(-)$ to denote the inverses to these maps.

We use the name _autonomous multicategories_ to denote symmetric representable
closed multicategories. We have categories of representable multicategories
($\mathsf{RepM}$), symmetric representable multicategories ($\mathsf{RepsM}$),
closed multicategories ($\mathsf{ClosedM}$) and autonomous multicategories
($\mathsf{autoM}$), whose morphisms are functors that preserve the structure
on the nose.

#### Signatures

We introduce signatures for the structures we consider.

######  Definition 2.8.

A _representable signature_ is a pair $\langle\mathsf{At},\mathcal{R}\rangle$
where $\mathsf{At}$ is a set of atoms $\mathsf{At}$ and $\mathcal{R}$ is a
multigraph with nodes generated by the following inductive grammar:

$\mathcal{R}_{0}\ni a::=o\in\mathsf{At}\mid(a_{1}\otimes\dots\otimes
a_{k})\qquad(k\in\mathbb{N}).$

######  Definition 2.9.

A _closed signature_ $\mathcal{L}$ is a pair
$\langle\mathsf{At},\mathcal{L}\rangle$ where $\mathsf{At}$ is a set of atoms
$\mathsf{At}$ and $\mathcal{L}$ is a multigraph with with nodes generated by
the following inductive grammar:

$\mathcal{L}_{0}\ni a::=o\in\mathsf{At}\mid(a_{1}\otimes\dots\otimes
a_{k})\multimap a\qquad(k\in\mathbb{N}).$

######  Definition 2.10.

An _autonomous signature_ is a pair $\langle\mathsf{At},\mathcal{H}\rangle$
where $\mathsf{At}$ is a set of atoms $\mathsf{At}$ and $\mathcal{H}$ is a
multigraph with nodes generated by the following inductive grammar:

$\mathcal{H}_{0}\ni a::=o\in\mathsf{At}\mid(a_{1}\otimes\dots\otimes
a_{k})\mid(a_{1}\otimes\dots\otimes a_{k})\multimap a\qquad(k\in\mathbb{N}).$

We shall often identify a signature with its graph. There are categories
$\mathsf{ClosedSig},\mathsf{RepSig}$ and $\mathsf{AutoSig}$ for, respectively,
closed, representable and autonomous signatures. We have forgetful functors
from the categories $\mathsf{ClosedM},\mathsf{RepM}$ and $\mathsf{autoM},$
which we denote by $(\overline{-}).$ One of the main goals of this paper is to
build the left adjoints to those functors via appropriate resource calculi.

#### Monoidal Categories vs Representable Multicategories

In order to transport coherence results from (symmetric) representable
multicategories to ordinary (symmetric) monoidal categories, we shall employ
an equivalence result due to Hermida [11, Theorem 9.8]. Let $\mathsf{Mon}$ be
the category of monoidal categories and lax monoidal functors.

######  Theorem 2.11 ([11]).

There is an equivalence of categories
${\mathsf{RepM}}$${\simeq}$${\mathsf{Mon}.}$$\scriptstyle{\mathsf{rep}(-)}$$\scriptstyle{\mathsf{mon}(-)}$

The representable structure of a monoidal category
$(\mathsf{\mathbb{M}},\otimes_{\mathbb{M}},1)$ is given by
$(a_{1}\otimes_{\mathsf{\mathbb{M}}}\dots\otimes_{\mathsf{\mathbb{M}}}a_{k})=(a_{1})\otimes_{\mathbb{M}}(a_{2}\otimes_{\mathbb{M}}(\dots\otimes_{\mathbb{M}}a_{k})\dots).$
Then composition needs a choice of structural isomorphisms of $\mathbb{M}$ to
be properly defined [11, Definition 9.2]222If we assume Mac Lane’s Coherence
Theorem, the choice is unique. However, we shall not do so, since we are going
to exploit Theorem 2.11 to _transport_ an appropriate coherence theorem on
representable multicategories to ordinary monoidal categories, thus obtaining
the Mac Lane’s result as corollary.. The former equivalence can be extended to
the symmetric case in the natural way.

#### Notations and Conventions

Given a set of terms $A$ and a reduction relation $\to_{\epsilon}\subseteq
A\times A,$ we denote respectively as $\twoheadrightarrow_{\epsilon}$ and
$\to^{\ast}_{\epsilon}$ its transitive closure and its transitive and
reflexive closure. We denote by $=_{\epsilon}\subseteq A\times A$ the smallest
equivalence relation generated by $\to_{\epsilon}.$ For a confluent reduction,
we denote by $\mathsf{nf}(s)_{\epsilon}$ the normal form of $s,$ if it exists.
Given an equivalence relation ${\mathsf{e}}\subseteq{A\times A},$ and $s\in
A,$ we denote by $[s]_{\mathsf{e}}$ the corresponding equivalence class. We
will often drop the annotation and just write $[s].$ We fix a countable set of
variables $\mathcal{V},$ that we will use to define each calculi. Terms are
always considered up to renaming of bound variables. Given terms
$s,t_{1},\dots,t_{k}$ and variables $x_{1},\dots,x_{k}$ we write
$s\\{t_{1},\dots,t_{k}/x_{1},\dots,x_{k}\\}$ to denote capture-avoiding
substitutions. We often use the abbreviation $s\\{\vec{t}/\vec{x}\\}.$ To
define reduction relations, we rely on appropriate notions of _contexts with
one hole_. Given a context with hole $\mathtt{C}$ and a term $s$ we write
$\mathtt{C}[s]$ for the capture-allowing substitution of the holes of
$\mathtt{C}$ by $s$. The _size_ of a term $\mathtt{size}\left(s\right)$ is the
number of syntactic constructors appearing in its body. The calculi we shall
introduce are typed _à la Church_ , but we will constantly keep the typing
implicit, to improve readability. Given $\gamma\vdash s:a$ we write
$\mathtt{C}[\delta\vdash p:b]=s$ meaning that $\mathtt{C}[p]=s$ and the type
derivation of $\gamma\vdash p:b$ contains a subderivation with conclusion
$\delta\vdash p:b.$ Given a typing judgment
$x_{1}:a_{1},\dots,x_{n}:a_{n}\vdash s:a$ we shall consider variables
appearing in the typing context as bound and we will work up to renaming of
those variables. We write ${\pi}\triangleright{\gamma\vdash s:a}$ meaning that
$\pi$ is a type derivation of conclusion $\gamma\vdash s:a.$ For any typing
rule with multiple typing contexts, we assume those contexts to be disjoint.

##  3 A Resource Calculus for Representable Multicategories

We present our calculus for representable multicategories. We begin by
introducing its syntax and typing, then we discuss its operational semantics.
We prove confluence and strong normalization for its reduction. We show that
equivalence classes of terms modulo reduction and a notion of _structural
equivalence_ define the morphisms of free representable multicategories over a
signature. As an application of this result, we give a proof of the coherence
theorem for representable multicategories.

$\displaystyle\prooftree\hypo{f\in\mathcal{R}(a_{1},\dots,a_{n};b)}\hypo{\gamma_{1}\vdash
s_{1}:a_{1}\dots\gamma_{n}\vdash s_{n}:a_{n}}\infer
2{{(\gamma_{1},\dots,\gamma_{n})}\vdash
f(s_{1},\dots,s_{n}):b}\qquad\prooftree\hypo{\gamma_{1}\vdash
s_{1}:a_{1}\dots\gamma_{k}\vdash s_{k}:a_{k}}\infer 1$
$\displaystyle\prooftree\hypo{a\in\mathcal{R}_{0}}\infer 1{x:a\vdash
x:a}\qquad\prooftree\hypo{\gamma\vdash s:(a_{1}\otimes\dots\otimes
a_{k})}\hypo{\delta,x_{1}:a_{1},\dots,x_{k}:a_{k},\delta^{\prime}\vdash
t:b}\infer
2{\delta,\gamma,\delta^{\prime}\vdash{t[x_{1}^{a_{1}},\dots,x_{k}^{a_{k}}:=s]}:b}$

$\displaystyle\mathtt{C}::=[\cdot]\mid\langle
s_{1},\dots,\mathtt{C},\dots,s_{k}\rangle\mid\mathtt{C}[\vec{x}:=t]\mid
s[\vec{x}:=\mathtt{C}]\mid f(s_{1},\dots,\mathtt{C},\dots,s_{k}).$
$\displaystyle\mathtt{E}::=[\cdot]\mid\langle
s_{1},\dots,\mathtt{E},\dots,s_{k}\rangle\mid\mathtt{E}[\vec{x}:=s]\mid
s[\vec{x}:=\mathtt{E}]\quad(\mathtt{E}\neq[\cdot])\mid
f(s_{1},\dots,\mathtt{E},\dots,s_{k}).$
$\displaystyle\mathtt{L}::=[\cdot]\mid\mathtt{L}[\vec{x}:=t].$

Figure 1: Representable Type System on a signature $\mathcal{R}$ and contexts
with one hole. Types are the elements of $\mathcal{R}_{0}.$

#### Representable Terms

Let $\mathcal{R}$ be a representable signature. The _representable resource
terms_ over $\mathcal{R}$ are defined by the following inductive grammar:

$\mathsf{\Lambda_{rep}}(\mathcal{R})\ni s,t::=x\in\mathcal{V}\mid\langle
s_{1},\dots,s_{k}\rangle\mid s[x^{a_{1}}_{1},\dots,x^{a_{k}}_{k}:=t]\mid
f(s_{1},\dots,s_{k})$

for $k\in\mathbb{N}$ and $f\in\text{arr}(\mathcal{R}),a_{i}\in\mathcal{R}.$ A
term of the shape $\langle s_{1},\dots,s_{k}\rangle$ is called a _list_. A
term of the shape $s[x_{1},\dots,x_{k}:=t]$ is called an _(explicit)
substitution_. Variables under the scope of an explicit substitution are
bound. Given a term $s,$ we denote by $\mathsf{ST}(s)$ the set of its
_subterms_ defined in the natural way.

######  Remark 3.1.

Our calculus follows the linear logic tradition of modelling the tensor
product structure by means of a $\mathsf{let}$ constructor [4]. We opted for
the syntactic choice of an explicit substitution $s[x_{1},\dots,x_{k}:=t],$
which stands for the more verbose $\mathsf{let}$ expression, $\mathsf{let}\
\langle x,_{1},\dots,x_{k}\rangle:=t\ \mathsf{in}\ s.$ Terms of the shape
$f(s_{1},\dots,s_{k})$ are needed to capture the multiarrows induced by the
signature $\mathcal{R}.$

Typing and contexts with hole for representable terms is defined in Figure 3.
A context is _atomic_ when it contains just atomic types. We define the
following subset of terms $\mathsf{LT}=\\{\mathtt{L}[\langle
s_{1},\dots,s_{k}\rangle]\mid\text{ for some context }\mathtt{L}\text{ and
terms }s_{i}\\}.$

######  Remark 3.2.

The condition about disjoint contexts grants _linearity_. A term is _linear_
when each variable appears at most once in its body. It is easy to check that,
by construction, all typed terms are linear. Moreover, given $\gamma\vdash
s:a,$ the context $\gamma$ is _relevant_ , meaning that it contains just the
free variables of $s.$

A type of the shape $(a_{1}\otimes\dots\otimes a_{k})$ is called a $k$-ary
_tensor product_. We use a vector notation to refer to arbitrary tensors, eg.,
$\vec{a},\vec{b}\dots$ If $k=0,$ the type $()$ is also called the _unit_. We
set $\mathsf{\Lambda_{rep}}(\mathcal{R})(a_{1},\dots,a_{n};a)=\\{s\mid
x_{1}:a_{1},\dots,x_{n}:a_{n}\vdash_{\mathsf{rep}}s:a\text{ for some
}x_{i}\in\mathsf{fv}(s).\\}.$ We observe that, given a representable term
$\gamma\vdash s:a,$ there exists a unique type derivation for it.

#### Terms Under Reduction

We now introduce the reduction relation for representable terms. This relation
consists of the union of two different subreductions: $\beta$ and $\eta$
reductions, defined in Figure 2. The _structural equivalence_ on terms is
defined as the smallest congruence on terms generated by the rule of Figure 2.
We assume that the context $\mathtt{C}$ does not bind any variable of $t.$

######  Remark 3.3.

Our $\eta$-reduction consists of a restricted version of the standard notion
of $\eta$-expansion, the restriction is needed to achieve strong
normalization. We build on a well-established tradition in term rewriting [26,
15, 7]. Unrestricted $\eta$ is trivially non-terminating. Indeed, for
$x:(a\otimes b)\vdash x:(a\otimes b)$ we have the non-terminating chain
$x\to_{\eta}\langle x,y\rangle[x,y:=z]\to_{\eta}\langle
x,y\rangle[x,y:=\langle v,w\rangle[v,w:=z]]\to_{\eta}\dots$ Hence, we need to
forbid $\eta$-reduction on the right side of a substitution term, that is
exactly what the restricted $\eta$-contexts do. Moreover, there is also a
problem of interaction between $\eta$ and $\beta.$ Consider $s=\langle
x,y\rangle$ well-typed, then we can produce the non-terminating chain
$s\to_{\eta}\langle v,w\rangle[v,w:=\langle
x,y\rangle]\to_{\beta}s\to_{\eta}\dots$ For this reason, the root-step of
$\eta$ has to be restricted too. The presence of a substitution context in the
$\beta$-rule is an action-at-distance [2], that allows to ‘free’ possible
blocked redexes, as the following one $x[x:=(\langle y\rangle[y:=z])].$ In
this way, we can bypass traditional commutation rules and retrieve good
rewriting properties. Structural equivalence intuitively says that explicit
substitutions can ‘freely travel’ in the body of a term.

We prove that typings are preserved under reduction and structural
equivalence.

######  Proposition 3.4 (Subject Reduction and Equivalence).

Let $s\to_{\mathsf{rep}}s^{\prime}$ or $s\equiv s^{\prime}$ with $\gamma\vdash
s:a.$ then $\gamma\vdash s^{\prime}:a.$

###### Proof.

The proof is by induction on $s\to_{\mathsf{rep}}s^{\prime}$ and $s\equiv
s^{\prime}$ and exploits an appropriate substitution lemma. ∎

We now prove that the structural equivalence is a strong bisimulation for the
reduction $\to_{\mathsf{rep}}.$ Intuitively, this means that the equivalence
does not affect terms rewriting.

######  Proposition 3.5.

If $s^{\prime}\equiv s$ and $s\to_{\mathsf{aut}}t$ there exists a term
$t^{\prime}$ s.t. $t^{\prime}\equiv t$ and
$s^{\prime}\to_{\mathsf{rep}}t^{\prime}.$

We show that we can associate appropriate measures to terms that decrease
under reduction. For $\beta$, we just consider the size of terms. For $\eta$,
we build on Mints approach [26]. We define the _size_ of a type by induction:
$\mathtt{size}\left(o\right)=0,\mathtt{size}\left(\langle
a_{1},\dots,a_{k}\rangle\right)=1+\sum\mathtt{size}\left(a_{i}\right).$ Given
$\gamma\vdash s:a$ we define a set of typed subterms of $s$:
$\mathsf{EST}(s)=\\{\delta\vdash p:a\mid
p\in\mathsf{ST}(s)\setminus\mathsf{LT}\text{ s.t. }\mathtt{E}[\delta\vdash
p:a]=s\text{ for some context }\mathtt{E}\\}.$ We set
$\eta(s)=\sum_{\delta\vdash
p:a\in\mathsf{EST}(s)}\mathtt{size}\left(a\right).$

######  Remark 3.6.

The size of terms decreases under $\beta$-reduction as a consequence of
_linearity_. Redexes cannot be copied nor deleted under reduction, since the
substitution is linear. This fact is trivially false for standard
$\lambda$-calculi, where the size of terms can possibly grow during
computation. The intuition behind the $\eta$ measure is that we are counting
all subterms of $s$ on which we could perform the $\eta$-reduction. The
restrictions on the shape of $p\in\mathsf{EST}(s)$ is indeed directly derived
from the ones on $\eta$-reduction.

######  Proposition 3.7.

The following statements hold. If $s\to_{\beta}s^{\prime}$ then
$\mathtt{size}\left(s^{\prime}\right)<\mathtt{size}\left(s\right)$; if
$s\to_{\eta}s^{\prime}$ then $\eta(s^{\prime})<\eta(s).$

######  Proposition 3.8.

The reductions $\to_{\beta}$ and $\to_{\eta}$ are separately strongly
normalizing and confluent.

###### Proof.

Strong normalization is a corollary of the former proposition. For confluence,
first one proves local confluence by induction and then apply Newman’s Lemma.
∎

We want to extend the result of separate strong normalization and confluence
to the whole $\to_{\mathsf{rep}}$-reduction. To do so, we prove that $\beta$
and $\eta$ suitably _commutes_.

######  Proposition 3.9.

If $s\to_{\beta}^{\ast}t\to_{\eta}^{\ast}t^{\prime}$ there exists $s^{\prime}$
s.t. $s\to_{\eta}^{\ast}s^{\prime}$ and
$s^{\prime}\to_{\beta}^{\ast}t^{\prime}.$

######  Theorem 3.10.

The reduction $\to_{\mathsf{rep}}$ is confluent and strongly normalizing.

###### Proof.

Strong normalization is achieved by observing that any infinite reduction
chain of $\to_{\mathsf{rep}}$ would trigger, by Proposition 3.9, an infinite
reduction chain for $\eta$, that is strongly normalizing. Confluence is
achieved by first proving local confluence and then by applying Newman’s
Lemma. ∎

Given $s\in\mathsf{\Lambda_{reps}}(\mathcal{R})(\gamma;a),$ we denote by
$\mathsf{nf}(s)$ its unique normal form. As a corollary of subject reduction,
we get that $\mathsf{nf}(s)\in\mathsf{\Lambda_{reps}}(\mathcal{R})(\gamma;a).$
We shall now present an inductive characterization of
$\to_{\mathsf{rep}}$-normal terms for the case where $\mathcal{R}$ is a
_discrete_ signature.

######  Definition 3.11.

Consider the following set, inductively defined:

$\mathsf{nf}(\mathsf{\mathsf{\Lambda_{rep}}}(\mathcal{R}))\ni
s::=v[\vec{x}_{1}:=x_{1}]\dots[\vec{x}_{n}:=x_{n}]\qquad v::=\langle
v_{1},\dots,v_{k}\rangle\mid x$

where $k,n\in\mathbb{N},\gamma\vdash p:o$ with $o$ being an atomic type and
$\delta\vdash v:a$ with $\delta$ being atomic.

######  Proposition 3.12.

A term $s\in\mathsf{\Lambda_{rep}}(\mathcal{R})$ is a normal form for
$\to_{\mathsf{rep}}$ iff there exists
$s^{\prime}\in\mathsf{nf}(\mathsf{\Lambda_{rep}}(\mathcal{R}))$ s.t. $s\equiv
s^{\prime}.$

###### Proof.

$(\Rightarrow)$ By induction on $s.$ If $s=x$ then
$s\in\mathsf{nf}(\mathsf{\Lambda_{rep}}(\mathcal{R})).$ If $\langle
s_{1},\dots,s_{k}\rangle$ then $s_{i}$ are normal form. Then we apply the IH
and get $s^{\prime}_{i}\in\mathsf{nf}(\mathsf{\Lambda_{rep}}(\mathcal{R}))$
s.t. $s_{i}\equiv s^{\prime}_{i}$. By definition
$s^{\prime}_{i}=v_{i}[\vec{x}_{i,1}:=x_{i,1}]\dots[\vec{x}_{i,1}:=x_{i,n_{i}}].$
We then set $s^{\prime}=\langle
v_{1},\dots,v_{k}\rangle[\vec{x}_{1,1}:=x_{1,n_{1}}]\dots[\vec{x}_{k,1}:=x_{k,n_{k}}].$
If $s=p[\vec{x}:=q]$ we have that $p$ is a normal form and $q$ is a
$\beta$-normal form. We reason by cases on $q.$ If $q$ does not have
$\eta$-redexes, we apply the IH and conclude in a way similar to the list
case. If $q$ has $\eta$-redexes, since $s$ is $\beta$ normal we have that
$q\notin\mathsf{LT}.$ We can prove that
$q=x[\vec{x}_{1}:=q_{1}]\dots[\vec{x}_{1}:=q_{n}]$ with $q_{i}$ hereditarely
of the same shape. Hence we conclude by pushing out all the substitutions from
left to right. ∎

$\displaystyle\beta\ \text{\emph{Root step}:}\quad
s[x^{a_{1}}_{1},\dots,x^{a_{k}}_{k}:=\mathtt{L}[\langle
t_{1},\dots,t_{k}\rangle]]\to_{\beta}\mathtt{L}[s\\{t_{1},\dots,t_{k}/x_{1},\dots,x_{k}\\}].$
$\displaystyle\eta\ \text{\emph{Root step}:}\quad
s\to_{\eta}\vec{x}[\vec{x}^{\vec{a}}:=s]\qquad\text{where }\vec{x}\text{ fresh
},\ \gamma\vdash s:\vec{a},\ s\notin\mathsf{LT}.$
$\displaystyle\text{\emph{Contextual
extensions}:}\qquad\prooftree\hypo{s\to_{\beta}s^{\prime}}\infer
1{\mathtt{C}[s]\to_{\beta}\mathtt{C}[s^{\prime}]}\qquad\prooftree\hypo{s\to_{\eta}s^{\prime}}\infer
1{\mathtt{E}[s]\to_{\eta}\mathtt{E}[s^{\prime}]}\quad({\to_{\mathsf{rep}}}={\to_{\beta}\cup\to_{\eta}}).$
$\displaystyle\text{ \emph{Structural
equivalence}:}\quad\mathtt{C}[s[\vec{x}:=t]]\equiv\mathtt{C}[s][\vec{x}:=t]\qquad\vec{x}\notin\mathsf{fv}(\mathtt{C}).$
Figure 2: Representable reduction relations and structural equivalence.

#### Free Representable Multicategories

Let $\mathcal{R}$ be a representable signature. First, we define a
multicategory $\mathsf{RM}(\mathcal{R})$ by setting
$\mathrm{ob}(\mathsf{RM}(\mathcal{R}))=\mathcal{R}_{0}$ and
$\mathsf{RM}(\mathcal{R})(\gamma;a)=\mathsf{\Lambda_{rep}}(\mathcal{R})(\gamma;a){/}{\sim}$
where ${\sim}={(\equiv\cup=_{\mathsf{rep}})}.$ Composition is given by
substitution, identities are given by variables. The operation is well-defined
on equivalence classes and satisfies associativity, identity axioms. We also
have that if $s\sim s^{\prime},$ then
$\mathsf{nf}(s)\equiv\mathsf{nf}(s^{\prime}).$ We denote by
$\eta_{\mathcal{R}}:\mathcal{R}\to\overline{\mathsf{RM}(\mathcal{R})}$ the
evident inclusion.

######  Proposition 3.13 (Representability).

We have a bijection $\mathsf{RM}(\mathcal{R})(\gamma,(a_{1}\otimes\dots\otimes
a_{k}),\delta;a)\cong\mathsf{RM}(\mathcal{R})(\gamma,a_{1},\dots,a_{k},\delta;a)$
multinatural in $\gamma,\delta$ and natural in $a,$ induced by the map
$[s]\mapsto[s\\{\langle x_{1},\dots,x_{k}\rangle/x\\}].$

###### Proof.

Naturality follows from basic properties of substitution. Inverses are given
by the maps
$(-)[\vec{x}:=x]:\mathsf{RM}(\mathcal{R})(\gamma,a_{1},\dots,a_{k},\delta;a)\to\mathsf{RM}(\mathcal{R})(\gamma,(a_{1}\otimes\dots\otimes
a_{k}),\delta;a).$ ∎

######  Definition 3.14.

Let $\mathcal{R}$ be a representable signature and $\mathsf{S}$ be a
representable multicategory. Let $i:\mathcal{R}\to\overline{\mathsf{S}}$ be a
map of representable signatures. We define a family of maps
$\mathsf{RT}(i)_{\gamma,a}:\mathsf{\Lambda_{rep}}(\mathcal{R})(\gamma;a)\to\mathsf{S}(i(\gamma);i(a))$
by induction as follows:

$\mathsf{RT}(i)_{a,a}(x)=id_{i(a)}\qquad\mathsf{RT}(i)_{\gamma_{1},\dots,\gamma_{k},(a_{1}\otimes\dots\otimes
a_{k})}(\langle
s_{1},\dots,s_{k}\rangle)=\bigotimes_{i=1}^{k}\mathsf{RT}(i)_{\gamma_{i},a_{i}}(s_{i})$
$\mathsf{RT}(i)_{\delta_{1},\gamma,\delta_{2},a}(s[x_{1},\dots,x_{k}:=t])=\mathsf{let}(\mathsf{RT}(i)_{\delta_{1},a_{1},\dots,a_{k},\delta_{2},a}(s))\circ\langle
id_{\delta_{1}},\mathsf{RT}(i)_{\gamma,(a_{1}\otimes\dots\otimes
a_{k})}(t),id_{\delta_{2}}\rangle$
$\mathsf{RT}(i)_{\gamma_{1},\dots,\gamma_{n},a}(f(s_{1},\dots,s_{n}))=i(f)\circ\langle\mathsf{RT}(i)(s_{1}),\dots,\mathsf{RT}(i)(s_{n})\rangle.$

######  Theorem 3.15 (Free Construction).

Let $\mathsf{S}$ be a a representable multicategory and
$i:\mathcal{R}\to\overline{\mathsf{S}}$ a map of representable signatures.
There exists a unique representable functor
$i^{\ast}:\mathsf{RM}(\mathcal{R})\to\mathsf{S}$ such that
$i=\overline{i^{\ast}}\circ\eta_{\mathcal{R}}.$

###### Proof.

The functor is defined exploiting Definition 3.14.∎

#### Coherence Result

We fix a _discrete_ representable signature $\mathcal{R}.$ We show that if
$s,t\in\mathsf{RM}(\mathcal{R})(\gamma;a)$, then $s=t.$ Our proof strongly
relies on the characterization of normal forms given in Proposition 3.12.

######  Lemma 3.16.

Let $\gamma,\gamma^{\prime}$ be atomic contexts. If there exists a type $a$
and normal terms $s,s^{\prime}$ such that
$s,s^{\prime}\in\mathsf{\Lambda_{rep}}(\mathcal{R})(\gamma;a)$ then
$\gamma=\gamma^{\prime}$ and $s\equiv s^{\prime}.$

######  Theorem 3.17.

Let $s,s^{\prime}$ be normal terms s.t.
$s,s^{\prime}\in\mathsf{\Lambda_{rep}}(\mathcal{R})(\gamma;a),$ then $s\equiv
s^{\prime}.$

###### Proof.

By Proposition 3.12, $s\equiv
t=(v[\vec{x}_{1}:=x_{1}]\dots[\vec{x}_{p}:=x_{p}])$ and $s^{\prime}\equiv
t^{\prime}=(v^{\prime}[\vec{y}_{1}:=x^{\prime}_{1}]\dots[\vec{y}_{p}:=x^{\prime}_{p^{\prime}}]).$
We prove that $t\equiv t^{\prime}$ by induction on $p\in\mathbb{N}.$ If $p=0$
then $t$ is either a list or a variable. We proceed by cases. If $t=x$ then
$\gamma=o$ and $a=o$ for some atomic type $o.$ By the former lemma we have
that $t\equiv t^{\prime}.$ If $t=\langle v_{1},\dots,v_{k}\rangle$ the result
is again a corollary of the former lemma since, by Definition 3.11, $\gamma$
is atomic. If $p=n+1$ then
$t=v[\vec{x}_{1}:=x_{1}]\dots[\vec{x}_{n+1}:=x_{n+1}]$ and, by definition of
typing we have  $\prooftree\hypo{x_{n+1}:\vec{a}\vdash
x_{n+1}:\vec{a}}\hypo{\delta_{1},\vec{x}_{n+1}:\vec{a},\delta_{2}\vdash
v[\vec{x}_{1}:=x_{1}]\dots[\vec{x}_{n}:=x_{n}]:a}\infer
2{\delta_{1},x_{n+1}:\vec{a},\delta_{2}\vdash s:a}$

with $\gamma=\delta_{1},x_{n+1}:\vec{a},\delta_{2}.$ Since
$t^{\prime}\in\mathsf{nf}(\mathsf{\Lambda_{rep}})(\gamma;a),$ there exists
$i\in\mathbb{N}$ such that
$t^{\prime}=v^{\prime}[\vec{y}_{1}:=x^{\prime}_{1}]\dots[\vec{y}_{i}:=x^{\prime}_{i}]\dots[\vec{y}_{p}:=x^{\prime}_{p^{\prime}}]$
and $x^{\prime}_{i}=x_{n+1}.$ By _structural equivalence_ we have that
$t^{\prime}\equiv
v^{\prime}[\vec{y}_{1}:=x^{\prime}_{1}]\dots[\vec{y}_{p}:=x^{\prime}_{p^{\prime}}]\dots[\vec{y}_{i}:=x_{i}].$
By definition of typing and by the hypothesis we have that

$\prooftree\hypo{x^{\prime}_{i}:\vec{a}\vdash
x^{\prime}_{i}:\vec{a}}\hypo{\delta_{1},\vec{x}_{i}:\vec{a},\delta_{2}\vdash
v^{\prime}[\vec{y}_{1}:=x^{\prime}_{1}]\dots[\vec{y}_{p^{\prime}}:=x^{\prime}_{p^{\prime}}]:a}\infer
2{\delta_{1},x_{n+1}:\vec{a},\delta_{2}\vdash s^{\prime}:a}$

By IH we have that $v[\vec{x}_{1}:=x_{1}]\dots[\vec{x}_{p}:=x_{n}]\equiv
v^{\prime}[\vec{y}_{1}:=x^{\prime}_{1}]\dots[\vec{y}_{p}:=x^{\prime}_{p^{\prime}}]$
. We can then conclude that $t\equiv t^{\prime},$ by structural equivalence. ∎

######  Theorem 3.18 (Coherence for Representable Multicategories).

Let $[s],[t]\in\mathsf{RM}(\mathcal{R})(\gamma;a).$ Then $[s]=[t].$

######  Theorem 3.19 (Coherence for Monoidal Categories).

All diagrams in the free monoidal category on a set commute.

###### Proof.

Corollary of the former theorem and Theorem 2.11, by noticing that
$\mathsf{mon}(\mathsf{RM}(\mathcal{R}))$ is the free monoidal category on the
underlying set of $\mathcal{R}.$ ∎

##  4 A Resource Calculus for Symmetric Representable Multicategories

The symmetric representable terms have exactly the same syntax and operational
semantics as the representable ones. We first extend the type system in order
to account for symmetries. We then study the free constructions establishing
an appropriate coherence result.

The typing is defined in Figure 3. It is easy to see that the representable
type system consists of a fragment of the symmetric one, where we just
consider identity permutations. We write $\gamma\vdash_{\mathsf{srep}}s:a$
when we need to specify that the type judgment refers to the symmetric
representable type system. We set
$\mathsf{\Lambda_{reps}}(\mathcal{R})(a_{1},\dots,a_{n};a)=\\{s\mid
x_{1}:a_{1},\dots,x_{n}:a_{n}\vdash_{\mathsf{srep}}s:a\text{ for some
}x_{i}\in\mathsf{fv}(s).\\}.$

######  Remark 4.1.

The role of permutations in the type system of Figure 3 deserves some
commentary. Instead of having an independent permutation rule, variables in
contexts can be permuted only when contexts have to be merged. In this way,
the system is _syntax directed_. The limitation to the choice of _shuffle
permutation_ is needed to get uniqueness of type derivations for terms.
Indeed, consider $s=\langle\langle x,y\rangle,z\rangle.$ If we allow the
choice of arbitrary permutations, we could build the following derivations:

$\prooftree\hypo{x:a\vdash x:a\quad y:b\vdash y:b}\hypo{\sigma}\infer
2{y:b,x:a\vdash\langle x,y\rangle:(a\otimes b)}\hypo{z:a\vdash
z:a}\hypo{id}\infer 3{y:b,x:a,z:a\vdash s:((a\otimes b)\otimes
a)}\qquad\prooftree\hypo{x:a\vdash x:a\quad y:b\vdash y:b}\hypo{id}\infer
2{x:a,y:b\vdash\langle x,y\rangle:(a\otimes b)}\hypo{z:a\vdash
z:a}\hypo{\sigma\oplus id}\infer 3{y:b,x:a,z:a\vdash s:((a\otimes b)\otimes
a)}$

where $\sigma$ is the swap. Thanks to the shuffle limitation, only the one on
the left is allowed.

######  Proposition 4.2 (Canonicity of Typing).

If $\pi\triangleright\gamma\vdash s:a$ and
$\pi^{\prime}\triangleright\gamma\vdash s:a^{\prime}$ then $a=a^{\prime}$ and
$\pi=\pi^{\prime}.$

###### Proof.

By induction on $s.$ In the cases where a merging of type contexts happens,
such as the list case, we rely on the properties of shuffle permutations and
on the fact that type contexts are repetitions-free. Hence, the action of
permutations on contexts is always fixedpoint-free. ∎

$\displaystyle\prooftree\hypo{a\in\mathcal{R}_{0}}\infer 1{x:a\vdash
x:a}\qquad\prooftree\hypo{\gamma_{1}\vdash s_{1}:a_{1}\dots\gamma_{k}\vdash
s_{k}:a_{k}}\hypo{\sigma\in\mathsf{shu}(\gamma_{1},\dots,\gamma_{k})}\infer
2{{(\gamma_{1},\dots,\gamma_{k})}\cdot{\sigma}\vdash{\langle
s_{1},\dots,s_{k}\rangle}:(a_{1}\otimes\dots\otimes a_{k})}$
$\displaystyle\qquad\prooftree\hypo{\gamma\vdash s:(a_{1}\otimes\dots\otimes
a_{k})}\hypo{\delta,x_{1}:a_{1},\dots,x_{k}:a_{k},\delta^{\prime}\vdash
t:b}\hypo{\sigma\in\mathsf{shu}(\delta,\gamma^{\prime},\delta^{\prime})}\infer
3{{(\delta,\gamma,\delta^{\prime})}\cdot{\sigma}\vdash{t[x_{1}^{a_{1}},\dots,x_{k}^{a_{k}}:=s]}:b}$
Figure 3: Symmetric Representable Type System on a signature $\mathcal{R}$. We
omit the case $f(\vec{s}).$

######  Proposition 4.3.

The following rule is admissible: $\prooftree\hypo{\gamma\vdash
s:a}\hypo{\sigma\in S_{k}}\infer 2{{\gamma}\cdot{\sigma}\vdash s:a}.$

###### Proof.

Easy induction on the structure of $s,$ exploiting Lemma 2.2. ∎

The reduction relation is the same as the representable one, that we know to
be strongly normalizing and confluent. We also have preservation of typing
under reduction and structural equivalence. Given
$s\in\mathsf{\Lambda_{reps}}(\mathcal{R})(\gamma;a),$ we denote by
$\mathsf{nf}(s)$ its unique normal form. As a corollary of subject reduction,
we get that $\mathsf{nf}(s)\in\mathsf{\Lambda_{reps}}(\mathcal{R})(\gamma;a).$

#### Free Symmetric Representable Multicategories

We now characterize the free symmetric representable construction. Given a
representable signature $\mathcal{R},$ we define a multicategory by setting
$\mathrm{ob}(\mathsf{SRM}(\mathcal{R}))=\mathcal{R}_{0}$ and
$\mathsf{SRM}(\mathcal{R})(\gamma;a)=\mathsf{\Lambda_{reps}}(\mathcal{R})(\gamma;a){/}{(\equiv\cup=_{\mathsf{rep}})}.$
Composition is given by substitution, identities are given by variables. The
operation is well-defined on equivalence classes and satisfies associativity,
identity axioms. One can prove that $\mathsf{SRM}(\mathcal{R})$ is
representable, by repeating the argument given for Proposition 3.13. The proof
that $\mathsf{SRM}(\mathcal{R})$ is symmetric is a direct corollary of
Proposition 4.3:

######  Proposition 4.4 (Symmetry).

We have that
$\mathcal{M}(\gamma,a_{1},\dots,a_{k};a)=\mathcal{M}(\gamma;a_{\sigma(1)},\dots,a_{\sigma(k)};a).$

######  Example 4.5.

An interesting example of structural equivalence is the following. Let
$s=\langle\rangle[-:=x][-:=y]\text{ and
}s^{\prime}=\langle\rangle[-:=y][-:=x],$ with
$s,s^{\prime}\in\mathsf{\Lambda_{reps}}(\mathcal{R})((),();()).$ We have that
$\langle\rangle[-:=x][-:=y]\equiv\langle\rangle[-:=y][-:=x],$ with
$x:(),y:()\vdash s:()$ and $y:(),x:()\vdash s^{\prime}:().$ This is the way
our syntax validates the fact that permutations of the unit type _collapse_ to
the identity permutation, since $s$ corresponds to the identity permutation,
while $s^{\prime}$ to the swapping of $x$ with $y$.

######  Definition 4.6.

Let $\mathcal{R}$ be a representable signature and $\mathsf{S}$ be a symmetric
representable multicategory. Let $i:\mathcal{R}\to\overline{\mathsf{S}}$ be a
map of representable signatures. We define a family of maps
$\mathsf{RT}(i)_{\gamma,a}:\mathsf{\Lambda_{reps}}(\mathcal{R})(\gamma;a)\to\mathsf{S}(i(\gamma);i(a))$
by induction as follows:

$\mathsf{RT}(i)_{a,a}(x)=id_{i(a)}\qquad\mathsf{RT}(i)_{{(\gamma_{1},\dots,\gamma_{k})}\cdot{\sigma},\langle
a_{1},\dots,a_{k}\rangle}(\langle
s_{1},\dots,s_{k}\rangle)=\left(\bigotimes_{j=1}^{k}\mathsf{RT}(i)_{\gamma_{j},a_{j}}(s_{j})\right)\circ\sigma$
$\mathsf{RT}(i)_{{\delta_{1},\gamma,\delta_{2}}\cdot{\sigma},a}(s[x_{1}^{a_{1}},\dots,x_{k}^{a_{k}}:=t])={((\mathsf{RT}(i)_{\delta_{1},a_{1},\dots,a_{k},a}(s))^{\ast}\circ\langle
id_{\delta_{1}},\mathsf{RT}(i)_{\gamma,\vec{a}}(t),id_{\delta_{2}}\rangle)}\circ{\sigma}.$

######  Theorem 4.7 (Free Construction).

Let $\mathsf{S}$ be a a symmetric representable multicategory and
$i:\mathcal{R}\to\overline{\mathsf{S}}$ a map of representable signatures.
There exists a unique symmetric representable functor $i^{\ast}$ such that
$i=\overline{i^{\ast}}\circ\eta_{\mathcal{R}}.$

#### Coherence Result

Fix a discrete signature $\mathcal{R}.$ We shall prove that morphisms in
$\mathsf{SRM}(\mathcal{R})$ can by characterized by means of appropriate
permutations of their typing context. This will lead the following coherence
result for symmetric representable multicategories: two morphisms in
$\mathsf{SRM}(\mathcal{R})$ are equal whenever their _underlying permutations_
are the same.

We start by defining the _strictification_ of a representable type
$\mathsf{strict}(a)$, by induction as follows: $\mathsf{strict}(o)=o,\
\mathsf{strict}((a_{1}\otimes\dots\otimes
a_{k}))=\mathsf{strict}(a_{1}),\dots,\mathsf{strict}(a_{k}).$
$\mathsf{strict}(a)$ is the list of atoms that appear in the type $a$. We
extend the strictification to contexts in the natural way. Let
$s\in\mathsf{nf}(\mathsf{\Lambda_{reps}}(\mathcal{R}))(\gamma,a)$ and
$\sigma\in\mathsf{Stab}(\mathsf{strict}(\gamma)).$ We define the _right
action_ of $\sigma$ on $s$, $s^{\sigma}$ by induction as follows:

$x^{id}=x\qquad\langle
s_{1},\dots,s_{k}\rangle^{\sigma\circ(\bigoplus_{i=1}^{k}\sigma_{i})}={\langle
s_{1}^{\sigma_{1}},\dots,s_{k}^{\sigma_{k}}\rangle}\cdot{\sigma}$
$(s[\vec{x}_{1}:=x_{1}]\dots[\vec{x}_{n}:=x_{n}])^{\sigma}=(s^{\sigma})[\sigma(\vec{x}_{1}):=x_{1}]\dots[\sigma(\vec{x}_{n}):=x_{n}]$

where $\sigma(x_{1},\dots,x_{k})$ stands for the image of $x_{1},\dots,x_{k}$
along the permutation $\sigma.$

######  Theorem 4.8.

Let $s\in\mathsf{nf}(\mathsf{\Lambda_{reps}}(\mathcal{R}))(\gamma,a).$ There
exists a unique $\sigma\in\mathsf{Stab}((\mathsf{strict}(\gamma))$ and a
unique non-symmetric representable normal term $t$ such that $s=t^{\sigma}.$

###### Proof.

By induction on $s,$ exploiting Proposition 4.2. ∎

Let $s\in\mathsf{nf}(\mathsf{\Lambda_{reps}}(\mathcal{R}))(\gamma;a).$ We
denote by $\mathsf{sym}(s)$ the unique permutation given by the former
theorem. Given $s\in\mathsf{\Lambda_{reps}}{A}(\gamma;a)$ we set
$\mathsf{sym}(s)=\mathsf{sym}(\mathsf{nf}(s)).$ This definition is clearly
coherent with the quotient on terms performed in the free construction.

######  Theorem 4.9.

Let
$s,s^{\prime}\in\mathsf{nf}(\mathsf{\Lambda_{reps}}(\mathcal{R}))(\gamma;a).$
If $\mathsf{sym}(s)=\mathsf{sym}(s^{\prime})$ then $s\equiv s^{\prime}.$

######  Theorem 4.10 (Coherence).

Let $[s],[s^{\prime}]\in\mathsf{SRM}(\mathcal{A})(\gamma;a).$ If
$\mathsf{sym}([s])=\mathsf{sym}[s^{\prime}]$ then $[s]=[s^{\prime}].$

######  Theorem 4.11 (Coherence for Symmetric Monoidal Categories).

Two morphisms in the free symmetric monoidal categories are equal if their
underlying permutations are equal.

###### Proof.

Corollary of Theorems 2.11 and 4.10. ∎

##  5 A Resource Calculus for Symmetric Closed Multicategories

We consider the case of symmetric closed multicategories, which is orthogonal
to the representable structures we introduced in the previous sections. This
calculus corresponds to the resource version of linear $\lambda$-calculus,
where we have unbiased $k$-ary $\lambda$-abstraction and (linear) application.
We begin by defining the terms and their typings, then proceed to introducing
their operational semantics. We conclude by characterizing the free
construction via well-typed equivalence classes of terms.

#### Symmetric Closed Resource Terms

Let $\mathcal{L}$ be a closed signature. The _symmetric closed resource terms_
on $\mathcal{L}$ are defined by the following inductive grammar:

$\mathsf{\Lambda_{\mathsf{sc}}}(\mathcal{L})\ni
s::=x\in\mathcal{V}\mid\lambda\langle
x^{a_{1}}_{1},\dots,x^{a_{k}}_{k}\rangle.s\mid s\langle
s_{1},\dots,s_{k}\rangle\mid f(s_{1},\dots,s_{k})$

for $k\in\mathbb{N}$ and $f\in\mathsf{arr}(\mathcal{L}),a_{i}\in\mathcal{L}.$
A term of the shape $s\langle s_{1},\dots,s_{k}\rangle$ is called a _(
$k$-linear) application_. A term of the shape $\lambda\langle
x_{1},\dots,x_{k}\rangle.s$ is called a _( $k$-linear) $\lambda$-abstraction_.
Variables under the scope of a $\lambda$-abstraction are bound. We define the
following subset of terms
$\mathsf{AT}=\\{\mathtt{L}[\lambda\vec{x}.t]\mid\text{ for some substitution
context }\mathtt{L}\text{ and term }t.\\}.$ Typing and contexts with hole are
defined in Figure 4. Given a term $\gamma\vdash s:a$, there exists a unique
type derivation for it.

$\displaystyle\prooftree\hypo{a\in\mathcal{L}_{0}}\infer 1{x:a\vdash
x:a}\qquad\prooftree\hypo{\gamma,x_{1}:a_{1},\dots,x_{k}:a_{k}\vdash
s:b}\infer 1{\gamma\vdash\lambda\langle
x_{1}^{a_{1}},\dots,x_{k}^{a_{k}}\rangle.s:(a_{1}\otimes\dots\otimes
a_{k})\multimap b}$ $\displaystyle\prooftree\hypo{\gamma_{0}\vdash
s:(a_{1}\otimes\dots\otimes a_{k})\multimap b}\hypo{\gamma_{1}\vdash
t_{1}:a_{1}\dots\gamma_{k}\vdash
t_{k}:a_{k}}\hypo{\sigma\in\mathsf{shu}(\gamma_{0},\dots,\gamma_{k})}\infer
3{{(\gamma,\delta)}\cdot{\sigma}\vdash s\langle t_{1},\dots,t_{k}\rangle:b}$

$\displaystyle\mathtt{C}::=\mathtt{C}::=[\cdot]\mid s\langle
s_{1},\dots,\mathtt{C},\dots,s_{k}\rangle\mid\mathtt{C}\langle
s_{1},\dots,s_{k}\rangle\mid\lambda\langle
x_{1},\dots,x_{k}\rangle.\mathtt{C}\mid
f(s_{1},\dots,\mathtt{C},\dots,s_{k}).$ $\displaystyle\mathtt{E}::=[\cdot]\mid
s\langle s_{1},\dots,\mathtt{E},\dots,s_{k}\rangle\mid\mathtt{E}\langle
s_{1},\dots,s_{k}\rangle\quad(\mathtt{E}\neq[\cdot])\mid\lambda\langle
x_{1},\dots,x_{k}\rangle.\mathtt{E}\mid
f(s_{1},\dots,\mathtt{E},\dots,s_{k}).$

Figure 4: Symmetric closed type system on a signature $\mathcal{L}$ and
contexts with one hole. Types are the elements of $\mathcal{L}_{0}.$ We omit
the case of $f(\vec{s}).$

#### Terms under Reduction

The reduction relation is defined in Figure 5.

######  Remark 5.1.

The definition of the $\beta$-reduction follows the standard choices for
resource calculi. The novel technicality is the restriction of the
$\eta$-reduction, that is justified again by the goal of obtaining a strongly
normalizing reduction. Indeed, $\eta$-reduction is again not normalizing. The
situation recalls what happens in the standard $\lambda$-calculus and we deal
with it adapting to our framework the restrictions introduced in [26, 15].

$\displaystyle\text{\emph{$\beta$ Root-Step}: }(\lambda\langle
x_{1}^{a_{1}},\dots,x_{k}^{a_{k}}\rangle.s)\langle
t_{1},\dots,t_{k}\rangle\to_{\beta}s\\{t_{1},\dots,t_{k}/x_{1},\dots,x_{k}\\}.$
$\displaystyle\text{\emph{$\eta$ Root-Step}:
}s\to_{\eta}\lambda\vec{x}^{\vec{a}}.(s\vec{x})\qquad\text{where
}\vec{x}\text{ fresh },\gamma\vdash s:\vec{a}\multimap a,s\notin\mathsf{AT}.$
$\displaystyle\text{ \emph{Contextual extensions}:
}\quad\prooftree\hypo{s\to_{\beta}s^{\prime}}\infer
1{\mathtt{C}[s]\to_{\beta}\mathtt{C}[s^{\prime}]}\qquad\prooftree\hypo{s\to_{\eta}s^{\prime}}\infer
1{\mathtt{E}[s]\to_{\eta}\mathtt{E}[s^{\prime}]}\quad(\to_{\mathsf{sc}}=\to_{\beta}\cup\to_{\eta}).$
Figure 5: Symmetric closed reduction relations.

To study the rewriting, we adapt the method introduced for representable
terms. We first prove that typing is preserved under reduction. Then, we
introduce a measure that decreases under $\eta$. We define the _size_ of a
type by induction: $\mathtt{size}\left(o\right)=0,\mathtt{size}\left(\langle
a_{1},\dots,a_{k}\rangle\multimap
a\right)=1+\sum\mathtt{size}\left(a_{i}\right)+\mathtt{size}\left(a\right).$
Given $\gamma\vdash s:a$ we define a set of typed subterms of $s$:
$\mathsf{EST}(s)=\\{\delta\vdash p:a\mid
p\in\mathsf{ST}(s)\setminus\mathsf{AT}\text{ s.t. }\mathtt{E}[\delta\vdash
p:a]=s\text{ for some context }\mathtt{E}\\}.$ We set
$\eta(s)=\sum_{\delta\vdash
p:a\in\mathsf{EST}(s)}\mathtt{size}\left(a\right).$ The proof of strong
normalization and confluence is completely symmetrical to the representable
case. Given $s\in\mathsf{\Lambda_{\mathsf{sc}}}(\mathcal{R})(\gamma;a),$ we
denote by $\mathsf{nf}(s)$ its unique normal form. As a corollary of subject
reduction, we get that
$\mathsf{nf}(s)\in\mathsf{\Lambda_{\mathsf{sc}}}(\mathcal{R})(\gamma;a).$

#### Free Symmetric Closed Multicategories

Let $\mathcal{L}$ be a closed signature, we define a multicategory
$\mathsf{SCM}(\mathcal{L})$ by setting
$\mathrm{ob}(\mathsf{SCM}(\mathcal{L}))=\mathcal{L}_{0}$ and
$\mathsf{SCM}(\mathcal{L})(\gamma;a)=\mathsf{\Lambda_{\mathsf{sc}}}(\mathcal{L})(\gamma;a){/}{\sim}$
where ${\sim}={=_{\mathsf{sc}}}.$ Composition is given by substitution,
identities are given by variables. The operation is well-defined equivalence
classes and satisfies associativity and identity axioms. We also have that if
$s\sim s^{\prime},$ then $\mathsf{nf}(s)=\mathsf{nf}(s^{\prime}).$ We denote
by $\eta_{\mathcal{L}}:\mathcal{L}\to\overline{\mathsf{SCM}(\mathcal{L})}$ the
evident inclusion. One can prove that $\mathsf{SCM}(\mathcal{R})$ is
symmetric, by repeating the argument given in the previous section. This
multicategory is also _closed_ :

######  Theorem 5.2.

We have a bijection $\mathsf{SCM}(\mathcal{L})(\gamma;\langle
a_{1},\dots,a_{k}\rangle\multimap
a)\cong\mathsf{SCM}(\mathcal{L})(\gamma,a_{1},\dots,a_{k};a)$ natural in $a$
and multinatural in $\gamma,$ induced by the maps $[s]\mapsto[s\langle
x_{1},\dots,x_{k}\rangle].$

###### Proof.

Naturality derives from basic properties of substitution. Inverses are given
by the maps $[s]\mapsto[\lambda\langle x_{1},\dots,x_{k}\rangle.s].$ ∎

######  Definition 5.3.

Let $\mathsf{E}$ be a symmetric closed multicategory and let
$i:\mathcal{L}\to\overline{\mathsf{E}}$ be a map of closed signatures. We
define a family of maps
$\mathsf{RT}_{\gamma,a}:\mathsf{\Lambda_{\mathsf{sc}}}(\mathcal{L})(\gamma,a)\to\mathsf{E}(i(\gamma),i(a))$
by induction as follows:

$\mathsf{RT}_{a,a}(x)=1_{i(a)}\qquad\mathsf{RT}_{\gamma,\vec{a}\multimap
a}(\lambda\vec{x}.s)=\lambda(\mathsf{RT}_{\gamma,\vec{a},a}(s))$
$\mathsf{RT}_{(\gamma_{0},\dots,\gamma_{k}),a}(s\langle
t_{1},\dots,t_{k}\rangle)=(ev\circ\langle\mathsf{RT}_{\gamma_{0},\langle
a_{1},\dots,a_{k}\rangle\multimap
a}(s),\mathsf{RT}_{\gamma_{1},a_{1}}(t_{1}),\dots,\mathsf{RT}_{\gamma_{k},a_{1}}(t_{k})\rangle)\cdot\sigma.$

######  Theorem 5.4 (Free Construction).

Let $\mathsf{S}$ be a a symmetric closed multicategory and
$i:\mathcal{L}\to\overline{\mathsf{S}}$ a map of representable signatures.
There exists a unique symmetric closed functor
$i^{\ast}:\mathsf{SCM}(\mathcal{L})\to\mathsf{S}$ such that
$\overline{i^{\ast}}\circ\eta_{\mathcal{L}}=i.$

######  Theorem 5.5 (Coherence).

Let $[s],[s^{\prime}]\in\mathsf{SCM}(\mathcal{R})(\gamma;a).$ Then
$[s]=[s^{\prime}]$ iff $\mathsf{nf}([s])\equiv\mathsf{nf}([s^{\prime}]).$

##  6 A Resource Calculus for Autonomous Multicategories

In this section we present our calculus for autonomous multicategories. These
structures bring together representability, symmetry and closure. For this
reason, the calculus we will present is a proper extension of the ones we
introduced before. Again, we follow the same pattern of Sections 3 and 5,
first introducing the typing, then studying the operational semantics and
finally characterizing the free constructions.

#### Autonomous Terms

Let $\mathcal{A}$ be an autonomous signature. The _autonomous resource terms_
on $\mathcal{A}$ are defined by the following inductive grammar:

$\mathsf{\Lambda_{aut}}(\mathcal{A})\ni s,t::=x\mid\lambda\langle
x^{a_{1}}_{1},\dots,x^{a_{k}}_{k}\rangle.s\mid st\mid\langle
s_{1},\dots,s_{k}\rangle\mid s[x^{a_{1}}_{1},\dots,x^{a_{k}}_{k}:=t]\mid
f(s_{1},\dots,s_{k})$

for $k\in\mathbb{N}$ and $f\in\mathsf{arr}(\mathcal{A}),a_{i}\in\mathcal{A}.$
Variables under the scope of a $\lambda$-abstraction and of a substitution are
bound. The typing is given in Figure 6. The calculi introduced in the previous
sections can be seen as subsystems of the autonomous one.

Given a subterm $p$ of $s$ we write $\mathsf{ty}(p)_{s}$ for the type of $p$
in the type derivation of $s.$ The mapping is functional as corollary of the
former proposition.

$\displaystyle\qquad\qquad\prooftree\hypo{a\in\mathcal{A}_{0}}\infer
1{x:a\vdash x:a}\qquad\prooftree\hypo{\gamma_{1}\vdash
s_{1}:a_{1}\dots\gamma_{k}\vdash
s_{k}:a_{k}}\hypo{\sigma\in\mathsf{shu}(\gamma_{1},\dots,\gamma_{k})}\infer
2{{(\gamma_{1},\dots,\gamma_{k})}\cdot{\sigma}\vdash{\langle
s_{1},\dots,s_{k}\rangle}:(a_{1}\otimes\dots\otimes a_{k})}$
$\displaystyle\prooftree\hypo{\gamma,x_{1}:a_{1},\dots,x_{k}:a_{k}\vdash
s:b}\infer 1{\gamma\vdash\lambda\langle
x_{1}^{a_{1}},\dots,x_{k}^{a_{k}}\rangle.s:(a_{1}\otimes\dots\otimes
a_{k})\multimap b}\qquad\prooftree\hypo{\gamma\vdash s:\vec{a}\multimap
b}\hypo{\delta\vdash
t:\vec{a}}\hypo{\sigma\in\mathsf{shu}(\gamma,\delta)}\infer
3{{(\gamma,\delta)}\cdot{\sigma}\vdash{st}:b}$
$\displaystyle\qquad\qquad\prooftree\hypo{\gamma\vdash
s:(a_{1}\otimes\dots\otimes
a_{k})}\hypo{\delta_{1},x_{1}:a_{1},\dots,x_{k}:a_{k},\delta_{2}\vdash
t:b}\hypo{\sigma\in\mathsf{shu}(\gamma,\delta_{1},\delta_{2})}\infer
3{{(\gamma,\delta_{1},\delta_{2})}\cdot{\sigma}\vdash{t[x_{1}^{a_{1}},\dots,x_{k}^{a_{k}}:=s]}:b}$
Figure 6: Autonomous type system on a signature $\mathcal{A}$. We omit the
case of $f(\vec{s}).$

#### Terms under Reduction

The reduction relation $\to_{\mathsf{aut}}$, together with its subreductions
$\beta$ and $\eta$ are defined by putting together the reductions
$\to_{\mathsf{rep}}$ (Figure 2) and $\to_{\mathsf{sc}}$ (Figure 5). The same
happens with structural equivalence. The reduction satisfies subject
reduction, strong normalization and confluence. The proofs build on the
results of the previous sections. As decreasing measures, we use the size of a
term for $\beta$-reduction and the sum of the two $\eta$ measures we defined
in the previous sections for $\eta$-reduction.

#### Free Autonomous Multicategories

Let $\mathcal{A}$ be an autonomous signature, we define a multicategory
$\mathsf{AUT}(\mathcal{A})$ by setting
$\mathrm{ob}(\mathsf{AUT}(\mathcal{A}))=\mathcal{A}_{0}$ and
$\mathsf{AUT}(\mathcal{A})(\gamma;a)=\mathsf{\Lambda_{aut}}(\mathcal{A})(\gamma;a){/}{\sim}$
where $\sim$ is the equivalence $\equiv\cup=_{\mathsf{aut}}.$ Composition is
given by substitution, identities are given by variables. The operation is
well-defined on equivalence classes and satisfies associativity and identity
axioms. We also have that if $s\sim s^{\prime}$ then
$\mathsf{nf}(s)\equiv\mathsf{nf}(s^{\prime}).$ We denote by
$\eta_{\mathcal{A}}:\mathcal{A}\to\overline{\mathsf{AUT}(\mathcal{A})}$ the
evident inclusion. One can prove that this multicategory is symmetric,
representable and closed by importing the proofs given in the previous
sections.

######  Definition 6.1.

Let $\mathsf{S}$ be an autonomous multicategory and let
$i:\mathcal{A}\to\overline{\mathsf{S}}$ be a map of autonomous signatures. We
define a family of maps
$\mathsf{RT}_{\gamma,a}:\mathsf{\Lambda_{aut}}(\mathcal{A})(\gamma,a)\to\mathsf{E}(i(\gamma),i(a))$
by induction, extending Definitions 4.6 and 5.3 in the natural way.

######  Theorem 6.2 (Free Construction).

Let $\mathsf{S}$ be a an autonomous multicategory and
$i:\mathcal{A}\to\overline{\mathsf{S}}$ a map of autonomous signatures. There
exists a unique autonomous functor
$i^{\ast}:\mathsf{AUT}(\mathcal{A})\to\mathsf{S}$ such that
$\overline{i^{\ast}}\circ\eta_{\mathcal{A}}=i.$

######  Theorem 6.3 (Coherence).

Let $[s],[s^{\prime}]\in\mathsf{AUT}(\mathcal{R})(\gamma;a).$ Then
$[s]=[s^{\prime}]$ iff $\mathsf{nf}([s])\equiv\mathsf{nf}([s^{\prime}]).$

##  7 Conclusion

We established a formal correspondence between resource calculi and
appropriate linear multicategories, providing coherence theorems by means of
normalization. As future work, we consider two possible perspectives. It is
tempting to parameterize our construction over the choice of allowed
_structural rules_ on typing contexts. For instance, while the choice of
permutations (i.e., symmetries) gives _linear_ structures, the choice of
arbitrary functions between indexes would give _cartesian_ structures. In this
way, we would achieve a general method to produce type theories for
appropriate _algebraic theories_ , in the sense of [14]. Another perspective
is the passage to the _second dimension_ , following the path of [9]. In this
way, the rewriting of terms would become visible in the multicategorical
structure itself. Coherence by normalization could then be upgraded to a
method of _coherence by standardization_ , exploiting a rewriting relation on
reduction paths.

## References

  * [1] Beniamino Accattoli  “Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic”  In _LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022_ ACM, 2022, pp. 49:1–49:15  DOI: 10.1145/3531130.3532445
  * [2] Beniamino Accattoli, Eduardo Bonelli, Delia Kesner and Carlos Lombardi  “A nonstandard standardization theorem”  In _The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014_ ACM, 2014, pp. 659–670  DOI: 10.1145/2535838.2535886
  * [3] Davide Barbarossa and Giulio Manzonetto  “Taylor subsumes Scott, Berry, Kahn and Plotkin”  In _Proc. ACM Program. Lang._ 4.POPL, 2020, pp. 1:1–1:23  DOI: 10.1145/3371069
  * [4] Nick Benton, Gavin Bierman, Valeria de Paiva and Martin Hyland  “A Term Calculus for Intuitionistic Linear Logic”  In _Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA)_ Springer, 1993
  * [5] R.F. Blute, J.R.B. Cockett, R.A.G. Seely and T.H. Trimble  “Natural deduction and coherence for weakly distributive categories”  In _Journal of Pure and Applied Algebra_ 113.3, 1996, pp. 229–296  DOI: https://doi.org/10.1016/0022-4049(95)00159-X
  * [6] Gérard Boudol  “The lambda-calculus with multiplicities”  In _CONCUR’93_ Berlin, Heidelberg: Springer Berlin Heidelberg, 1993, pp. 1–6
  * [7] Roberto Di Cosmo and Delia Kesner  “Combining algebraic rewriting, extensional lambda calculi, and fixpoints”  In _Theoretical Computer Science_ 169.2, 1996, pp. 201–220  DOI: https://doi.org/10.1016/S0304-3975(96)00121-1
  * [8] Thomas Ehrhard and Laurent Regnier  “Uniformity and the Taylor Expansion of ordinary $\lambda$-terms”  In _Theoretical Computer Science_ 403.2-3, 2008  DOI: 10.1016/j.tcs.2008.06.001
  * [9] Marcelo Fiore and Philip Saville  “Coherence and Normalisation-by-Evaluation for Bicategorical Cartesian Closed Structure”, LICS ’20  Saarbrücken, Germany: Association for Computing Machinery, 2020, pp. 425–439  DOI: 10.1145/3373718.3394769
  * [10] Jean-Yves Girard  “Linear logic”  In _Theoretical Computer Science_ 50.1, 1987, pp. 1–101  DOI: https://doi.org/10.1016/0304-3975(87)90045-4
  * [11] Claudio Hermida  “Representable Multicategories”  In _Advances in Mathematics_ 151.2, 2000, pp. 164–225  DOI: https://doi.org/10.1006/aima.1999.1877
  * [12] Dominic J.D. Hughes  “Simple free star-autonomous categories and full coherence”  In _Journal of Pure and Applied Algebra_ 216.11, 2012, pp. 2386–2410  DOI: https://doi.org/10.1016/j.jpaa.2012.03.020
  * [13] J… Hyland  “Classical lambda calculus in modern dress”  In _Mathematical Structures in Computer Science_ 27.5, 2017, pp. 762–781  DOI: 10.1017/S0960129515000377
  * [14] J.M.E. Hyland  “Elements of a theory of algebraic theories” Models of Interaction: Essays in Honour of Glynn Winskel  In _Theoretical Computer Science_ 546, 2014, pp. 132–144  DOI: https://doi.org/10.1016/j.tcs.2014.03.005
  * [15] C. Jay and Neil Ghani  “The virtues of eta-expansion”  In _Journal of Functional Programming_ 5.2 Cambridge University Press, 1995, pp. 135–154  DOI: 10.1017/S0956796800001301
  * [16] G.M. Kelly and S. Maclane  “Coherence in closed categories”  In _Journal of Pure and Applied Algebra_ 1.1, 1971, pp. 97–140  DOI: https://doi.org/10.1016/0022-4049(71)90013-2
  * [17] Delia Kesner  “The Theory of Calculi with Explicit Substitutions Revisited”  In _Computer Science Logic_ Berlin, Heidelberg: Springer Berlin Heidelberg, 2007, pp. 238–252
  * [18] AJ Kfoury  “A linearization of the Lambda-calculus and consequences”  In _Journal of Logic and Computation_ 10.3, 2000, pp. 411–436  DOI: 10.1093/logcom/10.3.411
  * [19] Joachim Lambek  “Deductive systems and categories II. Standard constructions and closed categories”  In _Category Theory, Homology Theory and their Applications I_ Berlin, Heidelberg: Springer Berlin Heidelberg, 1969, pp. 76–122
  * [20] Joachim Lambek and Philip J. Scott  “Introduction to Higher Order Categorical Logic”  USA: Cambridge University Press, 1986
  * [21] Tom Leinster  “Higher Operads, Higher Categories”, 2003  arXiv:math/0305049 [math.CT]
  * [22] Saunders Maclane  “Natural Associativity and Commutativity”  In _Rice Institute Pamphlet - Rice University Studies_ 49, 1963, pp. 28–46
  * [23] Damiano Mazza  “Polyadic Approximations in Logic and Computation”, 2017
  * [24] Damiano Mazza, Luc Pellissier and Pierre Vial  “Polyadic approximations, fibrations and intersection types”, 2018  DOI: 10.1145/3158094
  * [25] Paul-André Melliès, Federico Olimpieri and Lionel Vaux Auclair  “An explicit construction of the homotopy span model of differential linear logic”  In _In preparation_
  * [26] G.. Mints  “Closed categories and the theory of proofs”  In _Journal of Soviet Mathematics_ , 1981  DOI: 10.1007/BF01404107
  * [27] Yo Ohta and Masahito Hasegawa  “A Terminating and Confluent Linear Lambda Calculus”  In _Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings_ 4098, Lecture Notes in Computer Science  Springer, 2006, pp. 166–180  DOI: 10.1007/11805618\\_13
  * [28] Federico Olimpieri  “Intersection Types and Resource Calculi in the Denotational Semantics of Lambda-Calculus”, 2020
  * [29] P. Selinger  “A Survey of Graphical Languages for Monoidal Categories”  In _New Structures for Physics_ Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 289–355  DOI: 10.1007/978-3-642-12821-9_4
  * [30] Michael Shulman  “A practical type theory for symmetric monoidal categories”  In _Theory and Applications of Categories_ 37.25, 2021, pp. 863–907
  * [31] Takeshi Tsukada, Kazuyuki Asada and C.-H. Ong  “Generalised Species of Rigid Resource Terms”  In _Proceedings of the 32rd Annual ACM/IEEE Symposium on Logic in Computer Science_ , LICS 2017, 2017  DOI: 10.1109/LICS.2017.8005093
  * [32] Lionel Vaux  “Taylor Expansion, $\beta$-Reduction and Normalization”  In _Ccomputer Science Logic 2017_ , 2017  DOI: 10.4230/LIPIcs.CSL.2017.39

##  Appendix A Appendix

We detail some technical proofs. We use $::$ to denote list concatenation. If
we have $\gamma_{1}\vdash t_{1}:a_{1},\dots,\gamma_{k}\vdash t_{k};a_{k}$ we
will abuse the language and often abbreviate with
$\vec{\gamma}\vdash\vec{t}:\vec{a}.$ We denote by $\lvert\gamma\rvert$ the set
of variables appearing in $\gamma.$ We denote by $\gamma(x)$ the index of $x$
in $\gamma$ given by the linear order.

##  Appendix B Multicategories and Signatures

#### Multicategories

######  Definition B.1.

A _morphism_ of multigraphs $\mathcal{F}:\mathcal{G}\to\mathcal{H}$ is the
collection of the following data:

  * •

A function $\mathcal{F}_{0}:\mathcal{G}_{0}\to\mathcal{H}_{0}.$

  * •

For every $a_{1},\dots,a_{n},b\in\mathcal{G}_{0},$ a family of maps

$\mathcal{F}_{a_{1},\dots,a_{n},b}:\mathcal{G}(a_{1},\dots,a_{n},b)\to\mathcal{H}(\mathcal{F}_{0}(a_{1}),\dots,\mathcal{F}_{0}(a_{n}),\mathcal{F}_{0}(b))$

We shall just wrote $\mathcal{F}(A),\mathcal{F}(s)$ for the action of a
morphisms over nodes and edges. We shall write $s:a_{1},\dots,a_{n}\to
b,\mathsf{source}(s)=a_{1},\dots,a_{n},\mathsf{trg}(s)=b$ meaning that $s\in
G(a_{1},\dots,a_{n},b).$

######  Definition B.2.

A _functor_ of multicategories $\mathsf{F}:\mathsf{M}\to\mathsf{M}^{\prime}$
consists of a morphisms of multigraphs that preserves composition and
identities.

  1. 1.

A _representable functor_ between representable multicategories is a functor
$\mathsf{F}:\mathsf{M}\to\mathsf{M}^{\prime}$ s.t.
$\mathsf{F}(a_{1}\otimes_{\mathsf{M}}\dots\otimes_{\mathsf{M}}a_{k})=(\mathsf{F}(a_{1})\otimes_{\mathsf{M}^{\prime}}\dots\otimes_{\mathsf{M}^{\prime}}\mathsf{F}(a_{k}))$
and
$\mathsf{F}(\mathsf{re}^{\mathsf{M}}_{a_{1},\dots,a_{k}})=\mathsf{re}^{\mathsf{M}^{\prime}}_{\mathsf{F}(a_{1}),\dots,\mathsf{F}(a_{k})}.$

  2. 2.

A _symmetric_ functor between symmetric multicategories is a functor
$\mathsf{F}:\mathsf{M}\to\mathsf{M}^{\prime}$ s.t.
$\mathsf{F}(s\cdot\sigma)=\mathsf{F}(s)\cdot\sigma.$

  3. 3.

A _closed_ functor between closed multicategories is a functor
$\mathsf{F}:\mathsf{M}\to\mathsf{M}^{\prime}$ s.t.
$\mathsf{F}((a_{1}\otimes_{\mathsf{M}}\dots\otimes_{\mathsf{M}}a_{k})\multimap_{\mathsf{M}}a)=(\mathsf{F}(a_{1})\otimes_{\mathsf{M}^{\prime}}\dots\otimes_{\mathsf{M}^{\prime}}\mathsf{F}(a_{k}))\multimap_{\mathsf{M}^{\prime}}\mathsf{F}(a)$
and
$\mathsf{F}(ev_{a_{1},\dots,a_{k},a})=ev_{\mathsf{F}(a_{1}),\dots,\mathsf{F}(a_{k}),\mathsf{F}(a)}.$

#### Monoidal vs Representable

We discuss an adjunction between the 2-category $\mathsf{Mon}$ of monoidal
categories, strong monoidal functors and monoidal natural transformations and
the 2-category $\mathsf{rep}$ of representable multicategories, representable
functors and representable multinatural transformations. We shall also show
how this adjunction lift to the symmetric case.

Given a monoidal category $(\mathit{M},\otimes,I)$ we shall define a
representable multicategory $\mathsf{rep}(\mathit{M})\in\mathsf{rep}$ by
exploiting its monoidal structure. Given $a_{1}.\dots,a_{k}\in\mathit{M},$ let
$(a_{1}\otimes\dots\otimes a_{k}):=(\dots(a_{1}\otimes
a_{2})\otimes\dots)\otimes a_{k}$ for $k>0$ and $(a_{1}\otimes\dots\otimes
a_{k}):=I$ for $k=0.$ Then we fix
$\mathsf{rep}(\mathit{M})(a_{1},\dots,a_{n},a)=\mathit{M}((a_{1}\otimes\dots\otimes
a_{n}),a).$ composition is defined as follows: given
$f_{1}\in\mathsf{rep}(\mathit{M})(\gamma_{1},b_{1}),\dots,f_{1}\in\mathsf{rep}(\mathit{M})(\gamma_{n},b_{n})$
and $f\in\mathsf{rep}(\mathit{M})(b_{1},\dots,b_{n},a),$ we set

$f\circ\langle f_{1},\dots,f_{n}\rangle:=f\circ((f_{1}\otimes\cdots\otimes
f_{n})\circ\alpha)$

where $\alpha$ is an appropriate choice of isomorphism built out of the
associators in $\mathit{M}.$ The former construction can be extended to the
symmetric case in the natural way, by defining symmetries of
$\mathsf{symon}(\mathit{M})$ via the right action of permutations on
representable maps, i.e. $\sigma_{a,b}:b\otimes a\to a\otimes
b:={\mathsf{let}(\mathsf{re}_{a,b})}\cdot{\sigma}.$

Given a multicategory $\mathsf{M},$ we shall define a monoidal category
$\mathsf{mon}(\mathsf{M})$ as follows. We set
$\mathrm{ob}(\mathsf{mon}(\mathsf{M}))=\mathrm{ob}(\mathsf{M})$ and
$\mathsf{mon}(\mathsf{M})(a,b)=\mathsf{M}(a,b).$ Composition and identities
are then inherited. The tensor product is given by the binary tensors of
$\mathsf{M},$ the unit is the 0-ary tensor $().$ The tensor on morphisms is
defined as $f\otimes g=\mathsf{re}\circ\langle f,g\rangle.$ The associators
$\alpha_{a,b,c}:(a\otimes b)\otimes c\cong a\otimes(b\otimes c)$ are given by
the maps $\mathsf{let}_{(a\otimes
b),c}(\mathsf{let}_{a,b}(\mathsf{re}_{a,(b\otimes c)})).$

#### Signatures

Let $\langle\mathsf{At},\mathcal{N}\rangle$ be either a representable or a
closed signature. We denote by $\mathsf{aut}(\mathcal{N})$ the autonomous
signature generated from $\mathcal{N},$ whose node are freely generated on
$\mathsf{At}$ as follows:

$\mathsf{aut}(\mathcal{N})_{0}\ni
a::=o\in\mathsf{At}\mid(a_{1}\otimes\dots\otimes
a_{k})\mid(a_{1}\otimes\dots\otimes a_{k})\multimap a\quad(k\in\mathbb{N}).$

We remark that we have a structure-preserving injective function
$\iota:\mathcal{N}_{0}\hookrightarrow\mathsf{aut}(\mathcal{N})_{0}.$ Then we
set

$\mathsf{aut}(\mathcal{N})(\gamma,a)=\begin{cases}\mathcal{N}(\gamma^{\prime},a^{\prime})&\text{
if }\gamma=\iota(\gamma^{\prime}),\quad a=\iota(a^{\prime});\\\
\emptyset&\text{ otherwise.}\end{cases}$

We get and evident structure-preserving embedding
$\mathcal{N}\hookrightarrow\mathsf{aut}(\mathcal{N}).$

##  Appendix C  (Symmetric) Representable Resource Terms

###  C.1 Representable Case

#### Substitution and Reduction

######  Definition C.1.

Let $s\in\mathsf{\Lambda_{rep}}$ and $x_{1},\ dots,x_{k}\in\mathcal{V}.$ We
define the list of _occurrences_ of $x_{1},\dots,x_{k}s$ in $s$ by induction
as follows:

$\mathsf{occ}_{\vec{x}}(x)=\begin{cases}x&\text{ if }x\in\vec{x};\\\
\langle\rangle&\text{
otherwise.}\end{cases}\qquad\mathsf{occ}_{\vec{x}}(\langle
s_{1},\dots,s_{k}\rangle)=\bigoplus\mathsf{occ}_{\vec{x}}(s_{i})$
$\mathsf{occ}_{\vec{x}}(s[\vec{y}:=u])=\mathsf{occ}_{\vec{x}}(s)::\mathsf{occ}_{\vec{x}}(u).$

From now on, whenever we deal with linear substitutions we shall always assume
that they are well-defined, hence the substituted variables are contained in
the free variables of the considered term.

######  Definition C.2 (Representable Linear Substitution).

Let $s,t_{1},\dots,t_{k}\in\mathsf{\Lambda_{rep}}$ and $\
x_{1},\dots,x_{k}\subseteq\mathsf{fv}(s).$ We define the _( $k$-ary linear)
substitution_ of $x_{1},\dots,x_{k}$ by $t_{1},\dots,t_{k}$ in $s$ by
induction as follows:

$x\\{t/x\\}=t\qquad x\\{/\\}=x\quad(\text{ if }k=0)$ $\langle
s_{1},\dots,s_{n}\rangle\\{\vec{t}/\vec{x}\\}=\langle
s_{1}\\{\vec{t}_{1}/\vec{x}_{1}\\},\dots,s_{n}\\{\vec{t}_{n}/\vec{x}_{n}\\}\rangle\quad(\vec{x}=\bigoplus\vec{x}_{i},\vec{t}=\bigoplus\vec{t}_{i}\text{
and }\vec{x}_{i}=\mathsf{occ}_{\vec{x}}(s_{i}))$
$s_{1}[\vec{y}:=s_{2}]\\{\vec{t}/\vec{x}\\}=s_{1}\\{\vec{u}_{1}/\vec{x}_{1}\\}[\vec{y}:=s_{2}\\{\vec{t}_{2}/\vec{x}_{2}\\}]\quad(\vec{x}=\vec{x}_{1}::\vec{x}_{2},\vec{t}=\vec{t}_{1}::\vec{t}_{2}\text{
and }\vec{x}_{i}=\mathsf{occ}_{\vec{x}}(s_{i}).$

We characterize $\beta$-normal forms as follows:

$\mathsf{nf}(\mathsf{\Lambda_{rep}})_{\beta}\ni s::=\langle
s_{1},\dots,s_{k}\rangle[\vec{x}_{1}:=v_{1}]\dots[\vec{x}_{n}:=v_{n}]\mid
v\qquad v:=x[x:=v]$

######  Lemma C.3.

A term $s$ is a $\beta$-normal form iff
$s\in\mathsf{nf}(\mathsf{\Lambda_{rep}})_{\beta}.$

###### Proof.

By induction on $s.$ If $s=\langle s_{1},\dots,s_{k}\rangle$ we have that
$s_{i}$ are $\beta$-normal, we conclude by applying the IH. If
$s=p[\vec{x}:=q]$ then $p$ and $q$ are $\beta$-normal. By IH
$p,q\in\mathsf{nf}(\mathsf{\Lambda_{rep}})_{\beta}.$ We reason by cases on
$q.$ The case $p=\langle
s_{1},\dots,s_{k}\rangle[\vec{x}_{1}:=v_{1}]\dots[\vec{x}_{n}:=v_{n}]$ is not
possible, otherwise we would have a $\beta$-redex. ∎

We consider another inductive set of normal forms:

$\mathsf{nf}(\mathsf{\Lambda_{rep}})^{\prime}_{\beta}\ni
s::=p[\vec{x}_{1}:=x_{1}]\dots[\vec{x}_{n}:=x_{n}]\mid p::=\langle
p_{1},\dots,p_{k}\rangle\mid x$

######  Proposition C.4.

If $s\in\mathsf{nf}(\mathsf{\Lambda_{rep}})_{\beta}$ there exists
$t\in\mathsf{nf}(\mathsf{\Lambda_{rep}})^{\prime}_{\beta}$ s.t. $s\equiv t.$

###### Proof.

By induction on $s.$ If $\langle
s_{1},\dots,s_{k}\rangle[\vec{x}_{1}:=v_{1}]\dots[\vec{x}_{n}:=v_{n}]$ then
$s_{i}$ are $\beta$-normal form. Then we apply the IH and get
$s^{\prime}_{i}\in\mathsf{nf}(\mathsf{\Lambda_{rep}}(\mathcal{R}))^{\prime}$
s.t. $s_{i}\equiv s^{\prime}_{i}$. By definition
$s^{\prime}_{i}=p_{i}[\vec{x}_{i,1}:=x_{i,1}]\dots[\vec{x}_{i,1}:=x_{i,n_{i}}].$
We then set $s^{\prime}=\langle
p_{1},\dots,p_{k}\rangle[\vec{x}_{1,1}:=x_{1,n_{1}}]\dots[\vec{x}_{k,1}:=x_{k,n_{k}}][\vec{x}_{1}:=v_{1}]\dots[\vec{x}_{n}:=v_{n}].$
If $s=x[x:=v]$ by IH we have $v\equiv t$ with
$t^{\prime}=p[\vec{x}_{1}:=x_{1}]\dots[\vec{x}_{n}:=x_{n}]$ with $p=y$,
otherwise we would have a $\beta$-redex. Then we set
$t=x[x:=y][\vec{x}_{1}:=x_{1}]\dots[\vec{x}_{n}:=x_{n}].$ ∎

######  Proposition C.5.

A term $s\in\mathsf{\Lambda_{rep}}(\mathcal{R})$ is a normal form for
$\to_{\mathsf{rep}}$ iff there exists
$s^{\prime}\in\mathsf{nf}(\mathsf{\Lambda_{rep}}(\mathcal{R}))$ s.t. $s\equiv
s^{\prime}.$

###### Proof.

Corollary of the former proposition. ∎

#### Free Construction

######  Definition C.6.

Let $\mathcal{R}$ be a representable signature and $\mathsf{S}$ be a
representable multicategory. Let $i:\mathcal{R}\to\overline{\mathsf{S}}$ be a
map of representable signatures. We define a family of maps
$\mathsf{RT}(i)_{\gamma,a}:\mathsf{\Lambda_{rep}}(\mathcal{R})(\gamma;a)\to\mathsf{S}(i(\gamma);i(a))$
by induction as follows:

$\mathsf{RT}(i)_{a,a}(x)=id_{i(a)}\qquad\mathsf{RT}(i)_{\gamma_{1},\dots,\gamma_{k},(a_{1}\otimes\dots\otimes
a_{k})}(\langle
s_{1},\dots,s_{k}\rangle)=\bigotimes_{i=1}^{k}\mathsf{RT}(i)_{\gamma_{i},a_{i}}(s_{i})$
$\mathsf{RT}(i)_{\delta_{1},\gamma,\delta_{2},a}(s[x_{1},\dots,x_{k}:=t])=\mathsf{let}(\mathsf{RT}(i)_{\delta_{1},a_{1},\dots,a_{k},\delta_{2},a}(s))\circ\langle
id_{\delta_{1}},\mathsf{RT}(i)_{\gamma,(a_{1}\otimes\dots\otimes
a_{k})}(t),id_{\delta_{2}}\rangle$
$\mathsf{RT}(i)_{\gamma_{1},\dots,\gamma_{n},a}(f(s_{1},\dots,s_{n}))=i(f)\circ\langle\mathsf{RT}(i)(s_{1}),\dots,\mathsf{RT}(i)(s_{n})\rangle.$

We recall that in a representable category, $f\otimes g$, with $\gamma\vdash
f:a,\delta\vdash g:b$ is defined via the maps
$\mathsf{re}_{a,b}:a,b\to(a\otimes b)$ as $\mathsf{re}_{a,b}\circ\langle
f,g\rangle.$ We have that $\mathsf{re}_{a,b}\circ\langle f\circ
f^{\prime},g\circ g^{\prime}\rangle=(\mathsf{re}_{a,b}\circ\langle
f,g\rangle)\circ\langle f^{\prime},g^{\prime}\rangle$ by associativity of
composition. We shall constantly abbreviate
$\langle\mathsf{RT}_{\gamma_{i},a_{i}}(t_{i})\rangle_{i\in\mathsf{len}(\gamma)}$
as $\mathsf{RT}_{\vec{\gamma},\vec{a}}(\vec{t}).$

######  Proposition C.7.

The following statements hold.

  1. 1.

$\mathsf{RT}_{\vec{\gamma},a}(s\\{\vec{t}/\vec{x}\\})=\mathsf{RT}_{\gamma,a}(s)\circ\langle\mathsf{RT}_{\gamma_{i},a_{i}}(t_{i})\rangle_{i\in\mathsf{len}(\gamma)}.$

  2. 2.

If $s\to_{\mathsf{rep}}s^{\prime}$ then
$\mathsf{RT}_{\gamma,a}(s)=\mathsf{RT}_{\gamma,a}(s^{\prime}).$

  3. 3.

If $s=_{\mathsf{rep}}s^{\prime}\text{ or }s\equiv s^{\prime}$ then
$\mathsf{RT}_{\gamma,a}(s)=\mathsf{RT}_{\gamma,a}(s^{\prime}).$

  4. 4.

If $s\equiv s^{\prime}$ then
$\mathsf{RT}_{\gamma,a}(s)=\mathsf{RT}_{\gamma,a}(s^{\prime}).$

###### Proof.

  1. 1.

By induction on $s.$ If $s=x$ then $\vec{t}=t$ and $s\\{\vec{t}/\vec{x}\\}=t.$
Then we have
$\mathsf{RT}_{\vec{\gamma},a}(s\\{\vec{t}/\vec{x}\\})=\mathsf{RT}_{\gamma,a}(t)=id\circ\mathsf{RT}_{\gamma,a}(t).$
If $s=\langle s_{1},\dots,s_{k}\rangle$ with
$\delta_{i}^{1},\vec{x}_{i},\delta_{i}^{2}\vdash s_{i}:a_{i}$ with
$\vec{x}=\bigoplus\vec{x}_{i}.$ Then $s\\{\vec{t}/\vec{x}\\}=\langle
s_{1}\\{\vec{t}_{1}/\vec{x}_{1}\\},\dots,s_{k}\\{\vec{t}_{k}/\vec{x}_{k}\\}\rangle.$
By IH we have that
$\mathsf{RT}_{\delta_{i}^{1},\vec{\gamma},\delta_{i}^{2},a}(s_{i}\\{\vec{t}_{i}/\vec{x}_{i}\\})=\mathsf{RT}_{\delta_{i}^{1},\vec{a}_{i},\delta_{i}^{2},a}(s_{i})\circ\mathsf{RT}_{\vec{\gamma}_{i},\vec{a}}(\vec{t}_{i}).$
By associativity of composition, we have

$\bigotimes\left(\mathsf{RT}_{\delta_{i}^{1},\vec{a}_{i},\delta_{i}^{2},a}(s_{i})\circ\mathsf{RT}_{\vec{\gamma}_{i},\vec{a}}(\vec{t}_{i})\right)=\left(\bigotimes\mathsf{RT}_{\delta_{i}^{1},\vec{a}_{i},\delta_{i}^{2},a}(s_{i})\right)\circ\mathsf{RT}_{\vec{\gamma},\vec{a}}(\vec{t}).$

We can then conclude. If $s=p[\vec{y}:=q]$ then
$s\\{\vec{t}/\vec{x}\\}=p\\{\vec{t}_{1}/\vec{x}_{1}\\}[\vec{y}:=q\\{\vec{t}_{2}/\vec{x}_{2}\\}]$
with $\delta_{1},\vec{x}_{1}:\vec{a}_{1},\vec{y}:\vec{b},\delta_{3}\vdash p:a$
and $\vec{x}_{2}:\vec{a}_{2},\zeta\vdash q:\vec{b}.$

  2. 2.

By induction on $s\to_{\mathsf{rep}}s^{\prime}.$ If it is a $\beta$ step, then
it’s a direct corollary of the former point of this lemma. If
$s\to_{\mathsf{rep}}\vec{x}[\vec{x}:=s],$ we have that
$\mathsf{RT}_{\gamma,a}(\vec{x}[\vec{x}:=s])=(\mathsf{let}(\mathsf{re}))\circ
s.$ We observe that $(\mathsf{let}(\mathsf{re}))$ is the identity morphism; we
can then conclude. The contextual cases are a direct application of the IH.

  3. 3.

If $s=_{\mathsf{rep}}s^{\prime}$, we observe that there exists
$n\in\mathbb{N}$ s.t. $s=s_{0}\leftrightarrow
s_{1}\leftrightarrow\dots\leftrightarrow s_{n}=s^{\prime}$ where
$\leftrightarrow$ stands for the reflexive and symmetric closure of
$\to_{\mathsf{rep}}.$ We prove the result by induction on $n.$ If $n=0$ the
result is a direct corollary of the former point of the lemma. If $n=p+1$ the
result is a direct corollary of the IH.

  4. 4.

If $s\equiv s^{\prime},$ the result is by induction on the judgment $s\equiv
s^{\prime}.$ If $\langle
s_{1},\dots,s_{i}[\vec{x}:=t],\dots,s_{k}\rangle\equiv\langle
s_{1},\dots,s_{i}[,\dots,s_{k}\rangle\vec{x}:=t]$ we have that

$\mathsf{RT}_{\gamma_{1},\dots,\gamma_{k},\langle
a_{1},\dots,a_{k}\rangle}(\langle
s_{1},\dots,s_{i}[\vec{x}:=t],\dots,s_{k}\rangle)=$
$\mathsf{RT}_{\gamma_{1},a_{1}}(s_{1})\otimes\dots\mathsf{RT}_{\gamma_{i},a_{i}}(s_{i}[\vec{x}:=t])\otimes\dots\otimes\mathsf{RT}_{\gamma_{k},a_{k}}(s_{k})$

then we can conclude by associativity of the composition. A similar argument
can be applied to the other ground steps for structural equivalence. The
contextual cases are a direct application of the IH.

∎

######  Theorem C.8 (Free Construction).

Let $\mathsf{S}$ be a a representable multicategory and
$i:\mathcal{R}\to\overline{\mathsf{S}}$ a map of representable signatures.
There exists a unique representable functor
$i^{\ast}:\mathsf{RM}(\mathcal{R})\to\mathsf{S}$ such that
$i=\overline{i^{\ast}}\circ\eta_{\mathcal{R}}.$

###### Proof.

The functor is defined exploiting Definition 3.14. By the former proposition,
$\iota^{\star}$ is well-defined and preserves composition and the identities.
Given another functor $i^{\prime}:\mathsf{RM}(\mathcal{R})\to\mathsf{S}$ s.t.
$i=\overline{i^{\prime}}\circ\eta_{\mathcal{R}},$ one proves that
$i^{\ast}=i^{\prime}$ pointwise, exploiting the fact that $i^{\prime}$ has to
preserve the representable structure.∎

#### Coherence

######  Lemma C.9.

Let $\langle\mathsf{At},\mathcal{R}\rangle$ be a discrete signature. We have
that $\mathsf{mon}(\mathsf{RM}(\mathcal{R}))$ is the free monoidal category on
$\mathsf{At}.$

###### Proof.

the map $\mathsf{At}\to\mathrm{ob}(\mathsf{mon}(\mathsf{RM}(\mathcal{R})))$ is
trivial. Given a monoidal category $\mathit{M},$ the functor
$i^{\ast}:\mathsf{mon}(\mathsf{RM}(\mathcal{R})\to\mathsf{M}$ is build out of
Definition C.6. Uniqueness is proved pointwise. ∎

######  Lemma C.10.

Let $\gamma,\gamma^{\prime}$ be atomic contexts. If there exists a type $a$
and normal terms $s,s^{\prime}$ such that
$s,s^{\prime}\in\mathsf{nf}(\mathsf{\Lambda_{rep}}(\mathcal{R}))(\gamma;a)$
then $\gamma=\gamma^{\prime}$ and $s=s^{\prime}.$

###### Proof.

by induction of $a.$ We remark that the terms $s.s^{\prime}$ cannot be
substitution, since the contexts are atomic. If $a=o,$ since $s,s^{\prime}$
are normal, then $s=x=s^{\prime}.$ If $a=\langle a_{1},\dots,a_{k}\rangle$,
since $\gamma,\gamma^{\prime}$ are atomic, by definition $s=\langle
s_{1},\dots,s_{k}\rangle,s^{\prime}=\langle
s^{\prime}_{1},\dots,s^{\prime}_{k}\rangle$. By definition, we have
$\gamma_{i}\vdash s_{i}:a_{i}$ and $\gamma^{\prime}_{i}\vdash
s^{\prime}_{i}:a_{i}$ for $i\in[k].$ Moreover,
$\gamma=\gamma_{1},\dots,\gamma_{k}$ and
$\gamma^{\prime}=\gamma^{\prime}_{1},\dots,\gamma^{\prime}_{k}.$ By IH,
$\gamma_{i}=\gamma^{\prime}_{i}$ and $s_{i}=s^{\prime}_{i}.$ We can then
conclude. ∎

###  C.2 Symmetric Case

#### Type System

######  Proposition C.11 (Canonicity of Typing).

If $\pi\triangleright\gamma\vdash s:a$ and
$\pi^{\prime}\triangleright\gamma\vdash s:a^{\prime}$ then $a=a^{\prime}$ and
$\pi=\pi^{\prime}.$

###### Proof.

Corollary of Propositions E.1 and E.3.∎

#### Coherence

######  Theorem C.12.

Let $s\in\mathsf{nf}(\mathsf{\Lambda_{reps}}(\mathcal{R}))(\gamma,a).$ There
exists a unique $\sigma\in\mathsf{Stab}((\mathsf{strict}(\gamma))$ and a
unique non-symmetric representable normal term $t$ such that $s=t^{\sigma}.$

###### Proof.

If $s=x$ the result is immediate. If $s=\langle s_{1},\dots,s_{k}\rangle$ with
$\gamma={(\gamma_{1},\dots,\gamma_{k})}\cdot{\sigma}\vdash\langle
s_{1},\dots,s_{k}\rangle:(a_{1}\otimes\dots\otimes a_{k})$ and $\gamma$ being
atomic, by IH we have unique
$\sigma_{1},\dots,\sigma_{k}\in\mathsf{St}(\mathsf{strict}(\gamma_{i}))$ and
$t_{1},\dots,t_{k}\in\mathsf{nf}(\mathsf{\Lambda_{rep}}(A))$ s.t.
$s_{i}=t_{i}^{\sigma_{i}}$ for $i\in[k].$ Then, by definition, $s=\langle
t_{1},\dots,t_{k}\rangle^{\sigma\circ(\sigma_{1}\otimes\dots\otimes\sigma_{k})}.$
Uniqueness derives by Proposition C.11. If
$s=p[\vec{x}_{1}:=x_{1}]\dots[\vec{x}_{n}:=x_{n}],$ By IH there exists unique
$\sigma$ and $t$ s.t. $p=t^{\sigma}.$ Then we can conclude by the fact that
the action of $\sigma$ on variables is fixedpoint-free. 4.2. ∎

##  Appendix D Symmetric Closed Case

#### Substitution and Reduction

######  Definition D.1.

Let $s\in\mathsf{\Lambda_{\mathsf{sc}}}$ and $x_{1},\
\dots,x_{k}\in\mathcal{V}.$ We define the list of _occurrences_ of
$x_{1},\dots,x_{k}s$ in $s$ by induction as follows:

$\mathsf{occ}_{\vec{x}}(x)=\begin{cases}x&\text{ if }x\in\vec{x};\\\
\langle\rangle&\text{
otherwise.}\end{cases}\qquad\mathsf{occ}_{\vec{x}}(s\langle
s_{1},\dots,s_{k}\rangle)=\mathsf{occ}_{\vec{x}}(s)\oplus\bigoplus\mathsf{occ}_{\vec{x}}(s_{i})$
$\mathsf{occ}_{\vec{x}}(\lambda\vec{y}.s)=\mathsf{occ}_{\vec{x}}(s).$

######  Definition D.2 (Linear Substitution).

Let $s,t_{1},\dots,t_{k}\in\mathsf{\Lambda_{rep}}$ and $\
x_{1},\dots,x_{k}\subseteq\mathsf{fv}(s).$ We define the _( $k$-ary linear)
substitution_ of $x_{1},\dots,x_{k}$ by $t_{1},\dots,t_{k}$ in $s$ by
induction as follows:

$x\\{t/x\\}=t\qquad x\\{/\\}=x\quad(\text{ if }k=0)$ $s_{0}\langle
s_{1},\dots,s_{n}\rangle\\{\vec{t}/\vec{x}\\}=s_{0}\\{\vec{t}_{0}/\vec{x}_{0}\\}\langle
s_{1}\\{\vec{t}_{1}/\vec{x}_{1}\\},\dots,s_{n}\\{\vec{t}_{n}/\vec{x}_{n}\\}\rangle\quad(\vec{x}=\bigoplus\vec{x}_{i},\vec{t}=\bigoplus\vec{t}_{i}\text{
and }\vec{x}_{i}=\mathsf{occ}_{\vec{x}}(s_{i}))$
$\lambda\vec{y}.s\\{\vec{t}/\vec{x}\\}=\begin{cases}\lambda\vec{y}.s\\{\vec{t}/\vec{x}\\}&\text{
if }\vec{x}\cap\vec{y}=\emptyset;\\\ \lambda\vec{y}.s&\text{
otherwise.}\end{cases}$

#### Free Construction

######  Definition D.3.

Let $\mathsf{E}$ be a symmetric closed multicategory and let
$i:\mathcal{L}\to\overline{\mathsf{E}}$ be a map of closed signatures. We
define a family of maps
$\mathsf{RT}_{\gamma,a}:\mathsf{\Lambda_{\mathsf{sc}}}(\mathcal{L})(\gamma,a)\to\mathsf{E}(i(\gamma),i(a))$
by induction as follows:

$\mathsf{RT}_{a,a}(x)=1_{i(a)}\qquad\mathsf{RT}_{\gamma,\vec{a}\multimap
a}(\lambda\vec{x}.s)=\lambda(\mathsf{RT}_{\gamma,\vec{a},a}(s))$
$\mathsf{RT}_{(\gamma_{0},\dots,\gamma_{k}),a}(s\langle
t_{1},\dots,t_{k}\rangle)=(ev\circ\langle\mathsf{RT}_{\gamma_{0},\langle
a_{1},\dots,a_{k}\rangle\multimap
a}(s),\mathsf{RT}_{\gamma_{1},a_{1}}(t_{1}),\dots,\mathsf{RT}_{\gamma_{k},a_{1}}(t_{k})\rangle)\cdot\sigma.$

######  Proposition D.4.

The following statements hold.

  1. 1.

$\mathsf{RT}_{\vec{\gamma},a}(s\\{\vec{t}/\vec{x}\\})=\mathsf{RT}_{\gamma,a}(s)\circ\langle\mathsf{RT}_{\gamma_{i},a_{i}}(t_{i})\rangle_{i\in\mathsf{len}(\gamma)}.$

  2. 2.

If $s\to_{\mathsf{sc}}s^{\prime}$ then
$\mathsf{RT}_{\gamma,a}(s)=\mathsf{RT}_{\gamma,a}(s^{\prime}).$

  3. 3.

If $s=_{\mathsf{sc}}s^{\prime}$ then
$\mathsf{RT}_{\gamma,a}(s)=\mathsf{RT}_{\gamma,a}(s^{\prime}).$

###### Proof.

  1. 1.

By induction on $s.$ If $s=x$ the proof is the same as in Proposition C.7. If
$s=s_{0}\langle s_{1},\dots,s_{l}\rangle$ with
$(\delta_{0}^{1},\dots,\delta^{2}_{l})\cdot\sigma\vdash
s:a,\delta_{0}^{1},\vec{x}_{0}:\vec{a}_{0},\delta_{0}^{2}\vdash s_{0}:\langle
b_{1},\dots,b_{l}\rangle\multimap
a,\delta_{i}^{1},\vec{x}_{i}:\vec{a}_{i},\delta_{i}^{2}\vdash s_{i}:b_{i}$
with
$\left(\bigoplus\vec{x}_{i}\right)\cdot\sigma=x_{1},\dots,x_{k},\left(\bigoplus\vec{a}_{i}\right)\cdot\sigma=a_{1},\dots,a_{k}.$
By definition $s\\{\vec{t}/\vec{x}\\}=\langle
s\\{\vec{t}_{1}/\vec{x}_{1}\\},\dots,s_{l}\\{\vec{t}_{l}/\vec{x}_{l}\\}\rangle.$
We can then apply the IH and conclude by associativity of composition. The
abstraction case is a corollary of the IH and naturality of $\lambda(-)$.

  2. 2.

By induction on the step. If it is $\beta,$ then it is a corollary of the
former point of this lemma. If it is
$\eta,s\to_{\mathsf{sc}}\lambda\vec{x}.s\vec{x},$ we have that
$\mathsf{RT}_{\gamma,\vec{a}\multimap
a}(\lambda\vec{x}.s\vec{x})=\lambda(ev\circ\langle s,id\rangle).$ We can
conclude since $\lambda$ is the inverse of $ev\circ\langle-,id\rangle.$ The
contextual cases are a direct application of the IH.

  3. 3.

If $s_{\mathsf{sc}}s^{\prime}$, we observe that there exists $n\in\mathbb{N}$
s.t. $s=s_{0}\leftrightarrow s_{1}\leftrightarrow\dots\leftrightarrow
s_{n}=s^{\prime}$ where $\leftrightarrow$ stands for the reflexive and
symmetric closure of $\to_{\mathsf{sc}}.$ We prove the result by induction on
$n.$ If $n=0$ the result is a direct corollary of the former point of the
lemma. If $n=p+1$ the result is a direct corollary of the IH.

∎

######  Theorem D.5 (Free Construction).

Let $\mathsf{S}$ be a a symmetric closed multicategory and
$i:\mathcal{L}\to\overline{\mathsf{S}}$ a map of representable signatures.
There exists a unique symmetric closed functor
$i^{\ast}:\mathsf{SCM}(\mathcal{L})\to\mathsf{S}$ such that
$\overline{i^{\ast}}\circ\eta_{\mathcal{L}}=i.$

###### Proof.

The functor is defined exploiting Definition D.3. By the former proposition,
$i^{\star}$ is well-defined and preserves composition and the identities.
Given another functor $i^{\prime}:\mathsf{RM}(\mathcal{R})\to\mathsf{S}$ s.t.
$i=\overline{i^{\prime}}\circ\eta_{\mathcal{R}},$ one proves that
$i^{\ast}=i^{\prime}$ pointwise, exploiting the fact that $i^{\prime}$ has to
preserve the representable structure.∎

##  Appendix E Autonomous Case

######  Proposition E.1.

We have an embedding (injective map preserving the inductive structure and
substitution)
$\iota_{\spadesuit}:\mathsf{\Lambda}_{\spadesuit}(\mathcal{N})(\gamma;a)\hookrightarrow\mathsf{\Lambda_{aut}}(\mathsf{aut}(\mathcal{N}))(\gamma;a)$
for $\spadesuit\in\\{\mathsf{re},\mathsf{reps},\mathsf{sc}\\}$.

We treat these embeddings as they were inclusions. The embeddings concerns
also type derivations, meaning that we will identify representable or closed
type derivations with appropriate autonomous ones. Given a term $\gamma\vdash
t:a,$ there is a unique type derivation for it.

#### Type System

######  Definition E.2.

Let $s$ be an autonomous term. We define the set of its _subterms_ by
induction on $s$ as follows.

$\mathsf{ST}(x)=\\{x\\}\qquad\mathsf{ST}(\lambda\vec{x}.s)=\\{\lambda\vec{y}.s^{\prime}\mid
s^{\prime}\in\mathsf{ST}(s)\\}\sqcup\\{\lambda\vec{x}.s\\}$
$\mathsf{ST}(\langle
s_{1},\dots,s_{k}\rangle)=\bigsqcup_{i\in[k]}\mathsf{ST}(s_{i})\sqcup\\{\langle
s_{1},\dots,s_{k}\rangle\\}$
$\mathsf{ST}(pq)=\mathsf{ST}(p)\sqcup\mathsf{ST}(q)\sqcup\\{pq\\}\qquad\mathsf{ST}(s[\vec{x}:=t])=\mathsf{ST}(s)\sqcup\mathsf{ST}(t)\sqcup\\{s[\vec{x}:=t]\\}$

######  Proposition E.3 (Canonicity of Typing).

If $\pi\triangleright\gamma\vdash s:a$ and
$\pi^{\prime}\triangleright\gamma\vdash s:a^{\prime}$ then $a=a^{\prime}$ and
$\pi=\pi^{\prime}.$

###### Proof.

by induction on $s.$ In the cases where a merging of type contexts happens,
such as the list case, we rely on the properties of shuffle permutations and
on the fact that type contexts are _linear_. Hence, the action of permutations
on contexts is always fixedpoint-free. We prove the list case. Let $s=\langle
s_{1},\dots,s_{k}\rangle,$ with the following type derivations:

$\pi=\prooftree\hypo{\pi_{i}}\ellipsis{}{\gamma_{i}\vdash
s_{i}:a_{i}}\hypo{\sigma\in\mathsf{shu}(\gamma_{1},\dots,\gamma_{k})}\infer
2{{(\gamma_{1},\dots,\gamma_{k})}\cdot{\sigma}\vdash\langle
s_{1},\dots,s_{k}\rangle:\langle
a_{1},\dots,a_{k}\rangle}\qquad\pi^{\prime}=\prooftree\hypo{\pi^{\prime}_{i}}\ellipsis{}{\gamma^{\prime}_{i}\vdash
s_{i}:a^{\prime}_{i}}\hypo{\sigma^{\prime}\in\mathsf{shu}(\gamma^{\prime}_{1},\dots,\gamma^{\prime}_{k})}\infer
2{{(\gamma^{\prime}_{1},\dots,\gamma^{\prime}_{k})}\cdot{\sigma^{\prime}}\vdash\langle
s_{1},\dots,s_{k}\rangle:\langle a^{\prime}_{1},\dots,a^{\prime}_{k}\rangle}$

with
${(\gamma_{1},\dots,\gamma_{k})}\cdot{\sigma}={(\gamma^{\prime}_{1},\dots,\gamma^{\prime}_{k})}\cdot{\sigma^{\prime}}.$
We prove that $\gamma_{i}=\gamma^{\prime}_{i}$ for all $i\in[k].$ We know that
$\lvert\gamma_{i}\rvert=\lvert\gamma^{\prime}_{i}\rvert,$ since the variables
appearing in both contexts are _exactly_ the free variables of $s_{i},$ by
linearity. By contradiction, suppose that $\gamma_{i}\neq\gamma^{\prime}_{i}.$
This means that for some $x,y\in\lvert\gamma_{i}\rvert,$ we have that
$\gamma_{i}(x)<\gamma_{i}(y)$ and
$\gamma^{\prime}_{i}(y)<\gamma^{\prime}_{i}(x)$ or
$\gamma_{i}(y)<\gamma_{i}(x)$ and
$\gamma^{\prime}_{i}(x)<\gamma^{\prime}_{i}(y).$ However, $\sigma$ and
$\sigma^{\prime}$ are shuffles, meaning that if $\gamma_{i}(x)<\gamma_{i}(y)$
or $\gamma^{\prime}_{i}(x)<\gamma^{\prime}_{i}(y)$ then
$\sigma(\gamma_{i}(x))<\sigma(\gamma_{i}(y))$ and
$\sigma(\gamma^{\prime}_{i}(x))<\sigma(\gamma^{\prime}_{i}(y)),$
contradiction. Hence $\gamma_{i}=\gamma_{j}$ and $\sigma=\sigma^{\prime},$
being the action of permutation fixedpoint-free, since the contexts have no
repetitions of variables. We can the apply the IH, get
$\pi_{i}=\pi^{\prime}_{i}$ and conclude. ∎

#### Substitution and Reduction

$\displaystyle\mathtt{C}::=[\cdot]\mid\langle
s_{1},\dots,\mathtt{C},\dots,s_{n}\rangle\mid\mathtt{C}[\vec{x}:=t]\mid
s[\vec{x}:=\mathtt{C}]\mid\mathtt{C}s\mid
s\mathtt{C}\mid\lambda\vec{x}.\mathtt{C}\mid
f(s_{1},\dots,\mathtt{C},\dots,s_{n})$
$\displaystyle\mathtt{E}::=[\cdot]\mid\langle
s_{1},\dots,\mathtt{E},\dots,s_{n}\rangle\mid\mathtt{E}[\vec{x}:=s]\mid
s[\vec{x}:=\mathtt{E}]\quad(\mathtt{E}\neq[\cdot])\mid\mathtt{E}s\mid
s\mathtt{E}\mid\lambda\vec{x}.\mathtt{E}\mid
f(s_{1},\dots,\mathtt{E},\dots,s_{n})$
$\displaystyle\mathsf{D}::=[\cdot]\mid\langle
s_{1},\dots,\mathsf{D},\dots,s_{n}\rangle\mid\mathsf{D}[\vec{x}:=s]\mid
s[\vec{x}:=\mathsf{D}]\mid
s\mathsf{D}\mid\mathsf{D}t\quad(\mathsf{D}\neq[\cdot])\mid\lambda\vec{x}.\mathsf{D}\mid
fs_{1},\dots,\mathsf{D},\dots,s_{n})$
$\displaystyle\mathtt{L}::=[\cdot]\mid\mathtt{L}[\vec{x}:=t]$ Figure 7:
Autonomous contexts with hole. $\displaystyle\text{\emph{$\beta_{1}$ Root-
Step}: }s[x^{a_{1}}_{1},\dots,x^{a_{k}}_{k}:=\mathtt{L}[\langle
t_{1},\dots,t_{k}\rangle]]\to_{\beta
1}\mathtt{L}[s\\{t_{1},\dots,t_{k}/x_{1},\dots,x_{k}\\}]$
$\displaystyle\text{\emph{$\beta_{2}$ Root-Step}: }\mathtt{L}[\lambda\langle
x_{1}^{a_{1}},\dots,x_{k}^{a_{k}}\rangle.s]\langle
t_{1},\dots,t_{k}\rangle\to_{\beta
2}\mathtt{L}[s\\{t_{1},\dots,t_{k}/x_{1},\dots,x_{k}\\}].$
$\displaystyle\text{\emph{$\eta_{1}$ Root-Step}: }s\to_{\eta
1}\vec{x}[\vec{x}^{\vec{a}}:=s]\qquad\text{where }\vec{x}\text{ fresh },\
\gamma\vdash s:\vec{a},\ s\notin\mathsf{LT}.$
$\displaystyle\text{\emph{$\eta_{2}$ Root-Step}: }s\to_{\eta
2}\lambda\vec{x}^{\vec{a}}.(s\vec{x})\qquad\text{where }\vec{x}\text{ fresh
},\gamma\vdash s:\vec{a}\multimap a,s\notin\mathsf{AT}.$
$\displaystyle\text{\emph{Contextual extensions}:}\prooftree\hypo{s\to_{\beta
1}s^{\prime}}\infer 1{\mathtt{C}[s]\to_{\beta
1}\mathtt{C}[s^{\prime}]}\qquad\prooftree\hypo{s\to_{\beta 2}s^{\prime}}\infer
1{\mathtt{C}[s]\to_{\beta
2}\mathtt{C}[s^{\prime}]}\qquad\prooftree\hypo{s\to_{\eta 1}s^{\prime}}\infer
1{\mathtt{E}[s]\to_{\eta
1}\mathtt{E}[s^{\prime}]}\qquad\prooftree\hypo{s\to_{\eta 2}s^{\prime}}\infer
1{\mathsf{D}[s]\to_{\eta 2}\mathsf{D}[s^{\prime}]}$
$\displaystyle\qquad\qquad{\to_{\beta}}={\to_{\beta 1}\cup\to_{\beta
2}}\qquad{\to_{\eta}}={\to_{\eta 1}\cup\to_{\eta
2}}\qquad{\to_{\mathsf{aut}}}={\to_{\beta}\cup\to_{\eta}}.$
$\displaystyle\text{ \emph{Structural
equivalence}:}\quad\mathtt{C}[s[\vec{x}:=t]]\equiv\mathtt{C}[s][\vec{x}:=t]\qquad\vec{x}\notin\mathsf{fv}(\mathtt{C}).$
Figure 8: Autonomous reduction relations and structural equivalence.

######  Definition E.4.

Let $s\in\mathsf{\Lambda_{aut}}$ and $x_{1},\ dots,x_{k}\in\mathcal{V}.$ We
define the list of _occurrences_ of $x_{1},\dots,x_{k}s$ in $s$ by induction
as follows:

$\mathsf{occ}_{\vec{x}}(x)=\begin{cases}x&\text{ if }x\in\vec{x};\\\
\langle\rangle&\text{
otherwise.}\end{cases}\qquad\mathsf{occ}_{\vec{x}}(\langle
s_{1},\dots,s_{k}\rangle)=\bigoplus\mathsf{occ}_{\vec{x}}(s_{i})$
$\mathsf{occ}_{\vec{x}}(s[\vec{y}:=u])=\mathsf{occ}_{\vec{x}}(s)::\mathsf{occ}_{\vec{x}}(u)\qquad\mathsf{occ}_{\vec{x}}(st)=\mathsf{occ}_{\vec{x}}(s)\oplus\mathsf{occ}_{\vec{x}}(t)\qquad\mathsf{occ}_{\vec{x}}(\lambda\vec{y}.s)=\mathsf{occ}_{\vec{x}}(s).$

From now on, whenever we deal with linear substitutions we shall always assume
that they are well-defined, hence the substituted variables are contained in
the free variables of the considered term.

######  Definition E.5 (Linear Substitution).

Let $s,t_{1},\dots,t_{k}\in\mathsf{\Lambda_{aut}}$ and $\
x_{1},\dots,x_{k}\subseteq\mathsf{fv}(s).$ We define the _( $k$-ary linear)
substitution_ of $x_{1},\dots,x_{k}$ by $t_{1},\dots,t_{k}$ in $s$ by
induction as follows:

$x\\{t/x\\}=t\qquad x\\{/\\}=x\quad(\text{ if }k=0)$ $\langle
s_{1},\dots,s_{n}\rangle\\{\vec{t}/\vec{x}\\}=\langle
s_{1}\\{\vec{t}_{1}/\vec{x}_{1}\\},\dots,s_{n}\\{\vec{t}_{n}/\vec{x}_{n}\\}\rangle\quad(\vec{x}=\bigoplus\vec{x}_{i},\vec{t}=\bigoplus\vec{t}_{i}\text{
and }\vec{x}_{i}=\mathsf{occ}_{\vec{x}}(s_{i}))$
$s_{1}[\vec{y}:=s_{2}]\\{\vec{t}/\vec{x}\\}=s_{1}\\{\vec{u}_{1}/\vec{x}_{1}\\}[\vec{y}:=s_{2}\\{\vec{t}_{2}/\vec{x}_{2}\\}]\quad(\vec{x}=\vec{x}_{1}::\vec{x}_{2},\vec{t}=\vec{t}_{1}::\vec{t}_{2}\text{
and }\vec{x}_{i}=\mathsf{occ}_{\vec{x}}(s_{i})$
$s_{1}s_{2}\\{\vec{t}/\vec{x}\\}=s_{1}\\{\vec{t}_{1}/\vec{x}_{0}\\}s_{2}\\{\vec{t}_{2}/\vec{x}_{2}\\}\quad(\vec{x}=\vec{x}_{1}\oplus\vec{x}_{2},\vec{t}=\vec{t}_{1}\oplus\vec{t}_{2}\text{
and }\vec{x}_{i}=\mathsf{occ}_{\vec{x}}(s_{i}))$
$\lambda\vec{y}.s\\{\vec{t}/\vec{x}\\}=\begin{cases}\lambda\vec{y}.s\\{\vec{t}/\vec{x}\\}&\text{
if }\vec{x}\cap\vec{y}=\emptyset;\\\ \lambda\vec{y}.s&\text{
otherwise.}\end{cases}$

Contexts and reduction relation $\to_{\mathsf{aut}}$, together with its
subreductions $\beta$ and $\eta$ are defined by putting together the
reductions $\to_{\mathsf{rep}}$ (Figure 2) and $\to_{\mathsf{sc}}$ (Figure 5).
The embedding of representable terms and symmetric closed terms into
autonomous ones preserves the reduction.

######  Proposition E.6.

Let $\clubsuit\in\\{\beta,\eta\\},$
$s,s^{\prime}\in\mathsf{\Lambda_{rep}}(\mathcal{R})$ and
$t,t^{\prime}\in\mathsf{\Lambda_{\mathsf{sc}}}(\mathcal{L}).$
$s\to_{\mathsf{rep}}^{\clubsuit}s^{\prime}$ iff
$s\to_{\mathsf{aut}}^{\clubsuit}s^{\prime}$ and
$t\to_{\mathsf{sc}}^{\clubsuit}t^{\prime}$ iff
$t\to_{\mathsf{aut}}^{\clubsuit}t^{\prime}.$

The autonomous reductions are defined in Figure 8. In the structural
equivalence rule, we assume that $\mathtt{C}$ does not bind variables of $t.$
The structural equivalence is defined as the smallest congruence generated by
the rule in Figure 8.

######  Lemma E.7 (Subject Substitution).

Let $\gamma_{i}\vdash t_{i}:a_{i}$ and
$\delta_{1},x_{1}:a_{1},\dots,a_{k},\delta_{2}\vdash s:a.$ We have that
$\delta_{1},\gamma_{1},\dots,\gamma_{k},\delta_{2}\vdash
s\\{t_{1},\dots,t_{k}/x_{1},\dots,x_{k}\\}:a.$

###### Proof.

By induction on the structure of $s.$ The variable case is immediate.

let $s=\lambda\vec{y}.s^{\prime}.$ By definition we have
$\lambda\vec{y}.s^{\prime}\\{\vec{t}/\vec{x}\\}=\lambda\vec{y}.s^{\prime}\\{\vec{t}/\vec{x}\\}.$
We then apply the IH and conclude.

Let $s=\langle s_{1},\dots,s_{k}\rangle$ with $\zeta_{i}\vdash s_{i}:b_{i}$
for $i\in[n]$ and
$\zeta_{1},\dots,\zeta_{n}=\delta_{1},x_{1}:a_{1},\dots,a_{k},\delta_{2}.$
Hence, there exist decompositions
$x_{1},\dots,x_{k}=\vec{x}_{1}::\dots::\vec{x}_{n},a_{1},\dots,a_{k}=\vec{a}_{1}::\dots::\vec{a}_{n}$
and $\vec{x}_{j}\in\mathsf{fv}(s_{j})$ for all $j\in[n]$ s.t.
$\zeta_{j}=(\zeta^{1}_{j},\vec{x}_{j}:\vec{a}_{j},\zeta^{2}_{j})\vdash
s_{j}:b_{j}.$ By IH we have that
$\zeta^{1}_{j},\vec{\gamma}_{j},\zeta^{2}_{j}\vdash
s_{j}\\{\vec{t}_{j}/\vec{x}_{j}\\}:b_{j}.$ By definition of substitution we
have $s\\{\vec{t}/\vec{x}\\}=\langle
s_{1}\\{\vec{t}_{1}/\vec{x}_{1}\\},\dots,s_{n}\\{\vec{t}_{n}/\vec{x}_{n}\\}\rangle$.
Then
$\zeta^{1}_{1},\vec{\gamma}_{1},\zeta^{2}_{1},\dots,\zeta^{1}_{n},\vec{\gamma}_{n},\zeta^{2}_{n}\vdash
s\\{\vec{t}/\vec{x}\\}:a.$ By definition of typing, we know that
$(\delta_{1},\gamma_{1},\dots,\gamma_{k},\delta_{2})=(\zeta^{1}_{1},\vec{\gamma}_{1},\zeta^{2}_{1},\dots,\zeta^{1}_{n},\vec{\gamma}_{n},\zeta^{2}_{n}).$
We can then conclude.

The other cases follow a pattern similar to the list case. ∎

######  Theorem E.8 (Subject Reduction and Equivalence).

Let $s\to_{\mathsf{aut}}s^{\prime}$ or $s\equiv s^{\prime}$ and
$s\in\mathsf{\Lambda_{aut}}(\mathcal{A})(\gamma;a).$ Then
$\gamma\vdash_{\mathsf{aut}}s^{\prime}:a.$

###### Proof.

By induction on $s\to_{\mathsf{aut}}s^{\prime}$. The base case is a corollary
of the former lemma, the other cases are a direct application of the IH. ∎

######  Lemma E.9.

We have that
$s\\{\vec{t}/\vec{x}\\}\\{\vec{u}/\vec{y}\\}=s\\{\vec{u}_{1}/\vec{y}_{1}\\}\\{\vec{t}\\{\vec{u}_{2}/\vec{y}_{2}\\}/\vec{x}\\}$
with $\vec{u}=\vec{u}_{1}::\vec{u}_{2},\vec{y}=\vec{y}_{1}::\vec{y_{2}}$.

###### Proof.

By induction on $s.$ If $s=x$ and $\vec{x}=x,\vec{t}=t$ then
$\vec{y}\in\mathsf{fv}(t)$ and by definition we can conclude. If $s=\langle
s_{1},\dots,s_{k}\rangle,$ by definition $s\\{\vec{t}/\vec{x}\\}=\langle
s\\{\vec{t}_{1}/\vec{x}_{1}\\},\dots,s_{k}\\{\vec{t}_{k}/\vec{x}_{k}\\}\rangle.$
Again, by definition of substitution
$s\\{\vec{t}/\vec{x}\\}\\{\vec{u}/\vec{y}\\}=\langle
s_{1}\\{\vec{t}_{1}/\vec{x}_{1}\\}\\{\vec{u}_{1}/\vec{y}_{1}\\},\dots,s_{k}\\{\vec{t}_{k}/\vec{x}_{k}\\}\\{\vec{u}_{k}/\vec{y}_{k}\\}\rangle.$
We can then apply the IH and conclude. The explicit substitution case follows
a similar pattern. ∎

######  Lemma E.10.

The following statements hold. If $s\to_{\mathsf{aut}}s^{\prime}$ then
$s\\{\vec{t}/\vec{x}\\}\to_{\mathsf{aut}}^{\ast}s^{\prime}\\{\vec{t}/\vec{x}\\}$,
if $\vec{t}\to_{\mathsf{aut}}\vec{t}^{\prime}$ then
$s\\{\vec{t}/\vec{x}\\}\to_{\mathsf{aut}}^{\ast}s\\{\vec{t}^{\prime}/\vec{x}\\};$
if $s=_{\mathsf{aut}}s^{\prime}$ and $\vec{t}=_{\mathsf{aut}}\vec{t}^{\prime}$
then
$s\\{\vec{t}/\vec{x}\\}=_{\mathsf{aut}}s^{\prime}\\{\vec{t^{\prime}}/\vec{x}\\};$
if $s\equiv s^{\prime}$ and $\vec{t}\equiv\vec{t}^{\prime}$ then
$s\\{\vec{t}/\vec{x}\\}\equiv s^{\prime}\\{\vec{t^{\prime}}/\vec{x}\\}.$

###### Proof.

  1. 1.

By induction on $s\to_{\mathsf{aut}}s^{\prime}.$ Let $s=p[\vec{y}:=\vec{u}]$
and $s^{\prime}=p\\{\vec{u}/\vec{y}\\}.$ We need to prove that
$p[\vec{y}:=\vec{u}]\\{\vec{t}/\vec{x}\\}\to_{\mathsf{aut}}p\\{\vec{u}/\vec{y}\\}\\{\vec{t}/\vec{x}\\}.$
By definition of linear substitution, we have
$p[\vec{y}:=\vec{u}]\\{\vec{t}/\vec{x}\\}=p\\{\vec{t}_{1}/\vec{x}_{1}\\}[\vec{y}:=\vec{q}\\{\vec{t}_{2}/\vec{x}_{2}\\}]$
and
$p\\{\vec{t}_{1}/\vec{x}_{1}\\}[\vec{y}=\vec{q}\\{\vec{t}_{2}/\vec{x}_{2}\\}]\to_{\mathsf{aut}}p\\{\vec{t}_{1}/\vec{x}_{1}\\}\\{\vec{q}\\{\vec{t}_{2}/\vec{x}_{2}\\}/\vec{y}\\}.$
By the former lemma, we can conclude that

$p\\{\vec{t}_{1}/\vec{x}_{1}\\}\\{\vec{q}\\{\vec{t}_{2}/\vec{x}_{2}\\}/\vec{y}\\}=p\\{\vec{u}/\vec{y}\\}\\{\vec{t}/\vec{x}\\}.$

The other cases are a direct application of the IH.

  2. 2.

By induction on $s.$ If $s=x$ and $\vec{t}=t$ then $s\\{\vec{t}/\vec{x}\\}=t$
and the result is immediate. The other cases are direct applications of the
IH.

  3. 3.

We remark that if $s=_{\mathsf{aut}}s^{\prime}$ then there exists
$n\in\mathbb{N}$ and terms $s_{i}$ s.t.
$s=s_{0}\leftrightarrow_{\mathsf{re}}s_{1}\dots\leftrightarrow_{\mathsf{re}}s_{n}=s^{\prime},$
where $\leftrightarrow$ stands for the reflexive symmetric closure of
$\to_{\mathsf{rep}}.$ We prove the result by induction on $n.$ If $n=0,$ we
need to prove that if $\vec{t}=_{\mathsf{rep}}\vec{t}^{\prime}$ then
$s\\{\vec{t}/\vec{x}\\}=_{\mathsf{rep}}s\\{\vec{t}^{\prime}/\vec{x}\\}.$ We do
it by induction on $m$ s.t.
$\vec{t}=\vec{t}_{0}\leftrightarrow_{\mathsf{re}}\vec{t}_{1}\dots\leftrightarrow_{\mathsf{re}}\vec{t}_{m}=\vec{t}^{\prime}.$
If $m=0$ the result is immediate by reflexivity. If $m=p+1,$ by IH
$s\\{\vec{t}/\vec{x}\\}=_{\mathsf{aut}}s\\{\vec{t}_{p}/\vec{x}\\}.$ Since
$\vec{t}_{p}\leftrightarrow\vec{t}_{p+1},$ by definition this means that
either $\vec{t}_{p}=\vec{t}_{p+1}$ or
$\vec{t}_{p}\to_{\mathsf{aut}}\vec{t}_{p+1}.$ The first case is immediate, the
second is a direct corollary of the former point of this lemma. If $n=p+1$,
the result is a direct corollary of the first point of this lemma.

∎

We now prove that the structural equivalence is a strong bisimulation for the
reduction $\to_{\mathsf{rep}}.$ Intuitively, this means that the equivalence
does not affect the rewriting of terms.

######  Lemma E.11.

We have that $p[\vec{y}:=q]\\{\vec{t}/\vec{x}\\}\equiv
p\\{\vec{t}/\vec{x}\\}[\vec{y}:=q]$ and
$p\\{\vec{t}[\vec{y}:=q]/\vec{x}\\}\equiv p\\{\vec{t}/\vec{x}\\}[\vec{y}:=q]$

######  Proposition E.12.

If $s^{\prime}\equiv s$ and $s\to_{\mathsf{aut}}t$ there exists a term
$t^{\prime}$ s.t. $t\equiv t^{\prime}$ and
$s^{\prime}\to_{\mathsf{rep}}t^{\prime}.$

###### Proof.

By induction on $s\equiv t.$

Let $s^{\prime}=\lambda\vec{x}.(p[\vec{y}:=q])$ and
$s=(\lambda\vec{x}.p)[\vec{y}:=q]$ and
$(\lambda\vec{x}.p)[\vec{y}:=q]\to_{\mathsf{aut}}t.$ We reason by cases on the
reduction step. If $q=\vec{q}$ and $t=(\lambda\vec{x}.p)\\{\vec{q}/\vec{y}\\}$
then we set $t^{\prime}=\lambda\vec{x}.(p\\{\vec{q}/\vec{y}\\}).$ The other
possible cases are necessarily contextual and directly follow from the IH,
since we cannot apply an $\eta$ ground step on abstractions.

Let $s^{\prime}=\langle s_{1},\dots,s_{i}[\vec{y}:=q],\dots,s_{k}\rangle$ and
$s=\langle s_{1},\dots,s_{k}\rangle[\vec{y}:=q].$ Then either
$s_{j}\to_{\mathsf{aut}}p$ and $t=\langle
s_{1},\dots,p,\dots,s_{k}\rangle[\vec{y}:=q]$ or
$q\to_{\mathsf{aut}}q^{\prime}$ and $t=\langle
s_{1},\dots,s_{k}\rangle[\vec{y}:=q^{\prime}],$ since we cannot apply $\beta$
or $\eta$ ground steps on list terms. In both cases the result is then a
direct consequence of the IH.

Let $s^{\prime}=p[\vec{y}:=q]v$ and $s=(pv)[\vec{y}:=q].$ If
$p=\lambda\vec{x}.p^{\prime},b=\vec{v}$ and
$t=p^{\prime}\\{\vec{v}/\vec{x}\\}[\vec{y}:=q]$ then we set $t^{\prime}=t.$ If
$\gamma\vdash s:\vec{a}\multimap a$ and $t=((pv)[\vec{y}:=q])\vec{x}$ then by
Theorem E.8 $\gamma\vdash s^{\prime}:\vec{a}\multimap a$ and we set
$t^{\prime}=(p[\vec{y}:=q]v)\vec{x}.$ If $\gamma\vdash s:\vec{a}$ and
$t=x[x:=((pv)[\vec{y}:=q])]$ then by Theorem E.8 we have $\gamma\vdash
s^{\prime}:\vec{a}$ and we set $t^{\prime}=x[x:=(p[\vec{y}:=q]v)].$ The other
cases are contextual and follows directly from the IH.

The other application case follows a similar pattern, the only thing to check
is that $s\\{\vec{t}[\vec{y}:=\vec{q}]/\vec{x}\\}\equiv
s\\{\vec{t}/\vec{x}\\}[\vec{y}:=\vec{q}]$, which is a corollary of the former
lemma.

The explicit substitution cases follow a similar patter to the application
one, applying the former lemma for the case where $s\to_{\mathsf{aut}}t$ is a
$\beta$ ground step.

The contextual cases are direct consequences of the IH. ∎

######  Lemma E.13.

Let $s,t_{1},\dots,t_{k}\in\mathsf{\Lambda_{rep}}$ and
$x_{1},\dots,x_{k}\in\mathsf{fv}(s).$ We have that

$\mathtt{size}\left(s\\{t_{1},\dots,t_{k}/x_{1},\dots,x_{k}\\}\right)=(\mathtt{size}\left(s\right)+\sum\mathtt{size}\left(t_{i}\right))-k.$

###### Proof.

By induction on $s.$ If $s=x$ then $k=1$ and $s\\{\vec{t}/\vec{x}\\}=t$. Then
$\mathtt{size}\left(s\\{\vec{t}/\vec{x}\\}\right)=\mathtt{size}\left(t\right)=\mathtt{size}\left(t\right)+\mathtt{size}\left(x\right)-1,$
since $\mathtt{size}\left(x\right)=1.$ If $s=\langle
s_{1},\dots,s_{n}\rangle,$ we have $s\\{\vec{t}/\vec{x}\\}=\langle
s_{1}\\{\vec{t}_{1}/\mathsf{occ}_{\vec{x}}(s_{1})\\},\dots,s_{n}\\{\vec{t}_{n}/\mathsf{occ}_{\vec{x}}(s_{n})\\}\rangle.$
By IH,
$\mathtt{size}\left(s_{i}\\{\vec{t}_{i}/\mathsf{occ}_{\vec{x}}(s_{i})\\}\right)=\mathtt{size}\left(s_{i}\right)+\mathtt{size}\left(\vec{t}_{i}\right)-\mathsf{len}(\mathsf{occ}_{\vec{x}}(s_{i})).$
Since $k=\sum\mathsf{len}(\mathsf{occ}_{\vec{x}}(s_{i}))$ we can conclude. The
other cases follows a similar pattern. ∎

######  Lemma E.14.

Let $s,\vec{t},q$ be resource terms with $\vec{x}\subseteq\mathsf{fv}(s)$ and
$\mathsf{len}(\vec{t})=\mathsf{len}(\vec{x})$. If
$s\\{\vec{t}/\vec{x}\\}\to_{\eta}p$ then there exist
$s^{\prime},\vec{t}^{\prime}$ s.t.
$s\to_{\eta}s^{\prime},\vec{t}\to_{\eta}\vec{t}^{\prime},p=s^{\prime}\\{\vec{t}^{\prime}/\vec{x}\\}.$

###### Proof.

By induction on the structure of $s.$ If $s=x$ then $\vec{t}=\langle t\rangle$
and $s\\{\vec{t}/\vec{x}\\}=t.$ Then we set $s^{\prime}=x$ and
$\vec{t}^{\prime}=\langle p\rangle.$

If $s=\lambda\vec{y}.v$ then
$s\\{\vec{t}/\vec{x}\\}=\lambda\vec{y}.(v\\{\vec{t}/\vec{x}\\}).$ The result
is then a direct application of the IH.

If $s=vq$ then
$s\\{\vec{t}/\vec{x}\\}=v\\{\vec{t}_{1}/\mathsf{occ}_{\vec{x}(v)}\\}q\\{\vec{t}_{2}/\mathsf{occ}_{\vec{x}(q)}\\}.$
We have three possible cases.

  * •

If
$s\\{\vec{t}/\vec{x}\\}\to_{\eta}\lambda\vec{y}.s\\{\vec{t}/\vec{x}\\}\vec{y}$
then we set $s^{\prime}=\lambda\vec{y}.(vq)\vec{y}$ and
$\vec{t}^{\prime}=\vec{t}.$

  * •

If $s\\{\vec{t}/\vec{x}\\}\to_{\eta}\vec{x}[\vec{x}:=s\\{\vec{t}/\vec{x}\\}]$
then we set $s^{\prime}=\vec{x}[\vec{x}:=vq]$ and $\vec{t}^{\prime}=\vec{t}.$

  * •

If the $\eta$ step is a contextual case the result is a direct consequence of
the IH.

The cases of substitution and list follow a similar pattern to the one of the
application case. ∎

######  Proposition E.15.

If $s\to_{\beta}t\to_{\eta}t^{\prime}$ there exists $s^{\prime}$ s.t.
$s\to_{\eta}s^{\prime}$ and $s^{\prime}\to_{\beta}^{\ast}t^{\prime}.$

###### Proof.

By induction on the step $s\to_{\beta}t.$ If
$s=p[\vec{x}:=\mathtt{L}[\vec{q}]]\to_{\beta
1}t=\mathtt{L}[p\\{\vec{q}/\vec{x}\\}]$ the result is a corollary of Lemma
E.14. The same happens for the case $s\to_{\beta_{2}}t.$ We do the contextual
case of application. If $s=pq\to_{\beta}t=p^{\prime}q$ with
$p\to_{\beta}p^{\prime}$ and $p^{\prime}q\to_{\eta}t^{\prime}$ we have three
possible cases.

  * •

If $p^{\prime}q\to_{\eta}\lambda\vec{y}.(p^{\prime}q)\vec{y}.$ In that case we
set $s^{\prime}=\lambda\vec{y}.(pq)\vec{y}.$

  * •

If $p^{\prime}q\to_{\eta}\vec{x}[\vec{x}:=p^{\prime}q].$ In that case we set
$s^{\prime}=\vec{x}[\vec{x}:=pq].$

  * •

If the $\eta$ step is a contextual case the result is a direct consequence of
the IH.

∎

######  Proposition E.16.

If $s\to_{\beta}^{\ast}t\to_{\eta}^{\ast}t^{\prime}$ there exists $s^{\prime}$
s.t. $s\to_{\eta}^{\ast}s^{\prime}$ and
$s^{\prime}\to_{\beta}^{\ast}t^{\prime}.$

###### Proof.

The proof is by induction on the length of the reduction
$s\to_{\beta}^{\ast},$ by applying the former proposition. ∎

Given $\gamma\vdash s:a$ we define two sets of autonomous type judgments as
follows$\mathsf{EST}_{1}(s)=\\{\delta\vdash p:a\mid
p\in\mathsf{ST}(s)\setminus\mathsf{LT}\text{ s.t. }\mathtt{E}[\delta\vdash
p:a]=s\text{ for some context }\mathtt{E}\\}$ and
$\mathsf{EST}_{"}(s)=\\{\delta\vdash p:a\mid
p\in\mathsf{ST}(s)\setminus\mathsf{LT}\text{ s.t. }\mathsf{D}[\delta\vdash
p:a]=s\text{ for some context }\mathsf{D}\\}.$ We set
$\eta_{1}(s)=\sum_{\delta\vdash
p:a\in\mathsf{EST}(s)}\mathtt{size}\left(a\right)_{1}$ and
$\eta_{2}(s)=\sum_{\delta\vdash
p:a\in\mathsf{EST}_{2}(s)}\mathtt{size}\left(a\right)_{2}.$

######  Remark E.17.

The intuition behind the sets $\mathsf{EST}_{1}(s)$ and $\mathsf{EST}_{2}(s)$
is that we are considering all types of subterms of $s$ on which we could
perform the $\eta$-reduction. The restrictions on the shape of $p$ is indeed
directly derived from the ones on the $\eta$-reductions.

######  Proposition E.18.

The following statements hold. If $s\to_{\beta}s^{\prime}$ then
$\mathtt{size}\left(s^{\prime}\right)<\mathtt{size}\left(s\right)$; if
$s\to_{\eta 1}s^{\prime}$ then $\eta_{1}(t)<\eta(s)_{1}$; if $s\to_{\eta
2}s^{\prime}$ then $\eta_{2}(t)<\eta(s)_{2}.$

###### Proof.

  1. 1.

By induction on $s\to_{\beta}s^{\prime},$ exploiting Lemma E.13.

  2. 2.

By induction on $s\to_{\eta 1}s^{\prime}.$ Let $\gamma\vdash s:\langle
a_{1},\dots,a_{k}\rangle$ and $s\to_{\eta 1}\vec{x}[\vec{x}=s]$ where
$s\notin\mathsf{LT}.$ We have
$\mathsf{EST}_{1}(\vec{x}[\vec{x}=s])=\mathsf{EST}_{1}(s)\setminus\\{s\\}.$ We
can then conclude, since

$\eta_{1}(s)=\eta_{1}(\vec{x}[\vec{x}=s])+\mathtt{size}\left(\langle
a_{1},\dots,a_{k}\rangle\right)_{1}$

and $\mathtt{size}\left(\langle a_{1},\dots,a_{k}\rangle\right)\neq 0$. Let
$s=\lambda\vec{x}.t$ and $s^{\prime}=\lambda\vec{x}.t^{\prime}$ with
$t\to_{\eta 1}t^{\prime}.$ By IH we have that
$\eta_{1}(t^{\prime})<\eta_{1}(t).$ By subject reduction and definition of
$\eta_{1}$ we can conclude. Let $s=tq$ and $s^{\prime}=t^{\prime}q$ with
$t\to_{\eta 1}t^{\prime}.$ Again the result is a corollary of the IH and
subject reduction, by observing that $\eta_{1}(tq)=\eta_{1}(t)+\eta_{1}(q)$.
The same works for the substitution and list cases.

  3. 3.

By induction on $s\to_{\eta 2}s^{\prime}.$ Let $\gamma\vdash
s:\vec{a}\multimap a$ and $s\to_{\eta 2}\lambda\vec{x}.s\vec{x}.$ where
$s\notin\mathsf{LT}.$ We have
$\mathsf{EST}_{2}(\lambda\vec{x}.s\vec{x})=\mathsf{EST}_{2}(s)\setminus\\{s\\}\sqcup\\{\vec{x}\\}.$
We have that
$\eta_{2}(s)=\eta_{2}(\lambda\vec{x}.s\vec{x})+\mathtt{size}\left(\vec{a}\multimap
a\right)_{2}-\mathtt{size}\left(\vec{a}\right)_{2}.$ Since
$\mathtt{size}\left(\vec{a}\right)_{2}<\mathtt{size}\left(\vec{a}\multimap
a\right)_{2}$ we can conclude. We can then conclude.

∎

######  Proposition E.19 (Local Confluence).

The reduction $\to_{\mathsf{aut}}$ is locally confluent.

###### Proof.

Let $s\to_{\mathsf{aut}}t_{1}$ and $s\to_{\mathsf{aut}}t_{2}.$ We prove the
result by induction on the step $s\to_{\mathsf{aut}}t_{1}$ and by reasoning by
cases on $s\to_{\mathsf{aut}}t_{2}.$ If
$s=s^{\prime}[\vec{x}:=\mathtt{L}[\vec{t}]]$ with
$t_{1}=\mathtt{L}[s^{\prime}\\{\vec{t}/\vec{x}\\}]$ we reason by cases on
$s\to_{\mathsf{aut}}t_{2}.$ if
$t_{2}=s^{\prime\prime}[\vec{x}:=\mathtt{L}[\vec{t}]]$ then
$\mathtt{L}[s^{\prime}\\{\vec{t}/\vec{x}\\}]\to_{\mathsf{aut}}^{\ast}\mathtt{L}[s^{\prime\prime}\\{\vec{t}/\vec{x}\\}]$
by Lemma E.10. If $t_{2}=s[\vec{x}:=\mathtt{L}[\vec{t}^{\prime}]]$ then
$\mathtt{L}[s\\{\vec{t}/\vec{x}\\}]\to_{\mathsf{aut}}^{\ast}ctxl[s\\{\vec{t}/\vec{x}\\}]$
again by Lemma E.10. If $s\to_{\mathsf{aut}}t_{2}$ is an $\eta$-rule, the
result is immediate by contextuality.

If $s=(\lambda\vec{x}.p)\vec{q}$ and $t_{1}=p\\{\vec{q}/\vec{x}\\}$ we reason
by cases on $s\to_{\mathsf{aut}}t_{2}.$ if
$\lambda\vec{x}.p)\vec{q}\to_{\mathsf{aut}}\lambda\vec{x}.p^{\prime})\vec{q^{\prime}},$
then the result is a corollary of Lemma E.10. If $s\to_{\mathsf{aut}}t_{2}$ is
an $\eta$-rule, the result is immediate by contextuality.

Let $\gamma\vdash s:\vec{a}\multimap a$ with
$s\to_{\mathsf{aut}}\lambda\vec{x}.s\vec{x}.$ Then if
$s\to_{\mathsf{aut}}s^{\prime},$ by contextuality of the reduction
$\lambda\vec{x}.s\vec{x}\to_{\mathsf{aut}}\lambda\vec{x}.s^{\prime}\vec{x}.$

Let $\gamma\vdash s:\vec{a}$ with $s\to_{\mathsf{aut}}\vec{x}[\vec{x}:=s],$ we
can again conclude by contextuality. The contextual cases are direct
consequences of the IH. ∎