suppose $\delta_{M}=\delta_{N}$, from now on, for all $i\in X$, we indicate as
$x_{i}$ the variable $\delta_{M}(i)=\delta_{N}(i)$.

######  Definition 8.14.

For any $i\in X$, let $\phi_{i}M$ be the unique subterm of $M$ of the form
$x_{i}M_{1}\dots M_{k}$, and $\psi_{i}M$ the unique positive subterm of $M$ of
the form $F(N_{1},\dots,N_{m-1},\phi_{i}M,N_{m+1},\dots,N_{n})$. For all
$i,j\in X$, let $i\sqsubset_{M}j$ if $\phi_{i}M$ is a subterm of $\phi_{j}M$,
and $i\sim_{M}j$ if $\psi_{i}M=\psi_{j}M$.

######  Lemma 8.15.

$\sqsubseteq_{M}$ is a well-founded order on $X$.
$\sim_{M}$ is an equivalence relation on $X$.

The relation $\sqsubseteq_{M}$ extends naturally to $\mathsf{PS}_{0}(M)$, by
letting $F\sqsubset_{M}i$, for $F\in\mathsf{PS}_{0}(M)$, if $F$ is a subterm
of $\phi_{i}M$.

Let $X_{\sim_{M}}$ indicate the quotient of $X$ under $\sim_{M}$ and let
$X^{M}:=X_{\sim_{M}}\cup\mathsf{PS}_{0}(M)$. In the following we will use
$\xi,\chi,\dots$ to indicate elements of $X^{M}$.

Let us extend the relation $\sqsubseteq_{M}$ from $X$ to $X^{M}$:

######  Definition 8.16.

For all $\xi,\chi\in X^{M}$, $\xi\sqsubseteq_{M}^{*}\chi$ holds if either
$\xi=\chi$ or $\exists j\in\chi\ \forall i\in\xi\ i\sqsubset_{M}j$.

Moreover, we write $\xi\sqsubseteq_{M}^{0}\chi$ if $\xi\neq\chi$,
$\xi\sqsubseteq_{M}\chi$ and for all $\theta\in X^{M}$,
$\xi\sqsubseteq_{M}\theta$ and $\theta\sqsubseteq_{M}\chi$ implies
$\theta\in\\{\xi,\chi\\}$.

Observe that $\xi\sqsubseteq_{M}^{0}\chi$ holds precisely when there is
$j\in\chi$ such that for all $i\in\xi$, $\phi_{j}M=x_{j}Q_{1}\dots
Q_{l-1}(\psi_{i}M)Q_{l+1}\dots Q_{r}$. Moreover the following is easily
proved:

######  Lemma 8.17.

$\sqsubseteq_{M}^{*}$ is a well-founded preorder with a maximum element
$\top_{M}=\\{{i_{1}},\dots,{i_{r}}\\}$, where
$M=F(\phi_{i_{1}}M,\dots\phi_{i_{r}}M)$.

We can define a bijection $\theta_{M}:\mathsf{PS}(M)\to X^{M}$ sending each
positive subterm $P=F(N_{1},\dots,N_{n})$, where $N_{i}=x_{i}Q_{i1}\dots
Q_{in_{i}}$, onto the equivalence class $\\{x_{1},\dots,x_{n}\\}$, if $n>0$,
and onto the singleton $\\{P\\}$ otherwise (i.e. if $P\in\mathsf{PS}_{0}$).
The existence of bijections $\theta_{M}:\mathsf{PS}(M)\to X^{M}$,
$\theta_{N}:\mathsf{PS}(N)\to X^{N}$ together with
$\iota_{M}:\\{\Gamma^{-}\\}*\mathbf{R}$ and
$\iota_{M}:\\{\Gamma^{-}\\}*\mathbf{R}$ implies that the two sets
$X^{M}=X_{\sim_{M}}\cup\mathsf{PS}_{0}(M)$ and
$X^{N}=X_{\sim_{N}}\cup\mathsf{PS}_{0}(N)$ are also in bijection (being both
in bijection with $\\{\Gamma^{-}\\}*\mathbf{R}$).

Let
$L=(\theta_{N}\circ\delta_{N})\circ(\theta_{M}\circ\delta_{M})^{-1}:X^{M}\to
X^{N}$ be the bijection associating each element of $X^{M}$ with the unique
element of $X^{N}$ corresponding to the same occurrence of $R$ in
$\\{\Gamma^{-}\\}*\mathbf{R}$. Observe that the rightmost element of the list
$\\{\Gamma^{-}\\}*\mathbf{R}$ is associated with $\top_{M}=M$ and
$\top_{N}=N$, we deduce that $L(\top_{M})=\top_{N}$.

As a consequence of the bijections established above, we can enumerate the
int-terms of $M$ and $N$ using, as index set, $X^{M}$ rather than
$\\{\Gamma^{-}\\}*\mathbf{R}$. In particular, for all $\xi\in X^{M}$, we
indicate the associated positive subterm of $t$ as

$\displaystyle M_{\xi}$
$\displaystyle:=F_{\xi}\big{(}\phi_{j}M\big{)}_{j\in\xi}$ $\displaystyle
N_{\xi}$ $\displaystyle:=G_{\xi}\big{(}\phi_{j}N\big{)}_{j\in L(\xi)}$

and the associated int-terms as

$\displaystyle H^{M}_{\xi}$ $\displaystyle:=F_{\xi}(x_{j})_{j\in\xi}$
$\displaystyle H^{N}_{\xi}$ $\displaystyle:=G_{\xi}(x_{j})_{j\in L(\xi)}$

We now introduce a special class of terms:

######  Definition 8.18 (terms with brackets).

The set of _$\lambda$ -terms with brackets_ is defined by enriching the syntax
of $\lambda$-terms with a new clause: if $t$ is a term, then $[{t}]$ is a
term. For any term with brackets $M$, we let $M^{\downarrow}$ indicate the
term obtained by erasing all brackets from $M$.

For all $i\in X$, let
$\\{{\phi_{i}M}\\}=x_{i}(\lambda\vec{z}_{1}.[{M_{1}}])\dots(\lambda\vec{z}_{n}.[{M_{n}}])$,
where $\phi_{i}M=x_{i}(\lambda\vec{z}.M_{1})\dots(\lambda\vec{z}.M_{n})$.

######  Definition 8.19.

A set $U\subseteq X^{M}$ is _upward closed_ if $\alpha\in U$ and
$\alpha\sqsubseteq_{M}\alpha^{\prime}$ implies $\alpha^{\prime}\in U$. For all
upward closed sets $U$, the _frontier of $U$_, noted $\partial U$, is the set
of $\xi\in X^{M}-U$ such that, for some $\chi\in U$
$\xi\sqsubseteq_{M}^{0}\chi$. We conventionally let
$\partial\emptyset=\\{\top_{M}\\}$.

For any upward closed $U\subseteq X^{M}$, we define a set $U(M)$ of
$\lambda$-terms with brackets by induction on $M$ as follows:

  * •

if $U=\emptyset$ and $M=\lambda\vec{z}.M^{\prime}$, then
$U(M)=\\{\lambda\vec{z}.[Q]\mid Q\text{ is a $\lambda$-term}\\}$;

  * •

if $U\neq\emptyset$ (which implies $\top_{M}\in U$) and
$M=\lambda\vec{z}.F\big{(}\phi_{i}M\big{)}_{i\in\top_{M}}$, then

$\displaystyle
U(M)=\left\\{\lambda\vec{z}.F\big{(}x_{i}{Q^{i}_{1}},\dots,{Q^{i}_{r_{i}}}\big{)}_{i\in\top_{M}}\mid
Q^{i}_{j}\in U_{j}^{i}(M^{i}_{j})\right\\}$

where for all $i\in\top_{M}$, $\phi_{i}M=x_{i}P^{i}_{1}\dots P^{i}_{r_{i}}$
and $U_{j}^{i}=U\cap X^{P_{j}^{i}}$ is an upward closed set of
$X^{M_{j}^{i}}$.

Intuitively, $P\in U(M)$ if it is a term which is defined like $M$ at all
positions corresponding to elements of $U$, and has a term in brackets at all
positions of $\partial U$.

The following facts are easily established by induction on $M$:

######  Lemma 8.20.

  * i.

$P\in X^{M}(M)$ iff $P=M$.

  * ii.

if $P\in U(M)$ and $P$ is bracket-free, then $U=X^{M}$ and $P=M$.

We now have all ingredients to define, by induction, a sequence of terms
$S_{0},\dots,S_{k}$ and a sequence of upward closed sets
$U_{0}\subseteq\dots\subseteq U_{k}\subseteq X^{N}$, verifying at each step
$i$ that:

  * a.

$S_{i}\in U_{i}(N)$;

  * b.

for all $\xi\in\partial U_{i}$, $S_{i}$ contains the subterm
$[M_{L^{-1}(\xi)}]$ at position $\xi$.

Let $S_{0}:=[M]=[{M_{\alpha_{\top}}}]$, and $U_{0}=\emptyset$. Then $S_{0}\in
U_{0}(M)$ certainly holds. Moreover, $\partial U_{0}=\\{\top_{N}\\}$, and
$S_{0}$ contains at its root the subterm
$[{M_{L^{-1}(\top_{N})}}]=[{M_{\top_{M}}}]=[M]$.

Now, to define $S_{i+1}$, choose $\xi\in\partial U_{i}$, let
$\chi=L^{-1}(\xi)$ and

$\displaystyle
S_{i+1}:=S_{i}\Big{(}[{F_{\chi}\big{(}\phi_{i}M\big{)}_{i\in\chi}}]\mapsto
G_{\xi}\big{(}\\{{\phi_{j}M}\\}\big{)}_{j\in\xi}\Big{)}$

and finally let $U_{i+1}=U_{i}\cup\\{\xi\\}$. To check that $S_{i+1}$ is well-
defined let us observe that:

  * •

by the induction hypothesis $S_{i}$ contains the subterm
$[{M_{\chi}}]=[{F_{\chi}\big{(}\phi_{i}M\big{)}_{i\in\chi}}]$ at position
$\xi$;

  * •

