# Modelling Coefficients in the Relational Semantics of Linear Logic

Flavien Breuvart, Michele Pagani

► To cite this version:

Flavien Breuvart, Michele Pagani. Modelling Coefficients in the Relational Semantics of Linear Logic. 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), EACSL, Sep 2015, Berlin, Germany. 10.4230/LIPIcs.CSL.2015.567 . hal-04670088

HAL Id: hal-04670088

https://hal.science/hal-04670088v1

Submitted on 11 Aug 2024

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Modelling Coeffects in the Relational Semantics of Linear Logic*

Flavien Breuvart and Michele Pagani

Laboratoire PPS – Université Paris Diderot – Paris 7, France

`{breuvart, pagani}@pps.univ-paris-diderot.fr`

## Abstract

Various typing system have been recently introduced giving a parametric version of the exponential modality of linear logic, e.g. [6, 2]. The parameters are taken from a semi-ring, and allow to express *coeffects* – i.e. specific requirements of a program with respect to the environment (availability of a resource, some prerequisite of the input, etc.).

We show that all these systems can be interpreted in the relational category (*Rel*) of sets and relations. This is possible because of the notion of multiplicity semi-ring, introduced in [3] and allowing a great variety of exponential comonads in *Rel*. The interpretation of a particular typing system corresponds then to give a suitable notion of *stratification* of the exponential comonad associated with the semi-ring parametrising the exponential modality.

**1998 ACM Subject Classification** F.3.2 [Semantics of Programming Languages] Denotational semantics, F.4.1 [Mathematical Logic] Lambda calculus and related systems

**Keywords and phrases** relational semantics, bounded linear logic, lambda calculus

**Digital Object Identifier** 10.4230/LIPIcs.CSL.2015.567

## 1 Introduction

Various systems have been recently proposed based on a notion of parametrised exponential comonad [2, 6] in linear logic. The idea is to parametrise the of-course modality ! with elements taken from a semi-ring $S$. The multiplicative monoid of $S$ describes how the parameters interact under the comonad structure of ! (i.e. dereliction and digging) while the additive monoid of $S$ gives the interaction under the monoidal structure of ! (i.e. weakening and contraction). The axioms of the semi-ring allow then to define a parametrised version of the usual rules of cut-elimination, preserving the confluence property (see Figure 2).

This approach is related with Girard, Scedrov and Scott's *bounded linear logic* (BLL) [8], and thus we refer to it as $B_S$LL. It is in some sense both a generalisation and a restriction of BLL. It is a generalisation because it allows one to choose any semi-ring $S$, as a parameter grammar, while BLL is given with respect to a fixed notion of parameters. On the other hand, $B_S$LL is a significant restriction because its parameters are just elements of the semi-ring $S$ while BLL deals with first-order terms extending polynomials and allowing dependences.

The interest of $B_S$LL is to offer a logical ground to the design of type systems allowing to express various co-effects, that is requirements of a program with respect to the environment. For example, in [6] a semi-ring based on contractive affine transformations has been used to design a type system with annotations on the scheduling of processes; in [2], the semi-ring of non-negative real numbers is used to express the expected value of the number of times a probabilistic program calls its input during the evaluation. We briefly recall these examples

<figure><img src="image_2.png" /></figure>

<footnote>* Partially founded by French ANR project Coquas (number ANR 12 JS02 006 01).</footnote>
in Section 2.1. The interesting point is that although these type systems model quite different co-effects, their soundness is rooted in the same logical framework, that is $B_{\mathcal{S}}LL$.<fnref n="1" />

In this paper, we present various denotational models for $B_{\mathcal{S}}LL$. In the literature, there is a categorical axiomatisation of what is a model of $B_{\mathcal{S}}LL$ known by the name of *bounded exponential situation* (recalled here in Definition 5). This notion has been presented at first in [2], but it originates from Melliès' works on parametrised monads [10].<fnref n="2" /> However there is no known concrete category satisfying the axioms of a bounded exponential situation: the paper [2] gives only a realisability model for few specific examples of semi-ring $\mathcal{S}$.

We give a general recipe for getting a bounded exponential situation out of a model of linear logic (Section 3 and Theorem 7). Intuitively, the main point of our construction is that $B_{\mathcal{S}}LL$ corresponds to a stratification of the exponential comonad along the semi-ring $\mathcal{S}$: any model of linear logic admitting such a stratification (and one model can admit more than one) defines a model also of $B_{\mathcal{S}}LL$. From our point of view, this result, although simple, can be seen as the first step in relating the semantical notion of “approximant” (or “stratus”) of the linear logic exponential, with a notion of co-effect annotation in a type system.

In Section 4, we apply our recipe to the category *Rel* of sets and relations, showing various examples of bounded exponential situation. The category *Rel* provides one of the simplest models of linear logic, where the exponential comonad is given by the finite multiset functor. In fact, we consider a generalisation of this comonad given by the notion of *multiplicity semi-ring* in Carraro et al.'s [3]. A multiplicity semi-ring $\mathcal{R}$ is a semi-ring satisfying some properties (Definition 8) which generalise the notion of multiplicity given by the natural number semi-ring $\mathbb{N}$ in the finite multiset functor. This generalisation has been introduced in [3] for proving the existence of non-sensible models of the untyped $\lambda$-calculus in the category *Rel*. As a by-product, the authors show how many and different can be the exponential comonads living in the category *Rel*. We want to take advantage of this variety for giving relational models of $B_{\mathcal{S}}LL$, for any semi-ring $\mathcal{S}$.

We prove that one can stratify the exponential comonad associated with any multiplicity semi-ring $\mathcal{R}$ (so getting a model of $B_{\mathcal{S}}LL$) just by interpreting the parameter semi-ring $\mathcal{S}$ into the multiplicity semi-ring $\mathcal{R}$ (Theorem 11). Section 4.3 discusses some concrete examples of this construction, giving instances of $\mathcal{S}$ and $\mathcal{R}$.

Finally, Section 5 gives a taste of the fact that these constructions can be applied to different categories than *Rel*. For example, we briefly discuss the case of models based on coherence spaces, giving stratifications of linear categories that are not compact closed.

## 2 Preliminaries

