On the denotational semantics of Linear Logic with least and greatest fixed points of formulas

TL;DR

This paper develops a denotational semantics for Linear Logic with fixed points across various models, and demonstrates how G{"o}del System T can be embedded into it, highlighting its expressive power.

Contribution

It introduces a unified denotational semantics for Linear Logic with fixed points and embeds G{"o}del System T, enhancing understanding of their expressive capabilities.

Findings

Denotational semantics for LL with fixed points in coherence spaces and totality models.

Embedding of G{"o}del System T into LL with fixed points.

Demonstrates expressive power and normalization properties of the system.

Abstract

We develop a denotational semantics of Linear Logic with least and greatest fixed points in coherence spaces (where both fixed points are interpreted in the same way) and in coherence spaces with totality (where they have different interpretations). These constructions can be carried out in many different denotational models of LL (hypercoherences, Scott semantics, finiteness spaces etc). We also present a natural embedding of G{\"o}del System T in LL with fixed points thus enforcing the expressive power of this system as a programming language featuring both normalization and a huge expressive power in terms of data types.

Equations

$${\mathsf{n}}_{X_1,X_2}^2=\left(\text{oc}{\pi }_1\otimes \text{oc}{\pi }_2\right){\mathrm{contr}}_{X_1\&X_2}$$

$$\begin{array}{rl}{w}_{X_1\&X_2}{\mathsf{m}}_{X_1,X_2}^2& =w_{X_1}\otimes w_{X_2}\\ {\mathrm{der}}_{X_1\&X_2}{\mathsf{m}}_{X_1,X_2}^2& =⟨{\mathrm{der}}_X\otimes w_Y,w_X\otimes {\mathrm{der}}_Y⟩\\ {\mathrm{contr}}_{X_1\&X_2}{\mathsf{m}}_{X_1,X_2}^2& =\left({\mathsf{m}}_{X_1,X_2}^2\otimes {\mathsf{m}}_{X_1,X_2}^2\right){\gamma }_{2,3}\left({\mathrm{contr}}_X\otimes {\mathrm{contr}}_Y\right)\end{array}$$

Full text

1. Introduction

Propositional Linear Logic is a well-established logical system introduced by Girard in [Girard87]. It provides a fine-grain analysis of proofs in intuitionistic and classical logic, and more specifically of their cut-elimination. $\mathsf{LL}$ features indeed a well-behaved logical account of the structural rules (weakening, contraction) which are handled implicitly in intuitionistic and classical logic. For this reason, $\mathsf{LL}$ has many useful outcomes in the Curry-Howard based approach to the theory of programming: logical understanding of evaluation strategies (CBN and CBV correspond to two different translations from the lambda-calculus into $\mathsf{LL}$, and such translations extend naturally to abstract machines), new presentation of proofs/programs (proof-nets), connections with other branches of mathematics (linear algebra, differential calculus etc), new operational semantics (geometry of interaction)…

However, just as the simply typed lambda-calculus, propositional $\mathsf{LL}$ is not a reasonable programming language, by lack of data-types and iteration or recursion principles. This is usually remedied by extending propositional $\mathsf{LL}$ to the $2^{\mathrm{nd}}$ order, thus defining a logical system in which Girard’s System $\mathsf{F}$ [Girard89] can be embedded. As explained in [Girard89] for System $\mathsf{F}$, this extension allows to represent many data-types, for instance the type of natural numbers can be written as $\iota=\forall\zeta\,{\oc{({\oc{\zeta}}\multimap{\zeta}})}\multimap{{\oc{\zeta}}\multimap{\zeta}}$, and then integers are represented as Church numerals. The resulting logical system is extremely expressive in terms of representable computable functions: all functions ${\mathbb{N}}\to{\mathbb{N}}$ whose totality can be proven in second order arithmetics are representable. In contrast, its algorithmic expressiveness seems quite poor: as is well-known it is not possible to write a term ${\oc{\iota}}\multimap{\iota}$ which computes the predecessor function in one (or a uniformly bounded) number of reduction steps.

Another option to turn propositional $\mathsf{LL}$ into a programming language is to extend it with least and greatest fixed points of formulas. The kind of extension has early been suggested by Girard in an unpublished note [Girard92], though the first comprehensive proof-theoretic investigation of such an extension of $\mathsf{LL}$ is rather recent [Baelde12]: Baelde considers an extension of Multiplicative Additive $\mathsf{LL}$ sequent calculus with least and greatest fixed points, axiomatized by means of two deduction rules. His main motivation for introducing this extension of $\mathsf{LL}$ comes from the need of powerful logical systems for formal verification of programs and the investigations on $\mu\mathsf{LL}$ were carried out mainly from a proof-search perspectives (cut-elimination, focusing etc). However from a Curry-Howard viewpoint, fixed points allow to define inductive data-types (integers, lists, trees) and coinductive types (streams and other infinite structures). So $\mu\mathsf{LL}$ can also be considered as a programming language and it is this approach that we develop in this paper. Admittedly the rules associated with fixed points are complex (this is especially true of the $\nu$-introduction rule, the Park’s rule) and lead to subtle cut-elimination proof rewrite rules for which Baelde could prove a restricted form of cut-elimination, sufficient for establishing for instance that a proof of the type of integers $\mu\zeta\,({1}\oplus{\zeta})$ necessarily reduces to an integer. There are also alternative proof-systems for the same logic, involving infinite or cyclic proofs, see [BaeldeDoumaneSaurin16], whose connections with the aforementioned finitary proof-system are not completely clear.

Since the proof-theory (and hence the “operational semantics”) of $\mu\mathsf{LL}$ is sophisticated and still under development, it is particularly important to investigate its denotational semantics, whose definition does not rely on the rewrite system $\mu\mathsf{LL}$ is equipped with. We develop here a semantics of $\mu\mathsf{LL}$ using coherence spaces [Girard87] equipped with a notion of totality: our model accounts for the termination of computations in $\mu\mathsf{LL}$ and interprets least and greatest fixed points in different ways. It presents some similarities with the game-theoretic model of Clairambault [Clairambault09, Clairambault13] of intuitionistic logic with least and greatest fixed points (see below).

Girard introduced coherence spaces in [Girard86] in his denotational study of System $\mathsf{F}$. In this model, types (with free variables) are interpreted as continuous (actually, stable) functors on a category of coherence spaces and embedding-retraction pairs. Our basic observation is that such functors admit “least fixed points” in a categorical sense. In the case of $\mu\mathsf{LL}$ we have to depart from Girard’s setting because formulas must act on proofs and not only on embedding-retraction pairs: given a formula $F$ and a proof $\pi$ of ${A}\multimap{B}$, $\mu\mathsf{LL}$ uses crucially a proof ${F}\left[{\pi}/{\zeta}\right]$ of ${{F}\left[{A}/{\zeta}\right]}\multimap{{F}\left[{B}/{\zeta}\right]}$ defined by induction on $F$ (syntactic functoriality). This means that the functors interpreting formulas must act on all stable morphisms, and not only on embedding-retraction pairs. This is made possible by the fact that, in $\mu\mathsf{LL}$, type variables have only positive occurrences in formulas.

$\mu\mathsf{LL}$ has a construction $\mu\zeta\,F$ for least fixed points and a dual construction $\nu\zeta\,F$ for greatest fixed points. The logical rule for introducing $\nu\zeta\,F$ allows to deduce $\vdash{A^{{\mathord{\perp}}},\nu\zeta\,F}$ from $\vdash{A^{{\mathord{\perp}}},{F}\left[{A}/{\zeta}\right]}$ (Park’s Rule). We prefer to consider a slightly generalized version of this rule: deduce $\vdash{\wn{\Gamma},A^{{\mathord{\perp}}},\nu\zeta\,F}$ from $\vdash{\wn{\Gamma},A^{{\mathord{\perp}}},{F}\left[{A}/{\zeta}\right]}$ (which does not increase expressiveness but makes the embedding of functional formalisms such as Gödel’s System $\mathsf{T}$ in $\mu\mathsf{LL}$ much more natural). We need therefore a version of syntactic functoriality which accommodates these additional contexts $\wn{\Gamma}$. The denotational counterpart is that our functors interpreting types are equipped with a strength (as in [Clairambault09, Clairambault13], and essentially for the same reason). All together, these requirements lead to the definition of a variable coherence space (VCS). Such a functor has a fixed point which is at the same time an initial algebra and a final coalgebra, meaning that $\mu\zeta\,F$ and $\nu\zeta\,F$ have the same interpretation.

This first model, based on coherence spaces, admits morphisms which are not total (for instance the interpretation of ${\iota}\multimap{\iota}$, where $\iota=\mu\zeta\,({1}\oplus{\zeta})$ is the type of integers, contains non total functions ${\mathbb{N}}\to{\mathbb{N}}$). Following [Girard86] we equip our coherence spaces with a semantic notion of totality. We introduce accordingly variable coherence spaces with totality which are VCS’s equipped with a functorial notion of totality. Using Knaster-Tarski Theorem, we show that these functors have least and greatest fixed points, which now are distinct in general. The benefit of such models is that they give an abstract and compositional account of normalization: the interpretation of any proof $\pi$ of $\vdash{\iota}$ is an integer, which is the normal form of $\pi$: the model “computes” this integer without reducing the proof.

Contents

In Section 2 we recall basic categorical notions essential in the paper: Seely categories, Eilenberg-Moore and Kleisli categories of the exponential, strong functors and their extension to categories of comodules and, last, initial algebras (least fixed points) and final coalgebras (greatest fixed points) of (strong) functors. Section LABEL:sec:coherence-spaces is devoted to a general presentation of coherence spaces and to a well behaved notion of strong functors on coherence spaces admitting fixed points (Variable Coherence Spaces, VCSs). In this setting, there is no distinction between least fixed points and greatest fixed points, due to the presence of partial computations in the model. Section LABEL:sec:coh-tot endows coherence spaces with a notion of totality rejecting such partial morphisms and introduces an adapted notion of variables types (VCSTs), giving rise to a clear distinction between least and greatest fixed points in this model $\mathbf{CohT}$. In Section LABEL:sec:MULL we present $\mu\mathsf{LL}$ and various associated concepts: functorial extension of formulas, cut elimination, interpretation of formulas and proofs in the model $\mathbf{CohT}$. The idea that a semantic notion of totality enforces a distinction between least and greatest fixed points is of course not new, it is essential for instance in [Clairambault09, Clairambault13]. In Section LABEL:sec:examples we present various examples, stressing in particular that Gödel’s System $\mathsf{T}$ can be embedded in $\mu\mathsf{LL}$ (following Clairambault [Clairambault13]) and hence showing that this system has a significant expressive power from the viewpoint of the Curry-Howard correspondence. We also analyze in our model the encoding of exponentials using least and greatest fixed points proposed in [Baelde12]; we show in particular that these exponentials do not give rise to a Seely category, thus justifying our choice of considering the whole system $\mu\mathsf{LL}$, with exponentials. As an outcome of the paper, Section LABEL:sec:generalizations introduces a quite simple and general notion of categorical model of classical $\mu\mathsf{LL}$, of which the model $\mathbf{CohT}$ is an instance.

Related work

Most importantly, we want to mention again the work of Pierre Clairambault (see [Clairambault09] and the long version [Clairambault13]) who investigates the denotational semantics of an extension of intuitionistic logic with least and greatest fixed points. Our categorical notion of model of classical $\mu\mathsf{LL}$ of Definition LABEL:def:categorical-muLL-models can probably be seen as a “linearized version” of his notion of $\mu$-closed category (an extension of the notion of cartesian closed categories with least and greatest fixed points) — perhaps through some kind of Kleisli construction — though our setting seems simpler as we do not need contravariant strong functors, only covariant ones. The concrete model considered by Clairambault is based on games and features a notion of totality guaranteeing that all computations terminate and enforcing the distinction between least and greatest fixed points, just as in the present work. Due to technical limitations intrinsically related to game semantics, Clairambault’s model is restricted to the pseudo-polynomial fragment where free variables never appear at the right hand side of an implication. No such limitations are necessary in our coherence space interpretation.

Remark 1*.*

We use the following notational conventions: $\vec{a}$ stands for a list $(a_{1},\dots,a_{n})$. When we write natural transformations, we very often omit the objects where they are taken and prefer to keep these objects implicit for the sake of readability, because they can easily be retrieved from the context. If $\mathcal{F}:\mathcal{A}\times\mathcal{B}\to\mathcal{C}$ is a functor and $A$ is an object of $\mathcal{A}$ (notation $A\in\mathcal{A}$) then $\mathcal{F}_{A}:\mathcal{B}\to\mathcal{C}$ is the functor defined by $\mathcal{F}_{A}(B)=\mathcal{F}(A,B)$ and $\mathcal{F}_{A}(f)=\mathcal{F}(\operatorname{\mathsf{Id}}_{A},f)$.

2. Categorical models of $\mathsf{LL}$

A model of $\mathsf{LL}$ consists of the following data (our main reference is the notion of a Seely category as presented in [Mellies09]. We refer to that survey for all the technical material that we do not record here).

A symmetric monoidal closed category $(\mathcal{L},\otimes,1,\lambda,\rho,\alpha,\gamma)$ where $\lambda_{X}\in\mathcal{L}({1}\otimes{X},X)$, $\rho_{X}\in\mathcal{L}({X}\otimes{1},X)$, $\alpha_{X,Y,Z}\in\mathcal{L}({({X}\otimes{Y})}\otimes{Z},{X}\otimes{({Y}\otimes{Z})})$ and $\gamma_{X,Y}\in\mathcal{L}({X}\otimes{Y},{Y}\otimes{X})$ are natural isomorphisms satisfying coherence diagrams that we do not record here. We use ${X}\multimap{Y}$ for the object of linear morphisms from $X$ to $Y$, $\operatorname{\mathsf{ev}}\in\mathcal{L}({({X}\multimap{Y})}\otimes{X},Y)$ for the evaluation morphism and $\mathsf{cur}$ for the linear curryfication map $\mathcal{L}({Z}\otimes{X},Y)\to\mathcal{L}(Z,{X}\multimap{Y})$. We assume this SMCC to be $*$-autonomous with dualizing object $\mathord{\bot}$. We use $X^{{\mathord{\perp}}}$ for the object ${X}\multimap{\mathord{\bot}}$ of $\mathcal{L}$ (the dual, or linear negation, of $X$).

$\mathcal{L}$ is cartesian with final object $\top$, product $({X_{1}}\mathrel{\&}{X_{2}},(\pi_{i}:{X_{1}}\mathrel{\&}{X_{2}}\to X_{i})_{i=1,2})$. By $*$-autonomy $\mathcal{L}$ is cocartesian with initial object [math], coproduct $\oplus$ and injections $\overline{\pi}_{i}$.

We are given a comonad $\oc{\_}:\mathcal{L}\to\mathcal{L}$ with counit $\operatorname{\mathsf{der}}_{X}\in\mathcal{L}(\oc{X},X)$ (dereliction) and comultiplication $\operatorname{\mathsf{dig}}_{X}\in\mathcal{L}(\oc{X},\oc{\oc{X}})$ (digging) together with a strong symmetric monoidal structure (Seely natural isos $\mathsf{m}^{0}:1\to\oc{\top}$ and $\mathsf{m}^{2}$ with $\mathsf{m}^{2}_{X_{1},X_{2}}:{\oc{X_{1}}}\otimes{\oc{X_{2}}}\to\oc({{X_{1}}\mathrel{\&}{X_{2}}})$, we use $\mathsf{n}^{0}$ and $\mathsf{n}^{2}_{X_{1},X_{2}}$ for the inverses of these isos) for the functor $\oc{\_}$, from the symmetric monoidal category $(\mathcal{L},\mathrel{\&})$ to the symmetric monoidal category $(\mathcal{L},\otimes)$ satisfying an additional coherence condition wrt. $\operatorname{\mathsf{dig}}$. It is also important to remember that this strong monoidal structure allows to define a weak monoidal structure $(\mu^{0},\mu^{2})$ of “$\oc$” from $(\mathcal{L},\otimes)$ to itself. More precisely $\mu^{0}\in\mathcal{L}(1,\oc{1})$ and $\mu^{2}_{X_{1},X_{2}}\in\mathcal{L}({\oc{X_{1}}}\otimes{\oc{X_{2}}},\oc({{X_{1}}\otimes{X_{2}}}))$ are defined using $\mathsf{m}^{0}$ and $\mathsf{m}^{2}$. Also, for each object $X$ of $\mathcal{L}$, there is a canonical structure of commutative $\otimes$-comonoid on $\oc{X}$ given by $\operatorname{\mathsf{w}}_{X}\in\mathcal{L}(\oc{X},1)$ and $\operatorname{\mathsf{contr}}_{X}\in\mathcal{L}(\oc{X},{\oc{X}}\otimes{\oc{X}})$. The definition of these morphisms involves all the structure of “$\oc$” explained above, and in particular the Seely isos. In Section LABEL:sec:exclmu, we will use the fact that the following equation holds

[TABLE]

and also, as a consequence:

[TABLE]

We use $\wn{\_}$ for the “De Morgan dual” of $\oc{\_}$: $\wn{X}=(\oc({X^{{\mathord{\perp}}}}))^{{\mathord{\perp}}}$ and similarly for morphisms. It is a monad on $\mathcal{L}$.

2.1. Eilenberg-Moore category and free comodules

It is then standard to define the category ${\mathcal{L}}^{\oc}$ of ${\mathord{!}}$-coalgebras. An object of this category is a pair $P=(\underline{P},h_{P})$ where $\underline{P}\in\mathcal{L}$ and $h_{P}\in\mathcal{L}(\underline{P},\oc{\underline{P}})$ is such that $\operatorname{\mathsf{der}}_{\underline{P}}\,h_{P}=\operatorname{\mathsf{Id}}$ and $\operatorname{\mathsf{dig}}_{\underline{P}}\,h_{P}=\oc{h_{P}}\,h_{P}$. Then $f\in{\mathcal{L}}^{\oc}(P,Q)$ iff $f\in\mathcal{L}(\underline{P},\underline{Q})$ such that $h_{Q}\,f=\oc{f}\,h_{P}$. The functor $\oc{\_}$ can be seen as a functor from $\mathcal{L}$ to ${\mathcal{L}}^{\oc}$ mapping $X$ to $(\oc{X},\operatorname{\mathsf{dig}}_{X})$ and $f\in\mathcal{L}(X,Y)$ to $\oc{f}$. It is right adjoint to the forgetful functor ${\mathcal{L}}^{\oc}\to\mathcal{L}$. Given $f\in\mathcal{L}(\underline{P},X)$, we use $f^{!}\in{\mathcal{L}}^{\oc}(P,\oc{X})$ for the morphism associated with $f$ by this adjunction, one has $f^{!}=\oc{f}\,h_{P}$. If $g\in{\mathcal{L}}^{\oc}(Q,P)$, we have $f^{!}\,g=(f\,g)^{!}$.

Then ${\mathcal{L}}^{\oc}$ is cartesian (with product of shape ${P}\otimes{Q}=({\underline{P}}\otimes{\underline{Q}},h_{{P}\otimes{Q}})$ and final object $(1,h_{1})$, still denoted as $1$). Here is the definition of $h_{{P}\otimes{Q}}$:

{\underline{P}}\otimes{\underline{Q}}$${\oc{\underline{P}}}\otimes{\oc{\underline{Q}}}$$\oc({{\underline{P}}\otimes{\underline{Q}}})\,.$${h_{P}}\otimes{h_{Q}}$$\mu^{2}_{\underline{P},\underline{Q}}

This category is also cocartesian with coproduct of shape ${P}\oplus{Q}=({\underline{P}}\oplus{\underline{Q}},h_{{P}\oplus{Q}})$ and initial object $(0,h_{0})$ still denoted as [math]. Here is the definition of $h_{{P}\oplus{Q}}$. One first defines $h_{1}:\underline{P}\to\oc({{\underline{P}}\oplus{\underline{Q}}})$ as

\underline{P}$$\oc{\underline{P}}$$\oc({{\underline{P}}\oplus{\underline{Q}}})$$h_{P}$$\oc{\overline{\pi}_{1}}

and similarly one defines $h_{2}:\underline{Q}\to\oc({{\underline{P}}\oplus{\underline{Q}}})$ and then $h_{{P}\oplus{Q}}$ is defined as the unique morphism ${\underline{P}}\oplus{\underline{Q}}\to\oc({{\underline{P}}\oplus{\underline{Q}}})$ such that $h_{{P}\oplus{Q}}\,\overline{\pi}_{i}=h_{i}$ for $i=1,2$.

More details can be found in [Ehrhard16a]. We use $\operatorname{\mathsf{contr}}_{P}\in{\mathcal{L}}^{\oc}(P,{P}\otimes{P})$ (contraction) for the diagonal and $\operatorname{\mathsf{w}}_{P}\in{\mathcal{L}}^{\oc}(P,1)$ (weakening) for the unique morphism to the final object. These morphisms turn $\underline{P}$ into a commutative $\otimes$-comonoid, and are defined as

\underline{P}$$\oc{\underline{P}}$$\oc({{\underline{P}}\mathrel{\&}{\underline{P}}})$${\oc{\underline{P}}}\otimes{\oc{\underline{P}}}$${\underline{P}}\otimes{\underline{P}}$$h_{P}$$\oc{\langle{\operatorname{\mathsf{Id}}},{\operatorname{\mathsf{Id}}}\rangle}$$(\mathsf{m}^{2})^{-1}$${\operatorname{\mathsf{der}}_{\underline{P}}}\otimes{\operatorname{\mathsf{der}}_{\underline{P}}}

and

\underline{P}$$\oc{\underline{P}}$$\oc({\top})$$1$$h_{P}$$\oc{\tau_{\underline{P}}}$$(\mathsf{m}^{0})^{-1} .

2.1.1. The model of free comodules on a given

coalgebra.

Given an object $P$ of ${\mathcal{L}}^{\oc}$, we can define a functor $\mathsf{Comod}_{P}:\mathcal{L}\to\mathcal{L}$ which maps an object $X$ to ${\underline{P}}\otimes{X}$ and a morphism $f$ to ${\underline{P}}\otimes{f}$. This functor is clearly a comonad (with structure maps defined using $\operatorname{\mathsf{w}}_{P}$, $\operatorname{\mathsf{contr}}_{P}$ and the monoidal structure of $\mathcal{L}$). A coalgebra for this comonad is a $P$-comodule111This is just the dual notion of the standard algebraic notion of an $M$-module which can be defined as soon as a commutative $\otimes$-monoid $M$ is given.. It was observed by Girard in [Girard98c] that the Kleisli category $\mathcal{L}[P]={\mathcal{L}}_{\mathsf{Comod}_{P}}$ of this comonad (that is, the category of free $P$-comodules) is in turn a model of $\mathsf{LL}$ with operations on objects defined in the same way as in $\mathcal{L}$, and using the coalgebra structure of $P$ on morphisms. Let us summarize this construction which will be used in the sequel. First let $f_{i}\in\mathcal{L}[P](X_{i},Y_{i})$ for $i=1,2$. Then we define $f_{1}\otimes_{P}f_{2}\in\mathcal{L}[P]({X_{1}}\otimes{X_{2}},{Y_{1}}\otimes{Y_{2}})$ as

\underline{P}\otimes X_{1}\otimes X_{2}$$\underline{P}\otimes\underline{P}\otimes X_{1}\otimes X_{2}$$\underline{P}\otimes X_{1}\otimes\underline{P}\otimes X_{2}$${Y_{1}}\otimes{Y_{2}}\,.$$\operatorname{\mathsf{contr}}_{\underline{P}}\otimes\operatorname{\mathsf{Id}}$$\sim$${f_{1}}\otimes{f_{2}}

The object of linear morphisms from $X$ to $Y$ in $\mathcal{L}[P]$ is ${X}\multimap{Y}$, and the evaluation morphism $\operatorname{\mathsf{ev}}_{P}\in\mathcal{L}[P]({({X}\multimap{Y})}\otimes{X},Y)$ is simply (keeping implicit the $\otimes$-monoidality isos)

\underline{P}\otimes({X}\multimap{Y})\otimes X$$({X}\multimap{Y})\otimes X$$Y$$\operatorname{\mathsf{w}}_{P}\otimes Id$$\operatorname{\mathsf{ev}} . Then it is easy to check that if $f\in\mathcal{L}[P]({Z}\otimes{X},Y)$, that is $f\in\mathcal{L}(\underline{P}\otimes Z\otimes X,Y)$, the morphism $\mathsf{cur}f\in\mathcal{L}[P](Z,{X}\multimap{Y})$ satisfies the required monoidal closeness equations. With these definitions, the category $\mathcal{L}[P]$ is *-autonomous, with $\mathord{\bot}$ as dualizing object. Specifically, given $f\in\mathcal{L}[P](X,Y)$, then ${f}^{{\mathord{\perp}}[P]}$ is the following composition of morphisms:

{\underline{P}}\otimes{Y^{{\mathord{\perp}}}}$$\underline{P}\otimes({\underline{P}}\multimap{X^{{\mathord{\perp}}}})$$X^{{\mathord{\perp}}}$${\underline{P}}\otimes{f^{{\mathord{\perp}}}}$$\operatorname{\mathsf{ev}}

, using implicitly the iso between $({Z}\otimes{X})^{{\mathord{\perp}}}$ and ${Z}\multimap{X^{{\mathord{\perp}}}}$, and the *-autonomy of $\mathcal{L}$ allows to prove that indeed ${f}^{{\mathord{\perp}}[P]{\mathord{\perp}}[P]}=f$.

The category $\mathcal{L}[P]$ is easily seen to be cartesian with $\top$ as final object, ${X_{1}}\mathrel{\&}{X_{2}}$ as cartesian product (and projections defined in the obvious way, using the projections of $\mathcal{L}$ and the counit $\operatorname{\mathsf{w}}_{P}$). Last we define a functor $\oc_{P}{\_}:\mathcal{L}[P]\to\mathcal{L}[P]$ by $\oc_{P}{X}=\oc{X}$ and, given $f\in\mathcal{L}[P](X,Y)$, we define $\oc_{P}{f}\in\mathcal{L}[P](\oc{X},\oc{Y})$ as

{\underline{P}}\otimes{\oc{X}}$${\oc{\underline{P}}}\otimes{\oc{X}}$$\oc({{{\underline{P}}}\otimes{X}})$$\oc{Y}$${h_{P}}\otimes{\oc{X}}$$\mu^{2}$$\oc{f} and this functor is equipped with a comonad structure $(\operatorname{\mathsf{der}}[P],\operatorname{\mathsf{dig}}[P])$ easily defined using $\operatorname{\mathsf{der}}$, $\operatorname{\mathsf{dig}}$ and $\operatorname{\mathsf{w}}_{P}$ (for this crucial construction, we need $P$ to be a $\oc$-coalgebra and not simply a commutative $\otimes$-comonoid; notice however that if $\oc$ is the free exponential, as in [Girard98c], the latter condition implies the former).

2.2. Strong functors on $\mathcal{L}$

Given $n\in{\mathbb{N}}$, an $n$-ary strong functor on $\mathcal{L}$ is a pair $\mathbb{F}=(\overline{\mathbb{F}},\widehat{\mathbb{F}}))$ where $\overline{\mathbb{F}}:\mathcal{L}^{n}\to\mathcal{L}$ is a functor and $\widehat{\mathbb{F}}_{X,\vec{Y}}\in\mathcal{L}({\oc{X}}\otimes{\overline{\mathbb{F}}(\vec{Y})},\overline{\mathbb{F}}({\oc{X}}\otimes{\vec{Y}})$ is a natural transformation, called the strength of $\mathbb{F}$. We use the notation ${Z}\otimes{(Y_{1},\dots,Y_{n})}=({Z}\otimes{Y_{1}},\dots,{Z}\otimes{Y_{n}})$. It is assumed moreover that the diagrams of Figure 1 commute, expressing a monoidality of this strength.

The main purpose of this definition is that one can then define a functor ${\mathbb{F}}[P]:\mathcal{L}[P]^{n}\to\mathcal{L}[P]$ as follows. First one sets ${\mathbb{F}}[P](\vec{X})=\overline{\mathbb{F}}(\vec{X})$. Then, given $\vec{f}\in\mathcal{L}[P]^{n}(\vec{X},\vec{Y})$ we define ${\mathbb{F}}[P](\vec{f})\in\mathcal{L}[P]({\mathbb{F}}(\vec{X}),{\mathbb{F}}(\vec{Y}))$ as

{\underline{P}}\otimes{\mathbb{F}(\vec{X})}$${\oc{\underline{P}}}\otimes{\mathbb{F}(\vec{X})}$$\mathbb{F}({\oc{\underline{P}}}\otimes{\vec{X}})$$\mathbb{F}({{\underline{P}}}\otimes{\vec{X}})$$\mathbb{F}(\vec{Y})\,.$${h_{P}}\otimes{\operatorname{\mathsf{Id}}}$$\widehat{\mathbb{F}}$$\overline{\mathbb{F}}(\operatorname{\mathsf{der}}_{\underline{P}}\otimes\vec{X})$$\mathbb{F}(\vec{f})

The fact that we have defined a functor results from the two monoidality diagrams of Figure 1 and from the definition of $\operatorname{\mathsf{w}}_{P}$ and $\operatorname{\mathsf{contr}}_{P}$ based on the Seely isomorphisms.

Operations on strong functors.

There is an obvious unary identity strong functor $\mathcal{I}$ and for each object $Y$ of $\mathcal{L}$ there is an $n$-ary $Y$-valued constant strong functor $\mathcal{K}^{X}$; in the first case the strength natural transformation is the identity morphism and in the second case, it is defined using $\operatorname{\mathsf{w}}_{\oc{X}}$. Let $\mathbb{F}$ be an $n$-ary strong functor and $\mathbb{G}_{1},\dots,\mathbb{G}_{n}$ be $k$-ary strong functors. Then one defines a $k$-ary strong functor $\mathbb{H}=\mathbb{F}\mathrel{\circ}(\mathbb{G}_{1},\dots,\mathbb{G}_{n})$: the functorial component $\overline{\mathbb{H}}$ is defined in the obvious compositional way. The strength is defined as follows

{\oc{X}}\otimes{\overline{\mathbb{H}}(\vec{Y})}$$\overline{\mathbb{F}}(({\oc{X}}\otimes{\overline{\mathbb{G}_{i}}(\vec{Y})})_{i=1}^{n})$$\overline{\mathbb{F}}(({\overline{\mathbb{G}_{i}}({\oc{X}}\otimes{\vec{Y}})})_{i=1}^{n})=\overline{\mathbb{H}}({\oc{X}}\otimes{\vec{Y}})$$\widehat{\mathbb{F}}$$\overline{\mathbb{F}}((\widehat{\mathbb{G}_{i}})_{i=1}^{k})

and is easily seen to satisfy the required monoidality commutations.

Given an $n$-ary strong functor, we can define its De Morgan dual $\mathbb{F}^{{\mathord{\perp}}}$ which is also an $n$-ary strong functor. On objects, we set $\overline{\mathbb{F}^{{\mathord{\perp}}}}(\vec{Y})=\overline{\mathbb{F}}(\vec{Y}^{{\mathord{\perp}}})^{{\mathord{\perp}}}$ and similarly for morphisms. The strength of $\mathbb{F}^{{\mathord{\perp}}}$ is defined as the Curry transpose of the following morphism (remember that ${\oc{X}}\multimap{\vec{Y}^{{\mathord{\perp}}}}=({\oc{X}}\otimes{\vec{Y}})^{{\mathord{\perp}}}$ up to canonical iso):

\oc{X}\otimes{\overline{\mathbb{F}}(\vec{Y}^{{\mathord{\perp}}})^{{\mathord{\perp}}}}\otimes\overline{\mathbb{F}}({\oc{X}}\multimap{\vec{Y}^{{\mathord{\perp}}}})$$\oc{X}\otimes\overline{\mathbb{F}}({\oc{X}}\multimap{\vec{Y}^{{\mathord{\perp}}}})\otimes{\overline{\mathbb{F}}(\vec{Y}^{{\mathord{\perp}}})^{{\mathord{\perp}}}}$$\overline{\mathbb{F}}(\oc{X}\otimes({\oc{X}}\multimap{\vec{Y}^{{\mathord{\perp}}}}))\otimes{\overline{\mathbb{F}}(\vec{Y}^{{\mathord{\perp}}})^{{\mathord{\perp}}}}$$\overline{\mathbb{F}}(\vec{Y}^{{\mathord{\perp}}})\otimes{\overline{\mathbb{F}}(\vec{Y}^{{\mathord{\perp}}})^{{\mathord{\perp}}}}$$\mathord{\bot}$$\sim$$\widehat{\mathbb{F}}\otimes\operatorname{\mathsf{Id}}$$\overline{\mathbb{F}}(\operatorname{\mathsf{ev}})\otimes\operatorname{\mathsf{Id}}$$\operatorname{\mathsf{ev}}\,\gamma

Then it is possible to prove, using the *-autonomy of $\mathcal{L}$, that $\mathbb{F}^{{\mathord{\perp}}{\mathord{\perp}}}$ and $\mathbb{F}$ are canonically isomorphic (as strong functors)222In the concrete settings considered in this paper, these canonical isos are actuality identity maps..

Lemma 2*.*

$(\mathbb{F}\mathrel{\circ}(\mathbb{G}_{1},\dots,\mathbb{G}_{n}))^{{\mathord{\perp}}}=\mathbb{F}^{{\mathord{\perp}}}\mathrel{\circ}(\mathbb{G}^{{\mathord{\perp}}}_{1},\dots,\mathbb{G}^{{\mathord{\perp}}}_{n})$ up to canonical iso.

Proof 2.1*.*

Results straightforwardly from the definition of $\mathbb{F}^{{\mathord{\perp}}}$ and from the canonical iso between $\mathbb{F}^{{\mathord{\perp}}{\mathord{\perp}}}$ and $\mathbb{F}$. ∎

The bifunctor $\mathord{\otimes}$ can be turned into a strong functor: one defines the strength as

\oc{X}\otimes Y_{1}\otimes Y_{2}$$\oc{X}\otimes\oc{X}\otimes Y_{1}\otimes Y_{2}$$\oc{X}\otimes Y_{1}\otimes\oc{X}\otimes Y_{2}$$\operatorname{\mathsf{contr}}_{\oc{X}}\otimes\operatorname{\mathsf{Id}}$$\sim . By De Morgan duality, this endows $\mathord{\parr}$ with a strength as well. The bifunctor $\oplus$ is also endowed with a strength, simply using the distributivity of $\otimes$ over $\oplus$ (which in turn results from the fact that $\mathcal{L}$ is symmetric monoidal closed). By duality again, $\mathrel{\&}$ inherits a strength as well. Last the unary functor “$\oc$” can be equipped with a strength as follows
{\oc{X}}\otimes{\oc{Y}}$${\oc{\oc{X}}}\otimes{\oc{Y}}$$\oc({{{\oc{X}}}\otimes{Y}})$${\operatorname{\mathsf{dig}}_{X}}\otimes{\oc{X}}$$\mu^{2} . The functors on $\mathcal{L}[P]$ that these strong functors induce coincide with the corresponding operations defined in Section 2.1.1.

2.3. Fixed Points of functors.

The following definitions and properties are quite standard in the literature on fixed points of functors. {defi} Let $\mathcal{A}$ be a category and let $\mathcal{F}:\mathcal{A}\to\mathcal{A}$ be a functor. A coalgebra of $\mathcal{F}$ is a pair $(A,f)$ where $A$ is an object of $\mathcal{A}$ and $f\in\mathcal{A}(A,\mathcal{F}(A))$. Given two coalgebras $(A,f)$ and $(A^{\prime},f^{\prime})$ of $\mathcal{F}$, a coalgebra morphism from $(A,f)$ to $(A^{\prime},f^{\prime})$ is an $h\in\mathcal{A}(A,A^{\prime})$ such that the following diagram commutes

A$$A^{\prime}$$\mathcal{F}(A)$$\mathcal{F}(A^{\prime})$$h$$f$$f^{\prime}$$\mathcal{F}(h)

The category of coalgebras of the functor $\mathcal{F}$ will be denoted as $\mathbf{Coalg}_{\mathcal{A}}(\mathcal{F})$. The notion of algebra of an endofunctor is defined dually (reverse the directions of the arrows $f$ and $f^{\prime}$) and the corresponding category is denoted as $\mathbf{Alg}_{\mathcal{A}}(\mathcal{F})$.

Lemma 3* (Lambek’s Theorem).*

If $(A,f)$ is a final object in $\mathbf{Coalg}_{\mathcal{A}}(\mathcal{F})$ then $f$ is an iso.

In the sequel, we will always assume that this iso is the identity (because this holds in the concrete situations we consider in this paper) so that this final object $(\nu\mathcal{F},\operatorname{\mathsf{Id}})$ satisfies $\mathcal{F}(\nu\mathcal{F})=\nu\mathcal{F}$. We focus on coalgebras rather than algebras for reasons which will become clear when we shall deal with fixed points of strong functors.

This universal property of $\nu\mathcal{F}$ gives us a powerful tool for proving equalities of morphisms.

Lemma 4*.*

Let $A$ be an object of $\mathcal{A}$ and let $f_{1},f_{2}\in\mathcal{A}(A,\nu\mathcal{F})$. If there exists $l\in\mathcal{A}(A,\mathcal{F}(A))$ such that $\mathcal{F}(f_{i})\,l=f_{i}$ for $i=1,2$, then $f_{1}=f_{2}$.