if one of the newly introduced variables $j\in\xi$ is bound in $S_{i}$, it is
never introduced outside the scope of its abstraction $\lambda x_{j}$. Indeed,
by the induction hypothesis, $S_{i}$ coincides with $N$ at all positions
$\theta\in U_{i}$; hence, since $N$ has at position $\xi$ the subterm
$G_{\xi}(\phi_{j}N)_{j\in\xi}$, it follows that any of the variables $x_{j}$
is in the scope of an abstraction $\lambda x_{j}$ in $S_{i+1}$ iff it is in
the scope of the same abstraction in $N$.

Now, from $S_{i}\in U_{i}(N)$, that $S_{i+1}\in U_{i+1}(N)$ follows from the
definition of $U_{i+1}(N)$. Moreover, if $\xi^{\prime}\in\partial U_{i+1}$,
then either $\xi^{\prime}\in\partial U_{i}$, so by IH we deduce that $S_{i}$
contains $[{M}_{L^{-1}(\xi^{\prime})}]$, and since $\xi^{\prime}\neq\xi$, also
$S_{i+1}$ does; or $\xi^{\prime}\sqsubset_{M}^{0}\xi$, i.e. there is $j\in\xi$
such that $\xi^{\prime}\sqsubset_{M}^{0}j$; now, position $\xi^{\prime}$ in
$S_{i+1}$ contains one of the terms $Q_{i}$, for $i=1,\dots,s$, where
$[{\phi_{j}M}]=x_{j}{W_{1}}\dots W_{s}$ and $W_{i}=\lambda\vec{z}.Q_{i}$, and
indeed we have that $Q_{i}=[{M_{L^{-1}(\xi^{\prime})}}]$.

Let us define now $M_{1},\dots,M_{k}$ as $M_{i}:=S_{i}^{\downarrow}$. It is
clear then that $M_{1}=M$. Let us check that $N_{k}=N$: from $\sharp U_{0}=0$
and $\sharp U_{i+1}=\sharp U_{i}+1$, we deduce $\sharp U_{k}=k$ and thus
$\sharp\partial U_{k}=0$, which implies $U_{k}=X^{N}$. From $S_{k}\in
U_{k}(N)=X^{N}(N)$, using Lemma 8.20 we deduce then that
$M_{k}=S_{k}^{\downarrow}=S_{k}=N$.

We can now establish the main result:

######  Proposition 8.21.

For all $\vec{a}\in\llbracket\Gamma\rrbracket$ there exist
$\vec{r}\in\llbracket\Gamma\rrbracket_{+}$ such that

$|\llbracket M\rrbracket(\vec{\varphi})-\llbracket N\rrbracket(\vec{a})|\
\leq\ \sum_{i\in\\{\Gamma^{-}\\}*R}\llbracket
H^{M}_{i}\rrbracket(\vec{r})-\llbracket H^{N}_{i}\rrbracket(\vec{r})|.$

######  Proof 8.22.

Using the bijection $\delta:\Gamma^{+}\to V(M)$, let
$r_{l}:=\llbracket\phi_{\delta(l)}M\rrbracket(\vec{\varphi})$.

Recall that the terms $H^{M}_{i}$ and $H^{N}_{i}$, for
$i\in\\{\Gamma^{-}\\}*\mathbf{R}$, can be equivalently enumerated as
$H^{M}_{L^{-1}(\xi)}$, $H^{N}_{\xi}$, for $\xi\in X^{N}$. Let
$\xi_{0},\dots,\xi_{k}$ be the sequence in $X^{N}$ chosen in the construction
of the sequence $S_{0},\dots,S_{k}$, and let
$\chi_{0}=L^{-1}(\xi_{0}),\dots,\chi_{k}=L^{-1}(\xi_{k})$. We will show that
for all $i=1,\dots,k$, $|\llbracket M_{i-1}\rrbracket(\varphi)-\llbracket
M_{i}\rrbracket(\varphi)|\leq|\llbracket
H^{M}_{\chi_{i}}\rrbracket(\vec{r})-\llbracket
H^{N}_{\xi_{i}}\rrbracket(\vec{r})|$. Indeed we have

$\displaystyle\Big{|}\llbracket M_{i-1}\rrbracket(\vec{\varphi})-\llbracket
M_{i}\rrbracket(\vec{a})\Big{|}$ $\displaystyle=\Big{|}\llbracket
M_{i-1}\rrbracket(\vec{\varphi})-\llbracket
M_{i-1}\Big{(}F_{\chi_{i}}\big{(}r_{l}\big{)}_{l\in\chi_{i}}\mapsto
G_{\xi_{i}}\big{(}{r_{m}}\big{)}_{m\in\xi_{i}}\Big{)}\rrbracket(\vec{a})\Big{|}$
$\displaystyle=\Big{|}\llbracket M_{i-1}\rrbracket(\vec{\varphi})-\llbracket
M_{i-1}\Big{(}H^{M}_{\chi_{i}}(\vec{r})\mapsto
H^{N}_{\xi_{i}}(\vec{r})\Big{)}\rrbracket(\vec{a})\Big{|}$
$\displaystyle\leq\big{|}\llbracket
H^{M}_{\chi_{i}}\rrbracket(\vec{r})-\llbracket
H^{N}_{\xi_{i}}\rrbracket(\vec{r})\big{|}$

Using the fact that $M_{0}=M$ and $M_{k}=N$, as well as the triangular law, we
deduce then

$\displaystyle|\llbracket M\rrbracket(\vec{a})-\llbracket
N\rrbracket(\vec{a})|$ $\displaystyle\leq|\llbracket
M_{0}\rrbracket(\vec{a})-\llbracket
M_{1}\rrbracket(\vec{a})|+\dots+|\llbracket
M_{k-1}\rrbracket(\vec{a})-\llbracket M_{k}\rrbracket(\vec{a})|$
$\displaystyle\leq\sum_{i=1}^{k}\big{|}\llbracket
H^{M}_{\chi_{i}}\rrbracket(\vec{r})-\llbracket
H^{N}_{\xi_{i}}\rrbracket(\vec{r})\big{|}.$

##  9 A Linear Programming Language with Graded Exponentials

In the following part of this paper, we generalize some of our arguments to a
restriction of Fuzz, namely, Fuzz without additive (co)products and recursive
types where gradings are non-negative possibly infinite integers rather than
real numbers. We note that while we do not have recursive types, we have
recursion. Our generalization goes as follows.

  * •

We describe our target language, which we call $\Lambda_{S}^{!}$.

  * •

We extend the logical metric and the observational metric to
$\Lambda_{S}^{!}$, and we show that these extensions coincide.

  * •

We extend the denotational metric and the interactive metric to
$\Lambda_{S}^{!}$, and we show that the observational metric is bounded by
these metrics.

###  9.1 Syntax

Let us give our extended target language, which we call $\Lambda_{S}^{!}$, and
its operational semantics. For types, we have graded exponentials.

$\displaystyle\mathrm{Types}$
$\displaystyle\tau,\sigma:=\cdots\mid\oc_{n}\tau$
$\displaystyle\mathrm{Environments}$
$\displaystyle\Gamma,\Delta,\Xi:=\varnothing\mid\Gamma,x:_{n}\tau$

In the definition of types and environments, $n$ varies over the set
$\mathbb{N}_{>0}^{\infty}=\\{n\in\mathbb{N}\mid n>0\\}\cup\\{\infty\\}$
consisting of positive possibly infinite integers.

For an environment $\Gamma$, we write $|\Gamma|$ for the syntactic object
obtained by removing all gradings from $x:_{n}\tau$ in $\Gamma$. For
environments $\Gamma$ and $\Delta$ such that $|\Gamma|=|\Delta|$, we
inductively define an environment $\Gamma+\Delta$ by

$\varnothing+\varnothing=\varnothing,\qquad(\Gamma,x:_{n}\tau)+(\Delta,x:_{m}\tau)=(\Gamma+\Delta),x:_{n+m}\tau.$

When we write $\Gamma+\Delta$, we always suppose that $|\Gamma|$ is equal to
$|\Delta|$. We write $\Gamma\geq\Delta$ when $|\Gamma|=|\Delta|$ and for all
$x:_{n}\tau\in\Gamma$ and $x:_{m}\tau\in\Delta$, we have $n\leq m$. For an
environment $\Gamma$ and $n\in\mathbb{N}^{\infty}_{>0}$, we define
$n\cdot\Gamma$ to be the environment obtained by the componentwise
multiplication of gradings in $\Gamma$ by $n$.

Terms, values contexts are given by the following BNF.

$\displaystyle\mathrm{Terms}$ $\displaystyle M,N:=\ $
$\displaystyle\cdots\mid\oc M\mid\mathbf{let}\ \oc x\ \mathbf{be}\ M\
\mathbf{in}\ N\mid\mathbf{fix}_{\tau,\sigma}(f,x,M)\mid\overline{a}\cdot M\mid
M+N$ $\displaystyle\mathrm{Values}$ $\displaystyle V,U:=\ $
$\displaystyle\cdots\mid\mathbf{fix}_{\tau,\sigma}(f,x,M)\mid\oc V$ Contexts
$\displaystyle C[-]:=$ $\displaystyle\cdots\mid\oc C[-]\mid\mathbf{let}\ \oc
x\ \mathbf{be}\ C[-]\ \mathbf{in}\ M\mid\mathbf{let}\ \oc x\ \mathbf{be}\ M\
\mathbf{in}\ C[-]$

Namely, we have graded exponentials $\oc(-)$, let-bindings for the graded
comonad, recursion, unary multiplications and addition. We add these term
constructors so as to simplify the definition of the observational metric on
$\Lambda_{S}^{!}$. Typing rules are given in Figure 10, and evaluation rules
are given in Figure 11. We naturally extend the definition of
$\mathbf{Term}^{!}(\Gamma,\tau)$, $\mathbf{Value}^{!}(\tau)$ and
$\mathbf{Value}^{!}(\Gamma)$ to $\Lambda_{S}^{!}$. We write
$C[-]\colon(\Gamma,\tau)\to(\Delta,\sigma)$ when $C[-]$ satisfies the
following conditions.

  * •

For all terms $\Gamma\vdash M:\tau$, we have $\Delta\vdash C[M]:\sigma$.

  * •

For a fresh variable $y$, we have
$y:_{1}\oc_{k_{1}}\tau_{1}\multimap\cdots\oc_{k_{n}}\tau_{n}\multimap\tau,\Delta\vdash
C[y\,\oc x_{1}\cdots\,\oc x_{n}]:\sigma$ where
$\Gamma=(x_{1}:_{k_{1}}\tau_{1},\ldots,x_{n}:_{k_{n}}\tau_{n})$.

