# Higher-order distributions for differential linear logic.

Marie Kerjean, Jean-Simon Lemay

► To cite this version:

Marie Kerjean, Jean-Simon Lemay. Higher-order distributions for differential linear logic. Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Mikolaj Bojanczyk and Alex Simpson, 2019, Prague (Czech Republic), Czech Republic. 10.1007/978-3-030-17127-8_9.hal - 01969262v2

HAL Id: hal-01969262

https://inria.hal.science/hal-01969262v2

Submitted on 16 Jan 2019

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
# Higher-order distributions for differential linear logic *

Marie Kerjean¹ and Jean-Simon Pacaud Lemay²

1 Équipe Gallinette, INRIA, LS2N, Nantes, France. marie.kerjean@inria.fr

² University of Oxford jean-simon.lemay@kellogg.ox.ac.uk

**Abstract.** Linear Logic was introduced as the computational counterpart of the algebraic notion of linearity. Differential Linear Logic refines Linear Logic with a proof-theoretical interpretation of the geometrical process of differentiation. In this article, we construct a polarized model of Differential Linear Logic satisfying computational constraints such as an interpretation for higher-order functions, as well as constraints inherited from physics such as a continuous interpretation for spaces. This extends what was done previously by Kerjean for first order Differential Linear Logic without promotion. Concretely, we follow the previous idea of interpreting the exponential of Differential Linear Logic as a space of higher-order distributions with compact-support, which is constructed as an inductive limit of spaces of distributions on Euclidean spaces. We prove that this exponential is endowed with a co-monadic like structure, with the notable exception that it is functorial only on isomorphisms. Interestingly, as previously argued by Ehrhard, this still allows the interpretation of differential linear logic without promotion.

**Keywords:** Differential Linear Logic · Categorical semantics · Topological vector spaces.

## 1 Introduction

Denotational semantics interprets programs as functions which focuses not on how data from these programs are computed, but rather focusing on the input/output of programs and on data computed from other data [19]. Through the Curry-Howard-Lambek correspondence, this approach refines into the categorical semantics of type systems. In particular, a study of the denotational model of the λ-calculus for coherent spaces led Girard to Linear Logic [9] and the understanding of the use of resources as the computational counterpart of linearity in algebra. Differential Linear Logic (DiLL) [7] is a refinement of Linear Logic which allows for a notion of linear approximation of non-linear proofs. As a proof-net calculus, DiLL originated from studying vectorial models of Linear Logic which in general are based on spaces of sequences, such as Köthe spaces and finiteness spaces [5].

Recently the first author argued in [14] that as a sequent calculus DiLL has a "smooth" semantical interpretation where the exponential ! (the central object of Linear

<footnote>* Marie Kerjean was supported by the ANR Rapido, and would like to thanks Tom Hirschowitz for many comments and discussions on this work. Jean-Simon Pacaud Lemay would like to thank Kellogg College, the Clarendon Fund, and the Oxford-Google DeepMind Graduate Scholarship for financial support.</footnote>
Logic) is interpreted as a space of distributions with compact support [18]. This seman-
tical interpretation of DiLL (along with the Linear Logic typed phenomena of duality
and interaction) provides a strong argument that DiLL should be considered as a foun-
dation for a type theory of differential equations, whose semantics would be based on
structures developed for mathematical physics. However one of the many divergences
between the theoretical study of physical systems and the theoretical study of program-
ming languages lies in the treatment of input data. In the study of differential equations,
one generally only accepts a finite number of parameters: typically time and space [1].
While one of the fundamental aspects of the semantics of functional programming lan-
guages is the concept of higher-order types [4], which in particular allows programs
to take other programs as inputs. Linking these two concepts together requires
that when mathematical physics studies functions with finite dimensional domains, the
denotational semantical counterpart will be studying functions whose codomains are
spaces of functions (which are in general far from being finite dimensional).

This article gives a higher-order notion of distributions with compact support, fol-
lowing the model without higher order constructed by the first author in [14]. Indeed,
only functions whose domains are finite dimensional were defined in [14], while no
interpretation was given for functions whose domains are spaces of smooth functions.
This latter notion relies on the basic intuition that even with a continuous and infinite
set of input data, a program will at each computation use only a *finite* amount of data.

**Content and related work** In this paper, we interpret the exponential as an inductive limit of spaces of distributions with compact support (Definition 7). Non-linear proofs are thus interpreted as elements of a projective limit of spaces of smooth functions. In [3], Blute, Cockett, and Seely construct a general interpretation of an exponential as a *projective* limit of more basic spaces. In [13], Kriegl and Michor construct the free $C^\infty$-ring over a set $X$ (thus a space of smooth functions) as a projective limit of spaces of smooth functions between Euclidean spaces. Our work thus differs on the fact that we reverse the use of projective and inductive limits for defining the exponential and that we use a finer indexation than the indexation used in [3, 13]. The reverse use of limits compared to the literature is motivated by the fact that we are cautious about *polarities* [16], while the finer indexing is for topological considerations. Indeed, we need to carefully consider the functoriality of the exponential and the topology on the objects.

**Context** Differential Linear Logic (DiLL) is a sequent calculus enriching Linear Logic (LL) with the possibility of *linearizing* proofs. This linearization is semantically understood as the differentiation at 0. Motivated by the need to explore the similarities between the differential structures inherited from logic and those inherited from physics, one would like to interpret formulas of DiLL by general topological vector spaces and non-linear proofs by smooth functions. The interpretation of the involutive linear negation of DiLL leads to the requirement of *reflexive* topological vector spaces, that is, topological vector spaces *E* such that $\mathcal{L}(\mathcal{L}(E, \mathbb{R}), \mathbb{R}) \simeq E$, otherwise expressed as $E'' \simeq E$. In [14], the first author argued that in a classical smooth-linear setting, the exponential ! should be interpreted as a space of distributions with compact support [18], that is, $!E := C^\infty(E, \mathbb{R})'$. The first author also showed that this defines a strong
monoidal functor ! from the category of Euclidean vector spaces to the category of reflexive locally convex and Hausdorff vector spaces. As reflexive spaces typically do not form a *-autonomous category (or even a monoidal closed category), in [14] the first author constructs a *polarized* model of DiLL structured as chirality [17]. This polarized structure is also necessary here. In section 5, formulas of DiLL₀ are interpreted in two different categories, depending on whether they interpret a positive or a negative formula.

**Main content** In this paper we construct an interpretation for the exponential ! (Definition 10) which is strong monoidal (Theorem 3). The exponential constructed in this paper is a generalization of the compact-support exponential from [14]. Explicitly, for a reflexive space E, the exponential !E is defined as the inductive limit of spaces $C^\infty(\mathbb{R}^n, \mathbb{R})'$, indexed by *linear continuous* functions $f: \mathbb{R}^n \to E$ (Definition 7),

$$!E := \lim_{f:\mathbb{R}^n \to E} C^\infty(\mathbb{R}^n, \mathbb{R})'$$

We also consider the "why not" connective ? (Definition 9) where for a reflexive space E, ?E is interpreted as the space of smooth scalar functions on E, $C^\infty(E, \mathbb{R})$. Explicitly, being the dual of !E, ?E is the projective limit of spaces $C^\infty(\mathbb{R}^n, \mathbb{R})$, indexed by the injective linear continuous functions $f: \mathbb{R}^n \to E'$ (Proposition 4),

