University College London, United<EMAIL_ADDRESS>of
Minho & INESC-TEC<EMAIL_ADDRESS>Fredrik Dahlqvist and Renato
Neves [500]Theory of computation Models of computation

###### Acknowledgements.

This work was financed by the ERDF – European Regional Development Fund
through the Operational Programme for Competitiveness and Internationalisation
- COMPETE 2020 Programme and by National Funds through the Portuguese funding
agency, FCT - Fundação para a Ciência e a Tecnologia, within project
POCI-01-0145-FEDER-030947. This work was also financed by the UK Research
Institute in Verified Trustworthy Software Systems, via project “Quantitative
Algebraic Reasoning for Hybrid Programs”, and by the Leverhulme Project Grant
“Verification of Machine Learning Algorithms”. The authors are very grateful
for the reviewer’s incisive feedback.John Q. Open and Joan R. Access 2 42nd
Conference on Very Important Topics (CVIT 2016) CVIT 2016 CVIT 2016 December
24–27, 2016 Little Whinging, United Kingdom 42 23

# An Internal Language for Categories Enriched over Generalised Metric Spaces

Fredrik Dahlqvist  Renato Neves

###### Abstract

Programs with a _continuous_ state space or that interact with physical
processes often require notions of equivalence going beyond the standard
binary setting in which equivalence either holds or does not hold. In this
paper we explore the idea of equivalence taking values in a quantale
$\mathcal{V}$, which covers the cases of (in)equations and (ultra)metric
equations among others.

Our main result is the introduction of a _$\mathcal{V}$ -equational deductive
system_ for linear $\lambda$-calculus together with a proof that it is sound
and complete (in fact, an internal language) for a class of enriched
autonomous categories. In the case of inequations, we get an internal language
for autonomous categories enriched over partial orders. In the case of
(ultra)metric equations, we get an internal language for autonomous categories
enriched over (ultra)metric spaces.

We use our results to obtain examples of inequational and metric equational
systems for higher-order programs that contain real-time and probabilistic
behaviour.

###### keywords:

$\lambda$-calculus, enriched category theory, quantale, equational theory

###### category:

##  1 Introduction

Programs frequently act over a _continuous_ state space or interact with
physical processes like time progression or the movement of a vehicle. Such
features naturally call for notions of approximation and refinement integrated
in different aspects of program equivalence. Our paper falls in this line of
research. Specifically, our aim is to integrate notions of approximation and
refinement into the _equational system_ of linear $\lambda$-calculus [4, 27,
28].

The core idea that we explore in this paper is to have equations $t=_{q}s$
labelled by elements $q$ of a quantale $\mathcal{V}$. This covers a wide range
of situations, among which the cases of (in)equations [22, 2] and metric
equations [29, 30]. The latter case is perhaps less known: it consists of
equations $t=_{\epsilon}s$ labelled by a non-negative rational number
$\epsilon$ which represents the ‘maximum distance’ that the two terms $t$ and
$s$ can be from each other. In order to illustrate metric equations, consider
a programming language with a (ground) type $X$ and a signature of operations
$\Sigma=\\{\mathtt{wait_{n}}:X\to X\mid n\in\mathbb{N}\\}$ that model time
progression over computations of type $X$. Specifically,
$\mathtt{wait_{n}}(x)$ reads as “add a latency of $n$ seconds to the
computation $x$”. In this context, the following axioms involving metric
equations arise naturally:

$\displaystyle\mathtt{wait_{0}}(x)=_{0}x\hskip
28.45274pt\mathtt{wait_{n}}(\mathtt{wait_{m}}(x))=_{0}\mathtt{wait_{n+m}}(x)\hskip
28.45274pt\mathtt{wait_{n}}(x)=_{\epsilon}\mathtt{wait_{m}}(x)\epsilon=|m-n|$
(1)

An equation $t=_{0}s$ states that the terms $t$ and $s$ are exactly the same
and equations $t=_{\epsilon}s$ state that $t$ and $s$ differ by _at most_
$\epsilon$ seconds in their execution time.

Contributions. In this paper we introduce an equational deductive system for
linear $\lambda$-calculus in which equations are labelled by elements of a
quantale $\mathcal{V}$. By using key features of a quantale’s structure, we
show that this deductive system is _sound and complete_ for a class of
enriched symmetric monoidal closed categories (i.e. enriched autonomous
categories). In particular, if we fix $\mathcal{V}$ to be the Boolean quantale
this class of categories consists of autonomous categories enriched over
partial orders. If we fix $\mathcal{V}$ to be the (ultra)metric quantale, this
class of categories consists of autonomous categories enriched over
(ultra)metric spaces. The aforementioned example of wait calls fits in the
setting in which $\mathcal{V}$ is the metric quantale. Our result provides
this example with a sound and complete metric equational system, where the
models are all those autonomous categories enriched over metric spaces that
can soundly interpret the axioms of wait calls (1).

The next contribution of our paper falls in one of the major topics of
categorical logic: to establish _logical descriptions_ of certain classes of
categories. A famous result of this kind is the correspondence between
$\lambda$-calculus and Cartesian closed categories which states that the
former is the _internal language_ of the latter [23] – such a correspondence
allows to study Cartesian closed categories by means of logical tools. An
analogous result is presented in [27, 28] for linear $\lambda$-calculus and
symmetric monoidal closed (i.e. autonomous) categories. We show that linear
$\lambda$-calculus equipped with a $\mathcal{V}$-equational system is the
internal language of autonomous categories enriched over ‘generalised metric
spaces’.

Outline. Section 2 recalls linear $\lambda$-calculus, its equational system,
and the famous correspondence to autonomous categories, via soundness,
completeness, and internal language theorems. The contents of this section are
slight adaptations of results presented in [27, 4], the main difference being
that we forbid the exchange rule to be explicitly part of linear
$\lambda$-calculus (instead it is only admissible). This choice is important
to ensure that judgements in the calculus have _unique_ derivations, which
allows us to refer to their interpretations unambiguously [37]. Section 3
presents the main contributions of this paper. It walks a path analogous to
Section 2, but now in the setting of $\mathcal{V}$-equations (i.e. equations
labelled by elements of a quantale $\mathcal{V}$). As we will see, the
semantic counterpart of moving from equations to $\mathcal{V}$-equations is to
move from categories to categories enriched over _$\mathcal{V}$ -categories_.
The latter, often regarded as generalised metric spaces, are central entities
in a fruitful area of enriched category theory that aims to treat uniformly
different kinds of ‘structured sets’, such as partial orders, fuzzy partial
orders, and (ultra)metric spaces [24, 38, 39]. Our results are applicable to
all these examples. Section 4 presents some examples of
$\mathcal{V}$-equational axioms and corresponding models. Specifically, we
will revisit the axioms of wait calls (1) and consider an inequational
variant. Then we will study a metric axiom for probabilistic programs and show
that the category of Banach spaces and short linear maps is a model for the
resulting metric theory. We will additionally use this example to illustrate
how our deductive system allows to compute an approximate distance between two
probabilistic programs easily as opposed to computing an exact distance
‘semantically’ which tends to involve quite complex operators. Finally,
Section 5 establishes a functorial connection between our results and previous
well-known semantics for linear logic [10, 28], and concludes with a brief
exposition of future work. We assume knowledge of $\lambda$-calculus and
category theory [27, 28, 23, 26]. Proofs omitted in the main text are
available in the appendix.

Related work. Several approaches to incorporating quantitative information to
programming languages have been explored in the literature. Closest to this
work are various approaches targeted at $\lambda$-calculi. In [7, 8] a notion
of distance called _context distance_ is developed, first for an affine, then
for a more general $\lambda$-calculus, with probabilistic programs as the main
motivation. [13] considers a notion of quantale-valued _applicative
(bi)similarity_ , an operational _coinductive_ technique used for showing
contextual equivalence between two programs. Recently, [33] presented several
Cartesian closed categories of generalised metric spaces that provide a
quantitative semantics to simply-typed $\lambda$-calculus based on a
generalisation of logical relations. None of these examples reason about
distances in a quantitative equational system, and in this respect our work is
closer to the metric universal algebra developed in [29, 30].

A different approach consists in encoding quantitative information via a type
system. In particular, graded (modal) types [15, 12, 31] have found
applications in e.g. differential privacy [34] and information flow [1]. This
approach is to some extent orthogonal to ours as it mainly aims to model
coeffects, whilst we aim to reason about the intrinsic quantitative nature of
$\lambda$-terms acting e.g. on continuous or ordered spaces.

Quantum programs provide an interesting example of intrinsically quantitative
programs, by which we mean that the metric structure on quantum states does
not arise from (co)effects. Recently, [18] showed how the issue of noise in a
quantum while-language can be handled by developing a _deductive system_ to
determine how similar a quantum program is from its idealised, noise-free
version; an approach very much in the spirit of this work.

##  2 An internal language for autonomous categories

In this section we briefly recall linear $\lambda$-calculus, which can be
regarded as a term assignment system for the exponential free, multiplicative
fragment of _intuitionistic linear logic_. Then we recall that it is sound and
complete w.r.t. autonomous categories, and also that it is an internal
language for such categories. We mention only what is needed to present our
results, the interested reader will find a more detailed exposition in [27, 4,
28]. Let us start by fixing a _class_ $G$ of ground types. The grammar of
types for linear $\lambda$-calculus is given by:

$\mathbb{A}::=X\in
G\mid\mathbb{I}\mid\mathbb{A}\otimes\mathbb{A}\mid\mathbb{A}\multimap\mathbb{A}$

We also fix a class $\Sigma$ of sorted operation symbols
$f:\mathbb{A}_{1},\dots,\mathbb{A}_{n}\to\mathbb{A}$ with $n\geq 1$. As usual,
we use Greek letters $\Gamma,\Delta,E,\dots$ to denote _typing contexts_ ,
i.e. lists $x_{1}:\mathbb{A}_{1},\dots,x_{n}:\mathbb{A}_{n}$ of typed
variables such that each variable $x_{i}$ occurs at most once in
$x_{1},\dots,x_{n}$.

We will use the notion of a shuffle for building a linear typing system such
that the _exchange rule_ is admissible and each judgement $\Gamma\rhd
v:\mathbb{A}$ (details about these below) has a _unique derivation_ – this
will allow us to refer to a judgement’s denotation $\llbracket\Gamma\rhd
v:\mathbb{A}\rrbracket$ unambiguously. By shuffle we mean a permutation of
typed variables in a context sequence $\Gamma_{1},\dots,\Gamma_{n}$ such that
for all $i\leq n$ the relative order of the variables in $\Gamma_{i}$ is
preserved [37]. For example, if $\Gamma_{1}=x:\mathbb{A},y:\mathbb{B}$ and
$\Gamma_{2}=z:\mathbb{C}$ then $z:\mathbb{C},x:\mathbb{A},y:\mathbb{B}$ is a
shuffle but $y:\mathbb{B},x:\mathbb{A},z:\mathbb{C}$ is _not_ , because we
changed the order in which $x$ and $y$ appear in $\Gamma_{1}$. As explained in
[37] (and also in the proof of Lemma 2.1), such a restriction on relative
orders is crucial for judgements having unique derivations. We denote by
$\mathrm{Sf}(\Gamma_{1};\dots;\Gamma_{n})$ the set of shuffles on
$\Gamma_{1},\dots,\Gamma_{n}$.

The term formation rules of linear $\lambda$-calculus are listed in Fig. 1.
They correspond to the natural deduction rules of the exponential free,
multiplicative fragment of intuitionistic linear logic.

######  Lemma 2.1.

All judgements $\Gamma\rhd v:\mathbb{A}$ have a unique derivation.

Substitution is defined in the expected way, and the following result is
standard.

######  Lemma 2.2 (Exchange and Substitution).

For every judgement $\Gamma,x:\mathbb{A},y:\mathbb{B},\Delta\rhd v:\mathbb{C}$
we can derive $\Gamma,y:\mathbb{B},x:\mathbb{A},\Delta\rhd v:\mathbb{C}$. For
all judgements $\Gamma,x:\mathbb{A}\rhd v:\mathbb{B}$ and $\Delta\rhd
w:\mathbb{A}$ we can derive $\Gamma,\Delta\rhd v[w/x]:\mathbb{B}$.

We now recall the interpretation of judgements $\Gamma\rhd v:\mathbb{A}$ in a
symmetric monoidal closed (autonomous) category $\mathsf{C}$. But before
proceeding with this description, let us fix notation for some of the
constructions available in autonomous categories. For all $\mathsf{C}$-objects
$X,Y,Z$, $\operatorname{\mathsf{sw}}:X\otimes Y\to Y\otimes X$ denotes the
symmetry morphism, $\lambda:\mathbb{I}\otimes X\to X$ the left unitor,
$\mathrm{app}:(X\multimap Y)\otimes X\to Y$ the application, and
$\alpha:X\otimes(Y\otimes Z)\to(X\otimes Y)\otimes Z$ the left associator.
Moreover for all $\mathsf{C}$-morphisms $f:X\otimes Y\to Z$ we denote the
corresponding curried version (right transpose) by
$\overline{f}:X\to(Y\multimap Z)$.

For all ground types $X\in G$ we postulate an interpretation $\llbracket
X\rrbracket$ as a $\mathsf{C}$-object. Types are then interpreted by induction
over the type structure of linear $\lambda$-calculus, using the tensor
$\otimes$ and exponential $\multimap$ constructs of autonomous categories.
Given a non-empty context $\Gamma=\Gamma^{\prime},x:\mathbb{A}$, its
interpretation is defined by
$\llbracket\Gamma^{\prime},x:\mathbb{A}\rrbracket=\llbracket\Gamma^{\prime}\rrbracket\otimes\llbracket\mathbb{A}\rrbracket$
if $\Gamma^{\prime}$ is non-empty and
$\llbracket\Gamma^{\prime},x:\mathbb{A}\rrbracket=\llbracket\mathbb{A}\rrbracket$
otherwise. The empty context $-$ is interpreted as
$\llbracket-\rrbracket=\mathbb{I}$ where $\mathbb{I}$ is the unit of $\otimes$
in $\mathsf{C}$. To keep notation simple, given
$X_{1},\dots,X_{n}\in\mathsf{C}$ we write $X_{1}\otimes\dots\otimes X_{n}$ for
the $n$-tensor $(\dots(X_{1}\otimes X_{2})\otimes\dots)\otimes X_{n}$, and
similarly for $\mathsf{C}$-morphisms.

We will also need some ‘housekeeping’ morphisms to handle interactions between
context interpretation and the autonomous structure of $\mathsf{C}$.
Specifically, given contexts $\Gamma_{1},\dots,\Gamma_{n}$ we denote by
$\operatorname{\mathsf{sp}}_{\Gamma_{1};\dots;\Gamma_{n}}:\llbracket\Gamma_{1},\dots,\Gamma_{n}\rrbracket\to\llbracket\Gamma_{1}\rrbracket\otimes\dots\otimes\llbracket\Gamma_{n}\rrbracket$
the morphism that splits $\llbracket\Gamma_{1},\dots,\Gamma_{n}\rrbracket$
into
$\llbracket\Gamma_{1}\rrbracket\otimes\dots\otimes\llbracket\Gamma_{n}\rrbracket$,
and by $\operatorname{\mathsf{jn}}_{\Gamma_{1};\dots;\Gamma_{n}}$ the
corresponding inverse. Given a context
$\Gamma,x:\mathbb{A},y:\mathbb{B},\Delta$ we denote by
$\operatorname{\mathsf{exch}}_{\Gamma,\underline{x:\mathbb{A},y:\mathbb{B}},\Delta}:\llbracket\Gamma,x:\mathbb{A},y:\mathbb{B},\Delta\rrbracket\to\llbracket\Gamma,y:\mathbb{B},x:\mathbb{A},\Delta\rrbracket$
the morphism corresponding to the permutation of the variable $x:\mathbb{A}$
with $y:\mathbb{B}$. Whenever convenient we will drop variable names in the
subscripts of $\operatorname{\mathsf{sp}}$, $\operatorname{\mathsf{jn}}$, and
$\operatorname{\mathsf{exch}}$. For a context
$E\in\mathrm{Sf}(\Gamma_{1},\dots,\Gamma_{n})$ the morphism
$\operatorname{\mathsf{sh}}_{E}:\llbracket
E\rrbracket\to\llbracket\Gamma_{1},\dots,\Gamma_{n}\rrbracket$ denotes the
corresponding shuffling morphism.