We do not have $\mathbf{fix}$ in the definition of contexts because when a
hole of a context is under $\mathbf{fix}$, then the second condition never
holds. Intuitively, the second condition means that the hole $[-]$ appears
linearly in the context $C[]$.

$\prftree{a\in\mathbb{R}}{\Gamma\vdash\overline{a}:\mathbf{R}}\qquad\prftree{}{\Gamma\vdash\ast:\mathbf{I}}\qquad\prftree{f\in
S}{\Gamma_{1}\vdash M_{1}:\mathbf{R}}{\ldots}{\Gamma_{\mathrm{ar}(f)}\vdash
M_{\mathrm{ar}(f)}:\mathbf{R}}{\Gamma_{1}+\cdots+\Gamma_{\mathrm{ar}(f)}\vdash\overline{f}(M_{1},\ldots,M_{\mathrm{ar}(f)}):\mathbf{R}}$

$\prftree{x:_{n}\tau\in\Gamma}{n\geq 1}{\Gamma\vdash
x:\tau}\qquad\prftree{\Gamma\vdash
M:\tau}{n\cdot\Gamma\leq\Delta}{\Delta\vdash\oc
M:\oc_{n}\tau}\qquad\prftree{\Gamma,f:_{\infty}\tau\multimap\sigma,x:_{1}\tau\vdash
M:\sigma}{\infty\cdot\Gamma\vdash\mathbf{fix}_{\tau,\sigma}(f,x,M):\tau\multimap\sigma}$

$\prftree{\Gamma\vdash M:\mathbf{R}}{\Delta\vdash
N:\mathbf{R}}{\Gamma+\Delta\vdash M+N:\mathbf{R}}\qquad\prftree{\Gamma\vdash
M:\oc_{n}\mathbf{R}}{|a|\leq n}{\Gamma\vdash\overline{a}\cdot M:\mathbf{R}}$

$\prftree{\Gamma,x:_{1}\sigma\vdash M:\tau}{\Gamma\vdash\lambda
x:\sigma.\,M:\sigma\multimap\tau}\qquad\prftree{\Gamma\vdash
M:\sigma\multimap\tau}{\Delta\vdash N:\sigma}{\Gamma+\Delta\vdash
M\,N:\tau}\qquad\prftree{\Gamma\vdash M:\tau}{\Delta\vdash
N:\sigma}{\Gamma+\Delta\vdash M\otimes N:\tau\otimes\sigma}$

$\prftree{\Gamma\vdash M:\mathbf{I}}{\Xi\vdash
N:\tau}{n\cdot\Gamma\leq\Delta}{\Delta+\Xi\vdash\mathbf{let}\ \ast\
\mathbf{be}\ M\ \mathbf{in}\ N:\tau}\qquad\prftree{\Gamma\vdash
M:\sigma_{1}\otimes\sigma_{2}}{\Xi,x:_{n}\sigma_{1},y:_{n}\sigma_{2}\vdash
N:\tau}{n\cdot\Gamma\leq\Delta}{\Delta+\Xi\vdash\mathbf{let}\ x\otimes y\
\mathbf{be}\ M\ \mathbf{in}\ N:\tau}$

$\prftree{\Gamma\vdash M:\oc_{m}\sigma}{\Xi,x:_{n\cdot m}\sigma\vdash
N:\tau}{n\cdot\Gamma\leq\Delta}{\Delta+\Xi\vdash\mathbf{let}\ \oc x\
\mathbf{be}\ M\ \mathbf{in}\ N:\tau}$

Figure 10: Typing Rules

$\prftree{V\hookrightarrow
V}\qquad\prftree{M_{1}\hookrightarrow\overline{a_{1}}}{\ldots}{M_{n}\hookrightarrow\overline{a_{n}}}{\overline{f}(M_{1},\ldots,M_{n})\hookrightarrow\overline{f(a_{1},\ldots,a_{n})}}\qquad\prftree{M\hookrightarrow\overline{a}}{N\hookrightarrow\overline{b}}{c=a+b}{M+N\hookrightarrow\overline{c}}$

$\prftree{M\hookrightarrow\oc\overline{b}}{ab=c}{\overline{a}\cdot
M\hookrightarrow\overline{c}}\qquad\prftree{M\hookrightarrow\lambda
x:\tau.\,M^{\prime}}{N\hookrightarrow V}{M^{\prime}[V/x]\hookrightarrow
U}{M\,N\hookrightarrow U}$

$\prftree{M\hookrightarrow V}{N\hookrightarrow U}{M\otimes N\hookrightarrow
V\otimes U}\qquad\prftree{M\hookrightarrow\ast}{N\hookrightarrow
V}{\mathbf{let}\ \ast\ \mathbf{be}\ M\ \mathbf{in}\ N\hookrightarrow
V}\qquad\prftree{M\hookrightarrow V\otimes U}{N[V/x,U/y]\hookrightarrow
W}{\mathbf{let}\ x\otimes y\ \mathbf{be}\ M\ \mathbf{in}\ N\hookrightarrow W}$

$\prftree{M\hookrightarrow\mathbf{fix}_{\tau,\sigma}(f,x,M^{\prime})}{N\hookrightarrow
V}{M^{\prime}[\mathbf{fix}_{\tau,\sigma}(f,x,M^{\prime})/f,V/x]\hookrightarrow
U}{M\,N\hookrightarrow U}$

$\prftree{M\hookrightarrow V}{\oc M\hookrightarrow\oc
V}\qquad\prftree{M\hookrightarrow\oc V}{N[V/x]\hookrightarrow U}{\mathbf{let}\
\oc x\ \mathbf{be}\ M\ \mathbf{in}\ N\hookrightarrow U}$

Figure 11: Evaluation Rules

The following propositions can be shown by induction on derivations of type
judgements.

######  Proposition 9.1 (Substitution).

If $\Gamma\vdash M:\tau$ and $\gamma\in\mathbf{Value}^{!}(\Gamma)$, then
$\vdash M\gamma:\tau$.

######  Proposition 9.2 (Preservation).

If $\vdash M:\tau$ and $M\hookrightarrow V$, then $\vdash V:\tau$.

In general, a type judgement $\Gamma\vdash M:\tau$ may have different
derivations. For example, $x:_{3}\mathbf{R}\vdash x+x:\mathbf{R}$ has the
following derivations.

$\prftree{x:_{1}\mathbf{R}\vdash x:\mathbf{R}}{x:_{2}\mathbf{R}\vdash
x:\mathbf{R}}{x:_{3}\mathbf{R}\vdash
x+x:\mathbf{R}},\qquad\prftree{x:_{2}\mathbf{R}\vdash
x:\mathbf{R}}{x:_{1}\mathbf{R}\vdash x:\mathbf{R}}{x:_{3}\mathbf{R}\vdash
x+x:\mathbf{R}}.$

We can show that grading is the only source of non-uniqueness of derivations.
This observation is useful to define denotational semantics for
$\Lambda_{S}^{!}$ in Section 12.

######  Proposition 9.3.

For any environment $\Gamma$ and any term $M$, if $D_{1}$ is a derivation of
$\Gamma\vdash M:\tau$ and $D_{2}$ is a derivation of $\Gamma\vdash M:\sigma$,
then $\tau$ can be obtained by changing gradings in $\sigma$, and $D_{1}$ can
also be obtained by changing gradings in $D_{2}$.

##  10 Logical Metric and Observational Metric

###  10.1 Metric Logical Relation

We define metric logical relations

$\\{(-)\preceq_{r}^{\tau}(-)\subseteq\mathbf{Term}^{!}(\tau)\times\mathbf{Term}^{!}(\tau)\\}_{\tau\in\mathbf{Ty},\
r\in\mathbb{R}_{\geq 0}^{\infty}}$

for $\Lambda_{S}^{!}$ by induction on $\tau$ as follows.

$\displaystyle M\preceq_{r}^{\mathbf{R}}N$ $\displaystyle\iff\text{if}\
M\hookrightarrow a,\ \text{then}\ N\hookrightarrow b\ \text{and}\ |a-b|\leq r$
$\displaystyle M\preceq_{r}^{\mathbf{I}}N$ $\displaystyle\iff\text{if}\
M\hookrightarrow\ast,\ \text{then}\ N\hookrightarrow\ast$ $\displaystyle
M\preceq_{r}^{\tau\otimes\sigma}N$ $\displaystyle\iff\text{if}\
M\hookrightarrow V\otimes V^{\prime},\ \text{then}\ N\hookrightarrow U\otimes
U^{\prime}$ $\displaystyle\mathrel{\phantom{\iff}}\text{and}\ \exists
s,s^{\prime}\in\mathbb{R}_{\geq 0}^{\infty},\,V\preceq_{s}^{\tau}U\text{ and
}V^{\prime}\preceq_{s^{\prime}}^{\sigma}U^{\prime}\text{ and }s+s^{\prime}\leq
r$ $\displaystyle M\preceq_{r}^{\tau\multimap\sigma}N$
$\displaystyle\iff\text{if}\ M\hookrightarrow V,\ \text{then}\
N\hookrightarrow V^{\prime}$ $\displaystyle\mathrel{\phantom{\iff}}\text{and}\
\forall U,U^{\prime}\in\mathbf{Value}^{!}(\tau),\,\text{if}\
U\preceq_{s}^{\tau}U^{\prime},\ \text{then}\
V\,U\preceq_{r+s}^{\sigma}V^{\prime}\,U^{\prime}$ $\displaystyle
M\preceq_{r}^{\oc_{n}\tau}N$ $\displaystyle\iff\text{if}\ M\hookrightarrow\oc
V,\ \text{then}\ N\hookrightarrow\oc U$
$\displaystyle\mathrel{\phantom{\iff}}\text{and}\ \exists s\in\mathbb{R}_{\geq
0}^{\infty},\,V\precsim_{s}^{\tau}U\ \text{and}\ r\geq n\,s.$

