Higher-Order Distributions for Differential Linear Logic

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 .

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).

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.

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\).

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

As \(\mathscr {E}'(E)\) is reflexive, we give a special (yet obvious) notation for 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.

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: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)\) astaking 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].

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.

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.

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.

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.

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):

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.

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:

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 }\).

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.