For every operation symbol
$f:\mathbb{A}_{1},\dots,\mathbb{A}_{n}\to\mathbb{A}$ in $\Sigma$ we postulate
an interpretation $\llbracket
f\rrbracket:\llbracket\mathbb{A}_{1}\rrbracket\otimes\dots\otimes\llbracket\mathbb{A}_{n}\rrbracket\to\llbracket\mathbb{A}\rrbracket$
as a $\mathsf{C}$-morphism. The interpretation of judgements is defined by
induction over the structure of judgement derivation according to the rules in
Fig. 2.

$\displaystyle E\rhd f(v_{1},\dots,v_{n}):\mathbb{A}\Gamma_{i}\rhd
v_{i}:\mathbb{A}_{i}\quad
f:\mathbb{A}_{1},\dots,\mathbb{A}_{n}\to\mathbb{A}\in\Sigma\quad
E\in\mathrm{Sf}(\Gamma_{1};\dots;\Gamma_{n})\hskip 14.22636ptx:\mathbb{A}\rhd
x:\mathbb{A}$

$\displaystyle\hskip 51.21504pt-\rhd\ast:\mathbb{I}\hskip 56.9055ptE\rhd v\
\mathtt{to}\ \ast.\ w:\mathbb{A}\Gamma\rhd v:\mathbb{I}\quad\Delta\rhd
w:\mathbb{A}\quad E\in\mathrm{Sf}(\Gamma;\Delta)$

$\displaystyle\hskip 85.35826ptE\rhd v\otimes
w:\mathbb{A}\otimes\mathbb{B}\Gamma\rhd v:\mathbb{A}\quad\Delta\rhd
w:\mathbb{B}\quad E\in\mathrm{Sf}(\Gamma;\Delta)$

$\displaystyle\hskip 56.9055ptE\rhd\mathtt{pm}\ v\ \mathtt{to}\ x\otimes y.\
w:\mathbb{C}\Gamma\rhd
v:\mathbb{A}\otimes\mathbb{B}\quad\Delta,x:\mathbb{A},y:\mathbb{B}\rhd
w:\mathbb{C}\quad E\in\mathrm{Sf}(\Gamma;\Delta)$

$\displaystyle\Gamma\rhd\lambda
x:\mathbb{A}.\,v:\mathbb{A}\multimap\mathbb{B}\Gamma,x:\mathbb{A}\rhd
v:\mathbb{B}\hskip 28.45274ptE\rhd v\,w:\mathbb{B}\Gamma\rhd
v:\mathbb{A}\multimap\mathbb{B}\quad\Delta\rhd w:\mathbb{A}\quad
E\in\mathrm{Sf}(\Gamma;\Delta)$

Figure 1: Term formation rules for linear $\lambda$-calculus.

$\displaystyle\llbracket E\rhd
f(v_{1},\dots,v_{n}):\mathbb{A}\rrbracket=\llbracket
f\rrbracket\cdot(m_{1}\otimes\dots\otimes
m_{n})\cdot\operatorname{\mathsf{sp}}_{\Gamma_{1};\dots;\Gamma_{n}}\cdot\operatorname{\mathsf{sh}}_{E}\llbracket\Gamma_{i}\rhd
v_{i}:\mathbb{A}_{i}\rrbracket=m_{i}\quad
f:\mathbb{A}_{1},\dots,\mathbb{A}_{n}\to\mathbb{A}\in\Sigma\quad
E\in\mathrm{Sf}(\Gamma_{1}\dots\Gamma_{n})\hskip 9.95863pt\llbracket
x:\mathbb{A}\rhd
x:\mathbb{A}\rrbracket=\operatorname{\mathsf{id}}_{\llbracket\mathbb{A}\rrbracket}$

$\displaystyle\hskip
17.07182pt\llbracket-\rhd\ast:\mathbb{I}\rrbracket=\operatorname{\mathsf{id}}_{\llbracket\mathbb{I}\rrbracket}\hskip
56.9055pt\llbracket E\rhd v\ \mathtt{to}\ \ast.\
w:\mathbb{A}\rrbracket=n\cdot\lambda\cdot(m\otimes\operatorname{\mathsf{id}})\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta}\cdot\operatorname{\mathsf{sh}}_{E}\llbracket\Gamma\rhd
v:\mathbb{I}\rrbracket=m\quad\llbracket\Delta\rhd
w:\mathbb{A}\rrbracket=n\quad E\in\mathrm{Sf}(\Gamma;\Delta)$

$\displaystyle\llbracket E\rhd v\otimes
w:\mathbb{A}\otimes\mathbb{B}\rrbracket=(m\otimes
n)\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta}\cdot\operatorname{\mathsf{sh}}_{E}\llbracket\Gamma\rhd
v:\mathbb{A}\rrbracket=m\quad\llbracket\Delta\rhd
w:\mathbb{B}\rrbracket=n\quad E\in\mathrm{Sf}(\Gamma;\Delta)\hskip
2.84544pt\llbracket\Gamma\rhd\lambda
x:\mathbb{A}.\,v:\mathbb{A}\multimap\mathbb{B}\rrbracket=\overline{(m\cdot\operatorname{\mathsf{jn}}_{\Gamma;\mathbb{A}})}\llbracket\Gamma,x:\mathbb{A}\rhd
v:\mathbb{B}\rrbracket=m$

$\displaystyle\hskip 48.36958pt\llbracket E\rhd\mathtt{pm}\ v\ \mathtt{to}\
x\otimes y.\
w:\mathbb{C}\rrbracket=n\cdot\operatorname{\mathsf{jn}}_{\Delta;\mathbb{A};\mathbb{B}}\cdot\alpha\cdot\operatorname{\mathsf{sw}}\cdot(m\otimes\operatorname{\mathsf{id}})\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta}\cdot\operatorname{\mathsf{sh}}_{E}\llbracket\Gamma\rhd
v:\mathbb{A}\otimes\mathbb{B}\rrbracket=m\quad\llbracket\Delta,x:\mathbb{A},y:\mathbb{B}\rhd
w:\mathbb{C}\rrbracket=n\quad E\in\mathrm{Sf}(\Gamma;\Delta)$

$\displaystyle\hskip 76.82234pt\llbracket E\rhd
v\,w:\mathbb{B}\rrbracket=\mathrm{app}\cdot(m\otimes
n)\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta}\cdot\operatorname{\mathsf{sh}}_{E}\llbracket\Gamma\rhd
v:\mathbb{A}\multimap\mathbb{B}\rrbracket=m\quad\llbracket\Delta\rhd
w:\mathbb{A}\rrbracket=n\quad E\in\mathrm{Sf}(\Gamma;\Delta)$

Figure 2: Judgement interpretation on an autonomous category $\mathsf{C}$.

As detailed in [4, 27, 28], linear $\lambda$-calculus comes equipped with a
class of equations (Fig. 3), specifically _equations-in-context_ $\Gamma\rhd
v=w:\mathbb{A}$, that corresponds to the axiomatics of autonomous categories.
As usual, we omit the context and typing information of the equations in Fig.
3, which can be reconstructed in the usual way.

$\mathtt{pm}\ v\otimes w\ \mathtt{to}\ x\otimes y.\ u$ | $=$ | $u[v/x,w/y]$
---|---|---
$\mathtt{pm}\ v\ \mathtt{to}\ x\otimes y.\ u[x\otimes y/z]$ | $=$ | $u[v/z]$
$\ast\ \mathtt{to}\ \ast.\ v$ | $=$ | $v$
$v\ \mathtt{to}\ \ast.\ w[\ast/z]$ | $=$ | $w[v/z]$

(a) Monoidal structure

$(\lambda x:\mathbb{A}.\ v)\ w$ | $=$ | $v[w/x]$
---|---|---
$\lambda x:\mathbb{A}.(v\ x)$ | $=$ | $v$

(b) Higher-order structure

$u[v\ \mathtt{to}\ast.\ w/z]$ | $=$ | $v\ \mathtt{to}\ \ast.\ u[w/z]$
---|---|---
$u[\mathtt{pm}\ v\ \mathtt{to}\ x\otimes y.\ w/z]$ | $=$ | $\mathtt{pm}\ v\ \mathtt{to}\ x\otimes y.\ u[w/z]$

(c) Commuting conversions

Figure 3: Equations corresponding to the axiomatics of autonomous categories.

######  Theorem 2.3.

The equations presented in Fig. 3 are sound w.r.t. judgement interpretation.
Specifically if $\Gamma\rhd v=w:\mathbb{A}$ is one of the equations in Fig. 3
then $\llbracket\Gamma\rhd v:\mathbb{A}\rrbracket=\llbracket\Gamma\rhd
w:\mathbb{A}\rrbracket$.

######  Definition 2.4 (Linear $\lambda$-theories).

Consider a tuple $(G,\Sigma)$ consisting of a class $G$ of ground types and a
class $\Sigma$ of sorted operation symbols. A linear $\lambda$-theory
$((G,\Sigma),Ax)$ is a triple such that $Ax$ is a class of equations-in-
context over linear $\lambda$-terms built from $(G,\Sigma)$.

The elements of $Ax$ are called axioms (of the theory). Let $Th(Ax)$ be the
smallest congruence that contains $Ax$, the equations listed in Fig. 3, and
that is closed under the exchange and substitution rules. We call the elements
of $Th(Ax)$ theorems (of the theory).

######  Definition 2.5 (Models of linear $\lambda$-theories).

Consider a linear $\lambda$-theory $((G,\Sigma),Ax)$ and an autonomous
category $\mathsf{C}$. Suppose that for each $X\in G$ we have an
interpretation $\llbracket X\rrbracket$ that is a $\mathsf{C}$-object and
analogously for the operation symbols. This interpretation structure is a
_model_ of the theory if all axioms are satisfied by the interpretation.

Next let us turn our attention to the correspondence between linear
$\lambda$-calculus and autonomous categories, established via soundness,
completeness, and internal language theorems. Despite the proofs of such
theorems already being detailed in [27, 4, 28], we decided to briefly sketch
them below to render the presentation of some of our own results self-
contained.

######  Theorem 2.6 (Soundness & Completeness).

Consider a linear $\lambda$-theory $T$. An equation $\Gamma\rhd
v=w:\mathbb{A}$ is a theorem of $T$ iff it is satisfied by all models of the
theory.

######  Proof 2.7 (Proof sketch).

Soundness follows by induction over the rules that define $Th(Ax)$ (Definition
2.4) and by Theorem 2.3. Completeness is based on the idea of a Lindenbaum-
Tarski algebra: it follows from building the _syntactic category_
$\mathrm{Syn}(T)$ of $T$ (also known as term model), showing that it possesses
an autonomous structure and also that equality $\llbracket\Gamma\rhd
v:\mathbb{A}\rrbracket=\llbracket\Gamma\rhd w:\mathbb{A}\rrbracket$ in the
syntactic category is equivalent to provability $\Gamma\rhd v=w:\mathbb{A}$ in
the theory.

The syntactic category of $T$ has as objects the types of $T$ and as morphisms
$\mathbb{A}\to\mathbb{B}$ the equivalence classes (w.r.t. provability) of
terms $v$ for which we can derive $x:\mathbb{A}\rhd v:\mathbb{B}$.

Next let us focus on the topic of internal languages, for which the following
result is quite useful.

######  Theorem 2.8.

Consider a linear $\lambda$-theory $T$ and a model of $T$ on an autonomous
category $\mathsf{C}$. The model induces a functor
$F:\mathrm{Syn}(T)\to\mathsf{C}$ that (strictly) preserves the autonomous
structure.

######  Proof 2.9 (Proof sketch).

Consider a model of $T$ on a category $\mathsf{C}$. Then for any judgement
$x:\mathbb{A}\rhd v:\mathbb{B}$, the induced functor $F$ sends the equivalence
class $[v]$ into $\llbracket x:\mathbb{A}\rhd v:\mathbb{B}\rrbracket$.

An autonomous category $\mathsf{C}$ induces a linear $\lambda$-theory
$\mathrm{Lang}(\mathsf{C})$ whose ground types $X\in G$ are the objects of
$\mathsf{C}$ and whose signature $\Sigma$ of operation symbols consists of all
the morphisms in $\mathsf{C}$ plus certain isomorphisms that we describe in
(2). The axioms of $\mathrm{Lang}(\mathsf{C})$ are all the equations satisfied
by the obvious interpretation in $\mathsf{C}$. In order to explicitly
distinguish the autonomous structure of $\mathsf{C}$ from the type structure
of $\mathrm{Lang}(\mathsf{C})$ let us denote the tensor of $\mathsf{C}$ by
$\hat{\otimes}$, the unit by $\hat{\mathbb{I}}$, and the exponential by
$\widehat{\multimap}$. Consider then the following map on types:

$\displaystyle i(\mathbb{I})=\hat{\mathbb{I}}\qquad i(X)=X\qquad
i(\mathbb{A}\otimes\mathbb{B})=i(\mathbb{A})\ \hat{\otimes}\
i(\mathbb{B})\qquad i(\mathbb{A}\multimap\mathbb{B})=i(\mathbb{A})\
\widehat{\multimap}\ i(\mathbb{B})$ (2)

For each type $\mathbb{A}$ we add an isomorphism $\mathbb{A}\simeq
i(\mathbb{A})$ to the theory $\mathrm{Lang}(\mathsf{C})$.

######  Theorem 2.10 (Internal language).

For every autonomous category $\mathsf{C}$ there exists an equivalence of
categories $\mathrm{Syn}(\mathrm{Lang}(\mathsf{C}))\simeq\mathsf{C}$.

######  Proof 2.11 (Proof sketch).

By construction, we have an interpretation of $\mathrm{Lang}(\mathsf{C})$ in
$\mathsf{C}$ which behaves as the identity for operation symbols and ground
types. This interpretation is a model of $\mathrm{Lang}(\mathsf{C})$ on
$\mathsf{C}$ and by Theorem 2.8 we obtain a functor
$\mathrm{Syn}(\mathrm{Lang}(\mathsf{C}))\to\mathsf{C}$. The functor in the
opposite direction behaves as the identity on objects and sends a
$\mathsf{C}$-morphism $f$ into $[f(x)]$. The equivalence of categories is then
shown by using the aforementioned isomorphisms which connect the type
constructors of $\mathrm{Lang}(\mathsf{C})$ with the autonomous structure of
$\mathsf{C}$.

##  3 From equations to $\mathcal{V}$-equations

We now extend the results of the previous section to the setting of
$\mathcal{V}$-equations.

###  3.1 A $\mathcal{V}$-equational deductive system

Let $\mathcal{V}$ denote a commutative and unital quantale,
$\otimes:\mathcal{V}\times\mathcal{V}\to\mathcal{V}$ the corresponding binary
operation, and $k$ the corresponding unit [32]. As mentioned in the
introduction, $\mathcal{V}$ induces the notion of a $\mathcal{V}$-equation,
i.e. an equation $t=_{q}s$ labelled by an element $q$ of $\mathcal{V}$. This
subsection explores this concept by introducing a $\mathcal{V}$-equational
deductive system for linear $\lambda$-calculus and a notion of a linear
$\mathcal{V}\lambda$-theory.

Let us start by recalling two definitions concerning ordered structures [14,
16] and then explain their relevance to our work.

######  Definition 3.1.

Consider a complete lattice $L$. For every $x,y\in L$ we say that $y$ is _way-
below_ $x$ (in symbols, $y\ll x$) if for every subset $X\subseteq L$ whenever
$x\leq\bigvee X$ there exists a _finite_ subset $A\subseteq X$ such that
$y\leq\bigvee A$. The lattice $L$ is called _continuous_ iff for every $x\in
L$,

$\displaystyle x=\bigvee\\{y\mid y\in L\ \text{and}\ y\ll x\\}$

######  Definition 3.2.

Let $L$ be a complete lattice. A _basis_ $B$ of $L$ is a subset $B\subseteq L$
such that for every $x\in L$ the set $B\cap\\{y\mid y\in L\ \text{and}\ y\ll
x\\}$ is directed and has $x$ as the least upper bound.

From now on we assume that the underlying lattice of $\mathcal{V}$ is
continuous and has a basis $B$ which is closed under finite joins, the
multiplication of the quantale $\otimes$ and contains the unit $k$. These
assumptions will allow us to work _only_ with a specified subset of
$\mathcal{V}$-equations chosen e.g. for computational reasons, such as the
_finite_ representation of values $q\in\mathcal{V}$.

######  Example 3.3.