Let $\Gamma=(x_{1}:_{k_{1}}\sigma_{1},\ldots,x_{n}:_{k_{n}}\sigma_{n})$ be an
environment. For $\gamma=(V_{1},\ldots,V_{n})$ and
$\gamma^{\prime}=(V^{\prime}_{1},\ldots,V^{\prime}_{n})$ in
$\mathbf{Value}^{!}(\Gamma)$, and for
$\epsilon=(r_{1},\ldots,r_{n})\in(\mathbb{R}_{\geq 0}^{\infty})^{n}$, we write
$\gamma\preceq_{\epsilon}^{\Gamma}\gamma^{\prime}$ when we have
$V_{1}\preceq_{r_{1}}^{\sigma_{1}}V^{\prime}_{1},\ldots,V_{n}\preceq_{r_{n}}^{\sigma_{n}}V^{\prime}_{n}$.
We define $\epsilon\cdot\Gamma$ to be $r_{1}k_{1}+\cdots+r_{n}k_{n}$. Here, we
define $0\infty$ to be $0$. Then, for terms $\Gamma\vdash M:\tau$ and
$\Gamma\vdash N:\tau$, we define
$d^{\mathrm{log}}_{\Gamma,\tau}(M,N)\in\mathbb{R}_{\geq 0}^{\infty}$ by

$d^{\mathrm{log}}_{\Gamma,\tau}(M,N)=\inf\left\\{r\in\mathbb{R}_{\geq
0}^{\infty}\,\middle|\,\begin{array}[]{l}\forall\gamma,\gamma^{\prime}\in\mathbf{Value}^{!}(\Gamma),\,\text{if}\
\gamma\preceq_{\epsilon}^{\Gamma}\gamma^{\prime},\ \text{then}\\\
M\gamma\preceq_{r+\epsilon\cdot\Gamma}^{\tau}N\gamma^{\prime}\ \text{and}\
N\gamma\preceq_{r+\epsilon\cdot\Gamma}^{\tau}M\gamma^{\prime}\end{array}\right\\}.$

We call $d^{\mathrm{log}}$ the _logical metric_ on $\Lambda_{S}^{!}$. For
later use, we prove the fundamental lemma.

######  Lemma 10.1.

Let $\Gamma=(x_{1}:_{k_{1}}\tau_{1},\ldots,x_{n}:_{k_{n}}\tau_{n})$ be an
environment, and let $\Gamma\vdash M:\tau$ be a term. Given
$\gamma,\gamma^{\prime}\in\mathbf{Value}^{!}(\Gamma)$ such that
$\gamma\preceq_{\epsilon}^{\Gamma}\gamma^{\prime}$, then we have
$M\gamma\preceq_{\epsilon\cdot\Gamma}^{\tau}M\gamma^{\prime}$.

######  Proof 10.2.

The proof is essentially the same with [25] using step indexed logical
relations counting the number of $\mathbf{fix}$-reductions in
$M\hookrightarrow V$.

##  11 Observational Metric

For terms $\Gamma\vdash M:\tau$ and $\Gamma\vdash N:\tau$, we define
$d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)\in\mathbb{R}_{\geq 0}^{\infty}$ by

$d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)=\sup_{C[-]\colon(\Gamma,\tau)\to(\varnothing,\mathbf{R})}\inf\left\\{r\in\mathbb{R}_{\geq
0}^{\infty}\,\middle|\,C[M]\sqsubseteq_{r}C[N]\ \text{and}\
C[N]\sqsubseteq_{r}C[M]\right\\}$

where for $\vdash L,L^{\prime}:\mathbf{R}$,

$L\sqsubseteq_{r}L^{\prime}\iff\text{if}\ L\hookrightarrow a,\ \text{then}\
L^{\prime}\hookrightarrow b\ \text{and}\ |a-b|\leq r.$

######  Theorem 11.1.

For terms $\Gamma\vdash M:\tau$ and $\Gamma\vdash N:\tau$, we have
$d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)=d^{\mathrm{log}}_{\Gamma,\tau}(M,N)$.

######  Proof 11.2.

The statement follows from Lemma 11.3 and Lemma 11.5 shown below.

######  Lemma 11.3.

For any environment
$\Gamma=(x_{1}:_{k_{1}}\tau_{1},\ldots,x_{n}:_{k_{n}}\tau_{n})$ and any pair
of terms $\Gamma\vdash M:\tau$ and $\Gamma\vdash N:\tau$, if
$\gamma\in\mathbf{Value}^{!}(\Gamma)$ and
$d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)<\infty$, then
$M\gamma\preceq_{d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)}^{\tau}N\gamma$.

######  Proof 11.4.

By induction on $\tau$, we show that for all $\Gamma\vdash M:\tau$ and
$\Gamma\vdash N:\tau$, we have
$M\gamma\preceq^{\tau}_{d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)}N\gamma$. We only
give a proof for $\tau=\sigma\otimes\rho$ and $\tau=\sigma\multimap\rho$. (The
case of $\tau=\sigma\otimes\rho$) Given $\gamma\in\mathbf{Value}^{!}(\Gamma)$,
if $M\gamma$ diverges, then by the definition of $\preceq$, we obtain
$M\gamma\preceq_{d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)}N\gamma$. If we have
$M\gamma\hookrightarrow V_{1}\otimes V_{2}$, then since
$d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)<\infty$, there are
$U_{1}\in\mathbf{Value}^{!}(\sigma)$ and $U_{2}\in\mathbf{Value}^{!}(\rho)$
such that $N\gamma\hookrightarrow U_{1}\otimes U_{2}$. By the induction
hypothesis on $\sigma$ and $\rho$, we have
$V_{1}\preceq_{d^{\mathrm{obs}}_{\varnothing,\sigma}(V_{1},U_{1})}^{\sigma}U_{1}$
and
$V_{2}\preceq_{d^{\mathrm{obs}}_{\varnothing,\rho}(V_{2},U_{2})}^{\rho}U_{2}$.
It remains to check that
$d^{\mathrm{obs}}_{\varnothing,\sigma}(V_{1},U_{1})+d^{\mathrm{obs}}_{\varnothing,\rho}(V_{2},U_{2})\leq
d^{\mathrm{obs}}_{\Gamma,\sigma\otimes\rho}(M,N)$. Below, we suppose that
$\gamma=(W_{1},\ldots,W_{n})$. We write $\widetilde{M}$ and $\widetilde{N}$
for

$\displaystyle(\lambda x_{1}:\tau_{1}.\,\cdots\lambda
x_{n}:\tau_{n}.\,M)\,W_{1}\,\cdots\,W_{n}$ $\displaystyle(\lambda
x_{1}:\tau_{1}.\,\cdots\lambda x_{n}:\tau_{n}.\,N)\,W_{1}\,\cdots\,W_{n}$

respectively. Then,

$\displaystyle
d^{\mathrm{obs}}_{\varnothing,\sigma}(V_{1},U_{1})+d^{\mathrm{obs}}_{\varnothing,\rho}(V_{2},U_{2})$
$\displaystyle\leq\sup_{\begin{array}[]{c}\scriptstyle
C[-]\colon(\varnothing,\sigma)\to(\varnothing,\mathbf{R})\\\ \scriptstyle
D[-]\colon(\varnothing,\rho)\to(\varnothing,\mathbf{R})\\\
\end{array}}\inf\left\\{r\in\mathbb{R}_{\geq
0}\,\middle|\,\begin{array}[]{l}C[U_{1}]+D[U_{2}]\sqsubseteq_{r}C[V_{1}]+D[V_{2}]\\\
\ \text{and}\\\
C[V_{1}]+D[V_{2}]\sqsubseteq_{r}C[U_{1}]+D[U_{2}]\end{array}\right\\}$
$\displaystyle\leq\sup_{\begin{array}[]{c}\scriptstyle
C[-]\colon(\varnothing,\sigma)\to(\varnothing,\mathbf{R})\\\ \scriptstyle
D[-]\colon(\varnothing,\rho)\to(\varnothing,\mathbf{R})\\\
\end{array}}\inf\left\\{r\in\mathbb{R}_{\geq
0}\,\middle|\,\begin{array}[]{l}\mathbf{let}\ x\otimes y\ \mathbf{be}\
\widetilde{M}\ \mathbf{in}\ C[x]+D[y]\\\ \qquad\sqsubseteq_{r}\mathbf{let}\
x\otimes y\ \mathbf{be}\ \widetilde{N}\ \mathbf{in}\ C[x]+D[y]\\\ \
\text{and}\\\ \mathbf{let}\ x\otimes y\ \mathbf{be}\ \widetilde{N}\
\mathbf{in}\ C[x]+D[y]\\\ \qquad\sqsubseteq_{r}\mathbf{let}\ x\otimes y\
\mathbf{be}\ \widetilde{M}\ \mathbf{in}\ C[x]+D[y]\end{array}\right\\}$
$\displaystyle\leq d^{\mathrm{obs}}_{\Gamma,\sigma\otimes\rho}(M,N).$

We note that we use the addition to construct contexts. We need unary
multiplications to prove the case where $\tau=\oc_{n}\sigma$. (The case of
$\tau=\sigma\multimap\rho$) Given $\gamma\in\mathbf{Value}^{!}(\Gamma)$, if
$M\gamma$ diverges, then by the definition of $\preceq,$ we have
$M\gamma\preceq^{\tau}_{d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)}N\gamma$. Let us
assume that we have $M\gamma\hookrightarrow V$, and we show that
$M\gamma\preceq^{\tau}_{d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)}N\gamma$. From the
assumption, since $d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)<\infty$, we see that we
have $N\gamma\hookrightarrow V^{\prime}$ for some
$V^{\prime}\in\mathbf{Value}^{!}(\tau)$. In order to prove
$M\gamma\preceq^{\tau}_{d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)}N\gamma$, we show
that for all $U\preceq_{r}^{\sigma}U^{\prime}$, we have
$V\,U\preceq_{r+d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)}^{\rho}V^{\prime}\,U^{\prime}$.
By Lemma 10.1, we obtain
$V^{\prime}\,U\preceq_{r}^{\rho}V^{\prime}\,U^{\prime}$. Hence, by the
triangle inequality, it remains to check
$V\,U\preceq_{d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)}^{\rho}V^{\prime}\,U$. By
the definition of $\preceq$, this is equivalent to
$M\gamma\,U\preceq_{d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)}^{\rho}N\gamma\,U$. It
follows from the induction hypothesis on $\rho$ that we have

$M\gamma\,U\preceq_{d^{\mathrm{obs}}_{\Gamma,\rho}(M\,U,N\,U)}^{\rho}N\gamma\,U.$

Since $d^{\mathrm{obs}}_{\Gamma,\rho}(M\,U,N\,U)\leq
d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)$, we obtain the claim.

######  Lemma 11.5.

