Higher-Order Distributions for Differential Linear Logic

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.

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.

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 $\lambda$-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 ($\mathrm {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, $\mathrm {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 $\mathrm {DiLL}$ has a “smooth" semantical interpretation where the exponential (the central object of Linear Logic) is interpreted as a space of distributions with compact support [18]. This semantical interpretation of $\mathrm {DiLL}$ (along with the Linear Logic typed phenomena of duality and interaction) provides a strong argument that $\mathrm {DiLL}$ should be considered as a foundation 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 programming 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 languages 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, following 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 $\mathcal {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 ($\mathrm {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 $\mathrm {DiLL}$ by general topological vector spaces and non-linear proofs by smooth functions. The interpretation of the involutive linear negation of $\mathrm {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, . 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 $\mathrm {DiLL}$ structured as chirality [17]. This polarized structure is also necessary here. In Sect. 5, formulas of $\mathrm {DiLL}_0$ 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 is defined as the inductive limit of spaces $\mathcal {C}^\infty (\mathbb {R}^n, \mathbb {R})'$, indexed by linear continuous functions $f: \mathbb {R}^n \multimap E$ (Definition 7),

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

An important drawback of this work is that the functoriality of is ensured only on isomorphisms, that is, is an endofunctor on the category $\textsc {Refl} _{iso}$ 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 ($\mathrm {DiLL}_0$), that is, $\mathrm {DiLL}$ without the promotion rule. We also discuss how this construction also leads to a polarized model of $\mathrm {DiLL}_0$ (Sect. 5).

Organization of the Paper. Section 2 gives an overview of the development in $\mathrm {DiLL}$ which led to this paper and gives some background in functional analysis. In Sect. 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 Sect. 5 we discuss the polarized interpretation of formulas.

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

2 Preliminaries

2.1 Differential Linear Logic and Its Semantics

Linear Logic [9] refines Intuitionistic Logic with a linear negation, $(-)^\bot$, and a notion of linearity of proofs, $\multimap$. More precisely, Linear Logic introduces the fundamental isomorphism between $A \Rightarrow B$, proofs of B from A, and , linear proofs of B from 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:

Differential Linear Logic ($\mathrm {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:

In Linear Logic, the exponential group also features weakening and contraction rules. While $\mathrm {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). $\mathrm {DiLL}$ without promotion, or finitary Differential Linear Logic, is denoted $\mathrm {DiLL}_0$ and is the original version of Differential Linear Logic by Ehrhard and Regnier [7]. Its exponential rules for $\{?,!\}$ can be found in Fig. 1. The other rules of $\mathrm {DiLL}_0$ correspond to the usual ones for the MALL group . Non-finitary $\mathrm {DiLL}$ can be constructed by adding the promotion rule to $\mathrm {DiLL}_0$, which in particular requires functoriality of the exponential. Cut-elimination in $\mathrm {DiLL}$ and $\mathrm {DiLL}_0$ generates sums of proofs [7], and therefore the categorical interpretation of proofs must be done in a category enriched over commutative monoids.

Fig. 1.

Exponential rules of $\mathrm {DiLL}_0$

Following Fiore’s definition in [8], a categorical model of $\mathrm {DiLL}$ is an extension of Seely’s axiomatization of categorical models of Linear Logic [20]. Explicitly a model of $\mathrm {DiLL}$ consists of a $*$-autonomous category $(\mathcal {L}, \otimes , 1, (\_)^*)$ with a finite biproduct structure $\times$ with zero object 0, a strong monoidal comonad , and a natural transformation , 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 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 $\mathrm {DiLL}_0$ but not of $\mathrm {DiLL}$. The main reason for this is that in the formula

$$\mathscr {E}'(E):= \varinjlim _{f: \mathbb {R}^n \multimap E} \mathscr {E}'_f(\mathbb {R}^n),$$

injectivity of the indexes $f: \mathbb {R}^n \multimap 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 $\textsc {Refl} _{iso}$, the category of reflexive spaces and linear continuous isomorphisms between them.

Models of $\mathrm {DiLL}_0$ 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 axiomatization of Seely’s models.

Definition 1

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

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:

The above commutative diagrams allow for a direct interpretation of the cut-elimination process of $\mathrm {DiLL}_0$. Ehrhard shows in particular that the interpretation of the structural and co-structural rules of $\mathrm {DiLL}_0$ only needs the functoriality of the exponential on the isomorphisms [6, Sect. 2.5]. Indeed, in a classical model of $\mathrm {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 on each object [7, Sect. 2.6]. To sum up:

That we have a model of $\mathrm {DiLL}_0$ and not of $\mathrm {DiLL}$ fits well with our motivation, as we are looking for the computational counterpart of type theories modeled by analysis. $\mathrm {DiLL}_0$ 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 $\mathrm {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 $\mathrm {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 \rightarrow E''$ be the transpose of the evaluation map in $E'$, which is explicitly defined as follows:

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 reflexivity 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 \rightarrow \mathbb {R}$ is said to be smooth if it is infinitely differentiable. Let $\mathcal {E}(\mathbb {R}^n)= \mathcal {C}^\infty (\mathbb {R}^n, \mathbb {R})$ denote the space of all smooth functions $f: \mathbb {R}^n \rightarrow \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 \mathscr {E}(\mathbb {R}^n) \otimes \mathscr {E}(\mathbb {R}^m) \mapsto f \cdot g \in \mathscr {E}(\mathbb {R}^{n+m})$ is in fact an isomorphism on the completed tensor product $\mathscr {E}(\mathbb {R}^n) \hat{\otimes }\mathscr {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 $\mathrm {DiLL}_0$ in which the exponential is interpreted as a space of distributions: .

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

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 \hookrightarrow E}$ and $g: \mathbb {R}^m \hookrightarrow E$ be two linear continuous injective functions. We say that $f \leqslant g$ when $n \leqslant m$ and $f = g_{|\mathbb {R}^n}$, that is, $f = g \circ \iota _{n,m}$ where $\iota _{n,m}: \mathbb {R}^n \rightarrow \mathbb {R}^m$ is the canonical injection.

The ordering $\leqslant$ in the above definition provides an order on the set of dependent pairs (n, f) where $n \in \mathbb {N}$ and $f: \mathbb {R}^{\mathbb {N}} \hookrightarrow 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 \multimap E$, define the $lcs$ $\mathscr {E}'_f(\mathbb {R}^n)$ as follows:

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

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

  $$ \mathscr {E}'(E):= \varinjlim _{f: \mathbb {R}^n \multimap E} \mathscr {E}'_f(\mathbb {R}^n) $$

  that is, the inductive limit [12, Chapter4.5] (or colimit) in the category $\textsc {TopVec}$ of the family of $lcs$ $\{ \mathscr {E}'_f(\mathbb {R}^n) \vert f: \mathbb {R}^n \multimap E~linear~continuous~injective\}$  directed under the inclusion maps defined as

  $$S_{f,g}: \mathscr {E}'_g(\mathbb {R}^n) \rightarrow \mathscr {E}'_f(\mathbb {R}^m), \phi \mapsto ( h \mapsto \phi ( h \circ \iota _{n,m})) $$

  when $f \leqslant g$.

Intuitively this definition of $\mathscr {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, $\mathscr {E}'(E)$ is a reflexive lcs.

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

Proposition 3

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

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

Definition 8

For a reflexive lcs E, let $\mathscr {E}(E)$ denote the strong dual of $\mathscr {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, $\mathscr {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 \multimap E$, define the lcs $\mathscr {E}_f(\mathbb {R}^n):= \mathcal {C}^\infty (\mathbb {R}^n)$. Then we have the following linear homeomorphism:

$$\mathscr {E}(E) \simeq \varprojlim _{f: \mathbb {R}^n \multimap E} \mathscr {E}_f( \mathbb {R}^n)$$

where the lcs on the right is the projective limit [12, Chapter 2.6] in $\textsc {TopVec}$ of the family of lcs $\{\mathscr {E}_f(\mathbb {R}^n) \vert ~ f: \mathbb {R}^n \multimap E ~linear~continuous~injective \}$ with projections defined as:

$$T_{g,f} = S_{f,g}': \mathscr {E}_g(\mathbb {R}^m) \rightarrow \mathscr {E}_f(\mathbb {R}^n), \mathbf g \mapsto \mathbf g \circ \iota _{n,m}$$

when $f \leqslant g$.

The elements of $\mathbf f \in \mathscr {E}(E)$ are families $\mathbf f := (\mathbf f _f)_{f: \mathbb {R}^n \multimap E}$ such that if $f \leqslant 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 \rightarrow \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 \subset [| 1, n |] } a_{\alpha } x_1^{\alpha ^1} \dots x_n^{\alpha ^I_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 $\mathscr {E}(\mathbb {R}^n)$ as

$$ h \in \mathscr {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 \multimap E'= \mathscr {E}'(\mathbb {R}^n)$ as defined in Definition 4.

The Kernel Theorem. We now provide the Kernel theorem for spaces $\mathscr {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 }$. While we do not provide a proof here, we would like to highlight that the proof of this theorem 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:

$$\mathscr {E}(E) \hat{\otimes }_{\pi } \mathscr {E}(F) \simeq \mathscr {E}( E \oplus F).$$

We now give the definitions of functors and , 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 $\textsc {Refl} _{iso}$ denote the category of reflexive lcs and linear homeomorphism between them.

Definition 9

Define the endofunctor as follows:

(1)

where for $\mathbf f \in \mathscr {E}(E')$, the $g: \mathbb {R}^m \multimap F'$ component of is defined as:

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

Note that is defined by the universal property of the projective limit, that is, is uniquely defined by post-composing by the projections $\pi _g: \mathscr {E}(F') \rightarrow \mathscr {E}(\mathbb {R}^n)$ for each linear continuous injective function $g: \multimap F'$. We also note that $\mathbf 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 is an isomorphism and that is functorial.

Definition 10

Define the functor on objects as and on isomorphisms as . Explicitly, is defined as follows:

(2)

where for the $f: \mathbb {R}^n \multimap E$ component of $\mathbf f \in \mathscr {E}'(E)$, is defined as:

As before, is defined by the co-universal property of the inductive limit, that is, is defined by pre-composition with the injections $\iota _{f}: \mathscr {E}'_f(\mathbb {R}^n) \hookrightarrow \mathscr {E}'(E)$ for every linear continuous injective function $f: \mathbb {R}\multimap E$. Functoriality of is ensured by functoriality of and reflexivity of the objects.

4 Structural Morphisms on the Exponential

We consider the exponential from the $\mathrm {DiLL}$ model of convenient vector spaces in [2] as a guideline for defining the structural morphisms on . 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 $\left( (\mathbf {f}_f)_f \in \mathscr {E}(E') \mapsto \mathbf {f}( f^{-1}(x) \right) \in \mathscr {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:

(3)

We stress that $d_E$ is a map in $\textsc {Refl}$ and not a map in $\textsc {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 \multimap \mathbb {R}$, and thus is smooth and belongs in particular to $\mathscr {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:

(4)

Lemma 1

The morphisms $d_E$ are natural with respect to linear homeomorphisms, that is, maps of $\textsc {Refl} _{iso}$. Explicitly, if $\ell : E \rightarrow F \in \textsc {Refl} _{iso}$ then .

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

$$\begin{aligned} D_0:\left\{ \begin{aligned} \mathcal {C}^\infty (\mathbb {R}^n)&\rightarrow (\mathbb {R}^n)' \\ \mathbf {f}&\mapsto \left( v \in \mathbb {R}^n \mapsto \lim \limits _{t \rightarrow 0} \frac{f(tx)- f(0)}{t} = \sum _{i=1}^n \frac{\partial f}{\partial x_i}(0) v_i \right) \end{aligned} \right. \end{aligned}$$

The operator $D_0$ is linear in $\mathbf {f} \in \mathcal {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 \mathcal {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:

(5)

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 \leqslant 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{aligned} 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) ))\qquad \qquad \qquad {(\text {as } \iota _{n,m} \text { is linear)}} \\&= D_0 \mathbf {f}_g ( g^{-1}(x) )) \end{aligned}$$

As any pair of of linear functions $f: \mathbb {R}^n \multimap E$ and $g: \mathbb {R}^m \rightarrow E$ is bounded by $f \times g: \mathbb {R}^{n+m} \rightarrow 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{aligned} \begin{aligned} \mathscr {E}(E')&\rightarrow E'' \simeq E \\ (\mathbf f _f)_{f: \mathbb {R}^n \multimap E'}&\mapsto ( \ell \in E' \mapsto D_0 \mathbf f _f ( f^{-1} ( \ell ) ) \end{aligned} \end{aligned}$$

(6)

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

Lemma 2

The morphisms $\bar{d}_E$ are natural with respect to linear homeomorphisms, that is, maps of $\textsc {Refl} _{iso}$. Explicitly, if $\ell : E \rightarrow F \in \textsc {Refl} _{iso}$ then .

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 lcs E, $d_E \circ \bar{d}_E = 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.

According to [8], the rules c and $\bar{c}$ are interpreted respectively via the kernel theorem and pre-composition with the diagonal $E \rightarrow E \times E$ and co-diagonal $E \times E \rightarrow 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.

Theorem 4

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

We note that this does not give an exponential structure per say since $\textsc {Refl}$ is not a monoidal category, as we will explain in Sect. 5. That said, in Sect. 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 co-monad . 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:

(7)

This is well defined, as we can show as for the codereliction (5) that the term $\mathbf {g}_g(g^{-1} (\phi ))$ is unique when linear and $\mathbf {g}_g \in \mathcal {C}^\infty _g(\mathbb {R}^m)$ varies. Moreover there is at least one linear function which has $\phi$ in its image.

Lemma 3

The morphisms $\mu _E$ are natural with respect to linear homeomorphisms, that is, maps of $\textsc {Refl} _{iso}$. Explicitly, if $\ell : E \rightarrow F \in \textsc {Refl} _{iso}$ then .

Proposition 6

For any reflexive lcs E,

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 $\mathrm {DiLL}_0$

In Sect. 4 we defined the structural morphisms on the exponential and proved the equations allowing to interpret proofs of $\mathrm {DiLL}_0$ by morphisms in $\textsc {Refl}$, independent of cut-elimination. We now detail which categories allow to interpret formulas of $\mathrm {MALL}$. This will be done in a polarized setting generalizing the one of [14].

Polarization. So far we have constructed an exponential which is strong monoidal. However, the category of reflexive spaces is too big to give us a model of $\mathrm {DiLL}_0$. 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 reflexivity follows from a more restrictive class of spaces. These spaces are however not stable by duality, thus resulting in a polarized model of $\mathrm {DiLL}_0$.

In this section we briefly show how the techniques develop above constructs a polarized model of $\mathrm {DiLL}_0$. The syntax of polarized (Differential) Linear Logic [16] is recalled below. A distinction is made between positive formulas (preserved by $\otimes$ and $\oplus$) and negative formulas (preserved by and ). The same deduction rule apply.

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 $\times$ and coproduct $\oplus$ 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 $\mathscr {E}(\mathbb {R}^n)$, while typical examples of nuclear (DF)-spaces are the spaces of distributions with compact support $\mathscr {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 Sect. 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 $\textsc {LNF}$. A lcs E is said to be a $\textsc {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 $\textsc {Lndf}$-space.

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

The difficulty of constructing a model of $\textsc {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 $\mathscr {E}(\mathbb {R}^n)$ and $\mathscr {E}'(\mathbb {R}^n)$, most of these tensor product coincide with one another. In [14], both multiplicative connectors ($\otimes$ and ) 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 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:

and shows that 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 $\mathrm {DiLL}$ without higher order constructed in [14] to a higher-order polarized model of $\mathrm {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 $\mathrm {LL}$ – this could be done through epi-mono decomposition of arrows in $\textsc {Refl}$. Another task is to properly work out which tensor product of reflexive space will provide a model of $\mathrm {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 $\mathrm {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.