The Boolean quantale $((\\{0\leq 1\\},\vee),\otimes:=\wedge)$ is _finite_ and
thus continuous [14]. Since it is continuous, $\\{0,1\\}$ itself is a basis
for the quantale that satisfies the conditions above. For the Gödel t-norm
[11] $(([0,1],\vee),\otimes:=\wedge)$, the way-below relation is the strictly-
less relation $<$ with the exception that $0<0$. A basis for the underlying
lattice that satisfies the conditions above is the set $\mathbb{Q}\cap[0,1]$.
Note that, unlike real numbers, rationals numbers always have a finite
representation. For the metric quantale (also known as Lawvere quantale)
$(([0,\infty],\wedge),\otimes:=+)$, the way-below relation corresponds to the
_strictly greater_ relation with $\infty>\infty$, and a basis for the
underlying lattice that satisfies the conditions above is the set of extended
non-negative rational numbers. The latter also serves as basis for the
ultrametric quantale $(([0,\infty],\wedge),\otimes:=\max)$.

We also assume that $\mathcal{V}$ is _integral_ , i.e. that the unit $k$ is
the top element of $\mathcal{V}$. This will allow us to establish a smoother
theory of $\mathcal{V}$-equations, whilst still covering e.g. all the examples
above. This assumption is common in quantale theory [39].

Recall the term formation rules of linear $\lambda$-calculus from Fig. 1. A
$\mathcal{V}$-equation-in-context is an expression $\Gamma\rhd
v=_{q}w:\mathbb{A}$ with $q\in B$ (the basis of $\mathcal{V}$), $\Gamma\rhd
v:\mathbb{A}$ and $\Gamma\rhd w:\mathbb{A}$. Let $\top$ be the top element in
$\mathcal{V}$. An equation-in-context $\Gamma\rhd v=w:\mathbb{A}$ now denotes
the particular case in which both $\Gamma\rhd v=_{\top}w:\mathbb{A}$ and
$\Gamma\rhd w=_{\top}v:\mathbb{A}$. For the case of the Boolean quantale,
$\mathcal{V}$-equations are labelled by $\\{0,1\\}$. We will see that
$\Gamma\rhd v=_{1}w:\mathbb{A}$ can be treated as an inequation $\Gamma\rhd
v\leq w:\mathbb{A}$, whilst $\Gamma\rhd v=_{0}w:\mathbb{A}$ corresponds to a
trivial $\mathcal{V}$-equation, i.e. a $\mathcal{V}$-equation that always
holds. For the Gödel t-norm, we can choose $\mathbb{Q}\cap[0,1]$ as basis and
then obtain what we call _fuzzy inequations_. For the metric quantale, we can
choose the set of extended non-negative rational numbers as basis and then
obtain _metric equations_ in the spirit of [29, 30]. Similarly, by choosing
the ultrametric quantale $(([0,\infty],\wedge),\otimes:=\max)$ with the set of
extended non-negative rational numbers as basis we obtain what we call
_ultrametric equations_.

######  Definition 3.4 (Linear $\mathcal{V}\lambda$-theories).

Consider a tuple $(G,\Sigma)$ consisting of a class $G$ of ground types and a
class of sorted operation symbols
$f:\mathbb{A}_{1},\dots,\mathbb{A}_{n}\to\mathbb{A}$ with $n\geq 1$. A linear
$\mathcal{V}\lambda$-theory $((G,\Sigma),Ax)$ is a tuple such that $Ax$ is a
class of $\mathcal{V}$-equations-in-context over linear $\lambda$-terms built
from $(G,\Sigma)$.

$\displaystyle v=_{\top}v\hskip 34.14322ptv=_{q\otimes r}uv=_{q}w\qquad
w=_{r}u\hskip 34.14322ptv=_{r}wv=_{q}w\qquad r\leq q$

$\displaystyle\hskip 56.9055ptv=_{q}w\forall r\ll q.\ v=_{r}w\hskip
42.67912ptv=_{\vee q_{i}}w\forall i\leq n.\ v=_{q_{i}}w$

$\displaystyle\hskip 56.9055ptf(v_{1},\dots,v_{n})=_{\otimes
q_{i}}f(w_{1},\dots,w_{n})\forall i\leq n.\ v_{i}=_{q_{i}}w_{i}\hskip
28.45274ptv\otimes v^{\prime}=_{q\otimes r}w\otimes w^{\prime}v=_{q}w\quad
v^{\prime}=_{r}w^{\prime}$

$\displaystyle\hskip 96.73918pt\mathtt{pm}\ v\ \mathtt{to}\ x\otimes y.\
v^{\prime}=_{q\otimes r}\mathtt{pm}\ w\ \mathtt{to}\ x\otimes y.\
w^{\prime}v=_{q}w\qquad v^{\prime}=_{r}w^{\prime}$

$\displaystyle v\ \mathtt{to}\ \ast.\ v^{\prime}=_{q\otimes r}w\ \mathtt{to}\
\ast.\ w^{\prime}v=_{q}w\qquad v^{\prime}=_{r}w^{\prime}\hskip
34.14322pt\lambda x:\mathbb{A}.\ v=_{q}\lambda x:\mathbb{A}.\ wv=_{q}w\hskip
34.14322ptv\,v^{\prime}=_{q\otimes r}w\,w^{\prime}v=_{q}w\quad
v^{\prime}=_{r}w^{\prime}$

$\displaystyle\hskip 28.45274pt\Delta\rhd v=_{q}w:\mathbb{A}\Gamma\rhd
v=_{q}w:\mathbb{A}\qquad\Delta\in perm(\Gamma)\hskip
56.9055ptv[v^{\prime}/x]=_{q\otimes r}w[w^{\prime}/x]v=_{q}w\qquad
v^{\prime}=_{r}w^{\prime}$

Figure 4: $\mathcal{V}$-congruence rules.

The elements of $Ax$ are the axioms of the theory. Let $Th(Ax)$ be the
smallest class that contains $Ax$ and that is closed under the rules of Fig. 3
and of Fig. 4 (as usual we omit the context and typing information). The
elements of $Th(Ax)$ are the theorems of the theory.

Let us examine the rules in Fig. 4 in more detail. They can be seen as a
generalisation of the notion of a congruence. The rules (refl) and (trans) are
a generalisation of equality’s reflexivity and transitivity. Rule (weak)
encodes the principle that the higher the label in the $\mathcal{V}$-equation,
the ‘tighter’ is the relation between the two terms in the
$\mathcal{V}$-equation. In other words, $v=_{r}w$ is subsumed by $v=_{q}w$,
for $r\leq q$. This can be seen clearly e.g. with the metric quantale by
reading $v=_{q}w$ as “the terms $v$ and $w$ are _at most_ at distance $q$ from
each other” (recall that in the metric quantale the usual order is reversed,
i.e. $\leq\ :=\ \geq_{[0,\infty]}$). (arch) is essentially a generalisation of
the Archimedean rule in [29, 30]. It says that if $v=_{r}w$ for all
_approximations_ $r$ of $q$ then it is also the case that $v=_{q}w$. (join)
says that deductions are closed under finite joins, and in particular it is
always the case that $v=_{\bot}w$. All other rules correspond to a
generalisation of _compatibility_ to a $\mathcal{V}$-equational setting.

The reader may have noticed that the rules in Fig. 4 do not contain a
$\mathcal{V}$-generalisation of symmetry w.r.t. standard equality. Such a
generalisation would be:

$\displaystyle w=_{q}vv=_{q}w$

This rule is not present in Fig. 4 because in some quantales $\mathcal{V}$ it
forces too many $\mathcal{V}$-equations. For example, in the Boolean quantale
the condition $v\leq w$ would automatically entail $w\leq v$ (due to
symmetry); in fact, for this particular case symmetry forces the notion of
inequation to collapse into the classical notion of equation. On the other
hand, symmetry is desirable in the (ultra)metric case because (ultra)metrics
need to respect the symmetry equation [16].

######  Definition 3.5 (Symmetric linear $\mathcal{V}\lambda$-theories).

A symmetric linear $\mathcal{V}\lambda$-theory is a linear
$\mathcal{V}\lambda$-theory whose set of theorems is closed under symmetry.

In Appendix A we further explore how specific families of quantales are
reflected in the $\mathcal{V}$-equational system here introduced, and briefly
compare the latter to metric algebra [29, 30].

###  3.2 Semantics of $\mathcal{V}$-equations

In this subsection we set the necessary background for presenting a sound and
complete class of models for (symmetric) linear $\mathcal{V}\lambda$-theories.
We start by recalling basics concepts of $\mathcal{V}$-categories, which are
central in a field initiated by Lawvere in [24] and can be intuitively seen as
generalised metric spaces [38, 17, 39]. As we will see,
$\mathcal{V}$-categories provide structure to suitably interpret
$\mathcal{V}$-equations.

######  Definition 3.6.

A (small) $\mathcal{V}$-category is a pair $(X,a)$ where $X$ is a class (set)
and $a:X\times X\to\mathcal{V}$ is a function that satisfies:

$\displaystyle k\leq a(x,x)\qquad\text{ and }\qquad a(x,y)\otimes a(y,z)\leq
a(x,z)\hskip 56.9055pt(x,y,z\in X)$

For two $\mathcal{V}$-categories $(X,a)$ and $(Y,b)$, a $\mathcal{V}$-functor
$f:(X,a)\to(Y,b)$ is a function $f:X\to Y$ that satisfies the inequality
$a(x,y)\leq b(f(x),f(y))$ for all $x,y\in X$.

Small $\mathcal{V}$-categories and $\mathcal{V}$-functors form a category
which we denote by $\mathcal{V}\text{-}\mathsf{Cat}$. A $\mathcal{V}$-category
$(X,a)$ is called _symmetric_ if $a(x,y)=a(y,x)$ for all $x,y\in X$. We denote
by $\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sym}}$ the full subcategory of
$\mathcal{V}\text{-}\mathsf{Cat}$ whose objects are symmetric. Every
$\mathcal{V}$-category carries a natural order defined by $x\leq y$ whenever
$k\leq a(x,y)$. A $\mathcal{V}$-category is called _separated_ if its natural
order is anti-symmetric. We denote by
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$ the full subcategory of
$\mathcal{V}\text{-}\mathsf{Cat}$ whose objects are separated.

######  Example 3.7.

For $\mathcal{V}$ the Boolean quantale,
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$ is the category
$\mathsf{Pos}$ of partially ordered sets and monotone maps;
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sym,sep}}$ is simply the category
$\mathsf{Set}$ of sets and functions. For $\mathcal{V}$ the metric quantale,
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sym,sep}}$ is the category
$\mathsf{Met}$ of extended metric spaces and non-expansive maps. In what
follows we omit the qualifier ‘extended’ in ‘extended (ultra)metric spaces’.
For $\mathcal{V}$ the ultrametric quantale,
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sym,sep}}$ is the category of
ultrametric spaces and non-expansive maps.

The inclusion functor
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}\hookrightarrow\mathcal{V}\text{-}\mathsf{Cat}$
has a left adjoint [17]. It is constructed first by defining the equivalence
relation $x\sim y$ whenever $x\leq y$ and $y\leq x$ (for $\leq$ the natural
order introduced earlier). Then this relation induces the separated
$\mathcal{V}$-category $(X/_{\sim},\tilde{a})$ where $\tilde{a}$ is defined as
$\tilde{a}([x],[y])=a(x,y)$ for every $[x],[y]\in X/_{\sim}$. The left adjoint
of the inclusion functor
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}\hookrightarrow\mathcal{V}\text{-}\mathsf{Cat}$
sends every $\mathcal{V}$-category $(X,a)$ to $(X/_{\sim},\tilde{a})$. This
quotienting construct preserves symmetry, and therefore we automatically
obtain the following result.

######  Theorem 3.8.

The inclusion functor
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sym,sep}}\hookrightarrow\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sym}}$
has a left adjoint.

Next, we recall notions of enriched category theory [19] instantiated into the
setting of _autonomous categories enriched over $\mathcal{V}$-categories_. We
will use the enriched structure to give semantics to $\mathcal{V}$-equations
between linear $\lambda$-terms. First, note that every category
$\mathcal{V}\text{-}\mathsf{Cat}$ is autonomous with the tensor
$(X,a)\otimes(Y,b):=(X\times Y,a\otimes b)$ where $a\otimes b$ is defined as
$(a\otimes b)((x,y),(x^{\prime},y^{\prime}))=a(x,x^{\prime})\otimes
b(y,y^{\prime})$ and the set of $\mathcal{V}$-functors
$\mathcal{V}\text{-}\mathsf{Cat}((X,a),(Y,b))$ equipped with the map
$(f,g)\mapsto\bigwedge_{x\in X}b(f(x),g(x))$.

######  Theorem 3.9.

The categories $\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sym}}$,
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$, and
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sym,sep}}$ inherit the autonomous
structure of $\mathcal{V}\text{-}\mathsf{Cat}$ whenever $\mathcal{V}$ is
integral.

Since we assume that $\mathcal{V}$ is integral, this last theorem allows us to
formally define the notion of categories enriched over
$\mathcal{V}$-categories using [19].

######  Definition 3.10.

A category $\mathsf{C}$ is $\mathcal{V}\text{-}\mathsf{Cat}$-enriched (or
simply, a $\mathcal{V}\text{-}\mathsf{Cat}$-category) if for all
$\mathsf{C}$-objects $X$ and $Y$ the hom-set $\mathsf{C}(X,Y)$ is a
$\mathcal{V}$-category and if the composition of $\mathsf{C}$-morphisms,

$\displaystyle(\ \cdot\
):\mathsf{C}(X,Y)\otimes\mathsf{C}(Y,Z)\longrightarrow\mathsf{C}(X,Z)$

is a $\mathcal{V}$-functor. Given two
$\mathcal{V}\text{-}\mathsf{Cat}$-categories $\mathsf{C}$ and $\mathsf{D}$ and
a functor $F:\mathsf{C}\to\mathsf{D}$, we call $F$ a
$\mathcal{V}\text{-}\mathsf{Cat}$-functor if for all $\mathsf{C}$-objects $X$
and $Y$ the map $F_{X,Y}:\mathsf{C}(X,Y)\to\mathsf{D}(FX,F,Y)$ is a
$\mathcal{V}$-functor. An adjunction $\mathsf{C}:F\dashv G:\mathsf{D}$ is
called $\mathcal{V}\text{-}\mathsf{Cat}$-enriched if the underlying functors
$F$ and $G$ are $\mathcal{V}\text{-}\mathsf{Cat}$-functors and if for all
objects $X\in|\mathsf{C}|$ and $Y\in|\mathsf{D}|$ there exists a
$\mathcal{V}$-isomorphism $\mathsf{D}(FX,Y)\simeq\mathsf{C}(X,GY)$ natural in
$X$ and $Y$.

If $\mathsf{C}$ is a $\mathcal{V}\text{-}\mathsf{Cat}$-category then
$\mathsf{C}\times\mathsf{C}$ is also a
$\mathcal{V}\text{-}\mathsf{Cat}$-category via the tensor operation $\otimes$
in $\mathcal{V}\text{-}\mathsf{Cat}$. We take advantage of this fact in the
following definition.

######  Definition 3.11.

A $\mathcal{V}\text{-}\mathsf{Cat}$-enriched autonomous category $\mathsf{C}$
is an autonomous and $\mathcal{V}\text{-}\mathsf{Cat}$-category $\mathsf{C}$
such that the bifunctor $\otimes:\mathsf{C}\times\mathsf{C}\to\mathsf{C}$ is a
$\mathcal{V}\text{-}\mathsf{Cat}$-functor and the adjunction $(-\otimes
X)\dashv(X\multimap-)$ is a $\mathcal{V}\text{-}\mathsf{Cat}$-adjunction.

######  Example 3.12.

Recall that $\mathsf{Pos}\simeq\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$
when $\mathcal{V}$ is the Boolean quantale. According to Theorem 3.9 the
category $\mathsf{Pos}$ is autonomous. It follows by general results that the
category is $\mathsf{Pos}$-enriched [6]. It is also easy to see that its
tensor is $\mathsf{Pos}$-enriched and that the adjunction $(-\otimes
X)\dashv(X\multimap-)$ is $\mathsf{Pos}$-enriched. Therefore, $\mathsf{Pos}$
is an instance of Definition 3.11. Note also that
$\mathsf{Set}\simeq\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sym,sep}}$ for
$\mathcal{V}$ the Boolean quantale and that $\mathsf{Set}$ is an instance of
Definition 3.11.