For terms $\Gamma\vdash M:\tau$ and $\Gamma\vdash N:\tau$, we have
$d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)\leq d^{\mathrm{log}}_{\Gamma,\tau}(M,N)$.

######  Proof 11.6.

For simplicity, we suppose that $\Gamma=(x:_{k}\sigma)$. We show that if

$\displaystyle\lambda y:\oc_{k}\sigma.\,\mathbf{let}\ \oc x\ \mathbf{be}\ y\
\mathbf{in}\ M$ $\displaystyle\preceq_{r}^{\oc_{k}\sigma\multimap\tau}\lambda
y:\oc_{k}\sigma.\,\mathbf{let}\ \oc x\ \mathbf{be}\ y\ \mathbf{in}\ N$
$\displaystyle\lambda y:\oc_{k}\sigma.\,\mathbf{let}\ \oc x\ \mathbf{be}\ y\
\mathbf{in}\ N$ $\displaystyle\preceq_{r}^{\oc_{k}\sigma\multimap\tau}\lambda
y:\oc_{k}\sigma.\,\mathbf{let}\ \oc x\ \mathbf{be}\ y\ \mathbf{in}\ M$

for some $r\in\mathbb{R}_{\geq 0}^{\infty}$, then
$d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)\leq r$. Given a context
$C[-]\colon(\Gamma,\tau)\to(\varnothing,\mathbf{R})$, it follows from adequacy
of denotational model (Theorem 12.1) that

$\displaystyle C[M]\hookrightarrow a$ $\displaystyle\iff(\lambda
z:\oc_{k}\sigma\multimap\tau.\,C[z\,\oc x])(\lambda
y:\oc_{k}\sigma.\,\mathbf{let}\ \oc x\ \mathbf{be}\ y\ \mathbf{in}\
M)\hookrightarrow a,$ $\displaystyle C[N]\hookrightarrow b$
$\displaystyle\iff(\lambda z:\oc_{k}\sigma\multimap\tau.\,C[z\,\oc x])(\lambda
y:\oc_{k}\sigma.\,\mathbf{let}\ \oc x\ \mathbf{be}\ y\ \mathbf{in}\
N)\hookrightarrow b.$

Hence, it follows from Lemma 10.1 that $C[M]$ converges if and only if $C[N]$
converges. If $C[M]\hookrightarrow a$ and $C[N]\hookrightarrow b$, then we
have $|a-b|\leq r$. Since this holds for any context
$C[-]\colon(\Gamma,\tau)\to(\varnothing,\mathbf{R})$, we obtain
$d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)\leq r$.

##  12 Denotational Metric

Let $\mathbf{MetCpo}_{\bot}$ be the category of pointed metric cpos and strict
continuous and non-expansive functions. Concretely, objects in
$\mathbf{MetCpo}_{\bot}$ are metric cpos with least elements $\bot$ such that
the distances $d(\bot,x)$ are $\infty$ when $x\neq\bot$, and morphisms from
$X$ to $Y$ are bottom-preserving. As is shown in [3], $\mathbf{MetCpo}_{\bot}$
provides an adequate semantics for Fuzz. By restricting their result to our
language, we obtain adequacy for $\Lambda_{S}^{!}$. For a term $\Gamma\vdash
M:\tau$, let us write $\llbracket
M\rrbracket^{\mathrm{den}}\colon\llbracket\Gamma\rrbracket^{\mathrm{den}}\to\llbracket\tau\rrbracket^{\mathrm{den}}$
for the interpretation of $M$ in $\mathbf{MetCpo}_{\bot}$. We note that
$\llbracket M\rrbracket^{\mathrm{den}}$ is defined with respect to the type
judgement rather than type derivations of $\Gamma\vdash M:\tau$. This can be
checked by observing that the underlying continuous function of $\llbracket
M\rrbracket^{\mathrm{den}}$ is obtained by first transforming
$\Lambda_{S}^{!}$ into the $\lambda_{c}$-calculus [23] and then interpreting
the transformed term in $\mathbf{Cpo}_{\bot}$. In the transformation of
$\Lambda_{S}^{!}$ into the $\lambda_{c}$-calculus, gradings are dropped, and
therefore, all derivations of a type judgement $\Gamma\vdash M:\tau$ are
transformed into the same derivation in the $\lambda_{c}$-calculus.

######  Theorem 12.1 ([3]).

Let $\vdash M:\tau$ be a term in $\Lambda_{S}^{!}$.

  * •

If $M\hookrightarrow V$, then $\llbracket
M\rrbracket^{\mathrm{den}}=\llbracket V\rrbracket^{\mathrm{den}}$.

  * •

If $\llbracket M\rrbracket^{\mathrm{den}}\neq\bot$, then there is a value
$V\in\mathbf{Value}^{!}(\tau)$ such that $M\hookrightarrow V$.

For terms $\Gamma\vdash M:\tau$ and $\Gamma\vdash N:\tau$, we define
$d^{\mathrm{den}}_{\Gamma,\tau}(M,N)\in\mathbb{R}_{\geq 0}^{\infty}$ by

$d^{\mathrm{den}}_{\Gamma,\tau}(M,N)=d(\llbracket
M\rrbracket^{\mathrm{den}},\llbracket N\rrbracket^{\mathrm{den}}).$

It is easy to see that $d^{\mathrm{den}}$ is a metric on $\Lambda_{S}^{!}$. We
call $d^{\mathrm{den}}$ the _denotational metric_ on $\Lambda_{S}^{!}$.

It follows from adequacy of $\mathbf{MetCpo}_{\bot}$ that $d^{\mathrm{obs}}$
is bounded by $d^{\mathrm{den}}$.

######  Theorem 12.2.

$d^{\mathrm{obs}}\leq d^{\mathrm{den}}$.

######  Proof 12.3.

If there is a context $C[-]\colon(\Gamma,\tau)\to(\varnothing,\mathbf{R})$
such that $C[M]$ converges and $C[N]$ diverges, then, by adequacy, we have
$\llbracket C[M]\rrbracket=\llbracket\overline{a}\rrbracket$. $\llbracket
C[N]\rrbracket=\bot$ for some $a\in\mathbb{R}$. Hence,
$d^{\mathrm{den}}_{\Gamma,\tau}(M,N)\geq
d^{\mathrm{den}}_{\varnothing,\mathbf{R}}(C[M],C[N])=\infty\geq
d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)$. Similarly, when $C[M]$ diverges and
$C[N]$ converges, then $d^{\mathrm{den}}_{\Gamma,\tau}(M,N)\geq
d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)$. Below, we suppose that for any context
$C[-]\colon(\Gamma,\tau)\to(\varnothing,\mathbf{R})$, $C[M]$ diverges if and
only if $C[N]$ diverges. In this case, it follows from Theorem 12.1 that if
$C[M]\hookrightarrow a$ and $C[N]\hookrightarrow b$, then $|a-b|\leq
d^{\mathrm{den}}_{\Gamma,\tau}(M,N)$. Hence, we obtain the statement.

##  13 Interactive Semantic Model

###  13.1 Preparation

####  13.1.1 Structures for Interpreting Graded Exponentials

We prepare structures on the category $\mathbf{Int}(\mathbf{MetCppo})$ that we
use to interpret graded exponentials in $\Lambda_{S}^{!}$. For
$X\in\mathbf{MetCppo}$ and $n\in\mathbb{N}^{\infty}_{>0}$, we define $n\cdot
X$ to be the countably infinite product of the underlying cpo of $X$ equipped
with the following metric:

$d((x_{i})_{i\in\mathbb{N}},(y_{i})_{i\in\mathbb{N}})=\sum_{i<n}d(x_{i},y_{i}).$

It is not difficult to check that $n\cdot(-)$ is a traced symmetric monoidal
functor on $\mathbf{MetCppo}$. Hence, we can lift the functors $n\cdot(-)$ to
symmetric monoidal functors on $\mathbf{Int}(\mathbf{MetCppo})$. Abusing
notation, we also denote the functors on $\mathbf{Int}(\mathbf{MetCppo})$ by
$n\cdot(-)$. To be concrete, on objects $X=(X_{+},X_{-})$ in
$\mathbf{Int}(\mathbf{MetCppo})$, we have $n\cdot X=(n\cdot X_{+},n\cdot
X_{-})$.

In order to interpret dereliction, digging and contraction of
$\Lambda_{S}^{!}$, for $n,m\in\mathbb{N}^{\infty}_{>0}$, we choose bijections
$u_{n,m}\colon\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ and
$v_{n,m}\colon\\{0,1\\}\times\mathbb{N}\to\mathbb{N}$ such that

  * •

$u_{n,m}$ embeds $\\{(i,j)\in\mathbb{N}\times\mathbb{N}\mid i<n\ \text{and}\
j<m\\}$ into $\\{i\in\mathbb{N}\mid i<nm\\}$; and

  * •

$v_{n,m}$ embeds $\\{(0,i)\mid i<n\\}\cup\\{(1,i)\mid i<m\\}$ into
$\\{i\in\mathbb{N}\mid i<n+m\\}$.

Then, we define the following morphisms

$\displaystyle d_{n,X}\colon n\cdot X$ $\displaystyle\to X,$
$\displaystyle\delta_{n,m,X}\colon nm\cdot X$ $\displaystyle\cong
n\cdot(m\cdot X),$ $\displaystyle c_{n,m,X}\colon(n+m)\cdot X$
$\displaystyle\cong(n\cdot X)\otimes(m\cdot X)$

for $n,m\in\mathbb{N}^{\infty}_{>0}$ by

$\displaystyle d_{n,X}((x_{i})_{i\in\mathbb{N}},y)$
$\displaystyle=((y,\bot,\bot,\ldots),x_{0}),$
$\displaystyle\delta_{n,m,X}((x_{i})_{i\in\mathbb{N}},((y_{i,j})_{j\in\mathbb{N}})_{i\in\mathbb{N}})$
$\displaystyle=((y_{u^{-1}_{n,m}(i)})_{i\in\mathbb{N}},((x_{u_{n,m}(i,j)})_{j\in\mathbb{N}})_{i\in\mathbb{N}}),$
$\displaystyle
c_{X}((x_{i})_{i\in\mathbb{N}},((y_{0,i})_{i\in\mathbb{N}},(y_{1,i})_{i\in\mathbb{N}}))$
$\displaystyle=((y_{v_{n,m}(i)})_{i\in\mathbb{N}},((x_{v^{-1}_{n,m}(0,i)})_{i\in\mathbb{N}},(x_{v^{-1}_{n,m}(1,i)})_{i\in\mathbb{N}})).$