$$?E := \lim_{f:\mathbb{R}^n \to E'} C^\infty(\mathbb{R}^n, \mathbb{R})'$$

An important drawback of this work is that the functoriality of ! is ensured only on isomorphisms, that is, ! is an endofunctor on the category REFLᵢₐₛ of reflexive spaces and isomorphisms between them. We use a technique developed by Ehrhard in [6] to show that this still provides a model of *finitary* Differential linear logic (DiLL₀), that is, DiLL without the promotion rule. We also discuss how this construction also leads to a polarized model of DiLL₀ (Section 5).

**Organization of the paper** Section 2 gives an overview of the development in DiLL which led to this paper and gives some background in functional analysis. In section 3 we discuss higher-order functions and distributions, and prove strong monoidality. Section 4 provides the interpretation of the dereliction and codereliction and the bialgebraic structure of the exponential. Finally in Section 5 we discuss the polarized interpretation of formulas. We have chosen to put all the proofs but one in the appendix, where some of the proofs use the combinatorics of the categorical definition of the exponential, while others employ the theory of locally convex topological vector spaces [12].

**Notation** In this article, we borrow notation from Linear Logic. In particular, we use $\to^\infty$ to distinguish between linear functions and non-linear ones, for example, $f: E \to^\infty F$ would be *linear continuous* while $g: E \to F$ would only be smooth. We also denote elements of !E and ?E, which are index by linear continuous *injective* indexes $f: \mathbb{R}^n \to E$, in bold with their indexing in subscript: $g_f \in !E$ or $f_f \in ?E$.
# 2 Preliminaries

## 2.1 Differential Linear Logic and its Semantics

Linear Logic [9] refines Intuitionistic Logic with a linear negation, $(-)^{\perp}$, and a notion of linearity of proofs, $\neg$. More precisely, Linear Logic introduces the fundamental isomorphism between $A \Rightarrow B$, proofs of $B$ from $A$, and $!A \dashv B$, linear proofs of $B$ from $!A$ the exponential of $A$. In particular, Linear Logic features a *dereliction* rule $d$, which allows one to consider linear proofs as particular cases of non-linear proofs:

$$ \frac{A^{\perp} \vdash \Gamma \quad d}{!(A^{\perp}) \vdash \Gamma} $$

Differential Linear Logic (DiLL) brings a notion differentiation to the picture by introducing a *codereliction* rule $\bar{d}$. By cut-elimination, the codereliction rule allows one to *linearize* a non-linear proof:

$$ \frac{\vdash \Gamma, A \quad \bar{d}}{\vdash \Gamma, !A} $$

In Linear Logic, the exponential group also features weakening and contraction rules. While DiLL adds co-weakening and co-contraction rules, which in the context of this paper correspond respectively as integration and convolution (see [15] for more details). DiLL without promotion, or finitary Differential Linear Logic, is denoted DiLL₀ and is the original version of Differential Linear Logic by Ehrhard and Regnier [7]. Its exponential rules for `{?,!}` can be found in Figure 1. The other rules of DiLL₀ correspond to the usual ones for the MALL group `{\otimes, \aleph, \oplus, \times}`. Non-finitary DiLL can be constructed by adding the promotion rule to DiLL₀, which in particular requires functionality of the exponential. Cut-elimination in DiLL and DiLL₀ generates *sums of proofs* [7], and therefore the categorical interpretation of proofs must be done in a category enriched over commutative monoids.

<figure><img src="image_2.png" /><figcaption>Fig. 1: Exponential rules of DiLL₀</figcaption></figure>

Following Fiore's definition in [8], a categorical model of DiLL is an extension of Seely's axiomatization of categorical models of Linear Logic [20]. Explicitly a model of DiLL consists of a `*-autonomous category (<i>L</i>, ⊗, 1, (`_`)*`) with a finite biproduct structure `×` with zero object 0, a strong monoidal comonad `!`: (<i>L</i>, `×`, 0) `→` (<i>L</i>, ⊗, 1), and a natural transformation $\bar{d} : \mathrm{id}_L \Rightarrow !$, called the *codereliction* operator, which
interprets differentiation at zero. A particular important coherence for the codereliction
is that composing the co-unit of the co-monad $d : ! \Rightarrow id_\mathcal{L}$ with $\bar{d}$ results in the identity
(the top left triangle of Definition 1). Intuitively, this means that differentiating a linear
map results in the same linear map.

**Working without promotion** The special particularity of our work is that we do not interpret promotion and thus only obtain a denotational model of DiLL₀ but not of DiLL. The main reason for this is that in the formula

$$
\mathcal{E}'(E) := \lim_{f: \mathbb{R}^n \to E} \mathcal{E}'_f(\mathbb{R}^n),
$$

injectivity of the indexes $f : \mathbb{R}^n \to E$ is needed to have a well-defined order to properly define an inductive limit (Definition 6). Therefore the exponential constructed in this paper cannot be functorial with respect to every linear continuous morphism in TOPVEC. In the construction of the exponential, one needs to compose injective indexes $f$ with maps $\ell$ of the category (resp. their dual $\ell'$), and these composition $\ell \circ f$ (resp. $\ell' \circ g$) are required to again be injective. As shown by Treves [21, Chapter 23.2], $\ell'$ is injective if and only if $\ell$ has a dense image. Therefore we have no choice but to ask for isomorphisms and thus we obtain an endofunctor on REFL$_{iso}$, the category of reflexive spaces and linear continuous isomorphisms between them.

Models of DiLL₀ in which promotion is not necessarily interpreted were studied
by Ehrhard in his survey on Differential Linear Logic [6]. He introduces exponential
structures which provides a categorical setting which differs from the traditional ax-
iomatization of Seely’s models.

**Definition 1.** [6, Section 2.5] Let $\mathcal{L}$ be pre-additive *-autonomous category* (i.e. a com-
mutative monoid enriched *-autonomous category [6, Section 2.4]*) and let $\mathcal{L}_{iso}$ be the
wide subcategory of $\mathcal{L}$ with only isomorphisms as morphisms. An **exponential structure**
on a $\mathcal{L}$ is as tuple $(!, w, c, \bar{w}, \bar{c}, d, \bar{d})$ consisting of an endofunctor $! : \mathcal{L}_{iso} \to \mathcal{L}_{iso}$, and
families of morphisms of $\mathcal{L}$ (not necessarily of $\mathcal{L}_{iso}$) indexed by the objects of $\mathcal{L}$:

$$
\begin{align*}
w_A : !A \dashrightarrow 1 & \qquad c_A : !A \dashrightarrow !A \otimes !A & \qquad \bar{w}_A : 1 \dashrightarrow !A & \qquad \bar{c}_A : !A \otimes !A \dashrightarrow !A \\
d_A : !A \dashrightarrow A & \qquad \bar{d}_A : A \dashrightarrow !A
\end{align*}
$$

which are natural for morphisms of $\mathcal{L}_{\text{iso}}$, and such that for each object $A$, $(!A, w_A, c_A, \bar{w}_A, \bar{c}_A)$
is a commutative bialgebra in $\mathcal{L}$, and that the following diagrams to commute:

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

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

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

The above commutative diagrams allow for a direct interpretation of the cut-elimination process of DiLL₀. Ehrhard shows in particular that the interpretation of the structural and co-structural rules of DiLL₀ only needs the functoriality of the exponential on the isomorphisms [6, Section 2.5]. Indeed, in a *classical* model of DiLL (that is a model in which the interpretation of the linear negation is involutive) functoriality on isomorphisms is needed to guaranty the duality between ? and !. Otherwise, the structural exponential rules are interpreted by natural transformations c, $\bar{c}$, w, $\bar{w}$, d, and $\bar{d}$. These natural transformations can be constructed as in [8], following a co-monadic structure (!A, w_A, µ_A) on each object !A [7, Section 2.6]. To sum up:

*Functoriality of the exponential on isomorphisms is needed for duality but is not needed to interpret finitary proofs as morphisms of a category.*

That we have a model of DiLL₀ and not of DiLL fits well with our motivation, as we are looking for the computational counterpart of type theories modeled by analysis. DiLL₀ is indeed the sequent calculus which is refined into an understanding of Linear Partial Differential Equations in [14] and the meaning of promotion with respect to differential equations remains unclear. However, we are still able to construct a natural promotion-like morphism for our exponential (Definition 13).

## 2.2 Reflexive spaces and distributions

In this paper, we study and use the theory of locally convex topological vector spaces [12] to give concrete models of DiLL. Topological vector spaces are a generalization of normed spaces or metric spaces, in which continuity is only characterized by a collection of open sets (which may not necessarily come from a metric or a norm). In this section, we highlight some key concepts which hopefully will give the reader a better understanding of the difficulties of constructing models of DiLL using smooth spaces. We refer respectively to [12] or [18] for details on topological vector spaces or distribution theory.

By a locally convex topological vector space (lcs), we mean a locally convex and Hausdorff topological vector space on $\mathbb{R}$. Briefly, these are vector space endowed with a topology generated by convex open subsets such that the scalar multiplication and the addition are both continuous. For the rest of the section, we consider $E$ and $F$ two lcs.