Recall that
$\mathsf{Met}\simeq\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sym,sep}}$ when
$\mathcal{V}$ is the metric quantale. Thus, the category $\mathsf{Met}$ is
autonomous (Theorem 3.9) and $\mathsf{Met}$-enriched [6]. It follows as well
from routine calculations that its tensor is $\mathsf{Met}$-enriched and that
the adjunction $(-\otimes X)\dashv(X\multimap-)$ is $\mathsf{Met}$-enriched.
Therefore $\mathsf{Met}$ is an instance of Definition 3.11. An analogous
reasoning tells that the category of ultrametric spaces (enriched over itself)
is also an instance of Definition 3.11.

Finally, recall the interpretation of linear $\lambda$-terms on an autonomous
category $\mathsf{C}$ (Section 2) and assume that $\mathsf{C}$ is
$\mathcal{V}\text{-}\mathsf{Cat}$-enriched. Then we say that a
$\mathcal{V}$-equation $\Gamma\rhd v=_{q}w:\mathbb{A}$ is _satisfied_ by this
interpretation if $a(\llbracket\Gamma\rhd
v:\mathbb{A}\rrbracket,\llbracket\Gamma\rhd w:\mathbb{A}\rrbracket)\geq q$
where
$a:\mathsf{C}(\llbracket\Gamma\rrbracket,\llbracket\mathbb{A}\rrbracket)\times\mathsf{C}(\llbracket\Gamma\rrbracket,\llbracket\mathbb{A}\rrbracket)\to\mathcal{V}$
is the underlying function of the $\mathcal{V}$-category
$\mathsf{C}(\llbracket\Gamma\rrbracket,\llbracket\mathbb{A}\rrbracket)$.

######  Theorem 3.13.

The rules listed in Fig. 3 and Fig. 4 are sound for
$\mathcal{V}\text{-}\mathsf{Cat}$-enriched autonomous categories $\mathsf{C}$.
Specifically, if $\Gamma\rhd v=_{q}w:\mathbb{A}$ results from the rules in
Fig. 3 and Fig. 4 then $a(\llbracket\Gamma\rhd
v:\mathbb{A}\rrbracket,\llbracket\Gamma\rhd w:\mathbb{A}\rrbracket)\geq q$.

######  Proof 3.14 (Proof of Theorem 3.13).

Let us focus first on the equations listed in Fig. 3. Recall that an equation
$\Gamma\rhd v=w:\mathbb{A}$ abbreviates the $\mathcal{V}$-equations
$\Gamma\rhd v=_{\top}w:\mathbb{A}$ and $\Gamma\rhd w=_{\top}v:\mathbb{A}$.
Moreover, we already know that the equations listed in Fig. 3 are sound for
autonomous categories, specifically if $v=w$ is an equation of Fig. 3 then
$\llbracket v\rrbracket=\llbracket w\rrbracket$ in $\mathsf{C}$ (Theorem 2.3).
Thus, by the definition of a $\mathcal{V}$-category and by the assumption of
$\mathcal{V}$ being integral ($k=\top$) we obtain $a(\llbracket
v\rrbracket,\llbracket w\rrbracket)\geq k=\top$ and $a(\llbracket
w\rrbracket,\llbracket v\rrbracket)\geq k=\top$.

Let us now focus on the rules listed in Fig. 4. The first three rules follow
from the definition of a $\mathcal{V}$-category and the transitivity property
of $\leq$. Rule (arch) follows from the continuity of $\mathcal{V}$,
specifically from the fact that $q$ is the _least_ upper bound of all elements
$r$ that are way-below $q$. Rule (join) follows from the definition of least
upper bound. The remaining rules follow from the definition of the tensor
functor $\otimes$ in $\mathcal{V}\text{-}\mathsf{Cat}$, the fact that
$\mathsf{C}$ is $\mathcal{V}\text{-}\mathsf{Cat}$-enriched,
$\otimes:\mathsf{C}\times\mathsf{C}\to\mathsf{C}$ is a
$\mathcal{V}\text{-}\mathsf{Cat}$-functor, and the fact that $(-\otimes
X)\dashv(X\multimap-)$ is a $\mathcal{V}\text{-}\mathsf{Cat}$-adjunction. For
example, for the sixth rule we reason as follows:

$\displaystyle\,a(\llbracket f(v_{1},\dots,v_{n})\rrbracket,\llbracket
f(w_{1},\dots,w_{n})\rrbracket)$ $\displaystyle=a(\llbracket
f\rrbracket\cdot(\llbracket v_{1}\rrbracket\otimes\dots\otimes\llbracket
v_{n}\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma_{1};\dots;\Gamma_{n}}\cdot\operatorname{\mathsf{sh}}_{E},\llbracket
f\rrbracket\cdot(\llbracket w_{1}\rrbracket\otimes\dots\otimes\llbracket
w_{n}\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma_{1};\dots;\Gamma_{n}}\cdot\operatorname{\mathsf{sh}}_{E})$
$\displaystyle\geq a(\llbracket f\rrbracket\cdot(\llbracket
v_{1}\rrbracket\otimes\dots\otimes\llbracket v_{n}\rrbracket),\llbracket
f\rrbracket\cdot(\llbracket w_{1}\rrbracket\otimes\dots\otimes\llbracket
w_{n}\rrbracket))$ $\displaystyle\geq a(\llbracket
v_{1}\rrbracket\otimes\dots\otimes\llbracket v_{n}\rrbracket),(\llbracket
w_{1}\rrbracket\otimes\dots\otimes\llbracket w_{n}\rrbracket)$
$\displaystyle\geq a(\llbracket v_{1}\rrbracket,\llbracket
w_{1}\rrbracket)\otimes\dots\otimes a(\llbracket v_{n}\rrbracket,\llbracket
w_{n}\rrbracket)$ $\displaystyle\geq q_{1}\otimes\dots\otimes q_{n}$

where the second step follows from the fact that
$\operatorname{\mathsf{sp}}_{\Gamma_{1};\dots;\Gamma_{n}}\cdot\operatorname{\mathsf{sh}}_{E}$
is a morphism in $\mathsf{C}$ and that $\mathsf{C}$ is
$\mathcal{V}\text{-}\mathsf{Cat}$-enriched. The third step follows from an
analogous reasoning. The fourth step follows from the fact that
$\otimes:\mathsf{C}\times\mathsf{C}\to\mathsf{C}$ is a
$\mathcal{V}\text{-}\mathsf{Cat}$-functor. The last step follows from the
premise of the rule in question. As another example, the proof for the
substitution rule proceeds similarly:

$\displaystyle\,a(\llbracket v[v^{\prime}/x]\rrbracket,\llbracket
w[w^{\prime}/x]\rrbracket)$ $\displaystyle=a(\llbracket
v\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma,\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket
v^{\prime}\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta},\llbracket
w\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma,\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket
w^{\prime}\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta})$
$\displaystyle\geq a(\llbracket
v\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma,\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket
v^{\prime}\rrbracket),\llbracket
w\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma,\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket
w^{\prime}\rrbracket))$ $\displaystyle\geq
a(\operatorname{\mathsf{id}}\otimes\llbracket
v^{\prime}\rrbracket,\operatorname{\mathsf{id}}\otimes\llbracket
w^{\prime}\rrbracket)\otimes a(\llbracket
v\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma,\mathbb{A}},\llbracket
w\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma,\mathbb{A}})$
$\displaystyle\geq a(\operatorname{\mathsf{id}}\otimes\llbracket
v^{\prime}\rrbracket,\operatorname{\mathsf{id}}\otimes\llbracket
w^{\prime}\rrbracket)\otimes a(\llbracket v\rrbracket,\llbracket w\rrbracket)$
$\displaystyle\geq
a(\operatorname{\mathsf{id}},\operatorname{\mathsf{id}})\otimes a(\llbracket
v^{\prime}\rrbracket,\llbracket w^{\prime}\rrbracket)\otimes a(\llbracket
v\rrbracket,\llbracket w\rrbracket)$ $\displaystyle=a(\llbracket
v^{\prime}\rrbracket,\llbracket w^{\prime}\rrbracket)\otimes a(\llbracket
v\rrbracket,\llbracket w\rrbracket)$ $\displaystyle\geq q\otimes r$

The proof for the rule concerning $(\multimap_{i})$ additionally requires the
following two facts: if a $\mathcal{V}$-functor $f:(X,a)\to(Y,b)$ is an
isomorphism then $a(x,x^{\prime})=b(f(x),f(x^{\prime}))$ for all
$x,x^{\prime}\in X$. For a context $\Gamma$, the morphism
$\operatorname{\mathsf{jn}}_{\Gamma;x:\mathbb{A}}:\llbracket\Gamma\rrbracket\otimes\llbracket\mathbb{A}\rrbracket\to\llbracket\Gamma,x:\mathbb{A}\rrbracket$
is an isomorphism in $\mathsf{C}$. The proof for the rule concerning the
permutation of variables (exchange) also makes use of the fact that
$\llbracket\Delta\rrbracket\to\llbracket\Gamma\rrbracket$ is an isomorphism.

###  3.3 Soundness, completeness, and internal language

In this subsection we establish a formal correspondence between linear
$\mathcal{V}\lambda$-theories and $\mathcal{V}\text{-}\mathsf{Cat}$-enriched
autonomous categories, via soundness, completeness, and internal language
theorems. A key construct in this correspondence is the quotienting of a
$\mathcal{V}$-category into a _separated_ $\mathcal{V}$-category: we will use
it to identify linear $\lambda$-terms when generating a syntactic category
(from a linear $\mathcal{V}\lambda$-theory) that satisfies the axioms of
autonomous categories. This naturally leads to the following notion of a model
for linear $\mathcal{V}\lambda$-theories.

######  Definition 3.15 (Models of linear $\mathcal{V}\lambda$-theories).

Consider a linear $\mathcal{V}\lambda$-theory $((G,\Sigma),Ax)$ and a
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$-enriched autonomous category
$\mathsf{C}$. Suppose that for each $X\in G$ we have an interpretation
$\llbracket X\rrbracket$ as a $\mathsf{C}$-object and analogously for the
operation symbols. This interpretation structure is a model of the theory if
all axioms in $Ax$ are satisfied by the interpretation.

Another thing that we need to take into account is the size of categories. In
Section 2 we did not assume that autonomous categories should be locally
small. In particular linear $\lambda$-theories are able to generate
non-(locally small) categories. Now we need to be stricter because
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$-enriched autonomous
categories are always locally small (recall the definition of
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$). Thus for two types
$\mathbb{A}$ and $\mathbb{B}$ of a $\mathcal{V}\lambda$-theory $T$, consider
the class $\mathsf{Values}(\mathbb{A},\mathbb{B})$ of values $v$ such that
$x:\mathbb{A}\rhd v:\mathbb{B}$. We equip
$\mathsf{Values}(\mathbb{A},\mathbb{B})$ with the function
$a:\mathsf{Values}(\mathbb{A},\mathbb{B})\times\mathsf{Values}(\mathbb{A},\mathbb{B})\to\mathcal{V}$
defined by,

$\displaystyle a(v,w)=\bigvee\\{q\mid v=_{q}w\text{ is a theorem of }T\\}$

It is easy to see that $(\mathsf{Values}(\mathbb{A},\mathbb{B}),a)$ is a
(possibly large) $\mathcal{V}$-category. We then quotient this
$\mathcal{V}$-category into a _separated_ $\mathcal{V}$-category which we
suggestively denote by $\mathsf{C}(\mathbb{A},\mathbb{B})$ (as detailed in the
proof of the next theorem, $\mathsf{C}(\mathbb{A},\mathbb{B})$ will serve as a
hom-object of a syntactic category $\mathsf{C}$ generated from a linear
$\mathcal{V}\lambda$-theory). Following the nomenclature of [25], we call $T$
_varietal_ if $\mathsf{C}(\mathbb{A},\mathbb{B})$ is a _small_
$\mathcal{V}$-category. In the rest of the paper we will only work with
varietal theories and locally small categories.

######  Theorem 3.16 (Soundness & Completeness).

Consider a varietal $\mathcal{V}\lambda$-theory. A $\mathcal{V}$-equation-in-
context $\Gamma\rhd v=_{q}w:\mathbb{A}$ is a theorem iff it holds in all
models of the theory.

######  Proof 3.17 (Proof sketch).

Soundness follows by induction over the rules that define the class $Th(Ax)$
(Definition 3.4) and by Theorem 3.13. For completeness, we use a strategy
similar to the proof of Theorem 2.6, and take advantage of the quotienting of
a $\mathcal{V}$-category into a separated $\mathcal{V}$-category. Recall that
we assume that the theory is _varietal_ and therefore can safely take
$\mathsf{C}(\mathbb{A},\mathbb{B})$ to be a small $\mathcal{V}$-category. Note
that the quotienting process identifies all terms $x:\mathbb{A}\rhd
v:\mathbb{B}$ and $x:\mathbb{A}\rhd w:\mathbb{B}$ such that $v=_{\top}w$ and
$w=_{\top}v$. Such a relation contains the equations-in-context from Fig. 3
and moreover it is straighforward to show that it is compatible with the term
formation rules of linear $\lambda$-calculus (Fig. 1). So, analogously to
Theorem 2.6 we obtain an autonomous category $\mathsf{C}$ whose objects are
the types of the language and whose hom-sets are the underlying sets of the
$\mathcal{V}$-categories $\mathsf{C}(\mathbb{A},\mathbb{B})$.

Our next step is to show that the category $\mathsf{C}$ has a
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$-enriched autonomous
structure. We start by showing that the composition map
$\mathsf{C}(\mathbb{A},\mathbb{B})\otimes\mathsf{C}(\mathbb{B},\mathbb{C})\to\mathsf{C}(\mathbb{A},\mathbb{C})$
is a $\mathcal{V}$-functor:

$\displaystyle a(([v^{\prime}],[v]),([w^{\prime}],[w]))$
$\displaystyle=a([v],[w])\otimes a([v^{\prime}],[w^{\prime}])$
$\displaystyle=a(v,w)\otimes a(v^{\prime},w^{\prime})$
$\displaystyle=\bigvee\\{q\mid v=_{q}w\\}\otimes\bigvee\\{r\mid
v^{\prime}=_{r}w^{\prime}\\}$ $\displaystyle=\bigvee\\{q\otimes r\mid
v=_{q}w,v^{\prime}=_{r}w^{\prime}\\}$ $\displaystyle\leq\bigvee\\{q\mid
v[v^{\prime}/x]=_{q}w[w^{\prime}/x]\\}$ $\displaystyle(A\subseteq
B\Rightarrow\bigvee A\leq\bigvee B)$
$\displaystyle=a(v[v^{\prime}/x],w[w^{\prime}/x])$
$\displaystyle=a([v[v^{\prime}/x]],[w[w^{\prime}/x]])$
$\displaystyle=a([v]\cdot[v^{\prime}],[w]\cdot[w^{\prime}])$

The fact that $\otimes:\mathsf{C}\times\mathsf{C}\to\mathsf{C}$ is a
$\mathcal{V}\text{-}\mathsf{Cat}$-functor follows by an analogous reasoning.
Next, we need to show that $(-\otimes X)\dashv(X\multimap-)$ is a
$\mathcal{V}\text{-}\mathsf{Cat}$-adjunction. It is straightforward to show
that both functors are $\mathcal{V}\text{-}\mathsf{Cat}$-functors, and from a
similar reasoning it follows that the isomorphism
$\mathsf{C}(\mathbb{B},\mathbb{A}\multimap\mathbb{C})\simeq\mathsf{C}(\mathbb{B}\otimes\mathbb{A},\mathbb{C})$
is a $\mathcal{V}$-isomorphism.

The final step is to show that if an equation $\Gamma\rhd v=_{q}w:\mathbb{A}$
with $q\in B$ is satisfied by $\mathsf{C}$ then it is a theorem of the linear
$\mathcal{V}\lambda$-theory. By assumption $a([v],[w])=a(v,w)=\bigvee\\{r\mid
v=_{r}w\\}\geq q$. It follows from the definition of the way-below relation
that for all $x\in B$ with $x\ll q$ there exists a _finite_ set
$A\subseteq\\{r\mid v=_{r}w\\}$ such that $x\leq\bigvee A$. Then by an
application of rule (join) in Fig. 4 we obtain $v=_{\bigvee A}w$, and
consequently rule (weak) in Fig. 4 provides $v=_{x}w$ for all $x\ll q$.
Finally, by an application of rule (arch) in Fig. 4 we deduce that $v=_{q}w$
is part of the theory.