We also give a bit more general dereliction $\tilde{d}_{n,m,X}\colon(n+m)\cdot
X\to n\cdot X$ by

$\tilde{d}_{n,m,X}((x_{i})_{i\in\mathbb{N}},(y_{i})_{i\in\mathbb{N}})=((y_{0},y_{1},\ldots,y_{n-1},\overbrace{\bot,\ldots,\bot}^{m},y_{n},y_{n+1},\ldots),\\\
(x_{0},x_{1},\ldots,x_{n-1},x_{n+m-1},x_{n+m},\ldots)).$

We note that morphisms $d_{n,X}$, $\delta_{n,m,X}$, $c_{n,m,X}$,
$\tilde{d}_{n,m,X}$ and $w_{X}$ are not natural with respect to $X$. Still, we
can show that they are _pointwise_ natural transformation, that is, these
morphisms satisfy naturality conditions for global elements. For example, for
all $x\colon I\to X$, we have $d_{n,X}\circ(n\cdot x)=x\circ d_{n,I}=x$. For
more details on pointwise naturality, see [1].

####  13.1.2 Structures for Interpreting Weakening and Cbv Evaluation

We also need structures on $\mathbf{Int}(\mathbf{MetCppo})$ to interpret
weakening and call-by-value evaluation. For the former, for an object
$X\in\mathbf{Int}(\mathbf{MetCppo})$, we define $w_{X}\colon X\to I$ in
$\mathbf{Int}(\mathbf{MetCppo})$ to be $\bot\colon X_{+}\to X_{-}$ in
$\mathbf{MetCppo}$. For the latter, we use the Kleisli category of a
continuation monad

$TX=X\otimes(K,K)\cong(X\multimap(K,I))\multimap(K,I)$

on $\mathbf{Int}(\mathbf{MetCppo})$ where $K\in\mathbf{MetCppo}$ is the
Sierpiński space $\\{\bot\leq\top\\}$ equipped with $d(\bot,\top)=\infty$. We
denote the unit, the multiplication and the strength of the monad $T$ by

$\displaystyle\eta_{X}$ $\displaystyle\colon X\to TX,$ $\displaystyle\mu_{X}$
$\displaystyle\colon TTX\to TX,$ $\displaystyle\mathrm{str}_{X,Y}$
$\displaystyle\colon TX\otimes Y\to T(X\otimes Y),$

and we write $\mathrm{dstr}_{X,Y}\colon TX\otimes TY\to T(X\otimes Y)$ for the
double strength

$TX\otimes TY\longrightarrow T(X\otimes TY)\longrightarrow TT(X\otimes
Y)\longrightarrow T(X\otimes Y).$

For $n\in\mathbb{N}^{\infty}_{>0}$, we define a morphism

$\xi_{n,X}\colon n\cdot TX\to T(n\cdot X)$

in $\mathbf{Int}(\mathbf{MetCppo})$ to be

$n\cdot TX=n\cdot(X\otimes(K,K))\cong n\cdot X\otimes
n\cdot(K,K)\xrightarrow{(n\cdot X)\otimes d}(n\cdot X)\otimes(K,K)=T(n\cdot
X).$

We use this distributivity of $n\cdot(-)$ over $T$ to model the action of
graded exponentials on terms.

####  13.1.3 Structures for Interpreting Constants

For interpretation of constants $\overline{a}$ and
$\overline{f}(M_{1},\ldots,M_{\mathrm{ar}(f)})$, we follow the interpretation
of terms in $\Lambda_{S}$: we interpret the base type $\mathbf{R}$ by $(R,I)$,
and we use $\lfloor a\rfloor\colon I\to R$ and $\lfloor f\rfloor\colon
R^{\otimes\mathrm{ar}(f)}\to R$ to interpret real numbers and first order
functions. For interpretation of unary multiplications, we use

$\mathrm{mult}_{a,n}\colon n\cdot(R,I)\to(R,I)$

for $a\in\mathbb{R}$ and $n\in\mathbb{N}^{\infty}_{>0}$ such that $|a|\leq n$
given by

$\mathrm{mult}_{a,n}((x_{i})_{i\in\mathbb{N}},\ast)=(\ast,a(x_{0}+\cdots+x_{n-1})/n).$

###  13.2 Interactive Semantic Model and its Associated Metrics

Based on preparations in the previous sections, we give interpretation of
$\Lambda_{S}^{!}$ in the Kleisli category
$\mathbf{Int}(\mathbf{MetCppo})_{T}$.

Types in $\Lambda_{S}^{!}$ are interpreted as follows:

$\displaystyle\llbracket\mathbf{R}\rrbracket^{\mathrm{int}}$
$\displaystyle=(R,I),$
$\displaystyle\llbracket\mathbf{I}\rrbracket^{\mathrm{int}}$
$\displaystyle=(I,I),$
$\displaystyle\llbracket\tau\otimes\sigma\rrbracket^{\mathrm{int}}$
$\displaystyle=\llbracket\tau\rrbracket^{\mathrm{int}}\otimes\llbracket\sigma\rrbracket^{\mathrm{int}}$
$\displaystyle\llbracket\tau\multimap\sigma\rrbracket^{\mathrm{int}}$
$\displaystyle=\llbracket\tau\rrbracket^{\mathrm{int}}\multimap
T\llbracket\sigma\rrbracket^{\mathrm{int}}=(\llbracket\tau\rrbracket^{\mathrm{int}})^{\ast}\otimes\llbracket\sigma\rrbracket^{\mathrm{int}}\otimes(K,K)$
$\displaystyle\llbracket\oc_{n}\tau\rrbracket^{\mathrm{int}}$
$\displaystyle=n\cdot\llbracket\tau\rrbracket^{\mathrm{int}}$

where $(X_{+},X_{-})^{\ast}$ is defined to be $(X_{-},X_{+})$. As usual, we
interpret environments as follows:

$\llbracket(x:_{n}\tau,\ldots,y:_{m}\sigma)\rrbracket^{\mathrm{int}}=n\cdot\llbracket\tau\rrbracket^{\mathrm{int}}\otimes\cdots\otimes
m\cdot\llbracket\sigma\rrbracket^{\mathrm{int}}.$

We next define interpretation of type judgements in $\Lambda_{S}^{!}$ in
Figure 12 where we simply write $\llbracket-\rrbracket$ for
$\llbracket-\rrbracket^{\mathrm{int}}$ for the sake of legibility. We note
that the interpretation is given with respect to type derivations rather than
type judgements.

We call this model the _interactive semantic model_ for $\Lambda_{S}^{!}$. The
interactive semantic model gives rise to another semantically obtained family
of metrics. For terms $\Gamma\vdash M:\tau$ and $\Gamma\vdash N:\tau$, we
define $d^{\mathrm{int}}_{\Gamma,\tau}(M,N)\in\mathbb{R}_{\geq 0}^{\infty}$ by

$d^{\mathrm{int}}_{\Gamma,\tau}(M,N)=d(\llbracket
M\rrbracket^{\mathrm{int}},\llbracket N\rrbracket^{\mathrm{int}}).$

We prove adequacy of the interactive semantic model, which will be used to
prove $d^{\mathrm{obs}}\leq d^{\mathrm{int}}$. Below, for $\vdash M:\tau$, we
write $\llbracket M\rrbracket\Downarrow$ when there is no $f\colon
I\to\llbracket\tau\rrbracket$ such that $\llbracket
M\rrbracket=f\otimes\bot_{(K,K)}$ where $\bot_{X}$ denotes the least element
of $\mathbf{Int}(\mathbf{MetCppo})(I,X)$.

######  Theorem 13.1.

Let $\vdash M:\tau$ be a term in $\Lambda_{S}^{!}$.

  * •

If $M\hookrightarrow V$, then there is a derivation of $\vdash V:\tau$ such
that $\llbracket M\rrbracket=\llbracket V\rrbracket$.

  * •

If $\llbracket M\rrbracket\Downarrow$, then there is a value $V$ such that
$M\hookrightarrow V$.

######  Proof 13.2.

We can show the first claim by induction on the derivation of
$M\hookrightarrow V$ using pointwise naturality of morphisms in Section
13.1.1, and we omit the detail. We prove the second claim by means of logical
relations. For a type $\tau$, we define a binary relation

$P_{\tau}\subseteq\mathbf{Int}(\mathbf{MetCppo})(I,\llbracket\tau\rrbracket)\times\mathbf{Value}^{!}(\tau)$

by

$\displaystyle P_{\mathbf{R}}$
$\displaystyle=\\{(\llbracket\overline{a}\rrbracket,\overline{a})\mid
a\in\mathbb{R}\\},$ $\displaystyle P_{\mathbf{I}}$
$\displaystyle=\\{(\llbracket\ast\rrbracket,\ast)\\},$ $\displaystyle
P_{\tau\otimes\sigma}$ $\displaystyle=\\{(f\otimes g,V\otimes U)\mid(f,V)\in
P_{\tau}\ \text{and}\ (g,U)\in P_{\sigma}\\},$ $\displaystyle
P_{\tau\multimap\sigma}$ $\displaystyle=\\{(f,V)\mid\forall(g,U)\in
P_{\tau},\,(f\bullet g,V\,U)\in\overline{P}_{\sigma}\\},$ $\displaystyle
P_{\oc_{n}\tau}$ $\displaystyle=\\{(n\cdot f,\oc V)\mid(f,V)\in P_{\tau}\\}$

where

$\overline{P}_{\tau}=\\{(\eta\circ f,M)\mid M\hookrightarrow V\ \text{and}\
(f,V)\in P_{\tau}\\}\\\ {}\cup{}\\{(f\otimes\bot_{(K,K)},M)\mid f\colon
I\to\llbracket\tau\rrbracket\ \text{and}\ M\in\mathbf{Term}^{!}(\tau)\\}$

and $f\bullet g$ is given by

$I\xrightarrow{f\otimes g}(\llbracket\tau\rrbracket\multimap
T\llbracket\sigma\rrbracket)\otimes\llbracket\tau\rrbracket\xrightarrow{\text{eval}}T\llbracket\sigma\rrbracket.$