**Definition 2.** Denote $E \sim F$ for a linear isomorphism between $E$ and $F$ as $\mathbb{R}$-vector spaces, and $E \simeq F$ for a linear homeomorphism between $E$ and $F$ as topological vector spaces.

**Definition 3.** Denote $\mathcal{L}_b(E, F)$ as the lcs of all linear continuous functions between $E$ and $F$, which is endowed with the topology of uniform convergence on bounded subsets [12] of $E$. When $F = \mathbb{R}$, we denote $E' = \mathcal{L}_b(E, \mathbb{R})$ and is called the **strong dual** of $E$.
**Definition 4.** Let $\delta : E \to E''$ be the transpose of the evaluation map in $E'$, which is explicitly defined as follows:

$$ \delta: \begin{cases} E \to E'' \\ x \mapsto \delta_x : (f \to f(x)) \end{cases} $$

A lcs E is said to be semi-reflexive if $\delta$ is a linear isomorphism, that is, $E \sim E''$. A semi-reflexive lcs E is reflexive when $\delta$ is a linear homeomorphism, that is, $E \simeq E''$.

The following proposition is crucial to the constructions of this paper. In terms of polarization, it shows how semi-reflexivity is a negative construction, while convexity mixes positives and negative requirements.

**Proposition 1.** [12, Chapter 11.4]

- Semi-reflexivity is preserved by projective limits, that is, the projective limit of semi-reflexive lcs is a semi-reflexive lcs.

- A lcs E is reflexive if and only if it is semi-reflexive and barrelled, meaning that every convex, balanced, absorbing and closed subspace of E is a 0-neighbourhood.

- Barrelled spaces are preserved by inductive limits, that is, the inductive limit of barrelled spaces is a barrelled space.

Next we briefly recall a few facts about distributions.

**Definition 5.** For each $n \in \mathbb{N}$, a function $f : \mathbb{R}^n \to \mathbb{R}$ is said to be smooth if it is infinitely differentiable. Let $\mathcal{E}(\mathbb{R}^n) = C^\infty(\mathbb{R}^n, \mathbb{R})$ denote the space of all smooth functions $f : \mathbb{R}^n \to \mathbb{R}$, and which is endowed with the topology of uniform convergence of all differentials on all compact subsets of $\mathbb{R}^n$ [12]. The strong dual of $\mathcal{E}(\mathbb{R}^n)$, $\mathcal{E}'(\mathbb{R}^n)$, is called the **space of distributions with compact support**.

We now recall the famous Schwartz kernel theorem, which states that the construction of a kernel of $f \otimes g \in \mathcal{E}(\mathbb{R}^n) \otimes \mathcal{E}(\mathbb{R}^m) \mapsto f \cdot g \in \mathcal{E}(\mathbb{R}^{n+m})$ is in fact an isomorphism on the completed tensor product $\mathcal{E}(\mathbb{R}^n) \hat{\otimes} \mathcal{E}(\mathbb{R}^m)$:

**Theorem 1 ([18]).** For any $n, m \in \mathbb{N}$, we have the following:

$$ \mathcal{E}'(\mathbb{R}^m) \hat{\otimes}_\pi \mathcal{E}'(\mathbb{R}^m) \simeq \mathcal{E}'(\mathbb{R}^{n+m}) \simeq \mathcal{L}_b(\mathcal{E}'(\mathbb{R}^m), \mathcal{E}(\mathbb{R}^n)) $$

**Theorem 2 ([14]).** There is a first-order polarized denotational model of DiLL$_0$ in which the exponential is interpreted as a space of distributions: $! (\mathbb{R}^n) := \mathcal{E}'(\mathbb{R}^n)$.

This interpretation did not generalize to higher-order as we were unable to define $!E$ for an infinite dimensional space $E$, even for those sharing the topological properties of spaces of smooth functions$^3$. For example, the definition of $!!\mathbb{R}$ is in no way obvious. This is the problem we tackle in the following sections.

<footnote>$^3$ These spaces are in particular nuclear (F)-spaces, see [14].</footnote>
### 3 Higher-order distributions and Kernel

In this section we define spaces of higher-order functions and distributions, we prove that they are reflexive (Proposition 2) and verify a kernel theorem (Theorem 3).

**Definition 6.** Let $E$ be a lcs and $f: \mathbb{R}^n \to E$ and $g: \mathbb{R}^m \to E$ be two linear continuous injective functions. We say that $f \le g$ when $n \le m$ and $f = g|_{\mathbb{R}^n}$, that is, $f = g \circ \iota_{n,m}$ where $\iota_{n,m}: \mathbb{R}^n \to \mathbb{R}^m$ is the canonical injection.

The ordering $\le$ in the above definition provides an order on the set of dependent pairs $(n, f)$ where $n \in \mathbb{N}$ and $f: \mathbb{R}^N \to E$ is linear injective. This will allow us to construct an inductive limit (a categorical colimit) of lcs.

**Definition 7.** Let $E$ any lcs.

1. For every linear continuous injective function $f: \mathbb{R}^n \to E$, define the lcs $\mathcal{E}'_f(\mathbb{R}^n)$ as follows:

$$ \mathcal{E}'_f(\mathbb{R}^n) := C^\infty(\mathbb{R}^n)' $$

2. Define $\mathcal{E}'(E)$, the space of distributions on $E$, as follows:

$$ \mathcal{E}'(E) := \varinjlim_{f:\mathbb{R}^n \to E} \mathcal{E}'_f(\mathbb{R}^n) $$