Next we establish results that will be key in the proof of the internal
language theorem. Let $\mathrm{Syn}(T)$ be syntactic category of a linear
$\mathcal{V}\lambda$-theory $T$, as described in Theorem 3.16.

######  Theorem 3.18.

Consider a linear $\mathcal{V}\lambda$-theory $T$ and a model of $T$ on a
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$-enriched autonomous category
$\mathsf{C}$. The model induces a
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$-functor
$\mathrm{Syn}(T)\to\mathsf{C}$ that (strictly) preserves the autonomous
structure of $\mathrm{Syn}(T)$.

######  Proof 3.19.

Consider a model of $T$ over $\mathsf{C}$. Let $a$ denote the underlying
function of the hom-($\mathcal{V}$-categories) in $\mathrm{Syn}(T)$ and $b$
the underlying function of the hom-($\mathcal{V}$-categories) in $\mathsf{C}$.
Then note that if $[v]=[w]$ then, by completeness, the equations $v=_{\top}w$
and $w=_{\top}v$ are theorems, which means that $\llbracket
v\rrbracket=\llbracket w\rrbracket$ by the definition of a model and
_separability_. This allows us to define a mapping
$F:\mathrm{Syn}(T)\to\mathsf{C}$ that sends each type $\mathbb{A}$ to
$\llbracket\mathbb{A}\rrbracket$ and each morphism $[v]$ to $\llbracket
v\rrbracket$. The fact that this mapping is an autonomous functor follows from
an analogous reasoning to the one used in the proof of Theorem 2.8. We now
need to show that this functor is
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$-enriched. Recall that
$a([v],[w])=\bigvee\\{q\mid v=_{q}w\\}$ and observe that for every $v=_{q}w$
in the previous quantification we have $b(\llbracket v\rrbracket,\llbracket
w\rrbracket)\geq q$ (by the definition of a model), which establishes, by the
definition of a least upper bound, $a([v],[w])=\bigvee\\{q\mid v=_{q}w\\}\leq
b(\llbracket v\rrbracket,\llbracket w\rrbracket)$.

Consider now a $\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$-enriched
autonomous category $\mathsf{C}$. It induces a linear
$\mathcal{V}\lambda$-theory $\mathrm{Lang}(\mathsf{C})$ whose ground types and
operations symbols are defined as in the case of linear $\lambda$-theories
(recall Section 2). The axioms of $\mathrm{Lang}(\mathsf{C})$ are all the
$\mathcal{V}$-equations-in-context that are satisfied by the obvious
interpretation on $\mathsf{C}$.

######  Theorem 3.20.

The linear $\mathcal{V}\lambda$-theory $\mathrm{Lang}(\mathsf{C})$ is
varietal.

In conjunction with the proof of Theorem 3.16, a consequence of this last
theorem is that $\mathrm{Syn}(\mathrm{Lang}(\mathsf{C}))$ is a
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$-enriched category. Then we
state,

######  Theorem 3.21 (Internal language).

For every $\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$-enriched autonomous
category $\mathsf{C}$ there exists a
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$-equivalence of categories
$\mathrm{Syn}(\mathrm{Lang}(\mathsf{C}))\simeq\mathsf{C}$.

######  Proof 3.22.

Let $a$ denote the underlying function of the hom-($\mathcal{V}$-categories)
in $\mathrm{Syn}(\mathrm{Lang}(\mathsf{C}))$ and $b$ the underlying function
of the hom-($\mathcal{V}$-categories) in $\mathsf{C}$. We have, by
construction, a model of $\mathrm{Lang}(\mathsf{C})$ on $\mathsf{C}$ which
acts as the identity in the interpretation of ground types and operation
symbols. We can then appeal to Theorem 3.18 to establish a
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$-functor
$\mathrm{Syn}(\mathrm{Lang}(\mathsf{C}))\to\mathsf{C}$. Next, the functor
working on the inverse direction behaves as the identity on objects and sends
a morphism $f$ into $[f(x)]$. Let us show that it is
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$-enriched. First, observe that
if $q\ll b(f,g)$ in $\mathsf{C}$ and $q\in B$ then $f(x)=_{q}g(x)$ is a
theorem of $\mathrm{Lang}(\mathsf{C})$, due to the fact that $\ll$ entails
$\leq$ and by the definition of $\mathrm{Lang}(\mathsf{C})$. Using the
definition of a basis, we thus obtain $b(f,g)=\bigvee\\{q\in B\mid\>q\ll
b(f,g)\\}\leq\bigvee\\{q\in B\mid f(x)=_{q}g(x)\\}=a([f(x)],[g(x)])$. The
equivalence of categories is then shown as in the proof of Theorem 2.10.

All the results in this section can be extended straightforwardly to the case
of _symmetric_ linear $\mathcal{V}\lambda$-theories and
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sym,sep}}$-enriched autonomous
categories.

##  4 Examples of linear $\mathcal{V}\lambda$-theories and their models

######  Example 4.1 (Wait calls).

We now return to the example of wait calls and the corresponding metric axioms
(1) sketched in the Introduction. Let us build a model over $\mathsf{Met}$ for
this theory: fix a metric space $A$, interpret the ground type $X$ as
$\mathbb{N}\otimes A$ and the operation symbol $\mathtt{wait_{n}}:X\to X$ as
the non-expansive map,
$\llbracket\mathtt{wait_{n}}\rrbracket:\mathbb{N}\otimes A\to\mathbb{N}\otimes
A$ , $(i,a)\mapsto(i+n,a)$. Since we already know that $\mathsf{Met}$ is
enriched over itself (recall Definition 3.11 and Example 3.12) we only need to
show that the axioms in (1) are satisfied by the proposed interpretation. This
can be shown via a few routine calculations.

Now, it may be the case that is unnecessary to know the _distance_ between the
execution time of two programs – instead it suffices to know whether a program
finishes its execution _before_ another one. This leads us to linear
$\mathcal{V}\lambda$-theories where $\mathcal{V}$ is the Boolean quantale. We
call such theories _linear ordered $\lambda$-theories_. Recall the language
from the Introduction with a single ground type $X$ and the signature of wait
calls $\Sigma=\\{\mathtt{wait_{n}}:X\to X\mid n\in\mathbb{N}\\}$. Then we
adapt the metric axioms (1) to the case of the Boolean quantale by considering
instead:

$\displaystyle\mathtt{wait_{0}}(x)=x\hskip
28.45274pt\mathtt{wait_{n}}(\mathtt{wait_{m}}(x))=\mathtt{wait_{n+m}}(x)\hskip
28.45274pt\mathtt{wait_{n}}(x)\leq\mathtt{wait_{m}}(x)n\leq m$

where a classical equation $v=w$ is shorthand for $v\leq w$ (i.e. $v=_{1}w$)
and $w\leq v$ (i.e. $w=_{1}v$). In the resulting theory we can consider for
instance (and omitting types for simplicity) the $\lambda$-term that defines
the composition of two functions $\lambda f.\ \lambda g.\ g\ (f\ x)$, which we
denote by $v$, and show that:

$\displaystyle v\ (\lambda x.\ \mathtt{wait_{1}}(x))\leq v\ (\lambda x.\
\mathtt{wait_{1}}(\mathtt{wait_{1}}(x)))$

This inequation between higher-order programs arises from the argument
$\lambda x.\ \mathtt{wait_{1}}(\mathtt{wait_{1}}(x))$ being costlier than the
argument $\lambda x.\ \mathtt{wait_{1}}(x)$ – specifically, the former will
invoke one more wait call ($\mathtt{wait_{1}}$) than the latter. Moreover, the
inequation entails that for every argument $g$ the execution time of
computation $v\ (\lambda x.\ \mathtt{wait_{1}}(x))\ g$ will always be smaller
than that of computation $v\ (\lambda x.\
\mathtt{wait_{1}}(\mathtt{wait_{1}}(x)))\ g$ since it invokes one more wait
call. Thus in general the inequation tells that costlier programs fed as input
to $v$ will result in longer execution times when performing the corresponding
computation. In order to build a model for the ordered theory of wait calls,
we consider a poset $A$ and define a model over $\mathsf{Pos}$ by sending $X$
into $\mathbb{N}\otimes A$ and $\mathtt{wait_{n}}:X\to X$ to the monotone map
$\llbracket\mathtt{wait_{n}}\rrbracket:\mathbb{N}\otimes A\to\mathbb{N}\otimes
A$, $(i,a)\mapsto(i+n,a)$. Since we already know that $\mathsf{Pos}$ is
enriched over itself (recall Definition 3.11 and Example 3.12) we only need to
show that the ordered axioms are satisfied by the proposed interpretation. But
again, this can be shown via a few routine calculations.

######  Example 4.2 (Probabilistic programs).

We consider ground types $\real,{}^{+},\mathtt{unit}$ and a signature
consisting of $\\{r:\mathbb{I}\to\real\mid
r\in\mathbb{Q}\\}\cup\\{r^{+}:\mathbb{I}\to{}^{+}\mid r\in\mathbb{Q}_{\geq
0}\\}\cup\\{r^{u}:\mathbb{I}\to\mathtt{unit}\mid r\in[0,1]\cap\mathbb{Q}\\}$,
an operation $+$ of type $\real,\real\to\real$, and _sampling_ functions
$\mathtt{bernoulli}:\real,\real,\mathtt{unit}\to\real$ and
$\mathtt{normal}:\real,{}^{+}\to\real$. Whenever no ambiguities arise, we drop
the superscripts in $r^{u}$ and $r^{+}$. Operationally,
$\mathtt{bernoulli}(x,y,p)$ generates a sample from the Bernoulli distribution
with parameter $p$ on the set $\\{x,y\\}$, whilst $\mathtt{normal}(x,y)$
generates a normal deviate with mean $x$ and standard deviation $y$. We then
postulate the metric axiom,

$\displaystyle\mathtt{bernoulli}(x_{1},x_{2},p(\ast))=_{\left\lvert
p-q\right\rvert}\mathtt{bernoulli}(x_{1},x_{2},q(\ast))p,q\in[0,1]\cap\mathbb{Q}$
(3)

We interpret the resulting linear metric $\lambda$-theory in the category
$\mathsf{Ban}$ of Banach spaces and short operators, i.e. the semantics of [9,
20] without the order structure needed to interpret while loops. This is the
usual representation of Markov chains/kernels as matrices/operators.

######  Theorem 4.3.

The category $\mathsf{Ban}$ is a $\mathsf{Met}$-enriched autonomous category,
and thus an instance of Definition 3.11.

In particular, $\mathsf{Ban}$ forms a model for the theory of our small
probabilistic language via the following interpretation. We define
$\llbracket\real\rrbracket=\mathcal{M}\mathbb{R}$, the Banach space of finite
Borel measures on $\mathbb{R}$ equipped with the total variation norm, and
similarly $\llbracket{}^{+}\rrbracket=\mathcal{M}\mathbb{R}^{+}$ and
$\llbracket\mathtt{unit}\rrbracket=\mathcal{M}[0,1]$. We have
$\llbracket\mathbb{I}\rrbracket=\mathbb{R}\ni 1$, and for every
$r\in\mathbb{Q}$ we put $\llbracket
r\rrbracket:\mathbb{R}\to\mathcal{M}\mathbb{R},x\mapsto x\delta_{r}$, where
$\delta_{r}$ is the Dirac delta over $r$; thus $\llbracket
r\rrbracket(1)=\delta_{r}$. We define an analogous interpretation for the
operation symbols $r^{+}$ and $r^{u}$. For
$\mu,\upsilon\in\mathcal{M}\mathbb{R}$ we define
$\llbracket+\rrbracket(\mu\otimes\upsilon)\triangleq+_{\ast}(\mu\otimes\upsilon)$
the pushforward under $+$ of the product measure $\mu\otimes\upsilon$ (seen as
an element of $\mathcal{M}\mathbb{R}\otimes\mathcal{M}\mathbb{R}$, see [9]).
For $\mu,\upsilon,\xi\in\mathcal{M}\mathbb{R}$ we define
$\llbracket\mathtt{bernoulli}\rrbracket(\mu\otimes\upsilon\otimes\xi)\triangleq\mathrm{bern}_{\ast}(\mu\otimes\upsilon\otimes\xi)$,
the pushforward of the product measure $\mu\otimes\upsilon\otimes\xi$ under
the Markov kernel $\mathrm{bern}:\mathbb{R}^{3}\to\mathbb{R},(u,v,p)\mapsto
p\delta_{u}+(1-p)\delta_{v}$, and similarly for
$\llbracket\mathtt{normal}\rrbracket$ (see [9] for the definition of
pushforward by a Markov kernel).

This interpretation is sound (a proof is given in the Appendix) because the
norm on $\mathcal{M}\mathbb{R}$ is the total variation norm, and the metric
axiom (3) describes the total variation distance between the corresponding
Bernoulli distributions. Consider now the following $\lambda$-terms (where we
abbreviate the constants $0(\ast),1(\ast),p(\ast),q(\ast)$ to $0,1,p,q$,
respectively),

$\displaystyle\mathtt{walk1}\triangleq\lambda
x:\real.\mathtt{bernoulli}(0,x+\mathtt{normal}(0,1),p)$
$\displaystyle\mathtt{walk2}\triangleq\lambda
x:\real.\mathtt{bernoulli}(0,x+\mathtt{normal}(0,1),q),\qquad
p,q\in[0,1]\cap\mathbb{Q}.$

As the names suggest, these two terms of type $\real\multimap\real$ are
denoted by random walks on $\mathbb{R}$. At each call, $\mathtt{walk1}$ (resp.
$\mathtt{walk2}$) performs a jump drawn randomly from a standard normal
distribution, or is forced to return to the origin with probability $p$ (resp.
$q$). These are non-standard random walks whose semantics are concretely given
by complicated operators $\mathcal{M}\mathbb{R}\to\mathcal{M}\mathbb{R}$, but
the simple quantitative equational system of Fig. 4 and the axiom (3) allow us
to easily derive $\mathtt{walk1}=_{\left\lvert p-q\right\rvert}\mathtt{walk2}$
without having to compute the semantics of these terms. In other words, the
soundness of (3) is enough to tightly bound the distance between two non-
trivial random walks represented as higher-order terms in a probabilistic
programming language. Furthermore, the tensor in the $\lambda$-calculus allows
us to easily scale up this reasoning to random walks in higher dimensions such
as $\mathtt{walk1}\otimes\mathtt{walk2}$ on $\mathbb{R}^{2}$.

##  5 Conclusions and future work

We introduced the notion of a $\mathcal{V}$-equation which generalises the
well-established notions of equation, inequation [22, 2], and metric equation
[29, 30]. We then presented a sound and complete $\mathcal{V}$-equational
system for linear $\lambda$-calculus, illustrated with different examples of
programs containing real-time and probabilistic behaviour.

Functorial connection to previous work. As a concluding note, let us introduce
a simple yet instructive functorial connection between (1) the categorical
semantics of linear $\lambda$-calculus with the $\mathcal{V}$-equational
system, (2) the categorical semantics of linear $\lambda$-calculus with the
equational system of Section 2, and (3) the algebraic semantics of the
exponential free, multiplicative fragment of linear logic. First we need to
recall some well-known facts. As detailed before, typical categorical models
of linear $\lambda$-calculus and its equational system are locally small
autonomous categories. The latter form a quasicategory $\mathsf{Aut}$ whose
morphisms are autonomous functors. The usual algebraic models of the
exponential free, multiplicative fragment of linear logic are the so-called
_lineales_ [10]. In a nutshell, a lineale is a poset $(X,\leq)$ paired with a
commutative, monoid operation $\otimes:X\times X\to X$ that satisfies certain
conditions. Lineales are almost quantales: the only difference is that they do
not require $X$ to be cocomplete. The key idea in algebraic semantics is that
the order $\leq$ in the lineale encodes the logic’s entailment relation. A
functorial connection between autonomous categories and lineales (i.e. between
(2) and (3)) is stated in [10] and is based on the following two observations.
First, (possibly large) lineales can be seen as _thin_ autonomous categories,
i.e. as elements of the enriched quasicategory $\\{0,1\\}$-$\mathsf{Aut}$.
Second, the inclusion $\\{0,1\\}$-$\mathsf{Aut}$ $\hookrightarrow\mathsf{Aut}$
has a left adjoint which _collapses all morphisms_ of a given autonomous
category $\mathsf{C}$ (intuitively, it eliminates the ability of $\mathsf{C}$
to differentiate different terms between two types). This provides an adjoint
situation between (2) and (3). We can now expand this connection to our
categorical semantics of linear $\lambda$-calculus and corresponding
$\mathcal{V}$-equational system (i.e. (1)) in the following way. The forgetful
functor $\mathcal{V}\text{-}\mathsf{Cat}\to\mathsf{Set}$ has a left adjoint
$D:\mathsf{Set}\to\mathcal{V}\text{-}\mathsf{Cat}$ which sends a set $X$ to
$DX=(X,d)$,