By the definition of $P_{\tau}$, we can show that $P_{\tau}$ and
$\overline{P}_{\tau}$ are closed under taking least upper bounds of the first
component: for all $(x_{1},M),(x_{2},M),\ldots\in P_{\tau}$, if $x_{1}\leq
x_{2}\leq\cdots$, then we have
$\left(\bigvee_{n\in\mathbb{N}}x_{n},M\right)\in P_{\tau}$. We show basic
lemma for $P_{\tau}$: for any
$\Gamma=(x:_{n_{1}}\sigma,\ldots,y:_{n_{k}}\rho)$, any $\Gamma\vdash M:\tau$
and any $(v,V)\in P_{\sigma},\ldots,(u,U)\in P_{\rho}$, we have

$(\llbracket M\rrbracket\circ((n_{1}\cdot v)\otimes\cdots\otimes(n_{k}\cdot
u)),M[V/x,\ldots,U/y])\in\overline{P}_{\tau}.$

We only check the case for $\mathbf{fix}$. The other cases are not difficult
to check. What we check is: for environments
$\Gamma=(x_{1}:_{k_{1}}\rho_{1},\ldots,x_{n}:_{k_{n}}\rho_{n})$ and
$\Delta=(x_{1}:_{k^{\prime}_{1}}\rho_{1},\ldots,x_{n}:_{k^{\prime}_{n}}\rho_{n})$
such that $\infty\cdot\Gamma\leq\Delta$ and for a term
$\Delta\vdash\mathbf{fix}_{\tau,\sigma}(f,x,M):\tau\multimap\sigma$, given
$(v_{1},V_{1})\in P_{\rho_{1}},\ldots,(v_{n},V_{n})\in P_{\rho_{n}}$, we have

$(\llbracket\mathbf{fix}_{\tau,\sigma}(f,x,M)\rrbracket\circ((k_{1}\cdot
v_{n})\otimes\cdots\otimes(k_{n}\cdot
v_{n})),\mathbf{fix}_{\tau,\sigma}(f,x,M)[V_{1}/x_{1},\ldots,V_{n}/x_{n}])\in
P_{\tau\multimap\sigma}.$

Let
$\varphi\colon\mathbf{Int}(\mathbf{MetCppo})(\infty\cdot\llbracket\Gamma\rrbracket,\tau\multimap\sigma)\to\mathbf{Int}(\mathbf{MetCppo})(\infty\cdot\llbracket\Gamma\rrbracket,\tau\multimap\sigma)$
be the function given in Figure 12. Then, by induction on $m$, we can show
that

$\left(I\xrightarrow{(k^{\prime}_{1}\cdot
v_{1})\otimes\cdots(k^{\prime}_{n}\cdot
v_{n})}\llbracket\Delta\rrbracket\xrightarrow{d}\llbracket\infty\cdot\Gamma\rrbracket\xrightarrow{\varphi^{m}}\llbracket\tau\multimap\sigma\rrbracket,\mathbf{fix}_{\tau,\sigma}(f,x,M)[V_{1}/x_{1},\ldots,V_{n}/x_{n}]\right)$

is an element of $P_{\tau\multimap\sigma}$. Since
$P_{\tau\multimap\tau^{\prime}}$ is closed under least upper bounds on the
first component, we obtain the claim.

######  Theorem 13.3.

For any pair of terms $\Gamma\vdash M:\tau$ and $\Gamma\vdash N:\tau$, we have
$d^{\mathrm{obs}}_{\Gamma,\tau}(M,N)\leq d^{\mathrm{int}}(M,N)$.

######  Proof 13.4.

We can prove the statement in the same way with Theorem 12.2.

$\displaystyle\llbracket\Gamma\vdash\overline{a}:\mathbf{R}\rrbracket=\llbracket\Gamma\rrbracket\xrightarrow{w}I\xrightarrow{\lfloor
a\rfloor}(R,I)\xrightarrow{\eta}T(R,I)$
$\displaystyle\llbracket\Gamma\vdash\ast:\mathbf{I}\rrbracket=\llbracket\Gamma\rrbracket\xrightarrow{w}I\xrightarrow{\eta}TI$
$\displaystyle\llbracket\Gamma_{1}+\Gamma_{2}\vdash\overline{f}(M_{1},M_{2}):\mathbf{R}\rrbracket=$
$\displaystyle\quad\llbracket\Gamma_{1}+\Gamma_{2}\rrbracket\xrightarrow{c}\llbracket\Gamma_{1}\rrbracket\otimes\llbracket\Gamma_{2}\rrbracket\xrightarrow{\llbracket
M_{1}\rrbracket\otimes\llbracket
M_{2}\rrbracket}T\llbracket\mathbf{R}\rrbracket\otimes
T\llbracket\mathbf{R}\rrbracket\xrightarrow{\mathrm{dstr}}T(\llbracket\mathbf{R}\rrbracket\otimes\llbracket\mathbf{R}\rrbracket)\xrightarrow{T\lfloor
f\rfloor}T\llbracket\mathbf{R}\rrbracket$ $\displaystyle\llbracket
x:_{n}\tau\vdash
x:\tau\rrbracket=n\cdot\llbracket\tau\rrbracket\xrightarrow{d}\llbracket\tau\rrbracket\xrightarrow{\eta}T\llbracket\tau\rrbracket$
$\displaystyle\llbracket\Delta\vdash\oc
M:\oc_{n}\tau\rrbracket=\llbracket\Delta\rrbracket\xrightarrow{\tilde{d}}n\cdot\llbracket\Gamma\rrbracket\xrightarrow{n\cdot\llbracket
M\rrbracket}n\cdot
T\llbracket\tau\rrbracket\xrightarrow{\xi}T\llbracket\oc_{n}\tau\rrbracket$
$\displaystyle\llbracket\Delta\vdash\mathbf{fix}_{\tau,\sigma}(f,x,M):\tau\multimap\sigma\rrbracket=\llbracket\Delta\rrbracket\xrightarrow{\tilde{d}}\infty\cdot\llbracket\Gamma\rrbracket\xrightarrow{\text{the
least fixed point of $\varphi$}}\tau\multimap\sigma$
$\displaystyle\llbracket\Gamma+\Delta\vdash M+N:\mathbf{R}\rrbracket=$
$\displaystyle\qquad\llbracket\Gamma+\Delta\rrbracket\xrightarrow{c}\llbracket\Gamma\rrbracket\otimes\llbracket\Delta\rrbracket\xrightarrow{\llbracket
M\rrbracket\otimes\llbracket
N\rrbracket}T\llbracket\mathbf{R}\rrbracket\otimes
T\llbracket\mathbf{R}\rrbracket\xrightarrow{\mathrm{dstr}}T(\llbracket\mathbf{R}\rrbracket\otimes\llbracket\mathbf{R}\rrbracket)\xrightarrow{T(+)}T\llbracket\mathbf{R}\rrbracket$
$\displaystyle\llbracket\Delta\vdash\overline{a}\cdot
M:\mathbf{R}\rrbracket=\llbracket\Delta\rrbracket\xrightarrow{\tilde{d}}\llbracket\Gamma\rrbracket\xrightarrow{\llbracket
M\rrbracket}n\cdot\llbracket\mathbf{R}\rrbracket\xrightarrow{\mathrm{mult}_{n,a}}\llbracket\mathbf{R}\rrbracket\xrightarrow{\eta}T\llbracket\mathbf{R}\rrbracket$
$\displaystyle\llbracket\Gamma\vdash\lambda
x:\sigma.\,M:\sigma\multimap\tau\rrbracket=(\text{the currying of}\
\llbracket\Gamma\rrbracket\otimes\llbracket\sigma\rrbracket\xrightarrow{\llbracket
M\rrbracket}\llbracket\tau\rrbracket)\xrightarrow{\eta}T\llbracket\sigma\multimap\tau\rrbracket$
$\displaystyle\llbracket\Gamma+\Delta\vdash
M\,N:\tau\rrbracket=\llbracket\Gamma+\Delta\rrbracket\xrightarrow{c}\llbracket\Gamma\rrbracket\otimes\llbracket\Delta\rrbracket\xrightarrow{\llbracket
M\rrbracket\otimes\llbracket
N\rrbracket}\llbracket\tau\multimap\sigma\rrbracket\otimes\llbracket\tau\rrbracket\xrightarrow{\text{eval}}T\llbracket\sigma\rrbracket$
$\displaystyle\llbracket\Gamma+\Delta\vdash M\otimes
N:\tau\otimes\sigma\rrbracket=\llbracket\Gamma+\Delta\rrbracket\xrightarrow{c}\llbracket\Gamma\rrbracket\otimes\llbracket\Delta\rrbracket\xrightarrow{\llbracket
M\rrbracket\otimes\llbracket N\rrbracket}T\llbracket\tau\rrbracket\otimes
T\llbracket\sigma\rrbracket\xrightarrow{\mathrm{dstr}}T\llbracket\tau\otimes\sigma\rrbracket$
$\displaystyle\llbracket\Delta+\Xi\vdash\mathbf{let}\ \ast\ \mathbf{be}\ M\
\mathbf{in}\
N:\tau\rrbracket=\llbracket\Delta+\Xi\rrbracket\xrightarrow{c}\llbracket\Xi\rrbracket\otimes\llbracket\Delta\rrbracket\xrightarrow{\tilde{d}}\llbracket\Xi\rrbracket\otimes
n\cdot\llbracket\Gamma\rrbracket\xrightarrow{\llbracket
N\rrbracket\otimes((n\cdot\llbracket M\rrbracket);\xi)}$ $\displaystyle\quad
T\llbracket\tau\rrbracket\otimes
TI\xrightarrow{\mathrm{dstr}}T\llbracket\tau\rrbracket$
$\displaystyle\llbracket\Delta+\Xi\vdash\mathbf{let}\ x\otimes y\ \mathbf{be}\
M\ \mathbf{in}\
N:\tau\rrbracket=\llbracket\Delta+\Xi\rrbracket\xrightarrow{c}\llbracket\Xi\rrbracket\otimes\llbracket\Delta\rrbracket\xrightarrow{\tilde{d}}\llbracket\Xi\rrbracket\otimes
n\cdot\llbracket\Gamma\rrbracket\xrightarrow{\llbracket\Xi\rrbracket\otimes((n\cdot\llbracket
M\rrbracket);\xi)}$ $\displaystyle\quad\llbracket\Xi\rrbracket\otimes
T(n\cdot(\llbracket\sigma_{1}\rrbracket\otimes\llbracket\sigma_{2}\rrbracket))\xrightarrow{\cong}\llbracket\Xi\rrbracket\otimes
T(n\cdot\llbracket\sigma_{1}\rrbracket\otimes
n\cdot\llbracket\sigma_{2}\rrbracket)\xrightarrow{\mathrm{str};\llbracket
N\rrbracket;\mu}T\llbracket\tau\rrbracket$
$\displaystyle\llbracket\Delta+\Xi\vdash\mathbf{let}\ \oc x\ \mathbf{be}\ M\
\mathbf{in}\
N:\tau\rrbracket=\llbracket\Delta+\Xi\rrbracket\xrightarrow{c}\llbracket\Xi\rrbracket\otimes\llbracket\Delta\rrbracket\xrightarrow{\tilde{d}}\llbracket\Xi\rrbracket\otimes
n\cdot\llbracket\Gamma\rrbracket\xrightarrow{\llbracket\Xi\rrbracket\otimes((n\cdot\llbracket
M\rrbracket);\xi)}$ $\displaystyle\quad\llbracket\Xi\rrbracket\otimes T(n\cdot
m\cdot\llbracket\sigma\rrbracket)\xrightarrow{\cong}\llbracket\Xi\rrbracket\otimes
T(nm\cdot\llbracket\sigma\rrbracket)\xrightarrow{\mathrm{str};\llbracket
N\rrbracket;\mu}T\llbracket\tau\rrbracket$