that is, the inductive limit [12, Chapter 4.5] (or colimit) in the category TOPVEC of the family of lcs $\{\mathcal{E}'_f(\mathbb{R}^n) | f: \mathbb{R}^n \to E \text{ linear continuous injective}\}$ directed under the inclusion maps defined as

$$ S_{f,g}: \mathcal{E}'_g(\mathbb{R}^n) \to \mathcal{E}'_f(\mathbb{R}^m), \phi \mapsto (h \mapsto \phi(h \circ \iota_{n,m})) $$

when $f \le g$.

Intuitively this definition of $\mathcal{E}'(E)$ says that distributions with compact support on $E$ are the distributions with a finite dimensional compact support $K \subset \mathbb{R}^n$.

**Proposition 2.** For any lcs $E$, $\mathcal{E}'(E)$ is a reflexive lcs.

The following proposition justifies the notation of $\mathcal{E}'(\mathbb{R}^n)$ from Definition 5.

**Proposition 3.** If $E \simeq \mathbb{R}^n$ for some $n \in \mathbb{N}$, then $\mathcal{E}'(E) \simeq C^\infty(\mathbb{R}^n)'$.

As $\mathcal{E}'(E)$ is reflexive, we give a special (yet obvious) notation for the strong dual of $\mathcal{E}'(E)$.

**Definition 8.** For a reflexive lcs $E$, let $\mathcal{E}(E)$ denote the strong dual of $\mathcal{E}'(E)$.

Since the strong dual of a reflexive lcs is again reflexive [12], it follows by Proposition 3 that for any reflexive lcs $E$, $\mathcal{E}(E)$ is also reflexive.

The strong dual of a projective limit is linearly isomorphic to the inductive limit of the duals, however as noted in [12, Chapter 8.8.12], the topologies may not coincide. When $E$ is endowed with its Mackey topology (which is the case in particular when $E$ is reflexive), then the topologies do coincide.
**Proposition 4.** Let $E$ be a reflexive lcs. For every linear continuous injective function $f: \mathbb{R}^n \to E$, define the lcs $\mathcal{E}_f(\mathbb{R}^n) := C^\infty(\mathbb{R}^n)$. Then we have the following linear homeomorphism:

$$ \mathcal{E}(E) \approx \varinjlim_{f:\mathbb{R}^n \to E} \mathcal{E}_f(\mathbb{R}^n) $$

where the lcs on the right is the projective limit [12, Chapter 2.6] in TOPVEC of the family of lcs $\{\mathcal{E}_f(\mathbb{R}^n) | f: \mathbb{R}^n \to E \text{ linear continuous injective}\}$ with projections defined as:

$$ T_{g,f} = S'_{f,g} : \mathcal{E}_g(\mathbb{R}^m) \to \mathcal{E}_f(\mathbb{R}^n), g \mapsto g \circ \iota_{n,m} $$

when $f \le g$.

The elements of $\mathbf{f} \in \mathcal{E}(E)$ are families $\mathbf{f} := (\mathbf{f}_f)_{f:\mathbb{R}^n \to E}$ such that if $f \le g$, we have that $\mathbf{f}_f = \mathbf{f}_g \circ \iota_{n,m}$. The intuition here is that distributions of a reflexive lcs $E$ are in fact distributions with compact support on a finite dimensional space, or equivalently that smooth functions $E \to \mathbb{R}$ are functions which are smooth when restricted to $\mathbb{R}^n$ (viewed as a finite dimensional subspace of $E$). This makes it possible to define multinomials on $E$ in the following way:

$$ P(x \in \mathbb{R}^k) = \sum_{I \subseteq [1, n]} a_\alpha x_1^{\alpha_1} \dots x_n^{\alpha_n} $$

where we either embedded or projected $\mathbb{R}^k$ into $\mathbb{R}^n$ in the canonical way.

It also seems possible to provide a setting restricted specifically to higher order spaces of distributions and not to every reflexive space. Indeed, we would like to describe smooth scalar functions on $\mathcal{E}(\mathbb{R}^n)$ as

$$ h \in \mathcal{E}(\mathbb{R}^n) \mapsto h(0)^2 $$

taking into account that we have as inputs non-linear functions. This seem to indicate another direction of research, where we would construct smooth functions indexed by Dirac functions $\delta: \mathbb{R}^n \to E' = \mathcal{E}'(\mathbb{R}^n)$ as defined in Definition 4.

**The Kernel Theorem** We now provide the Kernel theorem for spaces $\mathcal{E}(E)$. Indeed, the spaces of functions are the one which can be described as projective limits, and projective limits are the ones which commute with the completed projective tensor product $\hat{\otimes}_\pi$. The proof of Theorem 3 can be found in the appendix, though we would like to highlight that the proof depends heavily on the fact that the considered spaces of functions are nuclear spaces [12].

**Theorem 3.** For every lcs $E$ and $F$, we have a linear homeomorphism:

$$ \mathcal{E}(E) \hat{\otimes}_\pi \mathcal{E}(F) \approx \mathcal{E}(E \oplus F). $$

We now give the definitions of functors $\otimes$ and $\oplus$, both of which agree with the previous characterization described by the first author in [14] on Euclidean spaces $\mathbb{R}^n$. However, as discussed in the introduction, while these functors can be defined properly on all objects, they will only be defined on isomorphisms. So let $\text{REFL}_{\text{iso}}$ denote the category of reflexive lcs and linear homeomorphism between them.
**Definition 9.** Define the endofunctor $?: \mathrm{REFL}_{iso} \to \mathrm{REFL}_{iso}$ as follows:

$$ \text{?:} \quad \left\{ \begin{array}{l} \mathrm{REFL}_{iso} \to \mathrm{REFL}_{iso} \\ E \mapsto \mathcal{E}(E') \\ \ell: E \to F \mapsto ?\ell: \mathcal{E}(E') \to \mathcal{E}(F') \end{array} \right. \qquad (1) $$

where for $f \in \mathcal{E}(E')$, the $g: \mathbb{R}^m \to F'$ component of $?\ell(f) \in \mathcal{E}(F')$ is defined as:

$$ ?\ell(f)_g = f_{\ell' \circ g} $$

where $\ell': F' \to E'$ denotes the transpose of $\ell$.

Note that $?\ell: \mathcal{E}(E') \to \mathcal{E}(F')$ is defined by the universal property of the projective limit, that is, $?\ell$ is uniquely defined by post-composing by the projections $\pi_g: \mathcal{E}(F') \to \mathcal{E}(\mathbb{R}^n)$ for each linear continuous injective function $g: \to F'$. We also note that $f_{\ell' \circ g}$ is well-defined since $\ell'$ is injective and therefore so is $\ell' \circ g$. The universality of the projective limit also insures that $?\ell$ is an isomorphism and that $?$ is functorial.

**Definition 10.** Define the functor $! : \mathrm{REFL}_{iso} \to \mathrm{REFL}_{iso}$ on objects as $!E := (?E')'$ and on isomorphisms as $!\ell = (?\ell)'$. Explicitly, $!$ is defined as follows:

$$ \text{!:} \quad \left\{ \begin{array}{l} \mathrm{REFL}_{iso} \to \mathrm{REFL}_{iso} \\ E \mapsto \mathcal{E}'(E) \\ \ell: E \to F \mapsto !\ell \in \mathcal{E}(F') \end{array} \right. \qquad (2) $$

where for the $f: \mathbb{R}^n \to E$ component of $f \in \mathcal{E}'(E)$, $!\ell(f_f) \in \mathcal{E}'(F)$ is defined as:

$$ !\ell(f_f) = f_{\ell \circ f: \mathbb{R}^n \to F} $$

As before, $!\ell$ is defined by the co-universal property of the inductive limit, that is, $!\ell$ is defined by pre-composition with the injections $\iota_f: \mathcal{E}'_f(\mathbb{R}^n) \to \mathcal{E}'(E)$ for every linear continuous injective function $f: \mathbb{R} \to E$. Factoriality of $!$ is ensured by functoriality of $?$ and reflexivity of the objects.

# 4 Structural morphisms on the exponential

We consider the exponential from the DiLL model of convenient vector spaces in [2] as a guideline for defining the structural morphisms on $!E$. In that setting, structural operations can be defined on Dirac operations. For example, the codereliction $d_{conv}$ maps $\delta_x$ to $x$. Here the mapping $\delta_x$ must be understood as the linear continuous function which maps $x \in E$ to $((f_f)_f \in \mathcal{E}(E') \to f(f^{-1}(x)) \in \mathcal{E}'(E))$, which we show is well defined below.
## 4.1 Dereliction and co-dereliction

**Definition 11.** For a reflexive lcs E, define the following linear continuous morphism:

$$d_E: \begin{cases} ! (E) \to E'' \simeq E \\ \phi \mapsto (\ell \in E' \mapsto \phi ((\ell \circ f)_{f:\mathbb{R}^n \to E} \in \mathcal{E} (E))) \end{cases} \quad (3)$$

We stress that $d_E$ is a map in REFL and not a map in REFL$_{iso}$ (though sufficient for Definition 1). The map $d_E$ is well defined as $\ell \circ f$ is a linear continuous injective function $\mathbb{R}^n \to \mathbb{R}$, and thus is smooth and belongs in particular to $\mathcal{E}(\mathbb{R}^n)$. Also, as we are working with reflexive spaces, $d_E$ could have been described equivalently as a map of the following type:

$$\begin{gathered} E \to ?(E) \\ x \mapsto (ev_x \circ f \in \mathcal{L}(\mathbb{R}^n, \mathbb{R}))_{f:\mathbb{R}^n \to E'} \end{gathered} \quad (4)$$

**Lemma 1.** The morphisms $d_E$ are natural with respect to linear homeomorphisms, that is, maps of REFL$_{iso}$. Explicitly, if $\ell: E \to F \in \text{REFL}_{iso}$ then $d_F \circ !\ell = \ell \circ d_E$.

We now study the interpretation of the codereliction $\bar{d}$. Let $D_0: C^\infty(\mathbb{R}^n) \to (\mathbb{R}^n)'$ denote the operator which maps a function to its differential at 0.

$$D_0: \left\{ \begin{array}{l} C^\infty(\mathbb{R}^n) \to (\mathbb{R}^n)' \\ \mathbf{f} \mapsto \left( v \in \mathbb{R}^n \mapsto \lim_{t \to 0} \frac{f(tx) - f(0)}{t} = \sum_{i=1}^n \frac{\partial f}{\partial x_i}(0)v_i \right) \end{array} \right.$$

The operator $D_0$ is linear in $\mathbf{f} \in C^\infty(\mathbb{R}^n)$. It is continuous: the reciprocal image by $D_0$ of the polar $B_{0,1}$ is the set of all functions $\mathbf{f} \in C^\infty(\mathbb{R}^n)$ whose partial derivatives of order one have maximal value 1 on the compact $\{0\}$. This contains the set $\{\mathbf{f}|\forall i, |\frac{\partial f}{\partial x_i}(0)| < 1\}$, which is open in the topology described in Definition 5.

**Definition 12.** For a reflexive lcs E, define the following linear continuous morphism:

$$\bar{d}_E: \begin{cases} E \to !E \simeq (\mathcal{E}(E))' \\ x \mapsto (\mathbf{f}_f \in C_f^\infty(\mathbb{R}^n, \mathbb{R}))_{f:\mathbb{R}^n \to E'} \mapsto D_0 \mathbf{f}_f(f^{-1}(x)) \end{cases} \quad (5)$$
where $f$ is injective such that $x \in \text{Im}(f)$.

We should explain why the choice of $f^{-1}(x)$ does not matter. Here $f^{-1}(x)$ is the linear argument of the differentiation. Indeed suppose that $f \le g$, that is, $f = g \circ \iota_{n,m}$. Thus by definition of the projective limit we have $\mathbf{f}_f = \mathbf{f}_g \circ \iota_{n,m}$ and:

$$\begin{align*} D_0 \mathbf{f}_f(f^{-1}(x)) &= D_0(\mathbf{f}_g \circ \iota_{n,m})((g \circ \iota_{n,m})^{-1}(x)) \\ &= D_0 \mathbf{f}_g(D_0 \iota_{n,m}(\iota_{n,m}^{-1}(g^{-1}(x)))) \\ &= D_0 \mathbf{f}_g(\iota_{n,m}(\iota_{n,m}^{-1}(g^{-1}(x)))) \quad (\text{as } \iota_{n,m} \text{ is linear}) \\ &= D_0 \mathbf{f}_g(g^{-1}(x))) \end{align*}$$
As any pair of linear functions $f: \mathbb{R}^n \to E$ and $g: \mathbb{R}^m \to E$ is bounded by $f \times g: \mathbb{R}^{n+m} \to E$, we obtain the required uniqueness.

Similar to the dereliction, the codereliction could alternatively have been described as a map of the following type:

$$ \begin{gathered} \mathcal{E}(E') \to E'' \approx E \\ (\mathbf{f}_f)_{f:\mathbb{R}^n \to E'} \mapsto (\ell \in E' \mapsto D_0 \mathbf{f}_f(f^{-1}(\ell))) \end{gathered} \qquad (6) $$

We again stress that $\bar{d}_E$ is not a map in $\mathrm{REFL}_{iso}$.

**Lemma 2.** The morphisms $\bar{d}_E$ are natural with respect to linear homeomorphisms, that is, maps of $\mathrm{REFL}_{iso}$. Explicitly, if $\ell: E \to F \in \mathrm{REFL}_{iso}$ then $\bar{d}_F \circ \ell = !\ell \circ \bar{d}_E$.

Finally, we observe that $d_E$ and $\bar{d}_E$ satisfy the all-important coherence condition between derelictions and coderelictions.

**Proposition 5.** For a reflexive $\mathrm{lcs} E$, $d_E \circ \bar{d}_E = \mathrm{Id}_E$.

## 4.2 (Co-)contraction and (co-)weakening

In this section, we define the interpretation of the other exponential rules: weakening $w$, co-weakening $\bar{w}$, contraction $c$, and co-contraction $\bar{c}$, which will be generalized from [14]. We start with weakening and co-weakening, which are fairly straightforward.

$$ w: \left\{ \begin{array}{l} !E \to \mathbb{R} \\ \phi \mapsto \sum_f \phi_f(\mathbf{1}) \end{array} \right. \qquad \bar{w}: \left\{ \begin{array}{l} \mathbb{R} \to !E \\ 1 \mapsto \delta_0 : ((\mathbf{f}_f)_f \in \mathcal{E}(E) \to \mathbf{f}(0)) \end{array} \right. \text{ for any } f $$

According to [8], the rules $c$ and $\bar{c}$ are interpreted respectively via the kernel theorem and pre-composition with the diagonal $E \to E \times E$ and co-diagonal $E \times E \to E$ maps of the biproduct. This is however not defined in a context where $!$ is functorial only on isomorphisms. Thus we give a direct, component-wise interpretation of contraction and co-contraction.

$$ c: \left\{ \begin{array}{l} !E \to ! (E \times E) \approx !E \otimes !E \\ \phi \mapsto (\mathbf{g}_g)_{g:\mathbb{R}^n \hookrightarrow E \times E} \mapsto \phi((\mathbf{g}_{(x \in \mathbb{R}^n \hookrightarrow (f(x), f(x)))})_{f:\mathbb{R}^n \hookrightarrow E}) \end{array} \right. $$

$$ \bar{c}: \left\{ \begin{array}{l} !E \otimes !E \to !E \\ \phi \otimes \psi \mapsto (\mathbf{f}_f)_{f:\mathbb{R}^n \hookrightarrow E} \mapsto \phi((x \in \mathbb{R}^n \mapsto \psi((y \in \mathbb{R}^m \mapsto \mathbf{f}_f(x) + \mathbf{f}'_f(y))_{f'})) \end{array} \right. $$

where $f: \mathbb{R}^n \to E$ and $f': \mathbb{R}^m \to E$.

**Theorem 4.** The morphisms $(w, \bar{w}, c, \bar{c}, d, \bar{d})$ satisfy the coherences of exponential structure on $!E$, as detailed in Definition 1.

We note that this does not give an exponential structure per say since $\mathrm{REFL}$ is not a monoidal category, as we will explain in Section 5. That said, in Section 5 we are still able to construct a *polarized* model of $\mathrm{DiLL}_0$.
## 4.3 Co-multiplication

The categorical interpretation of the exponential rules of linear logic requires a comonad ! : $\mathcal{L} \to \mathcal{L}$. However in the case of this paper, the exponential ! is functorial only on isomorphisms. As such, one cannot interpret the promotion rule of Linear Logic, as this requires functoriality of ! on the interpretation of any proof (and typically on linear continuous maps which are not isomorphisms). That said, functoriality is the only missing ingredient, and one can still define natural transformations of the same type as the co-multiplication and co-unit of the co-monad. This section details this point, leaving the exploration of a functorial ! for future work.

**Definition 13.** For a reflexive lcs E, define the following linear continuous morphism:

$$ \mu_E : \left\{ \begin{array}{l} !E \to !!E \\ \phi \mapsto \left( (g_g)_g \in \mathcal{E}(!)E \simeq \varinjlim_g C_g^\infty(\mathbb{R}^m) \right) \to g_g(g^{-1}(\phi)) \end{array} \right. \quad (7) \\ \text{when } \phi \in \mathrm{Im}(g) \text{ and } g \text{ is injective} $$

This is well defined, as we can show as for the coderelication (5) that the term $g_g(g^{-1}(\phi))$ is unique when $g : \mathbb{R}^m \to !E$ linear and $g_g \in C_g^\infty(\mathbb{R}^m)$ varies. Moreover there is at least one linear function $g : \mathbb{R}^m \to !E$ which has $\phi$ in its image.

**Lemma 3.** The morphisms $\mu_E$ are natural with respect to linear homeomorphisms, that is, maps of $\mathrm{REFL}_{iso}$. Explicitly, if $\ell : E \to F \in \mathrm{REFL}_{iso}$ then $\mu_F \circ !!\ell = !\ell \circ \mu_E$.

**Proposition 6.** For any reflexive lcs E, $d_1E \circ \mu_E = Id_1E$

The identity of Proposition 6 is one of the identities of a comonad. The other comonad identities require applying ! to $\mu$ and $d$, which we cannot do in our context as ! is only defined on isomorphisms.

# 5 A model of DiLL₀

In section 4 we defined the structural morphisms on the exponential and proved the equations allowing to interpret proofs of DiLL₀ by morphisms in REFL, independent of cut-elimination. We now detail which categories allow to interpret formulas of MALL. This will be done in a polarized setting generalizing the one of [14].

**Polarization** So far we have constructed an exponential ! : REFL<sub>iso</sub> → REFL<sub>iso</sub> which is strong monoidal. However, the category of reflexive spaces is too big to give us a model of DiLL₀. Interpreting the multiplicative connective requires a monoidal setting, and reflexive spaces are not stable by topological tensor products. If we study more closely the definition of spaces of higher-order smooth functions, we see that their re-flexivity follows from a more restrictive class of spaces. These spaces are however not stable by duality, thus resulting in a *polarized* model of DiLL₀.
In this section we briefly show how the techniques develop above constructs a polarized model of DiLL₀. The syntax of polarized (Differential) Linear Logic [16] is recalled below. A distinction is made between positive formulas (preserved by ⊗ and ⊕) and negative formulas (preserved by 2 and &). The same deduction rule apply.

Negative Formulas: $N, M := \perp|1||?P|N \ 2 \ M|N \times M|P^{\perp}$

Positive Formulas: $P, Q := \top|0|!N|P \otimes Q|P \oplus Q|N^{\perp}$

Models of polarized linear logic are axiomatized categorically as an *adjunction between a category of positives and a category of negative*, where two interpretations for negation play the role of adjoint functors. These categories obey the axiomatic of chiralities [17].

**Additives** Interpreting the additive connectives of linear logic is straightforward. The product × and coproduct ⊕ of lcs are linearly homeomorphic on finite indexes and therefore give biproducts, which leads to the usual commutative monoid enrichment as described in [8].

**Multiplicatives** When sticking to finite dimensional spaces or normed spaces, duality is pretty straightforward in the sense that the dual of a normed space is still normed. This, however, is no longer the case when one generalizes to metric spaces. Indeed, the dual of a metric space may not be endowed with a metric. A Fréchet space, or (F)-space, is a complete and metrizable lcs. The duals of these spaces are not metrizable in general, but they are (DF)-spaces (see [10] for the definition):

**Proposition 7** ([11] IV.3.1).

- If E is metrizable, then its strong dual E' is a (DF)-space.

- If E is a (DF)-space, then E' is an (F)-space.

Typical examples of nuclear (F)-spaces are the spaces of smooth functions $\mathcal{E}(\mathbb{R}^n)$, while typical examples of nuclear (DF)-spaces are the spaces of distributions with compact support $\mathcal{E}'(\mathbb{R}^n)$. In particular, all these spaces are reflexive. In [14], the first author interpreted positive formulas as Nuclear (DF)-spaces, while negative formulas were interpreted as (F)-spaces. Following the construction of section 3, we will consider respectively inductive limits and projective limits.

**Definition 14.** A lcs is said to be a LNF-space if it is a regular projective limit of nuclear Fréchet spaces. The category of LNF-spaces and linear continuous injective maps is denoted LNF. A lcs E is said to be a LNDF-space if it is an inductive limit of nuclear complete (DF)-spaces.

**Proposition 8.** 1. A LNF-space E is reflexive.

2. The dual of a LNF-space is a LNDF-space.

The above proposition can be proven using the same techniques as computing the dual of $\mathcal{E}(E)$.

The difficulty of constructing a model of MLL in topological vector spaces is choosing the topology which will make the tensor product associative and commutative on
the already chosen category of lcs. Contrary to what happens in a purely algebraic setting, the definition of a topological tensor product is not straightforward and several topologies can be defined, with each corresponding to a different notion of continuity for bilinear maps [10]. On nuclear spaces, such as $\mathcal{E}(\mathbb{R}^n)$ and $\mathcal{E}'(\mathbb{R}^n)$, most of these tensor product coincide with one another. In [14], both multiplicative connectors $(\otimes$ and $\mathcal{N})$ were interpreted as the completed projective (equivalently injective) tensor product $\hat{\otimes}_{\pi}$ (see [12, 15.1 and 21.2]) This property is lost when working with limits. However, there is still a good interpretation of $\mathcal{N}$ for LNF spaces (which are thus the interpretation of negatives formulas). Indeed, the completed injective tensor product $\hat{\otimes}_{\varepsilon}$ of a projective limit of lcs is the projective limit of the completed injective tensor products [12, 16.3.2]. Taking the duals of theorem 3 applied to $E'$ and $F'$ gives the following:

**Proposition 9.** For any reflexive spaces E and F we have a linear homeomorphism:

$$?E\hat{\otimes}_{\varepsilon}?F \simeq ?(E \oplus F).$$

and shows that $\mathcal{N}$ is interpreted by $\hat{\otimes}_{\varepsilon}$. The multiplicative conjunction $\otimes$ is interpreted as the dual of $\hat{\otimes}_{\varepsilon}$, which may not be necessarily linearly homeomorphic to $\hat{\otimes}_{\pi}$.

# 6 Conclusion

In this paper, we extended the polarized model of DiLL without higher order constructed in [14] to a higher-order polarized model of DiLL$_0$. The motivating idea was that computation on spaces of functions used only a finite number of arguments. This lead to constructing an exponential on a reflexive lcs as an inductive limit of exponentials of finite dimensional vector spaces. While this exponential is only functorial for linear homeomorphisms we were still able to provide structural morphisms interpreting (co)weakening, (co)contraction, and (co)dereliction, and hints of a co-monad.

The next step would be to extend the definition of the exponential in this paper to an interpretation of the promotion rule and thus of LL – this could be done through epimonod decomposition of arrows in REFL. Another task is to properly work out which tensor product of reflexive space will provide a model of DiLL. Such a model should use chiralities [17], and underline the similarities between shifts and (co-)dereliction.

More generally, this works highlights again that the interpretation of the exponential in lcs relies on a computing principle. Indeed, it always requires finding a higher-order extension of distributions. While what we have constructed here relies on a finitary principle, the construction of a free exponential in [3] relies on the principle that higher-order operations are computed on Dirac distributions $\delta_x$. That is, the exponential is constructed following a discretization scheme. The appearance of such numerical methods in a semantic study of DiLL provides another link between theoretical computer science and mathematical physics. This opens the door to studying relating numerical schemes of numerical analysis and the theoretical study of programming language.
Bibliography

[1] Blass, A.: A game semantics for linear logic. Annals of Pure and Applied Logic **56**(1), 183–220 (1992). https://doi.org/10.1016/0168-0072(92)90073-9

[2] Blute, R., Ehrhard, T., Tasson, C.: A convenient differential category. Cah. Topol. Géom. Différ. Catég. (2012)

[3] Blute, R.F., Cockett, J.R.B., Seely, R.A.G.: Differential categories. Math. Structures Comput. Sci. **16**(6) (2006). https://doi.org/10.1017/S0960129506005676

[4] Church, A.: A formulation of the simple theory of types. The journal of symbolic logic **5**(2), 56–68 (1940)

[5] Ehrhard, T.: On köthe sequence spaces and linear logic. Mathematical Structures in Computer Science **12**(5) (2002)

[6] Ehrhard, T.: An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science **28**(7), 995–1060 (2018). https://doi.org/10.1017/S0960129516000372

[7] Ehrhard, T., Regnier, L.: Differential interaction nets. Theoretical Computer Science **364**(2) (2006)

[8] Fiore, M.: Differential structure in models of multiplicative biadditive intuitionistic linear logic. TLCA (2007)

[9] Girard, J.Y.: Linear logic. Theoretical Computer Science **50**(1), 1 – 101 (1987). https://doi.org/10.1016/0304-3975(87)90045-4

[10] Grothendieck, A.: Produits tensoriels topologiques et espaces nucléaires. Memoirs of the AMS **16** (1966)

[11] Grothendieck, A.: Topological vector spaces. Gordon and Breach Science Publishers (1973), traducteur O. Chaljub

[12] Jarchow, H.: Locally convex spaces. B. G. Teubner (1981)

[13] Kainz, G., Kriegl, A., Michor, P.: $C^\infty$-algebras from the functional analytic view point. Journal of Pure and Applied Algebra **46**(1), 89 – 107 (1987)

[14] Kerjean, M.: A logical account for linear partial differential equations. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS. ACM (2018). https://doi.org/10.1145/3209108

[15] Kerjean, M.: Reflexive spaces of smooth functions: a logical account for linear partial differential equations. PhD thesis, Université Paris Diderot (Oct 2018)

[16] Laurent, O.: Etude de la polarisation en logique. Thèse de doctorat, Université Aix-Marseille II (Mar 2002)

[17] Melliès, P.A.: Dialogue categories and chiralities. Publ. Res. Inst. Math. Sci. **52**(4), 359–412 (2016)

[18] Schwartz, L.: Théorie des distributions. Publications de l'Institut de Mathématique de l'Université de Strasbourg, No. IX-X., Hermann, Paris (1966)

[19] Scott, D., Strachey, C.: Towards a mathematical semantics for programming languages (1971)

[20] Seely, R.: Linear logic, *-autonomous categories and cofree coalgebras. In: In Categories in Computer Science and Logic. American Mathematical Society (1989)

[21] Trèves, F.: Topological vector spaces, distributions and kernels. Academic Press, New York-London (1967)
# Appendix

*Proof (Propostion 2).* As $\mathcal{E}'(E)$ is the inductive limit of reflexive spaces, and thus barrelled spaces, it follows that $\mathcal{E}'(E)$ is also barrelled (see [12, Chapter 11.1]). Thus we just need to prove that $\mathcal{E}'(E)$ is semi-reflexive, that is that every bounded closed subset of $\mathcal{E}'(E)$ is weakly compact.

Using a well known method, we show that this inductive limit is regular, that is, any bounded set $B$ is contained in one of the $\mathcal{E}'_f(\mathbb{R}^n)$. Suppose that it is not. Then we have some bounded set $B$ such that for every $n$ there is $f_n$ such that we have $b_n \in B \setminus \mathcal{E}'_f(\mathbb{R}^n)$. The lcs $F = \lim_{n \to \infty} \mathcal{E}'_{f_n}(\mathbb{R}^n)$ is a strict (i.e. indexed by $\mathbb{N}$) inductive limit of spaces such that $\mathcal{E}'_{f_n}(\mathbb{R}^{n+1})$ is closed in $\mathcal{E}'_{f_n}(\mathbb{R}^{n+1})$, and as such it is regular ([12, 4.6.2]). But the topology on $F$ is the one induced its inclusion in $\mathcal{E}(E)$, and thus the image $B_F$ of $B$ in $F$ is bounded. So as $F$ is a regular limit, $B_F$ should be included in one of the $\mathcal{E}'_{f_n}(\mathbb{R}^n)$, and we have a contradiction.

Thus any bounded set $B$ of $\mathcal{E}'(E)$ is bounded in one $\mathcal{E}'_f(\mathbb{R}^n)$. As these spaces are reflexive, $B$ is $\mathcal{E}'_f(\mathbb{R}^n)$-weakly compact. But the dual of an inductive limit is contained in the product of the duals ([12, Chapter 8.8]) and so $B$ is also weakly compact in $\mathcal{E}(E)$. Thus $\mathcal{E}'(E)$ is semi-reflexive, and since $\mathcal{E}'(E)$ is also barrelled, $\mathcal{E}'(E)$ is reflexive. $\square$

*Proof (Proposition 3).* If $E \simeq \mathbb{R}^m$, the identity $id : \mathbb{R}^m \to \mathbb{R}^m$ results by definition of the inductive limit in a linear continuous injective map $\mathcal{E}_i'd(\mathbb{R}^m) \simeq \mathcal{E}'(\mathbb{R}^m) \to \mathcal{E}'(E)$. Now consider $\phi \in \mathcal{E}'(E)$. Suppose that we have an index $f : \mathbb{R}^n \to E$ on which $\phi$ is non-null. Then as $f$ is an injection one has $n \le m$ and thus a linear injection $\mathcal{E}'(\mathbb{R}^n) \hookrightarrow \mathcal{E}'(\mathbb{R}^m)$. This injection is continuous. Indeed any compact in $\mathbb{R}^n$ is compact in $\mathbb{R}^m$, and thus the topology induced by $\mathcal{E}'(\mathbb{R}^m)$ on $\mathcal{E}'(\mathbb{R}^n)$ is exactly the strong topology on $\mathcal{E}'(\mathbb{R}^n)$. In particular we have a linear map $f : \mathbb{R}^m \to \mathbb{R}^m$, therefore we have the desired equality. $\square$

*Proof (Proposition 4).* According to [12, Chapter 8.8.7], as $F = \lim_{f:\mathbb{R}^n \to E} C_f^\infty(\mathbb{R}^n)$ is reduced, then its dual is linearly isomorphic to

$$F' = \varinjlim_{f:\mathbb{R}^n \to E} C_f^\infty(\mathbb{R}^n)$$

by reflexivity of the spaces $C_f^\infty(\mathbb{R}^n)$. We prove that this is a linear homeomorphism. As a reflexive space, $\mathcal{E}_f(\mathbb{R}_n)_f$ is endowed with its Mackey topology. As the Mackey-topology is preserved by inductive limits, we have that the topology on the lcs:

$$F' \simeq \mathcal{E}'(E) \simeq \varinjlim_{f:\mathbb{R}^n \to E} C_f^\infty(\mathbb{R}^n)'$$

is also the Mackey-topology $\mu(F, F'')$. But as we know that $\mathcal{E}(E)$ is reflexive, this topology is exactly the strong dual topology. $\square$

*Proof (Theorem 3).* By [12, Chapter 15.4.2] we have that the completed projective tensor product of two projective limits indexed respectively by $I$ and $J$ is the projective
limit, indexed by $I \times J$ with the pointwise order, of the completed tensor product. Thus:

$$
\begin{align*}
\mathcal{E}'(E) \hat{\otimes}_{\pi} \mathcal{E}'(F) &\approx \left( \lim_{f:\mathbb{R}^n \to E} \mathcal{E}'_f(\mathbb{R}^n) \right) \hat{\otimes}_{\pi} \left( \lim_{g:\mathbb{R}^m \to F} \mathcal{E}'_g(\mathbb{R}^m) \right) \\
&\approx \lim_{(f,g)} \mathcal{E}'_f(\mathbb{R}^n) (\hat{\otimes}_{\pi} \mathcal{E}'_g(\mathbb{R}^m)) \\
&\approx \lim_{(f,g)} \mathcal{E}'(\mathbb{R}^n \oplus \mathbb{R}^m) \tag{Kernel theorem}
\end{align*}
$$

However, the direct sum $\mathbb{R}^n \times \mathbb{R}^m$ is isomorphic to $\mathbb{R}^{n+m}$. Thus any linear continuous injective function $h: \mathbb{R}^k \to E \otimes F$ is by definition of the biproduct topology a sum $f + g: \mathbb{R}^n \oplus \mathbb{R}^m \hookrightarrow E \otimes F^4$. Indeed, as $h$ is linear we have that $h^{-1}(E, 0)$ is a sub-linear space of $\mathbb{R}^k$, that is, a Euclidean space $\mathbb{R}^n$ for $n \le k$. Thus the indexation by pairs $(f,g): \mathbb{R}^{n+m} \hookrightarrow E \times F$ coincides with the indexation by continuous injections $h: \mathbb{R}^k \hookrightarrow E \times F'$, with corresponding pre-order, and thus:

$$
\begin{align*}
\mathcal{E}'(E) \hat{\otimes}_{\pi} \mathcal{E}'(F) &\approx \lim_{f:\mathbb{R}^k \to E \times F} \mathcal{E}'(\mathbb{R}^k) \\
&\approx \mathcal{E}'(E \times F)
\end{align*}
\hfill $\square$
$$

*Proof (Lemma 1).* The morphism $d_E$ is clearly linear, and it is continuous as it is continuous on every $\mathcal{E}'_f(\mathbb{R}^n)$. We need to show that it is natural. Consider a linear continuous map $\ell: E \to F$. We must then show that $d_F \circ \ell = \ell \circ d_E$. Consider $\phi \in !E$. Then $!\ell(\phi): g \in \mathcal{E}(F) \mapsto \phi(g_{\ell \circ f})_{f:\mathbb{R}^n \to E}$, and so

$$d_F \circ !\ell(\phi) = l_F \in F' \mapsto \phi(l_F \circ \ell \circ f)_{f:\mathbb{R}^n \to E}.$$

Conversely, $\ell \circ d_E(\phi) = \ell(l_E \in E' \mapsto \phi((l \circ f)_f)$, and thus:

$$\ell \circ d_E(\phi) = \ell(l_E \in E' \mapsto \phi((l_E \circ f)_f).$$

Seeing $\ell \circ d_E(\phi) \in F$ as an element of the dual of $F'$, we have that:

$$\ell \circ d_E(\phi) =_F F' \mapsto \phi(l_F \circ \ell \circ f)_f.$$

$\square$

*Proof (Lemma 2).* The linearity is deduced by the linearity of the indexes $f: \mathbb{R}^n \to E$. The continuity follows from the one of $D_0$. To prove naturality, we must prove that for any linear continuous function $\ell: E \to F$ we have: $!\ell \circ d_E = d_F \circ \ell$. Consider a family $(g_g)_g \in \mathcal{E}(F) \approx \lim_{g \in \mathcal{G}} C_g^\infty(\mathbb{R}^m)$ and $x \in E$. On one hand $d_F \circ \ell(x)$ maps $(g_g)_g$ to $D_0 g_g(g^{-1}(\ell(x)))$ when $\ell(x)$ is in the image of $g$. On the other hand, $!\ell \circ d_E(x)$ maps $(g_g)_g$ to $d_E(x)((g_{\ell \circ f})_{f:\mathbb{R}^n \to E}) = D_0 g_{\ell \circ f}(f^{-1}(x))$ when $x$ is in the image of $f$. Thus when we consider $g = \ell \circ f$, which has $x$ in his image, we have that

$$(!\ell \circ d_E(x))((g_g)_g) = (d_F \circ \ell(x))((g_g)_g).$$

$\square$

<footnote n="4">⁴ Notice here the link between direct sum, biproduct and sums of smooth functions $f: \mathbb{R}^K \to E$ and $g: \mathbb{R}^k \to F$, as exposed in [8].</footnote>
*Proof (Lemma 3).* Consider a linear continuous function $\ell : E \to F$ between two lcs. We need to show that we have an equality between the functions $\mu_F \circ !\ell$ and $!!\ell \circ \mu_E$. On one hand, we have for $\phi \in !E$ and $(g_g)_g \in \mathscr{E}(!F)$,

$$ (\mu_F \circ !\ell)(\phi)((g_g) = g_g(g^{-1}([((h_h)_h \in \mathscr{E}(F) \mapsto \phi(h_{\ell \circ f})_h]))$$

On the other hand,

$$ 
\begin{align*}
(!!\ell \circ \mu_E)(\phi) &= !!\ell(((h_{h:\mathbb{R}^m} \longrightarrow !E) \mapsto h_h(h^{-1}((\phi_f)_f)))) \\
&= (g_g)_g \mapsto [(((h_{h:\mathbb{R}^m} \longrightarrow !E) \mapsto h_h(h^{-1}((\phi_f)_f))) (g_{!\ell \circ h})_h \\
&= (g_g)_g \mapsto g_{!\ell \circ h}((h)^{-1}(\phi_f)_f)))
\end{align*}
$$

By denoting $g = !\ell \circ h$, we have $h = (!\ell)^{-1} \circ g$ on the image of $!\ell$, and thus

$$ 
\begin{align*}
(!!\ell \circ \mu_E)(\phi)(g_g)_g &= g_{!\ell \circ h}((h)^{-1}(\phi_f)_f)) \\
&= g_g(g^{-1} \circ !\ell((\phi_f)_f))
\end{align*}
$$

where the last line results exactly in $g_g(g^{-1}([((h_h)_h \in \mathscr{E}(F) \mapsto \phi(h_{\ell \circ f})_h]))$ by definition of $!\ell$. $\square$

*Proof (Proposition 6).* We want to check that $d_{!E} \circ \mu_E = \text{Id}_{!E}$. Consider $\phi \in !E$. On one hand, we have $d_{!E} \circ \mu_E(\phi) : \mathbf{h} \in \mathscr{E}'(E)' \mapsto (\mu^E(\phi))(\mathbf{h} \circ g)_{g:\mathbb{R}^n \to !E}$, thus $d_{!E} \circ \mu_E(\phi)(\mathbf{h}) = (\mathbf{h} \circ g(g^{-1}(\phi)))$ when $\phi \in \text{Im}(g)$, thus $d_{!E} \circ \mu_E(\phi)(\mathbf{h}) = \mathbf{h}(\phi)$. Through the isomorphism $!E \simeq (!E)'$, we obtain that:

$$ d_{!E} \circ \mu_E = \text{Id}_{!E}. \qquad \square $$

*Proof (Theorem 4).*

- We already proved that $d \circ \bar{d} = \text{Id}$. It is immediate that $\delta_0(\mathbf{1}) = 1$ and thus $w_e \circ \bar{w}_E = \text{Id}_1$ for any $E$.

- For any lcs $E$ and any $x \in E$, one has $w \circ \bar{d}(x) = ((\mathbf{f}_f)_f \mapsto D_0(\mathbf{f}_f(f^{-1}(x))))(\mathbf{1})$, that is $w \circ \bar{d}(x)$ is the differential of a constant function at some point, thus equals 0, and $w \circ \bar{d} = 0$. Likewise, $d_x \circ \bar{w}_x(1) = (\ell \in E' \mapsto \ell \circ f(0))$ for any $f \cdot \mathbb{R}^m \hookrightarrow E$. As both $f$ and $\ell$ are linear, we have $\ell \circ f(0) = 0$ and thus $d_E \circ \bar{w}_E = 0$.

- Let us prove that $d \otimes w + w \otimes d = d \circ \bar{c}$. Consider $\phi, \psi \in !E$. Then by definition :

$$ d \circ \bar{c}(\phi \otimes \psi) = \phi((x \mapsto \psi((y \mapsto (\ell \circ f)(x) + (\ell \circ f')(y))_{f'}))_{f}) $$

But $(\ell \circ f)(x)$ acts as a constant in the domain of $\psi$, thus

$$ \psi((y \mapsto (\ell \circ f)(x) + (\ell \circ f')(y))_{f'}) = \psi(\mathbf{1})(\ell \circ f(x)) + \psi((\ell \circ f')_{f'}). $$
With the same considerations for $\phi$ and $f'$ we get :

$$d \circ \bar{c}(\phi \otimes \psi) = \phi((\ell \circ f)_f)\psi(\mathbf{1}) + \phi(\mathbf{1})\psi((\ell \circ f')_f) = d \otimes w + w \otimes d(\phi \otimes \psi).$$

- Let us prove that $\bar{d} \otimes \bar{w} + \bar{w} \otimes \bar{d} = c \circ \bar{d}$. Consider $x \in E$. Then through Schwartz kernel theorem we have :

$$ \begin{aligned} c(\bar{d}(x))(\mathbf{f} \otimes \mathbf{g} \in \mathcal{E}(E) \otimes \mathcal{E}(E)) &= \bar{d}(x) ((\mathbf{f}_h \cdot \mathbf{g}_h)_{h:\mathbb{R}^k \hookrightarrow E}) \\ &= D_0(\mathbf{f}_h \cdot \mathbf{g}_h)(h^{-1}(x)) \\ &= D_0(\mathbf{f}_h)(h^{-1}(x))\mathbf{g}_h(0) + \mathbf{f}_h(0)D_0(\mathbf{g}_h)(h^{-1}(x)) \\ &= \bar{d} \otimes \bar{w} + \bar{w} \otimes \bar{d}(x)(\mathbf{f} \otimes \mathbf{g}) \end{aligned} $$

thus the desired result.

*Proof (Proposition 8).*

1. As nuclear (F)-space are reflexive, and as reflexive spaces are stables by projective limit (proposition 1), a LNF space is reflexive.

2. This follows from the fact that completed tensor product preserves projective limits [12, 15.4.1], and by the fact that nuclear and (DF)-spaces are stable by projective tensor product ([12, 21.2.3] and [12, 12.4.8]).

3. Again, by [12, 8.8.12], the dual $E'$ of a LNF-space $E = \lim_{\underset{i}{\longrightarrow}} E_i$ identifies as a linear space to a projective limit of complete nuclear (DF)-spaces. As the limit $\lim_{\underset{i}{\longrightarrow}} E_i$ is regular, we have that any bounded set in $E$ is bounded in some of the $E_i$. Thus the strong topology on $E'$ coincide with the projective topology. □