$\displaystyle d(x_{1},x_{2})=\begin{cases}k&\text{ if }x_{1}=x_{2}\\\
\bot&\text{otherwise}\end{cases}$

This left adjoint is strong monoidal, specifically we have $D(X_{1}\times
X_{2})=DX_{1}\otimes DX_{2}$ and $\mathbb{I}=(1,(\ast,\ast)\mapsto k)=D1$.
This gives rise to the functors,

${(\mathcal{V}\text{-}\mathsf{Cat})\text{-}\mathsf{Aut}}$${\mathsf{Aut}}$${\\{0,1\\}\text{-}\mathsf{Aut}}$$\scriptstyle{\hat{D}}$${\scriptscriptstyle{\bot}}$$\scriptstyle{c}$${\scriptscriptstyle{\bot}}$

where $\hat{D}$ equips the hom-sets of an autonomous category with the
corresponding discrete $\mathcal{V}$-category and $c$ collapses all morphisms
of an autonomous category as described earlier. The right adjoint of $\hat{D}$
forgets the $\mathcal{V}$-categorical structure between terms (i.e. morphisms)
and the right adjoint of $c$ is the inclusion functor mentioned earlier. Note
that $\hat{D}$ restricts to
$(\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}})$-$\mathsf{Aut}$ and
$(\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sym,sep}})$-$\mathsf{Aut}$, and
thus we obtain a functorial connection between the categorical semantics of
linear $\lambda$-calculus with the $\mathcal{V}$-equational system (i.e. (1)),
(2), and (3). In essence, the connection formalises the fact that our
categorical models admit a richer structure over terms (i.e. morphisms) than
the categorical models of linear $\lambda$-calculus and its classical
equational system. The latter in turn permits the existence of different terms
between two types as opposed to the algebraic semantics of the exponential
free, multiplicative fragment of linear logic. The connection also shows that
models for (2) and (3) can be mapped into models of our categorical semantics
by equipping the respective hom-sets with a trivial, discrete structure.

Future work. Recall that linear $\lambda$-calculus is at the root of different
ramifications of $\lambda$-calculus that relax resource-based conditions in
different ways. Currently, we are studying analogous ramifications of linear
$\lambda$-calculus in the $\mathcal{V}$-equational setting, particularly
affine and Cartesian versions. We are also studying the possibility of adding
an exponential modality in order to obtain a _mixed linear-non-linear_
calculus [3]. We also started to explore different definitions of a morphism
between $\mathcal{V}\lambda$-theories and respective categories. This is the
basis to establish a categorical equivalence between a (quasi)category of
$\mathcal{V}\lambda$-theories and a (quasi)category of
$\mathcal{V}\text{-}\mathsf{Cat}_{\mathsf{sep}}$-enriched autonomous
categories.

Next, our main examples of $\mathcal{V}\lambda$-theories (see Section 4) used
either the Boolean or the metric quantale. We would like to study linear
$\mathcal{V}\lambda$-theories whose underlying quantales are neither the
Boolean nor the metric one, for example the ultrametric quantale which is
(tacitly) used to interpret Nakano’s guarded $\lambda$-calculus [5] and also
to interpret a higher-order language for functional reactive programming [21].
Another interesting quantale is the Gödel one which is a basis for fuzzy logic
[11] and whose $\mathcal{V}$-equations give rise to what we call fuzzy
inequations.

Finally we plan to further explore the connections between our work and
different results on metric universal algebra [29, 30, 35] and inequational
universal algebra [22, 2, 35]. For example, an interesting connection is that
the monad construction presented in [29] crucially relies on quotienting a
pseudometric space into a metric space – this is a particular case of
quotienting a $\mathcal{V}$-category into a separated $\mathcal{V}$-category
(which we crucially use in our work).

## References

  * [1] Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G Riecke.  A core calculus of dependency.  In Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 147–160, 1999.
  * [2] Jiří Adámek, Chase Ford, Stefan Milius, and Lutz Schröder.  Finitary monads on the category of posets.  arXiv preprint arXiv:2011.14796, 2020.
  * [3] Nick Benton.  A mixed linear and non-linear logic: Proofs, terms and models.  In International Workshop on Computer Science Logic, pages 121–135. Springer, 1994.
  * [4] Nick Benton, Gavin Bierman, Valeria de Paiva, and Martin Hyland.  Term assignment for intuitionistic linear logic (preliminary report).  Citeseer, 1992.
  * [5] Lars Birkedal, Jan Schwinghammer, and Kristian Støvring.  A metric model of lambda calculus with guarded recursion.  In FICS, pages 19–25, 2010.
  * [6] Francis Borceux.  Handbook of categorical algebra, volume 2 of Encyclopedia of Mathematics and its Applications.  Cambridge University Press, 1994.
  * [7] Raphaëlle Crubillé and Ugo Dal Lago.  Metric reasoning about $\lambda$-terms: The affine case.  In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 633–644. IEEE, 2015.
  * [8] Raphaëlle Crubillé and Ugo Dal Lago.  Metric Reasoning About $lambda$-Terms: The General Case.  In European Symposium on Programming, pages 341–367. Springer, 2017\.
  * [9] Fredrik Dahlqvist and Dexter Kozen.  Semantics of higher-order probabilistic programs with conditioning.  In Proc. 47th ACM SIGPLAN Symp. Principles of Programming Languages (POPL’20), pages 57:1–29, New Orleans, January 2020. ACM.
  * [10] Valeria De Paiva.  Lineales: algebraic models of linear logic from a categorical perspective.  In Proceedings of LLC8, 1999.
  * [11] Klaus Denecke, Marcel Erné, and Shelly L Wismath.  Galois connections and applications, volume 565.  Springer Science & Business Media, 2013.
  * [12] Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu.  Combining effects and coeffects via grading.  ACM SIGPLAN Notices, 51(9):476–489, 2016.
  * [13] Francesco Gavazzo.  Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances.  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 452–461, 2018.
  * [14] Gerhard Gierz, Karl Heinrich Hofmann, Klaus Keimel, Jimmie D. Lawson, Michael W. Mislove, and Dana S. Scott.  Continuous lattices and domains, volume 93 of Encyclopedia of Mathematics and its Applications.  Cambridge University Press, Cambridge, 2003.
  * [15] Jean-Yves Girard, Andre Scedrov, and Philip J Scott.  Bounded linear logic: a modular approach to polynomial-time computability.  Theoretical computer science, 97(1):1–66, 1992.
  * [16] Jean Goubault-Larrecq.  Non-Hausdorff Topology and Domain Theory—Selected Topics in Point-Set Topology, volume 22 of New Mathematical Monographs.  Cambridge University Press, March 2013.
  * [17] Dirk Hofmann and Pedro Nora.  Hausdorff coalgebras.  Applied Categorical Structures, 28(5):773–806, 2020.
  * [18] Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu.  Quantitative robustness analysis of quantum programs.  Proceedings of the ACM on Programming Languages, 3(POPL):1–29, 2019\.
  * [19] Gregory Maxwell Kelly.  Basic concepts of enriched category theory, volume 64.  CUP Archive, 1982.
  * [20] Dexter Kozen.  Semantics of probabilistic programs.  J. Comput. Syst. Sci., 22(3):328–350, June 1981.  doi:10.1016/0022-0000(81)90036-2.
  * [21] Neelakantan R Krishnaswami and Nick Benton.  Ultrametric semantics of reactive programs.  In 2011 IEEE 26th Annual Symposium on Logic in Computer Science, pages 257–266. IEEE, 2011.
  * [22] Alexander Kurz and Jiří Velebil.  Quasivarieties and varieties of ordered algebras: regularity and exactness.  Mathematical Structures in Computer Science, 27(7):1153–1194, 2017\.
  * [23] Joachim Lambek and Philip J Scott.  Introduction to higher-order categorical logic, volume 7.  Cambridge University Press, 1988.
  * [24] F William Lawvere.  Metric spaces, generalized logic, and closed categories.  Rendiconti del seminario matématico e fisico di Milano, 43(1):135–166, 1973.
  * [25] Fred E. J. Linton.  Some aspects of equational categories.  In Proceedings of the Conference on Categorical Algebra, pages 84–94. Springer, 1966.
  * [26] Saunders Mac Lane.  Categories for the working mathematician, volume 5.  springer, 1998.
  * [27] Ian Mackie, Leopoldo Román, and Samson Abramsky.  An internal language for autonomous categories.  Applied Categorical Structures, 1(3):311–343, 1993.
  * [28] Maria Emilia Maietti, Paola Maneggia, Valeria De Paiva, and Eike Ritter.  Relating categorical semantics for intuitionistic linear logic.  Applied categorical structures, 13(1):1–36, 2005.
  * [29] Radu Mardare, Prakash Panangaden, and Gordon Plotkin.  Quantitative algebraic reasoning.  In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pages 700–709, 2016.
  * [30] Radu Mardare, Prakash Panangaden, and Gordon Plotkin.  On the axiomatizability of quantitative algebras.  In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12. IEEE, 2017.
  * [31] Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III.  Quantitative program reasoning with graded modal types.  Proceedings of the ACM on Programming Languages, 3(ICFP):1–30, 2019\.
  * [32] Jan Paseka and Jiří Rosickỳ.  Quantales.  In Current research in operational quantum logic, pages 245–262. Springer, 2000.
  * [33] Paolo Pistone.  On Generalized Metric Spaces for the Simply Typed $\lambda$-Calculus.  In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021.
  * [34] Jason Reed and Benjamin C Pierce.  Distance makes the types grow stronger: A calculus for differential privacy.  In Proceedings of the 15th ACM SIGPLAN international conference on Functional programming, pages 157–168, 2010.
  * [35] Jiří Rosickỳ.  Metric monads.  arXiv preprint arXiv:2012.14641, 2020.
  * [36] Raymond A Ryan.  Introduction to tensor products of Banach spaces.  Springer Science & Business Media, 2013.
  * [37] Michael Shulman.  A practical type theory for symmetric monoidal categories.  arXiv preprint arXiv:1911.00818, 2019.
  * [38] Isar Stubbe.  An introduction to quantaloid-enriched categories.  Fuzzy Sets and Systems, 256:95–116, 2014.
  * [39] Jiří Velebil, Alexander Kurz, and Adriana Balan.  Extending set functors to generalised metric spaces.  Logical Methods in Computer Science, 15, 2019.

##  Appendix A Linear $\mathcal{V}\lambda$-theories and linear quantales

We briefly study linear $\mathcal{V}\lambda$-theories where $\mathcal{V}$ is a
quantale with a _linear order_. The latter condition is respected by the
Boolean and (ultra)metric quantales (mentioned in the main text). Recall that
metric universal algebra [29, 30] tacitly uses the metric quantale.

######  Theorem A.1.

Assume that the underlying order of $\mathcal{V}$ is linear and consider a
(symmetric) linear $\mathcal{V}\lambda$-theory. Substituting the rule below on
the left by the one below on the right does not change the theory.

$\displaystyle v=_{\vee q_{i}}w\forall i\leq n.\ v=_{q_{i}}w\hskip
56.9055ptv=_{\bot}w$

######  Proof A.2.

Clearly, the rule on the left subsumes the one on the right by choosing $n=0$.
So we only need to show the inverse direction under the assumption that
$\mathcal{V}$ is linear. Thus, assume that $\forall i\leq n.\ v=_{q_{i}}w$. We
proceed by case distinction. If $n=0$ then we need to show that $v=_{\bot}w$
which is given already by the rule on the right. Suppose now that $n>0$. Then
since the order of $\mathcal{V}$ is linear the value $\vee q_{i}$ must already
be one of the values $q_{i}$ and $v=_{q_{i}}w$ is already part of the theory.
In other words, in case of $n>0$ the rule on the left is redundant.

The above result is in accordance with metric universal algebra [29, 30] which
also does not include rule (join). Interestingly, however, we still have
$v=_{\bot}w$ for all $\lambda$-terms $v$ and $w$ and such a rule is not
present in [29, 30]. This is explained by the fact that metric equations in
[29, 30] are labelled _only_ by non-negative rational numbers whilst we also
permit infinity to be a label (in our case, labels are given by a basis $B$
which for the metric case corresponds to the _extended_ non-negative rational
numbers). All remaining rules of our $\mathcal{V}$-equational system
instantiated to the metric case find a counterpart in the metric equational
system presented in [29, 30].

Next, note that if the quantale $\mathcal{V}$ is finite then for all
$q\in\mathcal{V}$ we have $q\ll q$ which means that rule (arch) is no longer
necessary. This observation is applicable to the Boolean quantale.

##  Appendix B Lemmata and omitted proofs

######  Proof B.1 (Proof sketch of Lemma 2.1).

The proof follows by induction over the structure of $\lambda$-terms. Here we
only consider the case $f(v_{1},\dots,v_{n})$, because the other cases follow
analogously.

Suppose that $E\rhd f(v_{1},\dots,v_{n}):\mathbb{A}$. Then according to the
typing system it is necessarily the case that the previous derivations were
$\Gamma_{i}\rhd v_{i}:\mathbb{A}$ for all $i\leq n$ with
$E\in\mathrm{Sf}(\Gamma_{1};\dots;\Gamma_{n})$ for some family of contexts
$(\Gamma_{i})_{i\leq n}$. The only room for choice is therefore in choosing
the contexts $\Gamma_{i}$. We will show that even this choice is unique.
Consider two families $(\Gamma_{i})_{i\leq n}$ and
$(\Gamma^{\prime}_{i})_{i\leq n}$ such that $\Gamma_{i}\rhd v_{i}:\mathbb{A}$
and $\Gamma^{\prime}_{i}\rhd v_{i}:\mathbb{A}$ for all $i\leq n$, and moreover
$E\in\mathrm{Sf}(\Gamma_{1};\dots;\Gamma_{n})$ and
$E\in\mathrm{Sf}(\Gamma^{\prime}_{1};\dots;\Gamma^{\prime}_{n})$. Since
$\Gamma_{i}\rhd v_{i}:\mathbb{A}_{i}$ and $\Gamma^{\prime}_{i}\rhd
v_{i}:\mathbb{A}_{i}$ we deduce (by linearity) that $\Gamma_{i}$ is a
permutation of $\Gamma^{\prime}_{i}$. Consequently, since
$E\in\mathrm{Sf}(\Gamma_{1},\dots,\Gamma_{n})$,
$E\in\mathrm{Sf}(\Gamma^{\prime}_{1},\dots,\Gamma^{\prime}_{n})$ and $E$ (by
the definition of a shuffle) cannot change the relative order of the elements
in $\Gamma_{i}$ and $\Gamma^{\prime}_{i}$ for all $i\leq n$, it must be the
case that $\Gamma_{i}=\Gamma^{\prime}_{i}$ for all $i\leq n$. In other words,
the choice of $(\Gamma_{i})_{i\leq n}$ is fixed _a priori_. The proof now
follows by applying the induction hypothesis to each $v_{i}$.

######  Proof B.2 (Proof sketch of Lemma 2.2).

We focus first on the exchange rule. The proof follows by induction over the
structure of derivations. Here we only consider the case
$\Gamma,x:\mathbb{A},y:\mathbb{B},\Delta\rhd f(v_{1},\dots,v_{n}):\mathbb{C}$,
the other cases follow analogously.