where
$\varphi\colon\mathbf{Int}(\mathbf{MetCppo})(\infty\cdot\llbracket\Gamma\rrbracket,\tau\multimap\sigma)\to\mathbf{Int}(\mathbf{MetCppo})(\infty\cdot\llbracket\Gamma\rrbracket,\tau\multimap\sigma)$
is given by

$\varphi(f)=\infty\cdot\llbracket\Gamma\rrbracket\xrightarrow{c}\infty\cdot\llbracket\Gamma\rrbracket\otimes\infty\cdot\llbracket\Gamma\rrbracket\xrightarrow{d\otimes\delta}\llbracket\Gamma\rrbracket\otimes\infty\cdot\infty\cdot\llbracket\Gamma\rrbracket\\\
\xrightarrow{\llbracket\Gamma\rrbracket\otimes\infty\cdot
f}\llbracket\Gamma\rrbracket\otimes\infty\cdot(\tau\multimap\sigma)\xrightarrow{\text{the
currying of $\llbracket M\rrbracket$}}\tau\multimap\sigma$

Figure 12: Interpretation of Terms

##  14 Conclusion

In this paper we study quantitative reasoning about linearly typed higher-
order programs. We introduce a notion of admissibility for families of metrics
on a purely linear programming language $\Lambda_{S}$, and among them, we
investigate five notions of program metrics and how these are related, namely
the logical metric, observational metric, equational metric, denotational
metric and interactive metric. Some of our results can be seen as quantitative
analogues of well-known results about program equivalences: the observational
metric is less discriminating than or equal to semantic metrics, and non-
definable functionals in the semantics are the source of inclusions. Existence
of fully abstract semantics for $\Lambda_{S}$ with respect to the
observational metric is left open. Our study reveals the intrinsic difficulty
of comparing denotational models with interactive semantic models obtained by
applying the Int-construction. Indeed, their relationship is not trivial
already at the level of program equivalences. It follows from [16] that there
is a symmetric monoidal coreflection between $\mathbf{Int}(\mathbf{MetCppo})$
and $\mathbf{MetCppo}$. This is a strong connection between these models.
However, we do not know whether this categorical structure sheds light on
their relationship at the level of higher-order programs.

Some of our results can be extended to a fragment of Fuzz where grading is
restricted to extended natural numbers. Providing a quantitative equational
theory and an interactive metric for full Fuzz is another very interesting
topic for future work. There are some notions of metric that we have not taken
into account in this paper. In [13], Gavazzo gives coinductively defined
metrics for an extension of Fuzz with algebraic effects and recursive types,
which we do not consider here. The so-called observational quotient [17] is a
way to construct less discriminating program metrics from fine-grained ones. A
thorough comparison of these notions of program distance with the ones we
introduce here is another intriguing problem on which we plan to work in the
future.

## References

  * [1] Abramsky, S., Haghverdi, E., Scott, P.: Geometry of interaction and linear combinatory algebras. Mathematical Structures in Computer Science 12(5), 625–665 (2002). 10.1017/S0960129502003730
  * [2] Abramsky, S., Jagadeesan, R.: New foundations for the geometry of interaction. Inf. Comput. 111(1), 53–119 (May 1994)
  * [3] Azevedo de Amorim, A., Gaboardi, M., Hsu, J., Katsumata, S.y., Cherigui, I.: A semantic account of metric preservation. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. pp. 545–556. POPL 2017, Association for Computing Machinery, New York, NY, USA (2017)
  * [4] Barber, A., Plotkin, G.D.: Dual intuitionistic linear logic (1996), unpublished draft. An early version appeared as a technical report ECS-LFCS-96-347, LFCS, University of Edinburgh
  * [5] Blum, A., Dwork, C., McSherry, F., Nissim, K.: Practical privacy: The sulq framework. In: Proceedings of the Twenty-Fourth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems. p. 128–138. PODS ’05, Association for Computing Machinery, New York, NY, USA (2005). 10.1145/1065167.1065184, https://doi.org/10.1145/1065167.1065184
  * [6] Crubillé, R., Dal Lago, U.: Metric reasoning about $\lambda$-terms: The affine case. In: Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). p. 633?644. LICS ’15, IEEE Computer Society, USA (2015). 10.1109/LICS.2015.64, https://doi.org/10.1109/LICS.2015.64
  * [7] Crubillé, R., Dal Lago, U.: Metric reasoning about $\lambda$-terms: The general case. In: Yang, H. (ed.) Programming Languages and Systems. pp. 341–367. Springer Berlin Heidelberg, Berlin, Heidelberg (2017)
  * [8] Crubillé, R., Lago, U.D.: On probabilistic applicative bisimulation and call-by-value $\lambda$-calculi. In: Shao, Z. (ed.) Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. Lecture Notes in Computer Science, vol. 8410, pp. 209–228. Springer (2014). 10.1007/978-3-642-54833-8_12, https://doi.org/10.1007/978-3-642-54833-8_12
  * [9] Crubillé, R., Lago, U.D., Sangiorgi, D., Vignudelli, V.: On applicative similarity, sequentiality, and full abstraction. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings. Lecture Notes in Computer Science, vol. 9360, pp. 65–82. Springer (2015). 10.1007/978-3-319-23506-6_7, https://doi.org/10.1007/978-3-319-23506-6_7
  * [10] Dahlqvist, F., Neves, R.: An internal language for categories enriched over generalised metric spaces. In: Manea, F., Simpson, A. (eds.) 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference). LIPIcs, vol. 216, pp. 16:1–16:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022). 10.4230/LIPIcs.CSL.2022.16, https://doi.org/10.4230/LIPIcs.CSL.2022.16
  * [11] Dal Lago, U., Honsell, F., Lenisa, M., Pistone, P.: On Quantitative Algebraic Higher-Order Theories. In: Felty, A.P. (ed.) 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 228, pp. 4:1–4:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2022). 10.4230/LIPIcs.FSCD.2022.4, https://drops.dagstuhl.de/opus/volltexte/2022/16285
  * [12] Ehrhard, T., Pagani, M., Tasson, C.: Full abstraction for probabilistic pcf. J. ACM 65(4) (apr 2018). 10.1145/3164540, https://doi.org/10.1145/3164540
  * [13] Gavazzo, F.: Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. p. 452–461. LICS ’18, Association for Computing Machinery, New York, NY, USA (2018). 10.1145/3209108.3209149, https://doi.org/10.1145/3209108.3209149
  * [14] Girard, J.Y.: Geometry of interaction 1: Interpretation of system F. In: Ferro, R., Bonotto, C., Valentini, S., Zanardo, A. (eds.) Logic Colloquium ’88, Studies in Logic and the Foundations of Mathematics, vol. 127, pp. 221–260. Elsevier (1989)
  * [15] Hasegawa, M.: Models of Sharing Graphs: A Categorical Semantics of Let and Letrec. Springer-Verlag, Berlin, Heidelberg (1999)
  * [16] Hasegawa, M.: On traced monoidal closed categories. Mathematical Structures in Computer Science 19(2), 217–244 (2009). 10.1017/S0960129508007184
  * [17] Hyland, J.M.E., Ong, C.H.L.: On Full Abstraction for PCF: I, II, and III. Information and Computation 163(2), 285–408 (2000). https://doi.org/10.1006/inco.2000.2917, https://www.sciencedirect.com/science/article/pii/S0890540100929171
  * [18] Joyal, A., Street, R., Verity, D.: Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society 119(3), 447—468 (1996)
  * [19] Lassen, S.B.: Relational Reasoning about Functions and Nondeterminism. Ph.D. thesis, University of Aarhus, available at https://www.brics.dk/DS/98/2/BRICS-DS-98-2.pdf (1998)
  * [20] Mackie, I., Román, L., Abramsky, S.: An internal language for autonomous categories. Applied Categorical Structures 1, 311–343 (1993)
  * [21] Mardare, R., Panangaden, P., Plotkin, G.: Quantitative algebraic reasoning. In: 2016 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–10 (2016)
  * [22] Milner, R.: Fully abstract models of typed $\lambda$-calculi. Theoretical Computer Science 4(1), 1–22 (1977). https://doi.org/10.1016/0304-3975(77)90053-6, https://www.sciencedirect.com/science/article/pii/0304397577900536
  * [23] Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science. pp. 14–23. IEEE Press (1989)
  * [24] Morris, James Hiram, J.: Lambda-calculus models of programming languages. Ph.D. thesis, Massachusetts Institute of Technology, available at https://dspace.mit.edu/handle/1721.1/64850 (1969)
  * [25] Reed, J., Pierce, B.C.: Distance makes the types grow stronger: A calculus for differential privacy. SIGPLAN Not. 45(9), 157–168 (sep 2010). 10.1145/1932681.1863568, https://doi.org/10.1145/1932681.1863568
  * [26] Selinger, P.: A survey of graphical languages for monoidal categories. In: Coecke, B. (ed.) New Structures for Physics, Lecture Notes in Physics, vol. 813, pp. 289–355. Springer-Verlag Berlin Heidelberg (2011)