**► Definition 1.** A *semiring* is given by $(S, \cdot, 1, +, 0)$ where $S$ is a set, the sum $+$ is an associative commutative binary operation with a neutral element $0 \in S$ and the product $\cdot$ is an associative binary operation distributing over $+$ (so $0$ is absorbing for $\cdot$) and with a neutral element $1 \in S$.

An *ordered semiring* $(S, \cdot, 1, +, 0, \le)$ is a semiring $(S, \cdot, 1, +, 0)$ with a partial order $\le$ such that sum and product are increasing monotone.

Notice that because of the monotonicity of the multiplication, $0 \le 1$ (resp. $1 \le 0$) implies

<footnote n="1">¹ Let us mention also [12, 13], giving several other examples of applications. These systems are not always described in the syntactical definition of $B_{\mathcal{S}}LL$, but they can be modeled in our concrete semantics.</footnote>

<footnote n="2">² See also Melliès' presentation "Sharing and Duplication in Tensorial Logic" at the workshop *Developments in Implicit Computational complExity* 2013.</footnote>
<figure><img src="image_3.png" /><figcaption>Figure 1 The sequent calculus of $B_S$LL. In a sequent $\Gamma \vdash A$, $\Gamma$ is supposed to be a multiset of formulas (no implicit contraction rule is admitted).</figcaption></figure>

that 0 is the bottom (resp. top) element of $\mathcal{S}$. However we will often consider examples of ordered semi-rings where the two neutral elements are incomparable. In [2] the authors impose 0 to be the bottom element, but this condition is not necessary.

**Definition 2.** Given a set $X$ and a semi-ring $\mathcal{S}$, we denote by $S_f\langle X\rangle$ the set of functions $\mu: X \mapsto \mathcal{S}$ with finite support (where $\text{supp}(\mu) = \{g \in X \mid \mu(g) \neq 0\}_{\mathcal{S}}$). We denote by $[]$ the constant function with value $0_{\mathcal{S}}$ and, for any $g \in X$, by $[g]$ the function with value $1_{\mathcal{S}}$ on $g$ and $0_{\mathcal{S}}$ everywhere else.

**Remark.** Any order on $\mathcal{S}$ implies an order on $S_f\langle X\rangle$: $\mu \leq \nu$ iff $\forall g \in \text{supp}(\mu), \mu(g) \leq_S \nu(g)$.

**Proposition 1.** If $\mathcal{X}$ is a monoid then the set $S_f\langle \mathcal{X} \rangle$ is endowed with a structure of semi-ring, defined by:

$$ 
\begin{align*}
0_{S_f\langle \mathcal{X} \rangle} &:= [], & (\mu +_{S_f\langle \mathcal{M} \rangle} \nu)(g) &:= \mu(g) +_{S} \nu(g), \\
1_{S_f\langle \mathcal{X} \rangle} &:= [1_{\mathcal{X}}], & (\mu \cdot_{S_f\langle \mathcal{X} \rangle} \nu)(g) &:= \sum_{\substack{g', g'' \in \mathcal{X} \\ g' \cdot \nu g'' = g}} \mu(g') \cdot_S \nu(g''),
\end{align*}
$$

Notice that the sum appearing in the definition of $\mu \cdot_{S_f\langle \mathcal{X} \rangle} \nu$ is well-defined because the supports of $\mu$ and $\nu$ are finite.

**Definition 3.** Given an ordered semiring $\mathcal{S}$, we call $B_S$LL the logic given by:

- the formulas are defined by the grammar, with $J \in \mathcal{S}$:
  $A, B, C := \alpha \mid A \otimes B \mid A \to B \mid A^J,$

- the sequent calculus is given in Figure 1,

- the cut-elimination procedure is defined by the usual rules of multiplicative linear logic plus the rules of Figure 2.

One can add the additive connectives without any effort, we prefer however to omit their account because they do not play any crucial role with respect to our results. In [2], the authors use a term calculus instead of a logical sequent system: the two presentations can be made in relation via a Curry-Howard correspondence.

## 2.1 Examples

**Trivial semi-ring:** the multiplicative exponential fragment of intuitionistic linear logic is recovered from $B_S$LL by taking $\mathcal{S}$ as the one element semi-ring.
<figure><img src="image_4.png" /><figcaption>■ **Figure 2** Cut-elimination rules (for the exponentials only). Given a sequent $\Delta = A_1^{I_1}, \dots, A_n^{I_n}$ and a parameter $J$, we denote by $\Delta^J$, the sequent $A_1^{J \cdot I_1}, \dots, A_n^{J \cdot I_n}$. Notice in particular that $\Delta^0 = A_1^0, \dots, A_n^0$, and $\Delta^1 = \Delta$.</figcaption></figure>
**Boolean semi-ring:** the Boolean semi-ring $\mathbb{B} = (\{t, ff\}, \wedge, t, \vee, ff)$ allows finer types than the trivial one, distinguishing between data that can be weakened (of type $A^{ff}$) from data that can be duplicated ($A^t$). The order over $\mathbb{B}$ plays a role, also: the discrete order will make the two types disjoint, while $t \ge ff$ will make $A^{ff}$ a subtype of $A^t$, so that the $(\cdot)^t$ modality behaves as the usual of-course modality ! of linear logic.

**Natural numbers:** the natural number semi-ring $(\mathbb{N}, \times, 1, +, 0)$ yields modalities expressing the number of times a resource is to be used. The order relation then allows some flexibility: for example, the natural order $0 < 1 < 2 < \dots$ makes $A^n$ to be the type of data that can be used up-to $n$ times. Notice that in this case there is no modality allowing a resource to be used an indefinite number of times, so the system is not an extension of linear logic. In order to recover the usual of-course modality ! one should take the order completion $\tilde{\mathbb{N}}$, adding a top-element $\omega$.

**Polynomial semi-ring:** by taking the semi-ring $(\mathbb{N}[X_i]_{i \in \mathbb{N}}, \times, 1, +, 0)$ of polynomials with natural numbers as coefficients (the choose order here is irrelevant for the discussion), one can express a basic form of resource dependency. One can write formulas like $A^{p(\vec{x})} \sim B^{q(\vec{x})}$ where $p, q$ are polynomials in the unknowns $\vec{x}$. Roughly speaking, this is the type of a function giving a result reusable $q(\vec{n})$ number of times as soon as its input can be used $p(\vec{n})$ number of times, for any sequence of natural numbers $\vec{n}$. This system has been discussed in [8] as an introduction to bounded linear logic (BLL). What is lacking with respect to the whole BLL is the possibility to bound first-order variables, so writing types of the form $A^{y \le p(x)}$, where $y$ is an unknown of a polynomial occurring inside $A$.

**Affine contractive transformations:** the one-dimensional contractive affine transformations $x \mapsto sx + p$ can be represented by real-valued matrices $x_{s,p} = \begin{pmatrix} s & p \\ 0 & 1 \end{pmatrix}$ with $0 \le s \le 1$ and $-1 \le s + p \le 1$. The value $s$ is a scaling factor relative to the unit interval, and $p$ is a delay from the time origin. The set of such transformations forms a monoid $Aff_1^c$ with composition given by matrix product.<fnref n="3" /> By Proposition 1, $\mathbb{N}_f \langle Aff_1^c \rangle$ is a semi-ring so it defines the logic $B_{\mathbb{N}_f(Aff_1^c)}$ LL. This system has been introduced by Ghica and Smith [6] in order to express at the level of types a scheduling on the execution of certain resources. For example, a formula $A[(\begin{smallmatrix} .5 & 0 \\ 0 & 1 \end{smallmatrix}) \cdot (\begin{smallmatrix} .5 & .25 \\ 0 & 1 \end{smallmatrix})]$ represents a resource of type $A$ that can be called twice, both calls will last $\frac{1}{2}$ the duration relative to which we are measuring, but one call starts at the beginning of the available time interval, while the other call starts when $\frac{1}{4}$ of the time has elapsed. Of course, such annotations have a meaning when the language has primitives describing processes to be scheduled. See [6] for more details.

**Positive real numbers:** in presence of random primitives, one can associate any resource with a discrete random variable quantifying on the number of times this resource is used during the evaluation. In [2], $B_{\text{SLL}}$ has been parametrised with the ordered semi-ring $\mathbb{R}^+ = (\mathbb{R}^+, \times, 1, +, 0, \le)$ of the non-negative real numbers endowed with the natural order, the parameters expressing the expected values of these random variables.

This system can be extended (syntactically) with true dependent types and be able to catch finer properties, like differential privacy [5].

<footnote n="3">³ Notice, however, that the semring product $I \cdot J$ denotes the reverse matrice product $J \cdot I$, this is due to a change in notation between us and [6].</footnote>
### 3 Stratifying Linear Logic Exponentials

We recall the notion of *linear category*, which has been introduced in [1] as a categorical axiomatization of a model of intuitionistic linear logic. This definition has been recently revisited in [2] with the notion of *bounded exponential situation*, which roughly corresponds to a variant of linear category where the exponentials are parametrised by the elements of a partially ordered semi-ring $\mathcal{S}$ and which gives a categorical model of $B_{\mathcal{S}}LL$. Our contribution is the definition of *stratification* (Definition 6), giving a general recipe for extracting a bounded exponential situation from a linear category (Theorem 7). Section 4 will apply this recipe to the concrete case of the relational category.

**Definition 4 ([1]).** A *linear category* consists of:

- a symmetric monoidal closed category $(\mathcal{L}, \otimes, 1, -^\circ)$,

- a comonad $(!, \mathbf{d} : !A \to A, \mathbf{p} : !A \to !!A)$ endowed with three natural transformations and a morphism: $w_A : !A \to 1, c_A : !A \to !A \otimes !A, m_1 : 1 \to !1, m_{A,B} : !A \otimes !B \to !(A \otimes B)$, satisfying a bunch of equations (see, for example, [1]).

A linear category $\mathcal{L}$ gives a model of $B_{\mathcal{S}}LL$ with $\mathcal{S}$ the trivial semi-ring (i.e. the usual intuitionistic MELL). In this case we have just one exponential modality, which is interpreted by the functor $!$ of $\mathcal{L}$ and its associated structure. When $\mathcal{S}$ is non-trivial, one has to parametrise the exponential modality $!$ by the elements of $\mathcal{S}$ and to add some equations making to interact these various modalities following the laws of the semi-ring $\mathcal{S}$. Such a structure has been suggested by Melliès and formally introduced in [2]:

**Definition 5 ([2]).** A *bounded exponential situation* consists of:

- a symmetric monoidal closed category $(\mathcal{L}, \otimes, 1, -^\circ)$, used to interpret the multiplicative fragment of $B_{\mathcal{S}}LL$;

- a categorical axiomatization of the notion of partially ordered semi-ring, that is a bimonoidal category $(\mathcal{S}, +, 0, \cdot, 1)$. The objects $I, J, H, \dots$ of $\mathcal{S}$ correspond to the elements of the semi-ring and the hom-sets define the order of the semiring: $I \leq J$ iff $\mathcal{S}(I, J)$ is non-empty$^4$.

- an exponential action $(\_\cdot\_)^{-}$ of $\mathcal{S}$ on $\mathcal{L}$, giving a parametric version of the exponential comonad and used to interpret the formulas $A^I$. Formally, it is a bifunctor $(\_\cdot\_)^{-} : \mathcal{S} \times \mathcal{L} \to \mathcal{L}$ together with six natural transformations: $\mathbf{p}'_{I,J,A} : A^{I \cdot J} \to (A^J)^I, \mathbf{d}'_A : A^1 \to A, \mathbf{w}'_A : A^0 \to 1, \mathbf{c}'_{I,J,A} : A^{I+J} \to A^I \otimes A^J, \mathbf{m}'_{I,1} : 1 \to 1^I, \mathbf{m}'_{I,A,B} : A^I \otimes B^I \to (A \otimes B)^I$, which should satisfy various diagrams, see [2] for details.

**Definition 6.** A stratification of a linear category $\mathcal{L}$ is a triplet $(\mathcal{S}, (\_\cdot\_)^{-}, \varrho)$, where:

- $\mathcal{S}$ is an ordered semi-ring (seen as a bimonoidal category);

- $(\_\cdot\_)^{-}$ is a bifunctor $\mathcal{S} \times \mathcal{L} \to \mathcal{L}$;

- $\varrho$ is a natural transformation from $!$ to $(\_\cdot\_)^{-}$, i.e. $\varrho_{I,A} : !A \mapsto A^I$ such that:

- each of the morphism $\varrho_{I,A} : !A \mapsto A^I$ is an epimorphism, i.e., for any $\phi, \psi : A^I \to B$, if $\varrho_{I,A}; \phi = \varrho_{I,A}; \psi$ then $\phi = \psi$,

- the diagrams of Figure 3 can be completed (in a unique way due to the epi property) by families of morphisms $\mathbf{d}'_A, \mathbf{p}'_{A,I,J}, \mathbf{w}'_A, \mathbf{c}'_{A,I,J}$ and $\mathbf{m}'_{A,B,I,J}$, for any $A, B, I, J$.

<footnote n="4">⁴ For our purposes, we can suppose that $\mathcal{S}$ has hom-sets of at most one element.</footnote>
<figure><img src="image_5.png" /><figcaption>Figure 3 Coherence diagrams between the natural transformation $\mathcal{E}$, the exponential structure ($!$, $d$, $p$, $w$, $c$, $m$) of a linear category and the exponential structure (($\mathbf{\cdot}$)$^-$, $d'$, $p'$, $w'$, $c'$, $m'$) of a bounded exponential situation.</figcaption></figure>

Notice that all the diagrams of Figure 3 simply state that each natural transformation $e$ required for the linearity of $\mathcal{L}$ is transported along $\mathcal{E}$ to its parametrized version $e'$. Notice also that the diagram $\mathcal{E}m_1$ of Figure 3 is always obtained for $m'_I := m_1; \mathcal{E}_{1,I}$.

Finally, the naturality of the families $d'_A$, $p'_A$, $w'_A$, $c'_A$, and $m'_A$ can be automatically retrieved from the diagrams of Figure 3 and the universal property of epimorphisms.

**Theorem 7.** A stratification $(S, (\mathbf{\cdot})^-, \mathcal{E})$ of a linear category yields a bounded exponential situation hence a model of $B_S$LL.

**Proof.** The transformations defining a bounded exponential situation are given by the families $d'_A$, $p'_A$, $w'_A$, $c'_A$, and $m'_A$. In fact, the naturality and coherence diagrams associated with these transformations are obtained by invoking the corresponding diagram from the linear category, by transporting the whole diagram through $\mathcal{E}$ (via pre/post composing and the diagrams of Figure 3), and finally by using the universal property of epimorphisms.

For example, Figure 4 gives the commutation that the morphism $p'_{A,I,J}$ should enjoy in order to give a positive action. The triangle **I** is naturality of $\mathcal{E}$ over the associativity of the semiring multiplication, the square **IV** is the usual one of a linear category, **V** uses the promotion of the square on the first line of Figure 3, **VI** and **VII** are the naturality of, resp., $\mathcal{E}$ and $p$, and finally **II**, **III** and **VIII** are again squares of Figure 3. Notice that this is a priori not sufficient to obtain the commutation of the external cell due to the first $\mathcal{E}$ that point on the wrong direction. However, we actually obtain that $\mathcal{E}; A^{\text{as}}; p'; p'^H = \mathcal{E}; p'; p'$ which results in the commutation of the external cell by the universal property of the tri $\mathcal{E}$.

<figure><img src="image_6.png" /></figure>

# 4 Relational Based Models

## 4.1 The linear category $Rel^\mathcal{R}$

The category *Rel* has sets as objects and relations as morphisms, i.e. *Rel*(X, Y) := P(X × Y). Composition and identities are given by:

$$f; g := \{(x, y) \mid \exists z, (x, z) \in f, (z, y) \in g\},$$

$$\mathrm{id}_X := \{(x, x) \mid x \in X\}.$$
<figure><img src="image_7.png" /><figcaption>Figure 4 An example of the proof of the commutation of the diagrams needed to have a bounded exponential situation.</figcaption></figure>

Rel is symmetric monoidal closed (in fact, compact closed) with tensor product given by:

$$X \otimes Y := X \times Y, \qquad f \otimes g := \{( (x, x'), (y, y') ) \mid (x, y) \in f, (x', y') \in g \}.$$

Associativity $(\alpha_{X,Y,Z}^{\otimes} := \{((x,(y,z)),((x,y),z)) \mid x \in X, y \in Y, z \in Z\} \in \mathbf{Rel}(X \otimes (Y \otimes Z), (X \otimes Y) \otimes Z))$ and commutativity $(\beta_{X,Y}^{\otimes} := \{((x,y),(y,x)) \mid x \in X, y \in Y\} \in \mathbf{Rel}(X \otimes Y, Y \otimes X))$ are natural bijections; the neutral object is the singleton $1 := \{\ast\}$. The internal hom functor is defined by: $X \to Y := X \otimes Y$ and $f \to g := f \otimes g$, the evaluation morphism is $\mathrm{eval} := \{((x,y),x),y) \mid x \in X, y \in Y\} \in \mathbf{Rel}((X \to Y) \otimes X, Y)$.

It is well-known that Rel models the linear logic exponential with the multi-set comonad. It is less known, however, that this is just an example of how one can express the exponential modality. Carraro et al. [3] have shown many other possibilities by introducing the notion of resource semi-ring (here Definition 8 and Theorem 9). We briefly recall this result, adding some examples.<fnref n="5" />

**► Definition 8 ([3]).** A multiplicity semi-ring is a semi-ring $\mathcal{R} = (|\mathcal{R}|, \cdot, 1, +, 0)$ such that $(p, q, r)$ will vary over $\mathcal{R}$:

(MS1) $\mathcal{R}$ is positive: $p+q = 0$ implies $p = q = 0$;

(MS2) $\mathcal{R}$ is discrete: $p+q = 1$ implies $p = 0$ or $q = 0$;

(MS3) $\mathcal{R}$ is additively splitting: $p_1 + p_2 = q_1 + q_2$ implies $\exists r_{1,1}, r_{1,2}, r_{2,1}, r_{2,2}$, such that

$$p_i = r_{i,1} + r_{i,2}, \qquad q_i = r_{1,i} + r_{2,i};$$

(MS4') $\mathcal{R}$ is multiplicatively splitting: $q_1+q_2 = p \cdot r$ implies there is $l \in \mathbb{N}$ such that for all $j \le l$, we can find $r_j, p_{1,j}, p_{2,j}$ such that

$$r = r_1 + \cdots + r_l,$$

$$p = p_{1,j} + p_{2,j}$$

for all $j \le l$,

$$q_i = p_{i,1} \cdot r_1 + \cdots + p_{i,l} \cdot r_k.$$

<footnote n="5">⁵ Notice once again that we have to reverse the semiring multiplication of [3] due to a change in notations.</footnote>
The notion of multiplicity semi-ring given by Definition 8 is a slight generalization of the one in [3], because the multiplicative splitting has been slightly relaxed. It is straightforward to check that all proofs in [3] still hold.

The semi-ring of natural numbers $\mathbb{N}$ is the prototypical example of multiplicity semi-ring, while the Boolean semi-ring (as well as any cyclic semi-ring) is a non-example because the discreteness condition fails. Other non-trivial examples can be obtained via the following propositions.

**Proposition 2.** For any multiplicity semi-ring $\mathcal{R}$, the extension with an idempotent (for $+$ and $\cdot$) element $\omega$ that is absorbing for the addition and the multiplication (except with 0) results in a semiring $\bar{\mathcal{R}} = \mathcal{R} \cup \{\omega\}$ that is a multiplicity semi-ring.

For example, the semi-ring $\bar{\mathbb{N}} = \mathbb{N} \cup \{\omega\}$ is a multiplicity semi-ring. The idea is that it allows an infinite number of resources (and by infinite we do not mean unbounded, but really infinite, obtained by taking a greatest fixpoint for example).

**Proposition 3.** Given a monoid $\mathbb{M}$, the semi-rings $\mathbb{N}_f\langle\mathbb{M}\rangle$ and $\bar{\mathbb{N}}_f\langle\mathbb{M}\rangle$ are multiplicity semi-rings.

For example, the semi-ring $\mathbb{N}_f\langle\mathrm{Aff}_1^c\rangle$ induced by the monoid $\mathrm{Aff}_1^c$ of one-dimensional affine contractive transformations [6] is an example of multiplicity semi-ring, different from $\mathbb{N}$.

**Theorem 9 (Rel<sup>\mathcal{R}</sup>, [3]).** Any multiplicity semi-ring $\mathcal{R}$ defines an exponential comonad over Rel (for $r \in \mathrm{Rel}(A, B)$):

$$ !_{\mathcal{R}} A := \mathcal{R}_f\langle A\rangle, $$

$$ !_{\mathcal{R}} r := \{(u, v) \in \mathrm{Rel}(!_{\mathcal{R}} A, !_{\mathcal{R}} B) \mid \exists \sigma \in \mathcal{R}_f\langle r\rangle, u(a) = \sum_{b \in B} \sigma(a, b), $$

$$ v(b) = \sum_{a \in A} \sigma(a, b) \} $$

Dereliction $\mathfrak{d}_A := \{(\delta_a, a) \mid a \in A\} : !_{\mathcal{R}} A \to A$, where $\delta_a(a) = 1$ and $\delta_a(a') = 0$ for every $a \neq a'$, digging $\mathfrak{p}_A := \{(m, M) \mid \forall a \in A, m(a) = \sum_{n \in !_{\mathcal{R}} A} n(a) \cdot M(n)\} : !_{\mathcal{R}} A \to !_{\mathcal{R}} !_{\mathcal{R}} A$, contraction $\mathfrak{c}_A := \{(u, (v_1, v_2)) \mid \forall a \in A, u(a) = v_1(a) + v_2(a)\} : !_{\mathcal{R}} A \to !_{\mathcal{R}} A \otimes !_{\mathcal{R}} A$, weakening $\mathfrak{w}_A := \{(0, *)\} : !_{\mathcal{R}} A \to 1$, where 0 denotes the constant zero function in $\mathcal{R}_f\langle A\rangle$, and the morphisms $\mathfrak{m}_1 = \{(*, u) \mid u \in !_{\mathcal{R}} 1\} : 1 \to !_{\mathcal{R}} 1$ and $\mathfrak{m}_{A, B} := \{((u_1, u_2), v) \mid u_1(a) = \sum_b v(b, a, b), u_2(b) = \sum_a v(a, b, b)\} : (!_{\mathcal{R}} A \otimes !_{\mathcal{R}} B) \to !_{\mathcal{R}} (A \otimes B)$ are natural and respect usual diagrams.

We denote by $\mathrm{Rel}^{\mathcal{R}}$ the linear category induced by this exponential comonad.

A construction due to Grellois and Melliès [9] can be used to extend these results in any semi-ring $\mathcal{R}$ of the form $\mathcal{R}'_f\langle\mathbb{M}\rangle$ (where $\mathcal{R}'$ is a multiplicity semi-ring and $\mathbb{M}$ a monoid). This uses the fact that $\mathcal{R}'_f\langle\mathbb{M}\rangle$ is a composition of the exponential comonad $!_{\mathcal{R}}$ and a writer comonad $(\mathbb{M}, \cdot, \otimes)$ that distributes over the former.

## 4.2 Stratifications over Rel<sup>\mathcal{R}</sup>

We show how to associate with an ordered semi-ring $\mathcal{S}$ a stratification of the linear category Rel<sup>\mathcal{R}</sup>, for any multiplicity semi-ring $\mathcal{R}$. The key-point is that such stratifications can be presented as a kind of interpretation of the ordered semi-ring $\mathcal{S}$ into the hom-set Rel<sup>\mathcal{R}</sup>(!_R 1, 1), which is isomorphic to the power-set $\mathcal{P}(\mathcal{R})$. Definition 10 gives the conditions that such interpretation should enjoy in order to induce a stratification over Rel<sup>\mathcal{R}</sup> (Theorem 11).
Given a semi-ring $\mathcal{R}$, one can define the following operations over $\mathcal{P}(\mathcal{R})$ $(\alpha, \beta, \gamma)$ vary over $\mathcal{P}(\mathcal{R}))$:

$$ \alpha \oplus \beta := \{p+q \mid p \in \alpha, q \in \beta\}, $$

$$ \alpha \odot \beta := \left\{ \sum_{i=1}^{h} p_i \cdot q_i \mid h \ge 0, \sum_{i=1}^{h} q_i \in \beta, \forall i \le h, p_i \in \alpha \right\}. $$

The operation $\oplus$ (resp. $\odot$) will be used to stratify contraction (resp. digging). Notice that the two operations are associative, $\oplus$ is commutative but not $\odot$, $\{0_{\mathcal{R}}\}$ (resp. $\{1_{\mathcal{R}}\}$) is the neutral element of $\oplus$ (resp. $\odot$). Moreover, $\odot$ left-distributes over $\oplus$ (i.e. $\gamma \odot (\alpha \oplus \beta) = (\gamma \odot \alpha) \oplus (\gamma \odot \beta)$), but it does not right-distribute. For example, take $\mathcal{R}$ to be the standard semi-ring over natural numbers, then:

$$ (\{1\} \oplus \{1\}) \odot \{1, 2\} = \{2, 4\}, \quad (\{1\} \odot \{1, 2\}) \oplus (\{1\} \odot \{1, 2\}) = \{2, 3, 4\}. $$

**Definition 10.** An interpretation of an ordered semi-ring $\mathcal{S}$ into a multiplicity semi-ring $\mathcal{R}$ is a function $\llbracket - \rrbracket : \mathcal{S} \mapsto \mathcal{P}(\mathcal{R})$ such that (for all $I, J \in \mathcal{S}$):

$$ I \le_S J \text{ implies } \llbracket I \rrbracket \subseteq \llbracket J \rrbracket, \quad \llbracket I \rrbracket \oplus \llbracket J \rrbracket \subseteq \llbracket I +_S J \rrbracket, \quad \llbracket I \rrbracket \odot \llbracket J \rrbracket \subseteq \llbracket I \cdot_S J \rrbracket, \\ \qquad \{0_{\mathcal{R}}\} \subseteq \llbracket 0_S \rrbracket, \quad \{1_{\mathcal{R}}\} \subseteq \llbracket 1_S \rrbracket. $$

Indeed, Definition 10 simply expresses the bimonoidal functoriality of $\llbracket - \rrbracket$, where $\mathcal{S}$ and $\mathcal{P}(\mathcal{R})$ are both considered as bimonoidal categories$^6$.

**Theorem 11.** Any interpretation $\llbracket - \rrbracket$ of an ordered semi-ring $\mathcal{S}$ into a multiplicity semi-ring $\mathcal{R}$ induces a stratification of the linear category $\mathbf{Rel}^{\mathcal{R}}$, defined by:

$$ A^I := \{ u \in !_{\mathcal{R}} A \mid \sum_{x \in A} u(x) \in \llbracket I \rrbracket \}, \quad f^{I \ge J} := \{(u, v) \in !_{\mathcal{R}} f \mid u \in A^I, v \in B^J\}, $$

$$ \vartheta_{I,A} := \{(u, u) \mid u \in A^I\}. $$

In particular, $\llbracket - \rrbracket$ extends to a sound interpretation of $B_S LL$ into $\mathbf{Rel}^{\mathcal{R}}$.

**Proof.** Notice that $\vartheta$ is an epi (in fact it is a «surjective» relation) and is natural. Moreover, the morphisms $d', p'$, etc... of Definition 6 are obtained by restraining the corresponding $\mathbf{Rel}$ morphisms to the domain/codomain, e.g.:

$$ c'_{A,I,J} := c_A \cap (A^{I+J} \times (A^I \otimes B^J)). $$

One should also prove that these transformations enjoy the diagrams of Figure 3. For example, we should prove that: $c_A; (\vartheta_{I,A} \otimes \vartheta_{J,A}) = \vartheta_{I+J,A}; c'_{I,J,A}$ (Diagram $\vartheta c$ of Figure 3). Indeed,

$$ c_A; (\vartheta_{I,A} \otimes \vartheta_{J,A}) = \{(u+v, (u,v)) \mid \sum_x u(x) \in \llbracket I \rrbracket, \sum_x v(x) \in \llbracket J \rrbracket\} $$

$$ \vartheta_{I+J,A}; c'_{I,J,A} = \{(u+v, (u,v)) \mid \sum_x (u(x)+v(x)) \in \llbracket I+J \rrbracket, \\ \qquad \sum_x u(x) \in \llbracket I \rrbracket, \sum_x v(x) \in \llbracket J \rrbracket\} $$

The two sets are the same because the conditions on $u$ and $v$ imply that on $u+v$, since $\llbracket I \rrbracket \oplus \llbracket J \rrbracket \subseteq \llbracket I+J \rrbracket$. $\quad$

<footnote>$^6$ Actually, $\mathcal{P}(\mathcal{R})$ is a bit less than bimonoidal because just left-distributive.</footnote>
## 4.3 Examples

Let us apply Theorem 11 to the ordered semi-rings discussed in Section 2.1.

There is only one possible interpretation of the trivial semi-ring into the multiplicity semi-ring $\mathbb{N}$, associating the unique element $*$ with the whole set $\mathbb{N}$. In fact, Definition 10 requires that $[[*]]$ contains 0, 1 and that it is closed under addition. This interpretation gives the usual multi-set based model of linear logic. By enlarging the multiplicity semi-ring, for example considering $\overline{\mathbb{N}}$, one can set $[[*]] = \overline{\mathbb{N}}$ and getting the model of linear logic giving rise to the non-sensible models of the untyped $\lambda$-calculus studied in [3].

The interpretation of a Boolean-based ordered semi-ring into $\mathbb{N}$ depends on the order between $t$ and $ff$. In the case $ff \leq t$, we can set either $[[t]] = \mathbb{N}$ and $[[ff]] = \{0\}$, or $[[t]] = \mathbb{N} = [[ff]]$.<fnref n="7" /> The latter collapses the two modalities to the usual multiset comonad, while the former interprets the formula $A^{ff}$ by the singleton of the empty multiset, representing the type of unused resources. In the case $ff$ and $t$ are incomparable in $\mathcal{S}$, then we can set $[[t]] = \mathbb{N} - \{0\}$ and $[[ff]] = \{0\}$, strictly distinguishing between used resources of type $A^t$ and unused resources of type $A^{ff}$.

In the case the syntactic semi-ring $\mathcal{S}$ is already a multiplicity semi-ring (like $\mathbb{N}$, $\mathbb{N}[X_i]_{i \in \mathbb{N}}$ and $\mathbb{N}_f(\text{Aff}_1^c)$), then we have a natural interpretation of $\mathcal{S}$ into itself, associating a scalar with the downward closure of its singleton. In fact, we have:

**Proposition 4.** For any ordered multiplicity semi-ring $(\mathcal{R}, \leq_{\mathcal{R}})$, the following is an interpretation of $\mathcal{R}$ into $\mathcal{R}$:

$$ [[I]] = \{J \mid J \leq_{\mathcal{R}} I\}. \qquad (1) $$

*Proof.* The only condition of Definition 10 which is not so immediate to check is the one dealing with $\odot$. Any element of $[[I]] \odot [[J]]$ is of the form $\sum_i I_i \cdot J_i$ such that $\sum_i J_i \leq_{\mathcal{R}} J$ and for all $i$, $I_i \leq_{\mathcal{R}} I$. Thus we have:

$$ \sum_i I_i \cdot J_i \leq_{\mathcal{R}} \sum_i I_i \cdot J_i = I \cdot (\sum_i J_i) \leq_{\mathcal{R}} I \cdot J $$

so that $\sum_i I_i \cdot J_i \in [[I \cdot J]]$. ◀

<figure><img src="image_8.png" /></figure>

For example, if $\mathcal{R}$ is $\mathbb{N}$, the interpretation of $A^n$ induced by Equation (1) is the set of the multisets with cardinally at most $n$, if we consider the standard order, or with cardinally exactly $n$, if we consider the discrete order. In the case of the polynomial semi-ring $(\mathbb{N}[X_i]_{i \in \mathbb{N}}, \times, 1, +, 0)$, Equation (1) associates with $A^{p(x)}$ the set of functions mapping an element $a \in A$ to a polynomial $q(x)$ bounded by $p(x)$ (according to the notion of boundedness described by the order considered).

The interpretation given by Equation (1) faithfully mirrors in the semantics the behavior of the typing system and hence it is uninteresting, at least in our setting. More relevant models can be obtained by shrinking the semantic semi-ring, via the following proposition.

**Proposition 5.** Given an ordered semi-ring $\mathcal{S}$, an interpretation $[[\cdot]]_{\mathcal{R}}$ of $\mathcal{S}$ into a multiplicity semi-ring $\mathcal{R}$ and a multiplicity sub-semi-ring $\mathcal{R}'$ of $\mathcal{R}$, we have that the map $[[\cdot]]_{\mathcal{R}'} : I \mapsto ([[I]] \cap \mathcal{R}')$ defines an interpretation of $\mathcal{S}$ into $\mathcal{R}'$ whenever it respects the order, i.e.:

$$ I \leq_{\mathcal{S}} J \text{ iff } [[I]]_{\mathcal{R}'} \subseteq [[J]]_{\mathcal{R}'} $$

<footnote n="7">⁷ There are other uninteresting possibilities.</footnote>
For example, $\bar{\mathbb{N}}$ can be interpreted into itself by Equation 1, or, by using Proposition 5, into its sub-semi-ring $\mathbb{N}$ by setting $[[\omega]] = \mathbb{N} = [[\omega]]_{\bar{\mathbb{N}}} \cap \mathbb{N}$. This latter interpretation has the virtue of expressing both finite and infinite scalars with sets of finite natural numbers.

If $\mathcal{S}$ is not a multiplicity semi-ring, one can interpret it into the “free” multiplicity semi-ring $\mathbb{N}_f\langle\mathcal{S}\rangle$ induced by the multiplicative monoid $\mathcal{S}$ of $\mathcal{S}$ (recall Proposition 3):

**Proposition 6.** For any ordered semi-ring $(\mathcal{S}, \leq_S)$, the following is an interpretation of $\mathcal{S}$ into $\mathbb{N}_f\langle\mathcal{S}\rangle$ (square brackets [...] below denote standard multisets):

$$[[I]] = \{[J_1, \dots, J_n] \mid \sum_{i \leq n} J_i \leq_S I\}. \qquad (2)$$

**Proof.** As in the previous proposition, one has to check (among other equations) that $[[I]] \oplus [[J]] \subseteq [[I + J]]$

$$ \begin{align*} [[I]] \oplus [[J]] &= \{[I_1, \dots, I_n, J_1, \dots, J_m] \mid \sum_{i \leq n} I_i \leq_S I, \sum_{i \leq m} J_i \leq_S J\} \\ &\subseteq \{[J_1, \dots, J_n] \mid \sum_{i \leq n} J_i \leq_S I + J\} \\ &= [[I + J]] \quad \blacksquare \end{align*} $$

This construction makes a sharp difference between the way syntax and semantics express sums between parameters. For example, if you take $\mathcal{S}$ to be $\mathbb{R}^+$ endowed with the usual order, then the interpretation of a type $A^r$, for $r \in \mathbb{R}^+$, induced by Equation (2) can be seen as the set of finite multisets $[(a_1, r_1), \dots, (a_n, r_n)]$ of elements in $A \times \mathbb{R}^+$ such that $r_1 + \dots + r_n \leq r$. The contraction between two types $A^r$ and $A^{r'}$ gives at the level of the syntax the type $A^{r+r'}$ where the two parameters $r, r'$ are totally merged into $r + r'$. While at the level of the semantics we have the set of the disjoint unions of a multiset in $A^r$ and one in $A^{r'}$, so that the real-values $r_1, \dots, r_n$ are kept distinct.

Such an interpretation of $\mathbb{R}^+$ into $\mathbb{N}_f\langle\mathbb{R}^+\rangle$ however is not completely satisfactory because it does not express a clear notion of probability. One can get something better by applying Proposition 5. Consider the semi-ring $\mathbb{N}_f\langle[0, 1]\rangle$ made by the elements of $\mathbb{N}_f\langle\mathbb{R}^+\rangle$ that can be seen as multisets of probabilities. Proposition 3 shows that $\mathbb{N}_f\langle[0, 1]\rangle$ is a multiplicity semi-ring, and one can easily check that the interpretation $\mathbb{R}^+ \mapsto \mathbb{N}_f\langle\mathbb{R}^+\rangle$ is still injective when restricted to $\mathbb{N}_f\langle[0, 1]\rangle$. So Proposition 5 states that $\mathbf{Rel}^{\mathbb{N}_f\langle[0, 1]\rangle}$ is a model of $\mathbb{B}_{\mathbb{R}^+\text{LL}}$ by the interpretation:

$$[[r]] := \{[p_1, \dots, p_n] \mid n \geq 0, p_i \in [0, 1], \sum_{i=1}^{n} p_i \leq r\}.$$

This interpretation is not only refining the previous one but perfectly fit the intuitive semantics. Indeed, a multiset $[r_1, \dots, r_n]$ represents $n$ independent calls to a resource, each call answered with a probability $r_i \in [0, 1]$. In particular, the expected value of the number of accessible resources is $r_1 + \dots + r_n \leq r$.

# 5 Beyond Rel

We have seen that the relational category provides a large panel of different semantics, but all of them are definitely degenerated because the ambient category is compact closed. Actually, our tools apply to various other categories, even not compact closed. Just to have a taste of
# 6 Conclusion

**Full Linear Logic.** $B_SLL$ is a refinement of the multiplicative exponential fragment of intuitionistic linear logic. One can wonder whether this approach can be extended to full linear logic, with additive connectives and involutive negation.

Additive connectives can be introduced without any difficulty, but the involutive negation, and especially the introduction of the why-not modality ? dual of the of-course !, is more delicate. Namely, one should grasp the computational meaning of the action of the $S$ parameters over the why-not modality.

**Toward true dependent types.** The major weakness of $B_SLL$ is the lack of dependent types, in particular $B_SLL$ is not an extension of bounded linear logic. The interest in this latter has been recently renewed by a series of work, like Dal Lago and Gaboardi's $D_\ell PCF$ [4] or Gaboardi et al.'s DFuzz [5]. These systems use parameters depending on variables which can be bounded and instantiated in the type derivation. This allows, for example, to distinguish between the resource usages of two branches of a conditional, or, combined with a fix-point combinator, to define a parameter depending on the number of loops performed during the evaluation of an iteration.

It is not clear to us whether and how our semantics extends to such a framework. The notion of dependence is delicate to catch semantically, namely it amounts to making the operator $\mathcal{O}$ parametrised by some context. We are, in fact, currently investigating in a different approach (that still use the same intuitions).

In this approach we do not start with a categorical model of linear logic, but with a richer 2-categorical model of linear logic (for example *Rel* endowed with inclusions as 2-functors). Rather than having to find manually a stratification, we can directly identify a structure of $B_SLL$ in the lax slice category $C/\bot$ (with morphisms of $C$ targeting $\bot$ as objects). There, the syntactic semiring $S$ is modeled by a sub category of $C[!\bot, \bot]$ (with arrows representing the order relation). This extends naturally to dependency by considering every lax slice category $C/A$ together, for duplicable objects $A \in C$ representing the values we are dependent on.

**Beyond Rel.** This paper is focused on the relational category *Rel* and on the notion of stratification (Definition 6). This was actually the original goal of our investigation: constructing relational models of $B_SLL$. Indeed, it is clear that a more general principle comes out from our results, relating the stratification to a semi-ring structure hidden behind the hom-sets $C(!\bot, \bot)$.

We have briefly discussed such a generality in Section 5, giving examples of stratifications of linear categories based on coherence spaces. The present setting however cannot explain how one can recover the target semi-ring of an interpretation out of $C(!\bot, \bot)$, for any (or a large class of) linear category $C$. To do that one should work in the framework of the 2-categorical models of linear logic, as mentioned in the previous paragraph, and this will be done in the future.

# References

1. Nick Benton, Gavin Bierman, Valeria de Paiva, and Martin Hyland. Linear lambda-calculus and categorical models revisited. In E. Börger, G. Jäger, H. Kleine Büning, S. Martini, and M. Richter, editors, *Proceedings of the Sixth Workshop on Computer Science Logic*, pages 61–84. Springer Verlag, 1993.
2 Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. A core quantitative coefficient calculus. In *Proceedings of ESOP 2014*, volume 8410 of LNCS, pages 351–370. Springer, 2014.

3 Alberto Carraro, Thomas Ehrhard, and Antonino Salibra. Exponentials with infinite multiplicities. In A. Dawar and H. Veith, editors, *Proceedings of CSL 2010*, volume 6247 of LNCS, pages 170–184, 2010.

4 Ugo Dal Lago and Marco Gaboardi. Linear dependent types and relative completeness. In *Proceedings of LICS 2011*, pages 133–142. IEEE, 2011.

5 Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. Linear dependent types for differential privacy. In R. Giacobazzi and R. Cousot, editors, *Proceedings of POPL 2013*, pages 357–370. ACM, 2013.

6 Dan R. Ghica and Alex I. Smith. Bounded linear types in a resource semiring. In Z. Shao, editor, *Proceedings of ESOP 2014*, volume 8410 of LNCS, pages 331–350. Springer, 2014.

7 Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50:1–102, 1987.

8 Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: A modular approach to polynomial-time computability. *Theor. Comput. Sci.*, 97(1):1–66, April 1992.

9 Charles Grellois and Paul-André Mellès. An infinitary model of linear logic. In *Proceedings of FoSSaCS 2015*, volume 9034 of LNCS, pages 41–55. Springer, 2015.

10 Paul-André Mellies. The parametric continuation monad. *Mathematical Structures in Computer Science*, Festschrift in honor of Corrado Böhm for his 90th birthday, 2013.

11 Paul-André Mellès, Nicolas Tabareau, and Christine Tasson. An explicit formula for the free exponential modality of linear logic. In S. Albers, A. Marchetti-Spaccamela, Y. Matias, S. E. Nikoletseas, and W. Thomas, editors, *Proceedings of ICALP 2009*, pages 247–260, 2009.

12 Tomas Petricek, Dominic Orchard, and Alan Mycroft. Coeffects: unified static analysis of context-dependence. In *Proceedings of International Conference on Automata, Languages, and Programming – Volume Part II*, ICALP, 2013.

13 Tomas Petricek, Dominic Orchard, and Alan Mycroft. Coeffects: A calculus of context-dependent computation. In *Proceedings of International Conference on Functional Programming*, ICFP, 2014.