Suppose that $\Gamma,x:\mathbb{A},y:\mathbb{B},\Delta\rhd
f(v_{1},\dots,v_{n}):\mathbb{C}$ with
$\Gamma,x:\mathbb{A},y:\mathbb{B},\Delta\in\mathrm{Sf}(\Gamma_{1};\dots;\Gamma_{n})$.
We proceed by case distinction: assume first that both $x:\mathbb{A}$ and
$y:\mathbb{B}$ are in some $\Gamma_{i}$, with $i\leq n$. We can thus decompose
$\Gamma_{i}$ into $\Gamma^{1}_{i},x:\mathbb{A},y:\mathbb{B},\Gamma^{2}_{i}$.
Then we apply the induction hypothesis on $\Gamma_{i}\rhd
v_{i}:\mathbb{A}_{i}$ and proceed by observing that if
$\Gamma,x:\mathbb{A},y:\mathbb{B},\Delta\in\mathrm{Sf}(\Gamma_{1};\dots;(\Gamma^{1}_{i},x:\mathbb{A},y:\mathbb{B},\Gamma^{2}_{i});\dots;\Gamma_{n})$
then it is also the case that
$\Gamma,y:\mathbb{B},x:\mathbb{A},\Delta\in\mathrm{Sf}(\Gamma_{1};\dots;(\Gamma^{1}_{i},y:\mathbb{B},x:\mathbb{A},\Gamma^{2}_{i});\dots;\Gamma_{n})$.
Assume now that $x:\mathbb{A}$ is in some $\Gamma_{i}$ and $y:\mathbb{B}$ is
in some $\Gamma_{j}$ with $i\not=j$. Then since
$\Gamma,x:\mathbb{A},y:\mathbb{B},\Delta\in\mathrm{Sf}(\Gamma_{1};\dots;\Gamma_{n})$
it must be the case that
$\Gamma,y:\mathbb{B},x:\mathbb{A},\Delta\in\mathrm{Sf}(\Gamma_{1};\dots;\Gamma_{n})$
so we only need to apply rule $(\mathrm{\mathbf{ax}})$.

Let us now focus on the substitution rule. The proof follows by induction over
the structure of derivations and also by the exchange rule that was just
proved. We exemplify this with rule $(\mathrm{\mathbf{ax}})$. The other cases
follow analogously.

Suppose that $\Gamma,x:\mathbb{A}\rhd f(v_{1},\dots,v_{n}):\mathbb{B}$. Then
for all $i\leq n$ we have $\Gamma_{i}\rhd v_{i}:\mathbb{A}_{i}$ and
$\Gamma,x:\mathbb{A}\in\mathrm{Sf}(\Gamma_{1};\dots;\Gamma_{n})$. By linearity
and by the definition of a shuffle there exists exactly one $\Gamma_{i}$ that
can be decomposed into $\Gamma_{i}=\Gamma^{\prime}_{i},x:\mathbb{A}$. We then
use the induction hypothesis to obtain $\Gamma^{\prime}_{i},\Delta\rhd
v_{i}[w/x]:\mathbb{A}_{i}$. Now observe that if
$\Gamma,x:\mathbb{A}\in\mathrm{Sf}(\Gamma_{1};\dots;(\Gamma^{\prime}_{i},x:\mathbb{A});\dots;\Gamma_{n})$
then
$\Gamma,\Delta\in\mathrm{Sf}(\Gamma_{1};\dots;(\Gamma^{\prime}_{i},\Delta);\dots;\Gamma_{n})$.
We use this last observation to build $\Gamma,\Delta\rhd
f(v_{1},\dots,v_{i}[w/x],\dots,v_{n})=f(v_{1},\dots,v_{n})[w/x]:\mathbb{B}$.

In order to keep calculations in the following proofs legible we will
sometimes abbreviate a denotation $\llbracket\Gamma\rhd
v:\mathbb{A}\rrbracket$ to $\llbracket\Gamma\rhd v\rrbracket$ or even just
$\llbracket v\rrbracket$.

######  Lemma B.3 (Exchange and Substitution).

Consider judgements $\Gamma,x:\mathbb{A},y:\mathbb{B},\Delta\rhd
v:\mathbb{C}$, $\Gamma,x:\mathbb{A}\rhd v:\mathbb{B}$, and $\Delta\rhd
w:\mathbb{A}$. Then the following equations hold in every autonomous category
$\mathsf{C}$:

$\displaystyle\llbracket\Gamma,x:\mathbb{A},y:\mathbb{B},\Delta\rhd
v:\mathbb{C}\rrbracket$
$\displaystyle=\llbracket\Gamma,y:\mathbb{B},x:\mathbb{A},\Delta\rhd
v:\mathbb{C}\rrbracket\cdot\operatorname{\mathsf{exch}}_{\Gamma,\underline{\mathbb{A},\mathbb{B}},\Delta}$
$\displaystyle\llbracket\Gamma,\Delta\rhd v[w/x]:\mathbb{B}\rrbracket$
$\displaystyle=\llbracket\Gamma,x:\mathbb{A}\rhd
v:\mathbb{B}\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma;\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket\Delta\rhd
w:\mathbb{A}\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta}$

######  Proof B.4 (Proof sketch).

For both cases the proof follows by induction over the structure of
derivations. Here we only consider rule $(\mathrm{\mathbf{ax}})$, because the
other ones follow analogously. In many of the calculations below we will
tacitly perform simple diagram chases that take advantage of naturality,
functoriality, and the coherence theorem of symmetric monoidal categories.

We start with the exchange property. Suppose that
$\Gamma,x:\mathbb{A},y:\mathbb{B},\Delta\rhd f(v_{1},\dots,v_{n}):\mathbb{C}$.
We proceed by case distinction: first, consider the case in which
$x:\mathbb{A}\in\Gamma_{i}$ and $y:\mathbb{B}\in\Gamma_{j}$ with $i\not=j$.
The proof then follows directly by observing that the two corresponding
shuffling morphisms
$\operatorname{\mathsf{sh}}_{\Gamma,\mathbb{A},\mathbb{B},\Delta}:\llbracket\Gamma,x:\mathbb{A},y:\mathbb{B},\Delta\rrbracket\to\llbracket\Gamma_{1},\dots,\Gamma_{n}\rrbracket$
and
$\operatorname{\mathsf{sh}}_{\Gamma,\mathbb{B},\mathbb{A},\Delta}:\llbracket\Gamma,y:\mathbb{B},x:\mathbb{A},\Delta\rrbracket\to\llbracket\Gamma_{1},\dots,\Gamma_{n}\rrbracket$
satisfy the equation
$\operatorname{\mathsf{sh}}_{\Gamma,\mathbb{B},\mathbb{A},\Delta}\cdot\operatorname{\mathsf{exch}}_{\Gamma,\underline{\mathbb{A},\mathbb{B}},\Delta}=\operatorname{\mathsf{sh}}_{\Gamma,\mathbb{A},\mathbb{B},\Delta}$.
Consider now the case in which $x:\mathbb{A}\in\Gamma_{i}$ and
$y:\mathbb{B}\in\Gamma_{i}$ for some $i\leq n$. We then calculate:

$\displaystyle\,\llbracket\Gamma,x:\mathbb{A},y:\mathbb{B},\Delta\rhd
f(v_{1},\dots,v_{n}):\mathbb{C}\rrbracket=\llbracket
f\rrbracket\cdot(\llbracket v_{1}\rrbracket\otimes\dots\otimes\llbracket
v_{i}\rrbracket\otimes\dots\otimes\llbracket
v_{n}\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma_{1};\dots;\Gamma_{n}}\cdot\operatorname{\mathsf{sh}}_{\Gamma,\mathbb{A},\mathbb{B},\Delta}$
$\displaystyle=\llbracket f\rrbracket\cdot(\llbracket
v_{1}\rrbracket\otimes\dots\otimes(\llbracket
v_{i}\rrbracket\cdot\operatorname{\mathsf{exch}}_{\Gamma^{1}_{i},\underline{\mathbb{A},\mathbb{B}},\Gamma^{2}_{i}})\otimes\dots\otimes\llbracket
v_{n}\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma_{1};\dots;\Gamma_{n}}\cdot\operatorname{\mathsf{sh}}_{\Gamma,\mathbb{A},\mathbb{B},\Delta}$
$\displaystyle=\llbracket f\rrbracket\cdot(\llbracket
v_{1}\rrbracket\otimes\dots\otimes\llbracket
v_{n}\rrbracket)\cdot(\operatorname{\mathsf{id}}\otimes\dots\otimes\operatorname{\mathsf{exch}}_{\Gamma^{1}_{i},\underline{\mathbb{A},\mathbb{B}},\Gamma^{2}_{i}}\otimes\dots\otimes\operatorname{\mathsf{id}})\cdot\operatorname{\mathsf{sp}}_{\Gamma_{1};\dots;\Gamma_{n}}\cdot\operatorname{\mathsf{sh}}_{\Gamma,\mathbb{A},\mathbb{B},\Delta}$
$\displaystyle=\llbracket f\rrbracket\cdot(\llbracket
v_{1}\rrbracket\otimes\dots\otimes\llbracket
v_{n}\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma^{\prime}_{1};\dots;\Gamma^{\prime}_{n}}\cdot\operatorname{\mathsf{exch}}_{\Gamma_{1},\dots,\Gamma^{1}_{i},\underline{\mathbb{A},\mathbb{B}},\Gamma^{2}_{i},\dots\Gamma_{n}}\cdot\operatorname{\mathsf{sh}}_{\Gamma,\mathbb{A},\mathbb{B},\Delta}$
$\displaystyle=\llbracket f\rrbracket\cdot(\llbracket
v_{1}\rrbracket\otimes\dots\otimes\llbracket
v_{n}\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma^{\prime}_{1};\dots;\Gamma^{\prime}_{n}}\cdot\operatorname{\mathsf{sh}}_{\Gamma,\mathbb{B},\mathbb{A},\Delta}\cdot\operatorname{\mathsf{exch}}_{\Gamma,\underline{\mathbb{A},\mathbb{B}},\Delta}$
$\displaystyle=\llbracket\Gamma,y:\mathbb{B},x:\mathbb{A},\Delta\rhd
f(v_{1},\dots,v_{n}):\mathbb{C}\rrbracket\cdot\operatorname{\mathsf{exch}}_{\Gamma,\underline{\mathbb{A},\mathbb{B}},\Delta}$

Let us now focus on proving the substitution lemma for rule
$(\mathrm{\mathbf{ax}})$:

$\displaystyle\,\llbracket\Gamma,\Delta\rhd
f(v_{1},\dots,v_{n})[w/x]:\mathbb{B}\rrbracket=\llbracket\Gamma,\Delta\rhd
f(v_{1},\dots,v_{i}[w/x],\dots,v_{n})\rrbracket$ $\displaystyle=\llbracket
f\rrbracket\cdot(\llbracket v_{1}\rrbracket\otimes\dots\otimes\llbracket
v_{i}[w/x]\rrbracket\otimes\dots\otimes\llbracket
v_{n}\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma_{1};\dots;\Gamma_{n}}\cdot\operatorname{\mathsf{sh}}_{\Gamma,\Delta}$
$\displaystyle=\llbracket f\rrbracket\cdot(\llbracket
v_{1}\rrbracket\otimes\dots\otimes(\llbracket
v_{i}\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma^{\prime}_{i};\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket
w\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma^{\prime}_{i};\Delta})\otimes\dots\otimes\llbracket
v_{n}\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma_{1};\dots;\Gamma_{n}}\cdot\operatorname{\mathsf{sh}}_{\Gamma,\Delta}$
$\displaystyle=\llbracket f\rrbracket\cdot(\llbracket
v_{1}\rrbracket\otimes\dots\otimes\llbracket
v_{n}\rrbracket)\cdot(\operatorname{\mathsf{id}}\otimes\dots\otimes(\operatorname{\mathsf{jn}}_{\Gamma^{\prime}_{i};\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket
w\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma^{\prime}_{i};\Delta})\otimes\dots\otimes\operatorname{\mathsf{id}})\cdot\operatorname{\mathsf{sp}}_{\Gamma_{1};\dots;\Gamma_{n}}\cdot\operatorname{\mathsf{sh}}_{\Gamma,\Delta}$
$\displaystyle=\llbracket f\rrbracket\cdot(\llbracket
v_{1}\rrbracket\otimes\dots\otimes\llbracket
v_{n}\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma_{1};\dots;\Gamma^{\prime}_{i},\mathbb{A};\dots\Gamma_{n}}\cdot\operatorname{\mathsf{sh}}_{\Gamma,\mathbb{A}}\cdot\operatorname{\mathsf{jn}}_{\Gamma;\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket
w\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta}$
$\displaystyle=\llbracket\Gamma,x:\mathbb{A}\rhd
f(v_{1},\dots,v_{n})\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma;\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket
w\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta}$

######  Proof B.5 (Proof sketch of Theorem 2.3).

The proof follows by an appeal to Lemma B.3, the coherence theorem for
symmetric monoidal categories, and naturality. We exemplify this with the
commuting conversions.

$\displaystyle\,\llbracket\Gamma,\Delta,E\rhd u[v\ \mathtt{to}\ \ast.\
w/x]:\mathbb{B}\rrbracket=\llbracket
u\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma;\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket
v\ \mathtt{to}\ \ast.\
w\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta,E}$
$\displaystyle=\llbracket
u\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma;\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes(\llbracket
w\rrbracket\cdot\lambda\cdot(\llbracket
v\rrbracket\otimes\operatorname{\mathsf{id}})\cdot\operatorname{\mathsf{sp}}_{\Delta;E}))\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta,E}$
$\displaystyle=\llbracket
u\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma;\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket
w\rrbracket)\cdot(\operatorname{\mathsf{id}}\otimes(\lambda\cdot(\llbracket
v\rrbracket\otimes\operatorname{\mathsf{id}})\cdot\operatorname{\mathsf{sp}}_{\Delta;E}))\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta,E}$
$\displaystyle=\llbracket
u\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma;\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket
w\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma;E}\cdot\operatorname{\mathsf{jn}}_{\Gamma;E}\cdot(\operatorname{\mathsf{id}}\otimes(\lambda\cdot(\llbracket
v\rrbracket\otimes\operatorname{\mathsf{id}})\cdot\operatorname{\mathsf{sp}}_{\Delta;E}))\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta,E}$
$\displaystyle=\llbracket
u[w/x]\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma;E}\cdot(\operatorname{\mathsf{id}}\otimes(\lambda\cdot(\llbracket
v\rrbracket\otimes\operatorname{\mathsf{id}})\cdot\operatorname{\mathsf{sp}}_{\Delta;E}))\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta,E}$
$\displaystyle=\llbracket u[w/x]\rrbracket\cdot\lambda\cdot(\llbracket
v\rrbracket\otimes\operatorname{\mathsf{id}})\cdot\operatorname{\mathsf{sp}}_{\Delta;\Gamma,E}\cdot\operatorname{\mathsf{sh}}_{\Gamma,\Delta,E}$
$\displaystyle=\llbracket\Gamma,\Delta,E\rhd v\ \mathtt{to}\ \ast.\
u[w/x]:\mathbb{B}\rrbracket$

The one but last step amounts to a diagram chase that recurs to naturality and
the coherence theorem of symmetric monoidal categories.

$\displaystyle\,\llbracket\Gamma,\Delta,E\rhd u[\mathtt{pm}\ v\ \mathtt{to}\
x\otimes y.\ w/z]:\mathbb{B}\rrbracket=\llbracket\Gamma,z:\mathbb{A}\rhd
u\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma;\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket\mathtt{pm}\
v\ \mathtt{to}\ x\otimes y.\
w\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta,E}$
$\displaystyle=\llbracket
u\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma;\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes(\llbracket
w\rrbracket\cdot\operatorname{\mathsf{jn}}_{E;\mathbb{C};\mathbb{D}}\cdot\alpha\cdot\operatorname{\mathsf{sw}}\cdot(\llbracket
v\rrbracket\otimes\operatorname{\mathsf{id}})\cdot\operatorname{\mathsf{sp}}_{\Delta;E}))\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta,E}$
$\displaystyle=\llbracket
u\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma;\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket
w\rrbracket)\cdot(\operatorname{\mathsf{id}}\otimes(\operatorname{\mathsf{jn}}_{E;\mathbb{C};\mathbb{D}}\cdot\alpha\cdot\operatorname{\mathsf{sw}}\cdot(\llbracket
v\rrbracket\otimes\operatorname{\mathsf{id}})\cdot\operatorname{\mathsf{sp}}_{\Delta;E}))\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta,E}$
$\displaystyle=\llbracket
u\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma;\mathbb{A}}\cdot(\operatorname{\mathsf{id}}\otimes\llbracket
w\rrbracket)\cdot\operatorname{\mathsf{sp}}_{\Gamma;E,\mathbb{C},\mathbb{D}}\cdot\operatorname{\mathsf{jn}}_{\Gamma;E,\mathbb{C},\mathbb{D}}\cdot(\operatorname{\mathsf{id}}\otimes(\operatorname{\mathsf{jn}}_{E;\mathbb{C};\mathbb{D}}\cdot\alpha\cdot\operatorname{\mathsf{sw}}\cdot(\llbracket
v\rrbracket\otimes\operatorname{\mathsf{id}})\cdot\operatorname{\mathsf{sp}}_{\Delta;E}))\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta,E}$
$\displaystyle=\llbracket
u[w/z]\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma;E,\mathbb{C},\mathbb{D}}\cdot(\operatorname{\mathsf{id}}\otimes(\operatorname{\mathsf{jn}}_{E;\mathbb{C};\mathbb{D}}\cdot\alpha\cdot\operatorname{\mathsf{sw}}\cdot(\llbracket
v\rrbracket\otimes\operatorname{\mathsf{id}})\cdot\operatorname{\mathsf{sp}}_{\Delta;E}))\cdot\operatorname{\mathsf{sp}}_{\Gamma;\Delta,E}$
$\displaystyle=\llbracket
u[w/z]\rrbracket\cdot\operatorname{\mathsf{jn}}_{\Gamma,E;\mathbb{C};\mathbb{D}}\cdot\alpha\cdot\operatorname{\mathsf{sw}}\cdot(\llbracket
v\rrbracket\otimes\operatorname{\mathsf{id}})\cdot\operatorname{\mathsf{sp}}_{\Delta;\Gamma,E}\cdot\operatorname{\mathsf{sh}}_{\Gamma,\Delta,E}$
$\displaystyle=\llbracket\Gamma,\Delta,E\rhd\mathtt{pm}\ v\ \mathtt{to}\
x\otimes y.\ u[w/z]:\mathbb{B}\rrbracket$

The one but last step amounts to a diagram chase that recurs to naturality and
the coherence theorem of symmetric monoidal categories.

######  Proof B.6 (Proof of Theorem 3.9).

The proof follows by showing that the closed monoidal structure of
$\mathcal{V}\text{-}\mathsf{Cat}$ preserves symmetry and separation. It is
immediate for symmetry. For separation, note that since $\mathcal{V}$ is
integral the inequation $x\otimes y\leq x$ holds for all $x,y\in\mathcal{V}$.
It follows that the monoidal structure preserves separation. The fact that the
closed structure also preserves separation uses the implication
$x\leq\bigwedge A\Rightarrow\forall a\in A.\ x\leq a$ for all $x\in
X,A\subseteq X$.

######  Proof B.7 (Proof of Theorem 3.20).

Let us denote by $\mathrm{Lang}^{\lambda}(\mathsf{C})$ the _linear
$\lambda$-theory_ generated from $\mathsf{C}$. According to Theorem 2.10, the
category $\mathrm{Syn}(\mathrm{Lang}^{\lambda}(\mathsf{C}))$ (i.e. the
syntactic category generated from $\mathrm{Lang}^{\lambda}(\mathsf{C})$) is
locally small whenever $\mathsf{C}$ is locally small. Then consider two types
$\mathbb{A}$ and $\mathbb{B}$. We will prove our claim by taking advantage of
the axiom of replacement in ZF set-theory, specifically by presenting a
_surjective_ map,

$\displaystyle\mathrm{Syn}(\mathrm{Lang}^{\lambda}(\mathsf{C}))(\mathbb{A},\mathbb{B})\longrightarrow\mathrm{Syn}(\mathrm{Lang}(\mathsf{C}))(\mathbb{A},\mathbb{B})$

The crucial observation is that if $v=w$ in
$\mathrm{Lang}^{\lambda}(\mathsf{C})$ then $v=_{\top}w$ and $w=_{\top}v$ in
$\mathrm{Lang}(\mathsf{C})$. This is obtained by the definition of a model,
the definition of a $\mathcal{V}$-category, and the definition of
$\mathrm{Lang}(\mathsf{C})$. This observation allows to establish the
surjective map that sends $[v]$ to $[v]$, i.e. it sends the equivalence class
of $v$ as a $\lambda$-term in $\mathrm{Lang}^{\lambda}(\mathsf{C})$ into the
equivalence class of $v$ as a $\lambda$-term in $\mathrm{Lang}(\mathsf{C})$.

######  Proof B.8 (Proof of Theorem 4.3).

The autonomous structure of $\mathsf{Ban}$ is well-known [9, 20], so let us
focus on showing that it is a _$\mathsf{Met}$ -enriched_ autonomous category.
The enrichment is simply given by distance function induced by the operator
norm, thus if $S,T\in\mathsf{Ban}(X,Y)$,

$d(S,T)=\bigvee\\{\left\lVert(S-T)(x)\right\rVert\mid\left\lVert
x\right\rVert\leq 1\\}$

Composition is a short map.

Let $T,T^{\prime}\in\mathsf{Ban}(X,Y)$ and $S,S^{\prime}\in\mathsf{Ban}(Y,Z)$,
we compute:

$\displaystyle d(ST,S^{\prime}T^{\prime})$
$\displaystyle\triangleq\bigvee\\{\left\lVert
ST(x)-S^{\prime}T^{\prime}(x)\right\rVert\mid\left\lVert x\right\rVert\leq
1\\}$ $\displaystyle=\bigvee\\{\left\lVert
ST(x)-ST^{\prime}(x)+ST^{\prime}(x)-S^{\prime}T^{\prime}(x)\right\rVert\mid\left\lVert
x\right\rVert\leq 1\\}$ $\displaystyle\leq\bigvee\\{\left\lVert
ST(x)-ST^{\prime}(x)\right\rVert+\left\lVert
ST^{\prime}(x)-S^{\prime}T^{\prime}(x)\right\rVert\mid\left\lVert
x\right\rVert\leq 1\\}$ $\displaystyle=\bigvee\\{\left\lVert
ST(x)-ST^{\prime}(x)\right\rVert\mid\left\lVert x\right\rVert\leq
1\\}+\bigvee\\{\left\lVert
ST^{\prime}(x)-S^{\prime}T^{\prime}(x)\right\rVert\mid\left\lVert
x\right\rVert\leq 1\\}$ $\displaystyle=\bigvee\\{\left\lVert
S(T-T^{\prime})(x)\right\rVert\mid\left\lVert x\right\rVert\leq
1\\}+\bigvee\\{\left\lVert
ST^{\prime}(x)-S^{\prime}T^{\prime}(x)\right\rVert\mid\left\lVert
x\right\rVert\leq 1\\}$
$\displaystyle\stackrel{{\scriptstyle(\star)}}{{\leq}}\bigvee\\{\left\lVert
T(x)-T^{\prime}(x)\right\rVert\mid\left\lVert x\right\rVert\leq
1\\}+\bigvee\\{\left\lVert
ST^{\prime}(x)-S^{\prime}T^{\prime}(x)\right\rVert\mid\left\lVert
x\right\rVert\leq 1\\}$ $\displaystyle\leq\bigvee\\{\left\lVert
T(x)-T^{\prime}(x)\right\rVert\mid\left\lVert x\right\rVert\leq
1\\}+\bigvee\\{\left\lVert S(y)-S^{\prime}(y)\right\rVert\mid\left\lVert
y\right\rVert\leq 1\\}$ $\displaystyle\triangleq
d(T,T^{\prime})+d(S,S^{\prime})$ $\displaystyle\triangleq
d((T,S),(T^{\prime},S^{\prime}))$

where $(\star)$ follows from the fact that,

$\left\lVert S(T-T^{\prime})(x)\right\rVert=\left\lVert
T(x)-T^{\prime}(x)\right\rVert\left\lVert
S\left(\frac{(T-T^{\prime})(x)}{\left\lVert
T(x)-T^{\prime}(x)\right\rVert}\right)\right\rVert\leq\left\lVert
T(x)-T^{\prime}(x)\right\rVert$

by linearity of $S$ and by the fact that $\left\lVert S\right\rVert\leq 1$.
This shows that $\mathsf{Ban}$ is $\mathsf{Met}$-enriched. We now turn to the
first clause of Definition 3.11.

The monoidal operation is an enriched bi-functor.

Note first that if $S\in\mathsf{Ban}(X,Y)$ and
$T,T^{\prime}\in\mathsf{Ban}(X^{\prime},Y^{\prime})$ then,

$S\widehat{\otimes}_{\pi}T-S\widehat{\otimes}_{\pi}T^{\prime}=S\widehat{\otimes}_{\pi}(T-T^{\prime})$

Indeed, since $S\widehat{\otimes}_{\pi}T$ is the unique linear operator such
that $S\widehat{\otimes}_{\pi}T(x\otimes x^{\prime})=S(x)\otimes
T(x^{\prime})$, we can reason pointwise and get,

$\displaystyle(S\widehat{\otimes}_{\pi}T-S\widehat{\otimes}_{\pi}T^{\prime})(x\otimes
x^{\prime})$ $\displaystyle=(S\widehat{\otimes}_{\pi}T)(x\otimes
x^{\prime})-(S\widehat{\otimes}_{\pi}T^{\prime})(x\otimes x^{\prime})$
$\displaystyle=S(x)\otimes T(x^{\prime})-S(x)\otimes T^{\prime}(x^{\prime})$
$\displaystyle=S(x)\otimes(T(x^{\prime})-T^{\prime}(x^{\prime}))$
$\displaystyle=(S\widehat{\otimes}_{\pi}(T-T^{\prime}))(x\otimes x^{\prime})$

where the penultimate step follows from the basic definition of the tensor
product of vector spaces. Now we can show that for any Banach spaces
$X,X^{\prime},Y,Y^{\prime}$ the projective tensor map,

$\mathsf{Ban}(X,Y)\otimes\mathsf{Ban}(X^{\prime},Y^{\prime})\to\mathsf{Ban}(X\widehat{\otimes}_{\pi}X^{\prime},Y\widehat{\otimes}_{\pi}Y^{\prime}),(S,T)\mapsto
S\widehat{\otimes}_{\pi}T$

where $\otimes$ once again denotes the monoidal operation in $\mathsf{Met}$,
is short. We simply compute,

$\displaystyle
d(S\widehat{\otimes}_{\pi}T,S^{\prime}\widehat{\otimes}_{\pi}T^{\prime})$
$\displaystyle\triangleq\left\lVert
S\widehat{\otimes}_{\pi}T-S^{\prime}\widehat{\otimes}_{\pi}T^{\prime}\right\rVert$
$\displaystyle=\left\lVert
S\widehat{\otimes}_{\pi}T-S\widehat{\otimes}_{\pi}T^{\prime}+S\widehat{\otimes}_{\pi}T^{\prime}-S^{\prime}\widehat{\otimes}_{\pi}T^{\prime}\right\rVert$
$\displaystyle\leq\left\lVert
S\widehat{\otimes}_{\pi}T-S\widehat{\otimes}_{\pi}T^{\prime}\right\rVert+\left\lVert
S\widehat{\otimes}_{\pi}T^{\prime}-S^{\prime}\widehat{\otimes}_{\pi}T^{\prime}\right\rVert$
$\displaystyle=\left\lVert
S\widehat{\otimes}_{\pi}(T-T^{\prime})\right\rVert+\left\lVert(S-S^{\prime})\widehat{\otimes}_{\pi}T^{\prime}\right\rVert$
$\displaystyle=\left\lVert S\right\rVert\left\lVert
T-T^{\prime}\right\rVert+\left\lVert S-S^{\prime}\right\rVert\left\lVert
T^{\prime}\right\rVert$ $\displaystyle\leq\left\lVert
T-T^{\prime}\right\rVert+\left\lVert S-S^{\prime}\right\rVert\triangleq
d((S,T),(S,T^{\prime}))$

where the last step uses the fact that $\left\lVert S\right\rVert,\left\lVert
T\right\rVert\leq 1$ and the penultimate step uses the basic fact that
$\left\lVert S\widehat{\otimes}_{\pi}T\right\rVert=\left\lVert
S\right\rVert\left\lVert T\right\rVert$ (see [36, §2.1]). Finally, we show the
second clause of Definition 3.11.

The adjunction $-\widehat{\otimes}_{\pi}Y\vdash Y\multimap-$ is a
$\mathsf{Met}$-adjunction.

The fact that the maps,

$\mathsf{Ban}(X,X^{\prime})\to\mathsf{Ban}(X\widehat{\otimes}_{\pi}Y,X\widehat{\otimes}_{\pi}Y),\
f\mapsto f\widehat{\otimes}_{\pi}\operatorname{\mathsf{id}}_{Y}$

are short follows by re-writing them as,

$\mathsf{Ban}(X,X^{\prime})\simeq\mathsf{Ban}(X,X^{\prime})\otimes
1\longrightarrow\mathsf{Ban}(X,X^{\prime})\otimes\mathsf{Ban}(Y,Y)\longrightarrow\mathsf{Ban}(X\widehat{\otimes}_{\pi}X^{\prime},Y\widehat{\otimes}_{\pi}Y)$

and the fact that the monoidal operation of $\mathsf{Ban}$ is an enriched bi-
functor. Similarly, the map,

$\mathsf{Ban}(X,X^{\prime})\to\mathsf{Ban}(Y\multimap X,Y\multimap
X^{\prime}),\ S\mapsto(T\mapsto ST)$

is short. This is a consequence of the following fact. Consider two operators
$S,S^{\prime}\in\mathsf{Ban}(X,X^{\prime})$. For all bounded operators $T\in
Y\multimap X$ with $\left\lVert T\right\rVert\leq 1$ we have
$d(S,S^{\prime})\triangleq\left\lVert S-S^{\prime}\right\rVert\geq\left\lVert
ST-S^{\prime}T\right\rVert$, which provides,

$d(S,S^{\prime})\geq\bigvee\\{\left\lVert
ST-S^{\prime}T\right\rVert\mid\left\lVert T\right\rVert\leq 1\\}\triangleq
d(T\mapsto ST,T\mapsto S^{\prime}T)$

Finally, we need to show that the adjunction $-\widehat{\otimes}_{\pi}Y\vdash
Y\multimap-$ defines an isometry,

$\mathsf{Ban}(X\widehat{\otimes}_{\pi}Y,Z)\simeq\mathsf{Ban}(X,Y\multimap Z).$

Indeed, the bijection from left to right is defined by,

$T\mapsto(Y\multimap-)(T)\cdot\eta_{Y}$

where $\eta$ is the unit of the adjunction. Since $Y\multimap-$ is
$\mathsf{Met}$-enriched, the assignment $T\mapsto(Y\multimap-)(T)$ is short,
and composition by $\eta_{Y}$ is short. Thus the invertible map
$\mathsf{Ban}(X\widehat{\otimes}_{\pi}Y,Z)\to\mathsf{Ban}(X,Y\multimap Z)$ is
short. By a similar argument using the co-unit of the adjunction and the fact
that $-\widehat{\otimes}_{\pi}Y$ is $\mathsf{Met}$-enriched we get that the
invertible map $\mathsf{Ban}(X,Y\multimap
Z)\to\mathsf{Ban}(X\widehat{\otimes}_{\pi}Y,Z)$ is also short. It follows that
both maps must be invertible isometries.

Proof that the axiom (3) is sound.

The total variation distance between
$\llbracket\mathtt{bernoulli}(x,y,p)\rrbracket$ and
$\llbracket\mathtt{bernoulli}(x,y,q)\rrbracket$ with $p,q\in[0,1]$ is given
by:

$\displaystyle\bigvee_{A}\left\lvert\int\int
p\delta_{u}(A)+(1-p)\delta_{v}(A)\leavevmode\nobreak\ d\llbracket
x\rrbracket(du)d\llbracket y\rrbracket(dv)-\int\int
q\delta_{u}(A)+(1-q)\delta_{v}(A)\leavevmode\nobreak\ d\llbracket
x\rrbracket(du)d\llbracket y\rrbracket(dv)\right\rvert$ $\displaystyle=$
$\displaystyle\bigvee_{A}\left\lvert\int\int(p-q)\delta_{u}(A)+((1-p)-(1-q))\delta_{v}(A)\leavevmode\nobreak\
d\llbracket x\rrbracket(du)d\llbracket y\rrbracket(dv)\right\rvert$
$\displaystyle=$ $\displaystyle\bigvee_{A}\left\lvert(p-q)\llbracket
x\rrbracket(A)+(q-p)\llbracket y\rrbracket(A)\right\rvert$ $\displaystyle=$
$\displaystyle\bigvee_{A}\left\lvert(p-q)(\llbracket x\rrbracket(A)-\llbracket
y\rrbracket(A))\right\rvert$ $\displaystyle\leq$
$\displaystyle\leavevmode\nobreak\ \left\lvert p-q\right\rvert$