Theory and Applications of Categories, Vol. 22, No. 10, 2009, pp. 269–301.

ON THE CATEGORICAL SEMANTICS OF ELEMENTARY LINEAR LOGIC

OLIVIER LAURENT

Abstract. We introduce the notion of elementary Seely category as a notion of categorical model of Elementary Linear Logic (ELL) inspired from Seely’s definition of models of Linear Logic (LL). In order to deal with additive connectives in ELL, we use the approach of Danos and Joinet [DJ03]. From the categorical point of view, this requires us to go outside the usual interpretation of connectives by functors. The ! connective is decomposed into a pre-connective ♯ which is interpreted by a whole family of functors (generated by id, ⊗ and &).

As an application, we prove the stratified coherent model and the obsessional coherent model to be elementary Seely categories and thus models of ELL.

Introduction

The goal of implicit computational complexity is to give characterizations of complexity classes which rely neither on a particular computation model nor on explicit bounds. In linear logic (LL) [Gir87], the introduction of the exponential connectives gives a precise status to duplication and erasure of formulas (the qualitative analysis). It has been shown that putting constraints on the use of exponentials permits one to give a quantitative analysis of the cut elimination procedure of LL and to define light sub-systems of LL characterizing complexity classes (for example BLL [GSS92], LLL [Gir98] or SLL [Laf04] for polynomial time and ELL [Gir98, DJ03] for elementary time).

In order to have a better understanding of the mathematical structures underlying these systems, various proposals have been made in the last years with the common goal of defining denotational models of light systems [MO00, Bai04, DLH05, LTdF06, Red07]. Our goal is to define a general categorical framework for the study of these systems. We will focus on ELL which is probably the simplest one.^{1}

Our starting point is quite simple: starting from Seely’s notion of categorical model of LL [See89], it is natural to define models of ELL by removing the comonad structure

Partially supported by the French ANR “NO-CoST” project (JC05 43380). Thanks to Lorenzo Tortora de Falco for the joint work on the models of ELL from which this work is coming. Thanks to Patrick Baillot for discussions about light linear logics and their denotational semantics. Thanks to Paul-André Melliès for discussions about monoidal categories and categorical models of linear logic.

Received by the editors 2008-06-02 and, in revised form, 2009-06-02. Transmitted by R. Brown. Published on 2009-06-03. 2000 Mathematics Subject Classification: 18C50. Key words and phrases: monoidal categories, elementary linear logic, categorical logic, denotational

semantics, coherent spaces.

\begin{matrix}c \\ ◯ \end{matrix} Olivier Laurent, 2009. Permission to copy for private use granted. 1Brian Redmond has independently studied the question of categorical semantics of SLL [Red07].

of ! since ELL is obtained from LL by removing the dereliction and digging rules which correspond to this comonad structure. Things become more interesting when one wants to deal with the additive connectives. The usual approach to categorical logic is based roughly on the interpretation: connective ↦ functor, formula ↦ object, rule ↦ natural transformation, proof ↦ morphism, ... The non-local definition of valid proof-nets with additives for ELL given in [DJ03] is presented here by means of the pre-connectives ♭ and ♯, pre-formulas and pre-proofs. Their categorical interpretation requires us to use the association: pre-connective ↦ family of functors. The particular choice of an element of such a family to interpret a pre-formula will depend on the particular proof being interpreted and on the particular occurrence of formula in this proof. The key point is that a proof whose conclusion does not contain any pre-connective can still be interpreted in the usual way.

A particular approach for building a denotational model of ELL is to start from a model of LL and to restrict morphisms (without restriction we, of course, get a model of ELL, but this has no interest from the ELL point of view). In such a case (the model we try to deal with lives inside a model of LL), we give conditions to prove that we have in fact defined a model of ELL. We apply this to the proof that obsessional coherent spaces [LTdF06] provide a model of ELL. We also prove that stratified coherent spaces [Bai00, Bai04] are an elementary Seely category.

Finally we propose an alternative definition for categorical models of ELL based on linear non-linear models of LL [Ben94], and we prove that the two proposals we give, for categories for ELL, are equivalent.

1. Elementary Linear Logic

We give a sequent calculus presentation of the ELL system [Gir98]. Our presentation of the additive connectives is inspired by [DJ03].

1.1. Formulas. Formulas are given by:

\begin{aligned}A, B & ::= & X & | & A � B & | & ⊥ & | & A & B & | & ⊤ & | & ?A \\ & | & X^{⊥} & | & A ⊗ B & | & 1 & | & A ⊕ B & | & 0 & | & !A \end{aligned}

and pre-formulas by:

F, G ::= A | ♭A

The dual ♯ of ♭ could be introduced, but it is not used in practice for defining the sequent calculus of ELL. This ♯ construction will however be used in the categorical setting.

A context is a multi-set of pre-formulas. We will use the notations Γ, Δ, Σ, ... for arbitrary contexts, the notations Θ, Ξ, ... for contexts containing only formulas and the notations ♭Γ, ♭Δ, ♭Σ, ... for contexts containing only pre-formulas which are not formulas.

We deal with classical elementary linear logic^{2} so that sequents have the shape ⊢ Γ.

2As usual with categories for linear logic, the intuitionistic case can be obtained by replacing any ⋆- autonomous category by a symmetric monoidal closed category, the assumption of having finite products being extended to the requirement of having also finite coproducts in such a setting.

1.2. Rules.

\begin{aligned}& ax \\ ⊢ A, A^{⊥} \end{aligned}  \begin{aligned}⊢ Γ, A & ⊢ Δ, A^{⊥} \\ & cut \\ ⊢ Γ, Δ \end{aligned}

\begin{aligned}⊢ Γ, A & ⊢ Δ, B \\ & ⊗ \\ ⊢ Γ, Δ, A ⊗ B \end{aligned}  \begin{aligned}⊢ Γ, A, B \\ & � \\ ⊢ Γ, A � B \end{aligned}  \begin{aligned}& 1 \\ ⊢ 1 \end{aligned}  \begin{aligned}⊢ Γ \\ & ⊥ \\ ⊢ Γ, ⊥ \end{aligned}

\begin{aligned}⊢ Γ, A & ⊢ Γ, B \\ & & \\ ⊢ Γ, A & B \end{aligned}  \begin{aligned}⊢ Γ, A \\ & ⊕_{1} \\ ⊢ Γ, A ⊕ B \end{aligned}  \begin{aligned}⊢ Γ, B \\ & ⊕_{2} \\ ⊢ Γ, A ⊕ B \end{aligned}  \begin{aligned}& ⊤ \\ ⊢ Γ, ⊤ \end{aligned}

\begin{aligned}⊢ Γ, A \\ & ♭ \\ ⊢ Γ, ♭A \end{aligned}  \begin{aligned}⊢ ♭Γ, A \\ & ! \\ ⊢ ?Γ,!A \end{aligned}

⊢ Γ, ♭A, ♭A ; ♭c ; ⊢ Γ, ♭A  \begin{aligned}⊢ Γ \\ & ♭w \\ ⊢ Γ, ♭A \end{aligned}  ⊢ Γ,?A,?A ; ?c ; ⊢ Γ,?A  \begin{aligned}⊢ Γ \\ & ?w \\ ⊢ Γ,?A \end{aligned}

Proof-trees built with these rules are called pre-proofs and we use the word proof only if the conclusion contains only formulas.

Here is an example of proof:

\begin{aligned}& ax \\ ⊢ A^{⊥}, A \end{aligned} ; ♭ ; ⊢ ♭A^{⊥}, A ; ♭w ; ⊢ ♭A^{⊥}, ♭B^{⊥}, A \begin{aligned}& ax \\ ⊢ B^{⊥}, B \end{aligned} ; ♭ ; ⊢ ♭B^{⊥}, B ; ♭w ; ⊢ ♭A^{⊥}, ♭B^{⊥}, B & ⊢ ♭A^{⊥}, ♭B^{⊥}, A & B ! ⊢ ?A^{⊥},?B^{⊥},!(A & B) � ⊢ ?A^{⊥} � ?B^{⊥},!(A & B)

1.2.1. Remark. If we translate pre-formulas into formulas by ♭A ↦ ?A and A ↦ A, we transform any pre-proof in ELL into a proof in LL.

2. Categorical semantics of ELL

2.1. Definitions. For the remainder of the paper, by Seely category we do not exactly mean the original notion introduced by Seely [See89] but the ⋆-autonomous version of the modified notion of new Seely category [Bie95, Mel03].

2.1.1. Definition. [Seely category] A Seely category C is a ⋆-autonomous category with finite products equipped with an endofunctor ! such that:

1. (!, δ, ε) is a comonad

2. (!, p, q) is a strong symmetric monoidal functor from (C, &, ⊤) to (C, ⊗, 1)

3. the following diagram commutes:

\xymatrix{!A ⊗!B \ar[r]^{^{p^{A,B}}} \ar[d]_{δ_{A}⊗δ_{B}} & !(A & B) \ar[d]^{δ_{A&B}} \\ !!A ⊗!!B \ar[dr]_{_{p_{!A,!B}}} & !!(A & B) \ar[d]^{!⟨!proj_{1},!proj_{2}⟩} \\  & !(!A & !B)}

If (C, ⊗, 1) is a symmetric monoidal category, we denote by coMON (C) the category of symmetric ⊗-comonoids (A, c_{A}, w_{A}) of C with comonoidal morphisms. (coMON (C), ⊗, 1) is a cartesian category thus a symmetric monoidal category.

2.1.2. Lemma. [Preservation of comonoids] A symmetric comonoidal functor between two symmetric monoidal categories preserves symmetric comonoids.

Proof. See [Mel03, Lemma 16] for example.

In a Seely category, each object A has a canonical symmetric &-comonoid structure (A, Δ_{A}, ∗_{A}) coming from the product structure of & and the terminal object ⊤. By the previous lemma, this induces a symmetric ⊗-comonoid structure (!A, c_{!A}, w_{!A}) on objects in the image of !.

2.1.3. Lemma. In a Seely category, ! is a symmetric monoidal functor from (C, ⊗, 1) to (coMON (C), ⊗, 1).

Proof. See [Mel03, Lemmas 22 and 5] for example.

We now give the main definition of the paper.

2.1.4. Definition. [Elementary Seely category] An elementary Seely category C is a ⋆-autonomous category with finite products equipped with an endofunctor ! such that:

1. (!, m, n) is a symmetric monoidal functor from (C, ⊗, 1) to (coMON (C), ⊗, 1)

2. (!, p, q) is a strong symmetric monoidal functor from (C, &, ⊤) to (C, ⊗, 1)

3. ! maps the &-comonoid structure of A to the ⊗-comonoid structure of !A

To be a bit more precise: Condition 1 endows any object !A with a symmetric ⊗- comonoid structure (!A, c_{!A}, w_{!A}) and Condition 3 corresponds to the commutation of the following two diagrams:

\xymatrix{!A \ar[r]^{^{c^{!A}}} \ar[dr]_{!Δ_{A}} & !A ⊗!A \ar[d]^{_{p_{A,A}}} & !A \ar[r]^{^{w^{!A}}} \ar[dr]_{!∗_{A}} & 1 \ar[d]^{q} \\  & !(A & A) &  & !⊤}

2.1.5. Remark. Any Seely category is an elementary Seely category (the key point is given by Lemma 2.1.3).

2.1.6. Lemma. In an elementary Seely category, ! is a strong symmetric monoidal functor from (C, &, ⊤) to (coMON (C), ⊗, 1).

Proof. We have to show that p_{A,B} and q are comonoidal morphisms.

The following diagram commutes:

[figure: (!A ⊗!B) ⊗ (!A ⊗!B); ≃; !A ⊗!B; (a); _{c_{!A⊗!B}}; c_{!A}⊗c_{!B}; !Δ_{A}⊗!Δ_{B}; _{p_{A,B}}; (!A ⊗!A) ⊗ (!B ⊗!B); p_{A,A}⊗p_{B,B}; (b); !(A & A) ⊗!(B & B); _{p_{A&A,B&B}}; (c); !((A & A) & (B & B)); ≃; !(A & B); (d); !(Δ_{A}&Δ_{B}); !Δ_{A&B}; _{c_{!(A&B)}}; !((A & B) & (A & B)); _{p{−1 \atop A&B,A&B}}; (e); !(A & B) ⊗!(A & B)]

by (a) definition of c_{!A⊗!B}, (b) Property 3 of elementary Seely categories, (c) naturality of p, (d) definition of Δ and (e) Property 3 again. Moreover the last column is equal to p_{A,B} ⊗ p_{A,B} by definition of a symmetric monoidal functor.

The following diagram commutes:

[figure: !A ⊗!B; _{w_{!A⊗!B}}; w_{!A}⊗w_{!B}; !∗_{A}⊗!∗_{B}; ^{p^{A,B}}; !(A & B); !(∗_{A}&∗_{B}); !∗_{A&B}; _{w_{!(A&B)}}; 1; ≃; (a); 1 ⊗ 1; q⊗q; (b); !⊤ ⊗!⊤; _{p_{⊤,⊤}}; (c); !(⊤ & ⊤); ≃; (d); !⊤; _{q_{−1}}; (e); 1]

by (a) definition of w_{!A⊗!B}, (b) Property 3, (c) naturality of p, (d) definition of ∗ and (e) Property 3 again. Moreover the last line is the identity by definition of a monoidal functor.

Finally, q^{−1} is equal to w_{!⊤} by Property 3:

\xymatrix{!⊤ \ar[r]^{^{w^{!⊤}}} \ar[dr]_{!∗_{⊤}} \ar[dr]_{_{id_{!⊤}}} & 1 \\  & !⊤ \ar[u]_{_{q_{−1}}}}

and thus it is comonoidal.

2.2. The family of functors S. In order to interpret proofs of ELL as morphisms in an elementary Seely category C, we are going to interpret pre-proofs with conclusion ⊢ A_{1}, …, A_{n}, ♭B_{1}, …, ♭B_{k} as a morphism from ♯⟦B_{1}⟧^{⊥} ⊗ … ⊗ ♯⟦B_{k}⟧^{⊥} to ⟦A_{1}⟧ � … � ⟦A_{n}⟧ where, if A is an object, ♯A is a notation which stands for “some object built by applying an arbitrary interleaving of ⊗ and & to copies of A (in particular 1 and ⊤)” (for example A ⊗ ((A ⊗ A) & 1 & A)). More formally, ♯ can be any element of the smallest family S of functors from C to C which:

• contains the constant functors 1 and ⊤,

• contains the identity functor,

• is closed under ⊗ and &. We immediately see that S is closed under composition.

2.2.1. Proposition. [Monoidality of ♯] All the elements of S are symmetric monoidal functors from (C, ⊗, 1) to (C, ⊗, 1).

Proof. See Appendix B.1.

We denote by (♯, m^{♯}, n^{♯}) this monoidal structure on elements of S (an explicit inductive definition is given in Appendix B.2).

As a consequence, for any element ♯ of S, (!♯, m^{!♯}, n^{!♯}) (with m_{A,B}^{!♯} = m_{♯A,♯B}; !m_{A,B}^{♯} and n^{!♯} = n ; !n^{♯}) is a symmetric monoidal functor from (C, ⊗, 1) to (coMON (C), ⊗, 1).

2.2.2. Definition. [The b morphisms] Let A be an object in C, the morphism b_{A}^{♯} from !A to !♯A is defined by induction on ♯ in S:

• b_{A}^{1} = !A ⟶^{w_{!A}} 1 ⟶^{n} !1

• b_{A}^{⊤} = !A ⟶^{w_{!A}} 1 ⟶^{q} !⊤

• b_{A}^{id} = !A ⟶^{id_{!A}} !A

• b_{A}^{♯_{1}⊗♯_{2}} = !A ⟶^{c_{!A}} !A ⊗!A ⟶^{b_{A}^{♯_{1}}⊗b_{A}^{♯_{2}}} !♯_{1}A ⊗!♯_{2}A ⟶^{m_{♯_{1}A,♯_{2}A}} !(♯_{1}A ⊗ ♯_{2}A)

• b_{A}^{♯_{1}&♯_{2}} = !A ⟶^{c_{!A}} !A ⊗!A ⟶^{b_{A}^{♯_{1}}⊗b_{A}^{♯_{2}}} !♯_{1}A ⊗!♯_{2}A ⟶^{p_{♯_{1}A,♯_{2}A}} !(♯_{1}A & ♯_{2}A)

This family of morphisms is parameterized over both ♯ in S and A object of C^{3}. If we fix the first parameter and let the second vary, we obtain the following property.

2.2.3. Proposition. [Monoidality of b^{♯}] For any element ♯ of S, b^{♯} is a monoidal natural transformation from (!, m, n) to (!♯, m^{!♯}, n^{!♯}).

Proof. See Appendix C.

3It would be interesting to understand the more general 2-categorical structures underlying the family of functors S. However it seems uneasy to do since, in particular, Definition 2.2.2 is strongly relying on the use of !A as source.

If we now fix the second parameter and let the first one vary, we have additional properties.

2.2.4. Proposition. Given two elements ♯_{1} and ♯_{2} of S, we have:

• b_{A}^{id} = id_{!A} and b_{A}^{♯_{2}♯_{1}} = !A ⟶^{b_{A}^{♯_{1}}} !♯_{1}A ⟶^{b_{♯_{1}A}^{♯_{2}}} !♯_{2}♯_{1}A

• b_{A}^{⊤} = !∗_{A} and b_{A}^{♯_{1}} = !A ⟶^{b_{A}^{♯_{1}&♯_{2}}} !(♯_{1}A & ♯_{2}A) ⟶^{!proj_{1}} !♯_{1}A

Proof. See Appendix D.

2.3. Soundness. A pre-proof π of the sequent ⊢ A_{1}, …, A_{n}, ♭B_{1}, …, ♭B_{k} will be interpreted as a morphism ⟦π⟧ from ♯_{1}⟦B_{1}⟧^{⊥} ⊗ … ⊗ ♯_{k}⟦B_{k}⟧^{⊥} to ⟦A_{1}⟧ � … � ⟦A_{n}⟧ for some (♯_{i})_{1≤i≤k} ∈ S^{k} which depends on π. Note that for a proof (not a pre-proof) the parameter (♯_{i})_{1≤i≤k} disappears and the source and the target of ⟦π⟧ only depend on the conclusion of π (not on π itself).

By implicitly using the ⋆-autonomous structure, we will not always distinguish between pre-formulas and formulas in contexts (when it is not crucial and makes things easier to follow) for the following definition of ⟦π⟧: if we have a pre-proof π of ⊢ Γ with Γ = Θ, ♭Δ, and if we write ⟦π⟧ as a morphism from 1 to ⟦Γ⟧, we really mean the unique corresponding morphism from ♯⟦Δ⟧^{⊥} to ⟦Θ⟧.

The interpretation of pre-proofs is given in the following way: if π_{1}, π_{2}, ... are the premises of the last rule of π, we define ⟦π⟧ according to this last rule:

• ax-rule: The identity morphism from ⟦A⟧ to ⟦A⟧ gives, by the ⋆-autonomous structure, a morphism from 1 to ⟦A⟧^{⊥} � ⟦A⟧.

• cut-rule: By the ⋆-autonomous structure, we can turn ⟦π_{1}⟧ into a morphism from ⟦Γ⟧^{⊥} to ⟦A⟧ and ⟦π_{2}⟧ into a morphism from ⟦A⟧ to ⟦Δ⟧. By composition, we get a morphism from ⟦Γ⟧^{⊥} to ⟦Δ⟧ and by the ⋆-autonomous structure again, we obtain ⟦π⟧ from 1 to ⟦Γ⟧ � ⟦Δ⟧.

• ⊗-rule: By the ⋆-autonomous structure, we can turn ⟦π_{1}⟧ into a morphism from ⟦Γ⟧^{⊥} to ⟦A⟧ (and the same for ⟦π_{2}⟧ from ⟦Δ⟧^{⊥} to ⟦B⟧) and by the bifunctor ⊗, we get a morphism from ⟦Γ⟧^{⊥} ⊗ ⟦Δ⟧^{⊥} to ⟦A⟧ ⊗ ⟦B⟧. By the ⋆-autonomous structure again, we obtain ⟦π⟧ from 1 to ⟦Γ⟧ � ⟦Δ⟧ � (⟦A⟧ ⊗ ⟦B⟧).

• �-rule: We just have to apply the associativity of �.

• 1-rule: ⟦π⟧ is just the identity from 1 to 1.

• ⊥-rule: We compose on the right with the appropriate unit morphism of ⊥ with respect to �.

• &-rule: We decompose the context Γ into Θ and ♭Δ. By the ⋆-autonomous structure, we can turn ⟦π_{1}⟧ into a morphism from ⟦Θ⟧^{⊥} ⊗ ♯_{1}⟦Δ⟧^{⊥} to ⟦A⟧ (resp. ⟦π_{2}⟧ into a morphism from ⟦Θ⟧^{⊥} ⊗♯_{2}⟦Δ⟧^{⊥} to ⟦B⟧). We compose it on the left with ⟦Θ⟧^{⊥} ⊗proj_{1} (resp. ⟦Θ⟧^{⊥} ⊗ proj_{2}) from ⟦Θ⟧^{⊥} ⊗ (♯_{1}⟦Δ⟧^{⊥} & ♯_{2}⟦Δ⟧^{⊥}) to ⟦Θ⟧^{⊥} ⊗ ♯_{1}⟦Δ⟧^{⊥} (resp. to ⟦Θ⟧^{⊥} ⊗ ♯_{2}⟦Δ⟧^{⊥}). The pair of the two thus obtained morphisms is a morphism from ⟦Θ⟧^{⊥} ⊗ (♯_{1}⟦Δ⟧^{⊥} & ♯_{2}⟦Δ⟧^{⊥}) to ⟦A⟧ & ⟦B⟧, that is a morphism from ⟦Θ⟧^{⊥} ⊗ ♯_{3}⟦Δ⟧^{⊥} to ⟦A⟧ & ⟦B⟧ with ♯_{3} = ♯_{1} & ♯_{2}. By the ⋆-autonomous structure, this gives a morphism from ♯_{3}⟦Δ⟧^{⊥} to ⟦Θ⟧ � (⟦A⟧ & ⟦B⟧).

• ⊕_{1}-rule: Since ⊕ is a coproduct we can compose on the right with the given morphism from ⟦A⟧ to ⟦A⟧ ⊕ ⟦B⟧

• ⊕_{2}-rule: Idem.

• ⊤-rule: Since ⊤ is a terminal object, there is a unique morphism from ⟦Γ⟧^{⊥} to ⊤ which gives ⟦π⟧ by applying the ⋆-autonomous structure.

• ♭-rule: ⟦π_{1}⟧ is a morphism from 1 to ⟦Γ⟧�⟦A⟧ which, by the ⋆-autonomous structure, is a morphism from ♯⟦A⟧^{⊥} to ⟦Γ⟧ with the trivial case ♯ = id.

• !-rule: If Γ = B_{1}, …, B_{k}, ⟦π_{1}⟧ is a morphism from ♯_{1}⟦B_{1}⟧^{⊥}⊗⋯⊗♯_{k}⟦B_{k}⟧^{⊥} to ⟦A⟧. We apply the functor ! and we get a morphism from !(♯_{1}⟦B_{1}⟧^{⊥} ⊗ ⋯ ⊗ ♯_{k}⟦B_{k}⟧^{⊥}) to !⟦A⟧. We compose it on the left with m to get a morphism from !♯_{1}⟦B_{1}⟧^{⊥} ⊗ ⋯ ⊗!♯_{k}⟦B_{k}⟧^{⊥} to !⟦A⟧. We compose it again on the left with b_{⟦B_{i}⟧^{⊥}}^{♯_{i}} from !⟦B_{i}⟧^{⊥} to !♯_{i}⟦B_{i}⟧^{⊥} for each B_{i} to get a morphism from !⟦Γ⟧^{⊥} to !⟦A⟧. By the ⋆-autonomous structure, we turn it into a morphism from 1 to ?⟦Γ⟧ � !⟦A⟧.

• ♭c-rule: ⟦π_{1}⟧ is a morphism from ♯_{1}⟦A⟧^{⊥} ⊗ ♯_{2}⟦A⟧^{⊥} to ⟦Γ⟧, thus it is a morphism ⟦π⟧ from ♯_{3}⟦A⟧^{⊥} to ⟦Γ⟧ with ♯_{3} = ♯_{1} ⊗ ♯_{2}.

• ♭w-rule: ⟦π_{1}⟧ is a morphism from 1 to ⟦Γ⟧. This is a morphism ⟦π⟧ from ♯⟦A⟧^{⊥} to ⟦Γ⟧ with ♯ = 1.

• ?c-rule: Since, for each object C, !C has a ⊗-comonoid structure, ?⟦A⟧ has a �- monoid structure and we can compose ⟦π_{1}⟧ on the right with the contraction morphism from ?⟦A⟧ � ?⟦A⟧ to ?⟦A⟧.

• ?w-rule: As for the ⊥-rule, we can get a morphism from 1 to ⟦Γ⟧ � ⊥. Using the �-monoid structure of ?⟦A⟧, we can compose this morphism on the right with the weakening morphism from ⊥ to ?⟦A⟧.

2.3.1. Theorem. [Soundness] According to the interpretation ⟦.⟧, any elementary Seely category is a model of ELL ( i.e. ⟦.⟧ is an invariant of cut elimination).

Proof. We first prove that, for any pre-proof π of ⊢ Θ, ♭Δ which reduces in one step to π′, if ⟦π⟧ is a morphism from ♯⟦Δ⟧^{⊥} to ⟦Θ⟧ then ⟦π′⟧ is a morphism from ♯′⟦Δ⟧^{⊥} to ⟦Θ⟧ where either ♯ = ♯′ and ⟦π⟧ = ⟦π′⟧, or ♯ = ♯′ & ♯′′ (or ♯ = ♯′′ & ♯′) and ⟦π⟧ = proj_{♯′⟦Δ⟧^{⊥}}; ⟦π′⟧.

We only consider the cut elimination steps given in Appendix A. First, the reader can check that the required complementary commutative steps do not modify the interpretation. Second, it would be possible to represent pre-proofs of ELL by proof-nets (with boxes for the additive connectives) [Gir98, LTdF06, Gir87] and to interpret these proof-nets into elementary Seely categories. In this setting the only cut elimination steps are those given in Appendix A (the additional commutative steps are invisible in the proof-net syntax).

We rely on the notations introduced in Appendix A, and we omit semantic brackets around the interpretations of formulas.

• ax: by properties of ⋆-autonomous categories.

• ⊗/�: by properties of ⋆-autonomous categories.

• 1/⊥: by properties of ⋆-autonomous categories.

• &/⊕_{1}: by properties of the cartesian product: the composition of ⟨(id ⊗ proj_{1}) ; ⟦π_{1}⟧, (id ⊗ proj_{2}) ; ⟦π_{2}⟧⟩ with proj_{1} is (id ⊗ proj_{1}) ; ⟦π_{1}⟧.

• ∗/&: Up to the ⋆-autonomous structure, ⟦π_{2}⟧ is a morphism from C ⊗ Θ^{⊥} ⊗ ♯_{1}Δ^{⊥} to A and ⟦π_{3}⟧ is a morphism from C ⊗ Θ^{⊥} ⊗ ♯_{2}Δ^{⊥} to B, and ⟦π_{1}⟧ is a morphism from Γ^{⊥} to C, by properties of pairs, we have:

\xymatrix{Γ^{⊥} ⊗ Θ^{⊥} ⊗ (♯_{1}Δ^{⊥} & ♯_{2}Δ^{⊥}) \ar[r]^{⟦π_{1}⟧⊗id} \ar@{-->}[dr]_{⟨(id⊗proj_{1});(⟦π_{1}⟧⊗id);⟦π_{2}⟧,(id⊗proj_{2});(⟦π_{1}⟧⊗id);⟦π_{3}⟧⟩} & C ⊗ Θ^{⊥} ⊗ (♯_{1}Δ^{⊥} & ♯_{2}Δ^{⊥}) \ar[d]^{⟨(id⊗proj_{1});⟦π_{2}⟧,(id⊗proj_{2});⟦π_{3}⟧⟩} \\  & A & B}

• ∗/⊤: ⊤ is a terminal object.

• ?c/!: A proof π_{0} ending with a !-rule is interpreted as a comonoidal morphism since b_{A}^{♯} is a comonoidal morphism (Proposition 2.2.3), m_{A,B} is a comonoidal morphism, and if f is a morphism, !f is a comonoidal morphism. This shows that the following diagram commutes:

\xymatrix{!Γ^{⊥} \ar[r]^{⟦π_{0}⟧} \ar[d]_{_{c_{!Γ⊥}}} & !A \ar[d]^{_{c_{!A}}} \\ !Γ^{⊥} ⊗!Γ^{⊥} \ar[r]_{⟦π_{0}⟧⊗⟦π_{0}⟧} & !A ⊗!A}

• ?w/!: Idem with:

\xymatrix{!Γ^{⊥} \ar[rr]^{⟦π_{0}⟧} \ar[dr]_{_{w_{!Γ^{⊥}}}} &  & !A \ar[dl]^{_{w_{!A}}} \\  & 1}

• !/!: We denote by D_{j} the formulas of Δ and by G_{i} the formulas of Γ. As a starting point, the following diagram commutes:

\xymatrix{⨂!D_{j}^{⊥} ⊗ ⨂!G_{i}^{⊥} \ar[r]_{(a)}^{⨂^{b}{♯_{j} \atop D^{⊥}_{j}} ⊗⨂ b{♯_{i} \atop G^{⊥}_{i}}} \ar[d]_{⨂_{b}{♯_{j} \atop D^{⊥}_{j}} ⊗⨂ b{♯♯_{i} \atop G^{⊥}_{i}}} & ⨂!♯_{j} D_{j}^{⊥} ⊗ ⨂!♯_{i}G_{i}^{⊥} \ar[dl]^{(b)}^{id⊗⨂ b{♯ \atop ♯_{i}G^{⊥}_{i}}} \ar[r]^{id⊗m} & ⨂!♯_{j} D_{j}^{⊥} ⊗ !⨂ ♯_{i}G_{i}^{⊥} \ar[r]_{(c)}^{id⊗!⟦π_{1}⟧} \ar[d]_{id⊗b♯ ; ⨂ ♯_{i}G^{⊥}_{i}} & ⨂!♯_{j} D_{j}^{⊥} ⊗ !A \ar[d]^{id⊗b{♯ \atop A}} \\ ⨂!♯_{j} D_{j}^{⊥} ⊗ ⨂!♯♯_{i}G_{i}^{⊥} \ar[r]_{(d)}_{id⊗m} \ar[dr]_{m} & ⨂!♯_{j} D_{j}^{⊥} ⊗ !⨂ ♯♯_{i}G_{i}^{⊥} \ar[r]_{(e)}_{id⊗!m^{♯}} \ar[d]_{m} & ⨂!♯_{j} D_{j}^{⊥} ⊗ !♯⨂ ♯_{i}G_{i}^{⊥} \ar[r]_{(f)}_{id⊗!♯⟦π_{1}⟧} \ar[d]^{m} & ⨂!♯_{j} D_{j}^{⊥} ⊗ !♯A \ar[d]^{m} \\  & !(⨂ ♯_{j} D_{j}^{⊥} ⊗ ⨂ ♯♯_{i}G_{i}^{⊥}) \ar[r]_{!(id⊗m^{♯})} & !(⨂ ♯_{j} D_{j}^{⊥} ⊗ ♯⨂ ♯_{i}G_{i}^{⊥}) \ar[r]_{!(id⊗♯⟦π_{1}⟧)} & !(⨂ ♯_{j} D_{j}^{⊥} ⊗ ♯A) \ar[d]^{!⟦π_{2}⟧} \\  &  &  & !B}

by (a) Proposition 2.2.4, (b) Proposition 2.2.3 (with m_{A,B}^{!♯} = m_{♯A,♯B} ; !m_{A,B}^{♯}),

(c) naturality of b^{♯}, (d) properties of m (monoidality of !), (e) naturality of m and (f) naturality of m.

By bifunctoriality of ⊗, the top-right path is ⟦π⟧, and by functoriality of !, the leftbottom path is the interpretation of a !-rule applied to (⨂ ♯_{j}D_{j}^{⊥} ⊗(m^{♯};♯⟦π_{1}⟧));⟦π_{2}⟧. We have to show this is the interpretation of the reduct. We prove it by induction on the pre-proof π_{2}. The key cases are when the last rule is a ⊤, &, ♭, ♭w or ♭c rule:

– ⊤-rule: Immediate since ⊤ is a terminal object.

– &-rule: We have ⟦π_{1}⟧ from ♯_{Γ}Γ ( = ⨂ ♯_{i}G_{i}^{⊥}) to A, ⟦π_{2}^{1}⟧ from Θ^{⊥}⊗⨂ ♯_{j}^{1}D_{j}^{⊥}⊗♯^{1}A to B and ⟦π_{2}^{2}⟧ from Θ^{⊥} ⊗ ⨂ ♯_{j}^{2}D_{j}^{⊥} ⊗ ♯^{2}A to C with ♯ = ♯^{1} & ♯^{2} and ♯_{j} = ♯_{j}^{1} & ♯_{j}^{2}, we want to show (Θ^{⊥} ⊗ ⨂ ♯_{j}D_{j}^{⊥} ⊗ (m^{♯}; ♯⟦π_{1}⟧)) ; ⟨(Θ^{⊥} ⊗ ⨂ proj_{♯_{j}^{1}D_{j}^{⊥}} ⊗ proj_{♯^{1}A}) ; ⟦π_{2}^{1}⟧, (Θ^{⊥} ⊗ ⨂ proj_{♯_{j}^{2}D_{j}^{⊥}} ⊗ proj_{♯^{2}A}) ; ⟦π_{2}^{2}⟧⟩ is the same as ⟨(Θ^{⊥} ⊗ ⨂ proj_{♯_{j}^{1}D_{j}^{⊥}} ⊗ ⨂ proj_{♯^{1}♯_{i}G_{i}^{⊥}});(Θ^{⊥}⊗⨂ ♯_{j}^{1}D_{j}^{⊥}⊗(m^{♯^{1}};♯^{1}⟦π_{1}⟧));⟦π_{2}^{1}⟧, (Θ^{⊥}⊗⨂ proj_{♯_{j}^{2}D_{j}^{⊥}}⊗⨂ proj_{♯^{2}♯_{i}G_{i}^{⊥}}); (Θ^{⊥} ⊗ ⨂ ♯_{j}^{2}D_{j}^{⊥} ⊗ (m^{♯^{2}} ; ♯^{2}⟦π_{1}⟧)) ; ⟦π_{2}^{2}⟧⟩. It comes from the commutation of the following diagram and from properties of the product:

\xymatrix{⨂ ♯♯_{i}G_{i}^{⊥} \ar[r]^{^{m^{♯}}} \ar[d]_{_{⨂ proj_{♯^{1}♯_{i}G^{⊥}_{i}}}} & ♯⨂ ♯_{i}G_{i}^{⊥} \ar[r]^{♯⟦π_{1}⟧} \ar[d]^{_{proj_{♯^{1}⨂ ♯_{i}G^{⊥}_{i}}}} & ♯A \ar[d]^{_{proj_{♯^{1}A}}} \\ ⨂ ♯^{1}♯_{i}G_{i}^{⊥} \ar[r]_{_{m_{♯^{1}}}} & ♯^{1}⨂ ♯_{i}G_{i}^{⊥} \ar[r]_{♯^{1}⟦π_{1}⟧} & ♯^{1}A}

which is obtained by definition of m^{♯_{1}&♯_{2}} since ♯ = ♯^{1} & ♯^{2} (Proposition 2.2.1 and Appendix B.2) and by naturality of projections.

– ♭-rule, ♭w-rule and ♭c-rule: These cases are immediate since they do not modify the interpretation of the pre-proof π_{2}.

To conclude we show that, given a proof (not only a pre-proof), its interpretation and the interpretation of a reduct are the same (not only up to composition with a projection). The key point is that if π is followed by a !-rule (it must be the case at some point since there is no ♭ in the conclusion of the whole proof), then the interpretation of the whole proof is invariant under reduction. We only consider the particular case where π is immediately followed by a !-rule and we show that if π reduces to π′ then ⟦!π⟧ = ⟦!π′⟧ (where !π is π followed by a !-rule). This corresponds to the commutation of the following diagram:

\xymatrix{ & ⨂!♯_{j}D_{j}^{⊥} \ar[r]|{m} \ar[dd]_{⨂!proj_{♯′_{j} D^{⊥}_{j}}} & !⨂ ♯_{j}D_{j}^{⊥} \ar[dr]^{!⟦π⟧} \ar[dd]^{!⨂ proj_{♯′_{j} D^{⊥}_{j}}} \\ ⨂!D_{j}^{⊥} \ar[ur]^{_{⨂ b{♯_{j} \atop D^{⊥}_{j}}}} \ar[dr]_{_{⨂ b{♯′_{j} \atop D^{⊥}_{j}}}} &  &  & !C \\  & ⨂!♯′_{j}D_{j}^{⊥} \ar[r]_{m} & !⨂ ♯′_{j}D_{j}^{⊥} \ar[ur]_{!⟦π′⟧}}

which is true by Proposition 2.2.4, naturality of m, and the first part of the present proof which gives the last triangle.

3. Examples and applications

Two of the main models of ELL one can find in the literature are the stratified coherent model [Bai04] and the obsessional coherent model [LTdF06]. We are going to show that they both give elementary Seely categories.

In the case of the obsessional model, we will use a simple criterion which can be applied to any model of ELL presented as a sub-model of a model of LL.

3.1. Coherent spaces. We first recall the definition and key properties of coherent spaces [Gir87] to be used in the two models of ELL.

3.1.1. Definition. [Coherent space] A coherent space is a pair A = (|A|, �_{A}) where |A| is a set and �_{A} is a reflexive symmetric relation on |A|.

A clique x in A, denoted x ⊏ A, is a set of elements of |A| such that if a, b ∈ x then a �_{A} b. A multiclique of A is a multiset of elements of |A| such that the underlying set (the support) is a clique.

We use the following notations: a �_{A} b if a �_{A} b ∧ a ≠ b, a �_{A} b if ¬(a �_{A} b), and a �_{A} b if a �_{A} b ∧ a ≠ b.

The basic constructions of coherent spaces are the following:

• A^{⊥} = (|A|, �_{A})

• ⊤ = 0 = (∅, ∅)

• ⊥ = 1 = ({⋆}, {(⋆, ⋆)})

• A � B: |A � B| = |A| × |B| and (a, b) �_{A�B} (a′, b′) ⟺ a �_{A} a′ ∨ b �_{B} b′

• A ⊗ B: |A ⊗ B| = |A| × |B| and (a, b) �_{A⊗B} (a′, b′) ⟺ a �_{A} a′ ∧ b �_{B} b′

• A ⊸ B = A^{⊥} � B

• A&B: |A&B| = |A|+|B|, (1, a) �_{A&B} (1, a′) ⟺ a �_{A} a′, (2, b) �_{A&B} (2, b′) ⟺ b �_{B} b′, (i, a) �_{A&B} (j, b) if i ≠ j

• A⊕B: |A⊕B| = |A|+|B|, (1, a) �_{A⊕B} (1, a′) ⟺ a �_{A} a′, (2, b) �_{A⊕B} (2, b′) ⟺ b �_{B} b′, (i, a) �_{A⊕B} (j, b) if i ≠ j

• !A: |!A| is the set of all finite multicliques of A and μ �_{!A} ν if μ + ν is a multiclique of A

• ?A: |?A| is the set of all finite multicliques of A^{⊥} and μ �_{?A} ν if μ + ν is not a multiclique of A^{⊥}

3.1.2. Proposition. [Category COH] The category COH given by:

• objects: coherent spaces

• morphisms: COH(A, B) is the set of cliques of A ⊸ B

is a Seely category.

Proof. See [Mel03] for example.

3.2. Stratified coherent spaces. We look at the first denotational model of ELL defined by Baillot [Bai04] from coherent spaces. In order to make things simpler, we consider the presentation of the model given in [Bai00].

3.2.1. Definition. [Stratified coherent space] A stratified coherent space A is a sequence of triples (|A|^{i}, �_{A}^{i}, φ_{A}^{i})_{i∈ℕ} where, for each i, A^{i} = (|A|^{i}, �_{A}^{i}) is a coherent space and φ_{A}^{i} is a partial function from |A|^{i+1} to |A|^{i} and moreover the sequence is stationary: there exists some d (the depth of A) such that for any i ≥ d, |A|^{i} = |A|^{d}, �_{A}^{i} = �_{A}^{d} and φ_{A}^{i} = id_{|A|^{d}}.

An element a of A^{i} is visible in A if φ_{A}^{0} ∘ φ_{A}^{1} ∘ ⋯ ∘ φ_{A}^{i−1}(a) is defined.

A clique of the stratified coherent space A is a clique of A^{d} (where d is the depth of A). A visible clique is a clique containing only visible elements. A stratified clique is a visible clique x such that for all i ≤ d, φ_{A}^{i} ∘ φ_{A}^{i+1} ∘ ⋯ ∘ φ_{A}^{d−1}(x) is a clique of A^{i}.

A stratified coherent space is called constant when its depth is 0. Any coherent space can be considered as a constant stratified coherent space.

The multiplicative and additive constructions of stratified coherent spaces are obtained from the corresponding constructions of coherent spaces applied level by level:

• (|A^{⊥}|^{i}, �_{A^{⊥}}^{i}) = (|A|^{i}, �_{A}^{i})^{⊥} and φ_{A^{⊥}}^{i} = φ_{A}^{i}

• (|A ⊗ B|^{i}, �_{A⊗B}^{i}) = (|A|^{i}, �_{A}^{i}) ⊗ (|B|^{i}, �_{B}^{i}) and φ_{A⊗B}^{i} = φ_{A}^{i} × φ_{B}^{i}

• 1 = ({⋆}, {(⋆, ⋆)}, id)_{i∈ℕ} (the constant stratified coherent space with one point)

• (|A & B|^{i}, �_{A&B}^{i}) = (|A|^{i}, �_{A}^{i}) & (|B|^{i}, �_{B}^{i}) and φ_{A&B}^{i} = φ_{A}^{i} + φ_{B}^{i}

• ⊤ = (∅, ∅, id)_{i∈ℕ} (the constant empty stratified coherent space)

and by orthogonality, we define: A � B = (A^{⊥} ⊗ B^{⊥})^{⊥}, A ⊕ B = (A^{⊥} & B^{⊥})^{⊥}, ⊥ = 1^{⊥}, 0 = ⊤^{⊥}, and A ⊸ B = (A ⊗ B^{⊥})^{⊥}.

The !A construction induces a lifting of levels:

• (|!A|^{0}, �_{!A}^{0}) = 1

• for i ≥ 1, (|!A|^{i}, �_{!A}^{i}) = !(|A|^{i−1}, �_{A}^{i−1})

• φ_{!A}^{0} is the constant function mapping any element to ⋆.

• for i ≥ 1, φ_{!A}^{i}([a_{1}, …, a_{n}]) = [φ_{A}^{i−1}(a_{1}), …, φ_{A}^{i−1}(a_{n})] if all the φ_{A}^{i−1}(a_{j}) are defined (1 ≤ j ≤ n) and if [φ_{A}^{i−1}(a_{1}), …, φ_{A}^{i−1}(a_{n})] belongs to |!A|^{i}; and φ_{!A}^{i}([a_{1}, …, a_{n}]) is undefined otherwise.

and by orthogonality, we define ?A = (!A^{⊥})^{⊥}.

3.2.2. Proposition. [Elementary Seely category SCOH] The category SCOH of stratified coherent spaces and stratified cliques is an elementary Seely category.

Proof. The main ingredients are given in [Bai00], we give some additional material in Appendix E.

3.3. Models of ELL inside models of LL. The previous example requires quite a number of verifications in order to check all the axioms of elementary Seely categories. In the particular case where the model of ELL under consideration lives inside a model of LL, it is possible to give a much simpler approach.

We consider a Seely category L (thus a model of LL) and a sub-category C of L containing all the objects of L (only some morphisms are removed). We are going to give a simple criterion to show that C is an elementary Seely category, thus a model of ELL.

We say that C satisfies the closure criterion if the following properties about morphisms of C hold:

• the morphisms for associativity, commutativity and neutral element of ⊗ corresponding to the ⋆-autonomous structure of L belong to C

• if A ⟶^{f} C ∈ C and B ⟶^{g} D ∈ C then A ⊗ B ⟶^{f⊗g} C ⊗ D ∈ C

• the morphism from (A ⊸ ⊥) ⊸ ⊥ to A coming from the ⋆-autonomous structure of L belongs to C

• A & B ⟶^{proj_{1}} A ∈ C, A & B ⟶^{proj_{2}} B ∈ C and A ⟶^{∗} ⊤ ∈ C

• if C ⟶^{f} A ∈ C and C ⟶^{g} B ∈ C then C ⟶^{⟨f,g⟩} A & B ∈ C

• !A ⊗!B ⟶^{m} !(A ⊗ B) ∈ C and 1 ⟶^{n} !1 ∈ C

• if A ⟶^{f} B ∈ C then !A ⟶^{!f} !B ∈ C

• !A ⊗!B ⟶^{p} !(A & B) ∈ C and 1 ⟶^{q} !⊤ ∈ C

• !(A & B) ⟶^{p^{−1}} !A ⊗!B ∈ C and !⊤ ⟶^{q^{−1}} 1 ∈ C

3.3.1. Theorem. [Elementarity criterion] If C satisfies the closure criterion then C is an elementary Seely category.

Proof. The key points are that any diagram concerning morphisms of C which commutes in L commutes in C, and that L is a Seely category thus an elementary Seely category (Remark 2.1.5).

C is a ⋆-autonomous category with finite products since the corresponding structure morphisms (together with the pairing construction) belong to C.

The restriction of ! to C defines an endofunctor of C.

By Property 3 of elementary Seely categories applied to L, c_{!A} = !ΔA ; p_{A,A}^{−1} and w_{!A} = !∗_{A}; q^{−1} thus c_{!A} and w_{!A} belong to C. Moreover (!A, c_{!A}, w_{!A}) is a ⊗-comonoid in C since the required diagrams commute in L. So that (!, m, n) is a functor from (C, ⊗, 1) to (coMON (C), ⊗, 1) which is symmetric monoidal since the appropriate diagrams commute in L.

(!, p, q) is a strong symmetric monoidal functor from (C, &, ⊤) to (C, ⊗, 1) since p and q belong to C, are isomorphisms in C and the required diagrams commute in L thus in C.

Finally the Property 3 of elementary Seely categories is satisfied since it is given by the commutation of two diagrams which are commutative in L.

The meaning of this result is in particular to show how the interaction between the additive connectives and the exponential connectives in ELL can be axiomatized exactly through the fact that ! is a strong symmetric monoidal functor from (C, &, ⊤) to (C, ⊗, 1) (thus the existence of p and q). This was not obvious to us from a purely syntactic point of view (additional conditions might have been required), and comes nicely from the categorical approach. Indeed this question was the starting point for the present work.

3.4. Obsessional coherent spaces. We apply the previous criterion to show that obsessional coherent spaces give an elementary Seely category. This second example is coming from [LTdF06]. It was described there in the relational setting. We give here the coherent version. All the results proved in [LTdF06] in the relational case are valid in the coherent case with the same proofs.

3.4.1. Definition. [ℕ-coherent space] A ℕ-coherent space is given by a coherent space A and a function, called the action:

ℕ^{∗} × |A| → |A|
(k, a) ↦ a^{(k)}

which is an action of the monoid (ℕ^{∗}, ·, 1) on |A| (where ℕ^{∗} = ℕ \ {0}), that is a^{(1)} = a and a^{(kk′)} = (a^{(k)})^{(k′)} and such that:

a �_{A} b ⟹ a^{(k)} �_{A} b^{(k)}
a �_{A} b ⟹ a^{(k)} �_{A} b^{(k)}

A clique x of A is obsessional if ∀a ∈ x, ∀k ∈ ℕ^{∗}, a^{(k)} ∈ x.

In the particular case where the action is the identity a^{(k)} = a, the space is called atomic. Any coherent space can be considered as an atomic ℕ-coherent space.

The constructions of ℕ-coherent spaces are obtained from the corresponding constructions of coherent spaces and the actions are built in the following way:

• the action on A^{⊥} is the same as the action on A

• for ⊥, 1, ⊤ and 0, we use the only possible action (making them atomic)

• the action on A ⊗ B or A � B is given by (a, b)^{(k)} = (a^{(k)}, b^{(k)})

• the action on A ⊕ B or A & B is given by (1, a)^{(k)} = (1, a^{(k)}) and (2, a)^{(k)} = (2, a^{(k)})

• the action on !A or ?A is given by [a_{1}, …, a_{n}]^{(k)} = [ka_{1}^{(k)}, …, ka_{n}^{(k)}] (that is we take k copies of each a_{i}^{(k)})

3.4.2. Definition. [Category ℕCOH] The category ℕCOH is given by:

• objects: ℕ-coherent spaces

• morphisms: ℕCOH(A, B) is the set of cliques of A ⊸ B

3.4.3. Proposition. [Elementary Seely category OCOH] By restraining ℕCOH to the obsessional cliques only, one gets a category OCOH which is an elementary Seely category.

Proof. The identity is obsessional and the composition of two obsessional cliques is obsessional [LTdF06], thus OCOH is a sub-category of ℕCOH.

The categories COH and ℕCOH are equivalent categories: the forgetful functor from ℕCOH to COH is full, faithful, surjective on objects (by considering atomic spaces) and strictly preserves all the structures. As a consequence ℕCOH is a Seely category.

Finally we apply Theorem 3.3.1 to ℕCOH and OCOH since OCOH satisfies the closure criterion: the properties concerning only the multiplicative and exponential structures are given in [LTdF06] and we now check those concerning the additive ones.

• If ((1, a), a) ∈ proj_{1} then ((1, a), a)^{(k)} = ((1, a^{(k)}), a^{(k)}) ∈ proj_{1}, thus proj_{1} is obsessional.

• ∗_{A} from A to ⊤ is the empty clique which is obsessional.

• If f ⊏ C ⊸ A and g ⊏ C ⊸ B are obsessional, ⟨f, g⟩ = {(c, (1, a)) | (c, a) ∈ f} ∪ {(c, (2, b)) | (c, b) ∈ g} ⊏ C ⊸ A & B is obsessional since (c, (1, a))^{(k)} = (c^{(k)}, (1, a^{(k)})) and (c^{(k)}, a^{(k)}) ∈ f (and the same with g).

• If (([a_{1}, …, a_{n}], [b_{1}, …, b_{m}]), [(1, a_{1}), …, (1, a_{n}), (2, b_{1}), …, (2, b_{m})]) ∈ p_{A,B} then:

(([a_{1}, …, a_{n}], [b_{1}, …, b_{m}]), [(1, a_{1}), …, (1, a_{n}), (2, b_{1}), …, (2, b_{m})])^{(k)}

= (([ka_{1}^{(k)}, …, ka_{n}^{(k)}], [kb_{1}^{(k)}, …, kb_{m}^{(k)}]),

[k(1, a_{1}^{(k)}), …, k(1, a_{n}^{(k)}), k(2, b_{1}^{(k)}), …, k(2, b_{m}^{(k)})]) ∈ p_{A,B}

thus p_{A,B} is obsessional.

• q = {(⋆, [ ])} is obsessional since (⋆, [ ])^{(k)} = (⋆, [ ]).

and if f is an isomorphism in ℕCOH which belongs to OCOH, it is an isomorphism in OCOH: f^{−1} = {(y, x) | (x, y) ∈ f} thus if f is obsessional then f^{−1} is obsessional.

4. Linear non-linear models

An important alternative to Seely categories as a notion of categorical model of linear logic is the notion of linear non-linear model introduced by Benton [Ben94]. We are going to consider an elementary version of these models. Since we are interested in additive connectives and classical linear logic, we directly consider the ⋆-autonomous case with products.

4.0.4. Definition. [Linear non-linear model] A linear non-linear model is given by a ⋆-autonomous category C with finite products and a cartesian category M (with product denoted × and terminal element I) with a symmetric monoidal adjunction between them (given by a symmetric monoidal functor (F, m_{0}, n_{0}) from C to M which is right adjoint to a symmetric monoidal functor (G, m_{1}, n_{1}) from M to C).

This entails the following two properties.

4.0.5. Lemma. In a linear non-linear model, G is strong.

Proof. See [Ben94, Proposition 1].

4.0.6. Lemma. In a linear non-linear model, F preserves products.

Proof. F is a right adjoint.

4.1. Elementary linear non-linear model. We now turn to an elementary version of linear non-linear models.

4.1.1. Definition. [Elementary linear non-linear model] An elementary linear nonlinear model is given by a ⋆-autonomous category C with finite products and a cartesian category M, and two functors F from C to M and G from M to C such that:

• (F, m_{0}, n_{0}) is a symmetric monoidal functor from C to M

• (G, m_{1}, n_{1}) is a strong symmetric monoidal functor from M to C

• F preserves products (with p_{0} : F A × F B ≃ F (A & B) and q_{0} : I ≃ F ⊤)

4.1.2. Remark. Any linear non-linear model is an elementary linear non-linear model (by Lemmas 4.0.5 and 4.0.6).

4.1.3. Proposition. Any elementary linear non-linear model induces an elementary Seely category.^{4}

Proof. C is a ⋆-autonomous category with finite products.

For any object A of C, (GF A, GΔ_{F A} ; m_{1}^{−1}, G ∗_{F A} ;n_{1}^{−1}) is a ⊗-comonoid, and we can define the symmetric monoidal functor ! = GF from C to coMON (C) (see [Mel03, Lemma 16] and the remark just after in [Mel03]).

GF, equipped with the composition of m_{1} : GF A ⊗ GF B → G(F A × F B) and Gp_{0} : G(F A × F B) → GF (A & B), and the composition of n_{1} : 1 → GI and Gq_{0} : GI → GF ⊤, is a strong symmetric monoidal functor from (C, &, ⊤) to (C, ⊗, 1).

Finally if we apply the definition of the ⊗-comonoid structure of GF A given above, we have to prove the commutation of the following two diagrams:

[figure: GF A; GΔ_{F A}; GF Δ; G(F A × F A); ^{m{−1 \atop 1}}; GF A ⊗ GF A; _{m_{1}}; G(F A × F A); Gp_{0}; GF (A & A); GF A; G∗_{F A}; GF ∗_{A}; GI; ^{n{−1 \atop 1}}; 1; _{n_{1}}; GI; Gq_{0}; GF ⊤]

They both commute, mainly by using the preservation of products by F.

4There is a proposal by P.-A. Melliès to introduce an intermediate affine category between C and M as a sufficient condition to get rid of the S family presented in Section 2.2.

4.1.4. Proposition. Any elementary Seely category induces an elementary linear nonlinear model.

Proof. By hypothesis, C is a ⋆-autonomous category with finite product. Moreover, the category M = (coMON (C), ⊗, 1) is a cartesian category.

Let us assume F = ! and G is the forgetful functor from M to C, (!, m, n) is a symmetric monoidal functor from (C, ⊗, 1) to (coMON (C), ⊗, 1) (thus from C to M). (G, id, id_{1}) is a strong symmetric monoidal functor from (coMON (C), ⊗, 1) to (C, ⊗, 1) (thus from M to C).

Finally, F preserves products since it maps & to ⊗ and the &-comonoid structure of A in C (which is the product structure in C) to the ⊗-comonoid structure of !A in M (which is the product structure in M).

4.2. Light linear non-linear model. As a final remark we just mention the existence of a natural refinement of elementary linear non-linear models which gives a proposal for categorical models of light linear logic [Gir98].

4.2.1. Definition. [Light linear non-linear model] A light linear non-linear model is given by a ⋆-autonomous category C with finite products and a cartesian category M, and three functors F from C to M and G and H from M to C, and a natural transformation α from G to H such that:

• (F, m_{0}, n_{0}) is a symmetric monoidal functor from C to M

• (G, m′_{1}, n′_{1}) is a symmetric comonoidal functor from M to C

• (H, m_{2}, n_{2}) is a symmetric monoidal functor from M to C

• F preserves products

4.2.2. Remark. Any elementary linear non-linear model is a light linear non-linear model (with G = H and α is the identity).

In this setting, we can define the functor ! = GF from C to C and the symmetric monoidal functor § = HF, and α_{F} is a natural transformation from ! to §. Moreover, for any object A of C, (!A, GΔ_{F};m′_{1}, G∗_{F};n′_{1}) is a ⊗-comonoid. These are the key ingredients required for interpreting light linear logic.

In order to model intuitionistic systems without additive connectives, elementary linear non-linear models and light linear non-linear models can be weakened by only requiring C to be a symmetric monoidal closed category and by removing the hypothesis that F preserves products.

Conclusion

We have proposed two possible axiomatizations of categorical models of ELL: elementary Seely categories and elementary linear non-linear models. They both come from natural restrictions of the corresponding notions for LL. As usual in categorical logic, such axiomatizations give a natural formalism for proving that a would-be model is indeed a model of the corresponding logical system. This is particularly important here to deal with the additive connectives of ELL. The ELL syntax with additives is not always easy to manipulate while the axioms of our elementary models allow us to hide such difficulties. These difficulties are moved into the soundness proof of our axiomatization, once and for all. In some way, categorical models confirm that the choices made by Danos and Joinet in the design of their syntax for ELL [DJ03] are the good one: the expressiveness of the obtained system fits well with categorical semantics.

We have applied our categorical axiomatizations to (re)prove the soundness of two crucial examples of models of ELL without reference to the syntax. In the particular case where such a model of ELL arrives as a sub-model of a model of LL, we have extracted a very simple criterion allowing us to check only minimal properties to derive a soundness result with respect to ELL. It was not possible to apply this criterion to the stratified model since it is not clear how to find a surrounding model of LL, but this would be an interesting question to investigate.

While the system ELL and its syntactic presentations could be considered as canonical, the situation is quite different with LLL: should the § modality be self-dual or not? should we restrict the context of the !-rule to only one formula or to at most one formula? etc. We have just proposed a definition of light linear non-linear model which comes naturally as a refinement of elementary linear non-linear models. A whole study of categorical models of LLL has to be given with the hope that the categorical setting will discriminate between the various possible choices in the design of the syntax of the LLL system.

Finally, concerning both ELL and LLL, it is often useful from the expressiveness point of view to consider their intuitionistic versions extended with general weakening (the affine systems IEAL and ILAL). It should not be difficult to adapt our results to these systems. Another interesting system to address would be DLAL [BT04] which is particularly adapted for type inference.

A. Cut elimination in ELL

We give the main steps of the cut elimination procedure of ELL.

\begin{aligned}\begin{matrix}π_{1} \\ ⊢ Γ, A \end{matrix} & \begin{aligned}& ax \\ ⊢ A^{⊥}, A \end{aligned} \\ & cut \\ & ⊢ Γ, A \end{aligned}  ⇝  \begin{matrix}π_{1} \\ ⊢ Γ, A \end{matrix}

\begin{aligned}\begin{matrix}π_{1} \\ ⊢ Γ, A \end{matrix} & \begin{matrix}π_{2} \\ ⊢ Δ, B \end{matrix} \\ & ⊗ \\ ⊢ Γ, Δ, A ⊗ B \end{aligned} \begin{matrix}π_{3} \\ ⊢ Σ, A^{⊥}, B^{⊥} \end{matrix} ; � ; ⊢ Σ, A^{⊥} � B^{⊥} cut ⊢ Γ, Δ, Σ  ⇝  \begin{matrix}π_{1} \\ ⊢ Γ, A \end{matrix}  \begin{aligned}\begin{matrix}π_{2} \\ ⊢ Δ, B \end{matrix} & \begin{matrix}π_{3} \\ ⊢ Σ, A^{⊥}, B^{⊥} \end{matrix} \\ & & cut \\ & ⊢ Δ, Σ, A^{⊥} \end{aligned} cut ⊢ Γ, Δ, Σ

288  OLIVIER LAURENT

\begin{aligned}\begin{aligned}& 1 \\ ⊢ 1 \end{aligned} & & \begin{matrix}π_{1} \\ ⊢ Γ \end{matrix} ; ⊥ ; ⊢ Γ, ⊥ \\ & & cut \\ & ⊢ Γ \end{aligned}  ⇝  \begin{matrix}π_{1} \\ ⊢ Γ \end{matrix}

\begin{aligned}\begin{matrix}π_{1} \\ ⊢ Γ, A \end{matrix} & \begin{matrix}π_{2} \\ ⊢ Γ, B \end{matrix} \\ & & \\ ⊢ Γ, A & B \end{aligned} \begin{matrix}π_{3} \\ ⊢ Δ, A^{⊥} \end{matrix} ; ⊕_{1} ; ⊢ Δ, A^{⊥} ⊕ B^{⊥} cut ⊢ Γ, Δ  ⇝  \begin{aligned}\begin{matrix}π_{1} \\ ⊢ Γ, A \end{matrix} & \begin{matrix}π_{3} \\ ⊢ Δ, A^{⊥} \end{matrix} \\ & & cut \\ & ⊢ Γ, Δ \end{aligned}

\begin{matrix}π_{1} \\ ⊢ Γ, C \end{matrix}  \begin{aligned}\begin{matrix}π_{2} \\ ⊢ C^{⊥}, Θ, ♭Δ, A \end{matrix} & \begin{matrix}π_{3} \\ ⊢ C^{⊥}, Θ, ♭Δ, B \end{matrix} \\ & & \\ ⊢ C^{⊥}, Θ, ♭Δ, A & B \end{aligned} cut ⊢ Γ, Θ, ♭Δ, A & B

⇝  \begin{matrix}π_{1} \\ ⊢ Γ, C \end{matrix}  \begin{matrix}π_{2} \\ ⊢ C^{⊥}, Θ, ♭Δ, A \end{matrix} cut ⊢ Γ, Θ, ♭Δ, A \begin{matrix}π_{1} \\ ⊢ Γ, C \end{matrix}  \begin{matrix}π_{3} \\ ⊢ C^{⊥}, Θ, ♭Δ, B \end{matrix} cut ⊢ Γ, Θ, ♭Δ, B & ⊢ Γ, Θ, ♭Δ, A & B

\begin{aligned}\begin{matrix}π_{1} \\ ⊢ Γ, C \end{matrix} & \begin{aligned}& ⊤ \\ ⊢ C^{⊥}, Δ, ⊤ \end{aligned} \\ & cut \\ & ⊢ Γ, Δ, ⊤ \end{aligned}  ⇝  \begin{aligned}& ⊤ \\ ⊢ Γ, Δ, ⊤ \end{aligned}

\begin{matrix}π_{1} \\ ⊢ ♭Γ, A \end{matrix} ; ! ; ⊢ ?Γ,!A \begin{matrix}π_{2} \\ ⊢ Δ,?A^{⊥},?A^{⊥} \end{matrix} ; ?c ; ⊢ Δ,?A^{⊥} cut ⊢ ?Γ, Δ  ⇝  \begin{matrix}π_{1} \\ ⊢ ♭Γ, A \end{matrix} ; ! ; ⊢ ?Γ,!A \begin{matrix}π_{1} \\ ⊢ ♭Γ, A \end{matrix} ; ! ; ⊢ ?Γ,!A \begin{matrix}π_{2} \\ ⊢ Δ,?A^{⊥},?A^{⊥} \end{matrix} cut ⊢ ?Γ, Δ,?A^{⊥} cut ⊢ ?Γ,?Γ, Δ ?c ⊢ ?Γ, Δ

\begin{matrix}π_{1} \\ ⊢ ♭Γ, A \end{matrix} ; ! ; ⊢ ?Γ,!A \begin{matrix}π_{2} \\ ⊢ Δ \end{matrix} ; ?w ; ⊢ Δ,?A^{⊥} cut ⊢ ?Γ, Δ  ⇝  \begin{matrix}π_{2} \\ ⊢ Δ \end{matrix} ; ?w ; ⊢ ?Γ, Δ

\begin{matrix}π_{1} \\ ⊢ ♭Γ, A \end{matrix} ; ! ; ⊢ ?Γ,!A ⋯  \begin{matrix}π_{2}^{i} \\ ⊢ Σ^{i}, A^{⊥} \end{matrix} ; ♭ ; ⊢ Σ^{i}, ♭A^{⊥} ⋯; ⋮ ; π_{2} ; ⋮ ; ⊢ ♭Δ, ♭A^{⊥}, B ; ! ; ⊢ ?Δ,?A^{⊥},!B cut ⊢ ?Γ,?Δ,!B  ⇝  ⋯  \begin{aligned}\begin{matrix}π_{1} \\ ⊢ ♭Γ, A \end{matrix} & \begin{matrix}π_{2}^{i} \\ ⊢ Σ^{i}, A^{⊥} \end{matrix} \\ & cut \\ ⊢ ♭Γ, Σ^{i} \end{aligned} ⋯; ⋮ ; π_{2} ; ⋮ ⊢ ♭Γ, ♭Δ, B ! ⊢ ?Γ,?Δ,!B

B. Proposition 2.2.1

B.1. Proof of Proposition 2.2.1.

Proof. The constructions presented here are related with the idea of multiplication on monoidal categories [JS93].

• A constant functor from (C, ⊗, 1) to (C, ⊗, 1) mapping all objects to Z is symmetric monoidal if and only if Z is a symmetric monoid in (C, ⊗, 1). This is the case for both 1 and ⊤.

• The identity functor is a symmetric monoidal functor from (C, ⊗, 1) to (C, ⊗, 1).

• The diagonal functor from (C, ⊗, 1) to (C × C, ⊗, (1, 1)) (with the tensor product given by tensor product on each component) is symmetric monoidal.

• The functor ⊗ from (C × C, ⊗, (1, 1)) to (C, ⊗, 1) is a symmetric monoidal functor if we use the following natural transformation and morphism:

M = (A ⊗ B) ⊗ (A′ ⊗ B′) ⟶^{≃} (A ⊗ A′) ⊗ (B ⊗ B′)

N = 1 ⟶^{≃} 1 ⊗ 1

The following three diagrams commute by properties of symmetric monoidal categories:

\xymatrix{((A ⊗ B) ⊗ (A′ ⊗ B′)) ⊗ (A′′ ⊗ B′′) \ar[r]^{α} \ar[d]_{M⊗(A′′⊗B′′)} & (A ⊗ B) ⊗ ((A′ ⊗ B′) ⊗ (A′′ ⊗ B′′)) \ar[d]^{(A⊗B)⊗M} \\ ((A ⊗ A′) ⊗ (B ⊗ B′)) ⊗ (A′′ ⊗ B′′) \ar[d]_{M} & (A ⊗ B) ⊗ ((A′ ⊗ A′′) ⊗ (B′ ⊗ B′′)) \ar[d]^{M} \\ ((A ⊗ A′) ⊗ A′′) ⊗ ((B ⊗ B′) ⊗ B′′) \ar[r]_{α⊗α} & (A ⊗ (A′ ⊗ A′′)) ⊗ (B ⊗ (B′ ⊗ B′′))}

\xymatrix{A ⊗ B \ar[r]^{≃} \ar[d]_{≃} & (A ⊗ B) ⊗ 1 \ar[d]^{(A⊗B)⊗N} \\ (A ⊗ 1) ⊗ (B ⊗ 1) & (A ⊗ B) ⊗ (1 ⊗ 1) \ar[l]^{M}}

\xymatrix{(A ⊗ B) ⊗ (A′ ⊗ B′) \ar[r]^{γ} \ar[d]_{M} & (A′ ⊗ B′) ⊗ (A ⊗ B) \ar[d]^{M} \\ (A ⊗ A′) ⊗ (B ⊗ B′) \ar[r]_{γ⊗γ} & (A′ ⊗ A) ⊗ (B′ ⊗ B)}

• The functor & from (C × C, ⊗, (1, 1)) to (C, ⊗, 1) is a symmetric monoidal functor if we use the following natural transformation and morphism:

M = (A & B) ⊗ (A′ & B′) ⟶^{⟨proj_{1}⊗proj_{1},proj_{2}⊗proj_{2}⟩} (A ⊗ A′) & (B ⊗ B′)

N = 1 ⟶^{Δ_{1}} 1 & 1

To prove the commutation of the following diagram:

\xymatrix{((A & B) ⊗ (A′ & B′)) ⊗ (A′′ & B′′) \ar[r]^{α} \ar[d]_{M⊗(A′′&B′′)} & (A & B) ⊗ ((A′ & B′) ⊗ (A′′ & B′′)) \ar[d]^{(A&B)⊗M} \\ ((A ⊗ A′) & (B ⊗ B′)) ⊗ (A′′ & B′′) \ar[d]_{M} & (A & B) ⊗ ((A′ ⊗ A′′) & (B′ ⊗ B′′)) \ar[d]^{M} \\ ((A ⊗ A′) ⊗ A′′) & ((B ⊗ B′) ⊗ B′′) \ar[r]_{α&α} & (A ⊗ (A′ ⊗ A′′)) & (B ⊗ (B′ ⊗ B′′))}

it is enough to prove the commutation of the next diagram and of the corresponding one with proj_{2} since the left side of the previous diagram is the pair of their left sides and its right side is the pair of their right sides.

\xymatrix{((A & B) ⊗ (A′ & B′)) ⊗ (A′′ & B′′) \ar[r]^{α} \ar[d]_{M⊗(A′′&B′′)} & (A & B) ⊗ ((A′ & B′) ⊗ (A′′ & B′′)) \ar[d]^{(A&B)⊗M} \\ ((A ⊗ A′) & (B ⊗ B′)) ⊗ (A′′ & B′′) \ar[d]_{proj_{1}⊗proj_{1}} & (A & B) ⊗ ((A′ ⊗ A′′) & (B′ ⊗ B′′)) \ar[d]^{proj_{1}⊗proj_{1}} \\ ((A ⊗ A′) ⊗ A′′) \ar[r]_{α} & (A ⊗ (A′ ⊗ A′′))}

since M ; proj_{1} = proj_{1} ⊗ proj_{1}, this is obtained by naturality of α. The following diagram commutes:

\xymatrix{A & B \ar[r]^{≃} \ar[d]_{≃} & (A & B) ⊗ 1 \ar[d]^{(A&B)⊗N} \ar@{-->}[dl]_{f} \\ (A ⊗ 1) & (B ⊗ 1) & (A & B) ⊗ (1 & 1) \ar[l]^{M}}

with f = ⟨proj_{1} ⊗ id_{1}, proj_{2} ⊗ id_{1}⟩. The first triangle commutes by properties of monoidal categories and of the product and the second triangle commutes by definition of M and N.

The following diagram commutes:

\xymatrix{(A & B) ⊗ (A′ & B′) \ar[r]^{γ} \ar[d]_{M} & (A′ & B′) ⊗ (A & B) \ar[d]^{M} \\ (A ⊗ A′) & (B ⊗ B′) \ar[r]_{γ&γ} & (A′ ⊗ A) & (B′ ⊗ B)}

ON THE CATEGORICAL SEMANTICS OF ELEMENTARY LINEAR LOGIC  291

by pairing the next diagram with the corresponding one obtained by using proj_{2} instead of proj_{1}:

\xymatrix{(A & B) ⊗ (A′ & B′) \ar[r]^{γ} \ar[d]_{proj_{1}⊗proj_{1}} & (A′ & B′) ⊗ (A & B) \ar[d]^{proj_{1}⊗proj_{1}} \\ A ⊗ A′ \ar[r]_{γ} & A′ ⊗ A}

which commutes by naturality of γ.

• Finally the composition of two symmetric monoidal functors is symmetric monoidal.

B.2. The monoidal structure. We explicitly give the monoidal structure on ♯ ∈ S obtained in the previous section/proof.

By induction on ♯, m_{A,B}^{♯} from ♯A ⊗ ♯B to ♯(A ⊗ B) is given by:

• m_{A,B}^{1} = 1 ⊗ 1 → 1 is the unit morphism of 1 with respect to ⊗

• m_{A,B}^{⊤} = ⊤ ⊗ ⊤ → ⊤ is the unique such morphism since ⊤ is terminal

• m_{A,B}^{id} = A ⊗ B ⟶^{id} A ⊗ B

• m_{A,B}^{♯_{1}⊗♯_{2}} = (♯_{1}A ⊗ ♯_{2}A) ⊗ (♯_{1}B ⊗ ♯_{2}B) ⟶^{≃} (♯_{1}A ⊗ ♯_{1}B) ⊗ (♯_{2}A ⊗ ♯_{2}B) ⟶^{m_{A,B}^{♯_{1}}⊗m_{A,B}^{♯_{2}}}

♯_{1}(A ⊗ B) ⊗ ♯_{2}(A ⊗ B)

• m_{A,B}^{♯_{1}&♯_{2}} = (♯_{1}A & ♯_{2}A) ⊗ (♯_{1}B & ♯_{2}B) ⟶^{⟨proj_{1}⊗proj_{1},proj_{2}⊗proj_{2}⟩} (♯_{1}A ⊗ ♯_{1}B) & (♯_{2}A ⊗

♯_{2}B) ⟶^{m_{A,B}^{♯_{1}}&m_{A,B}^{♯_{2}}} ♯_{1}(A ⊗ B) & ♯_{2}(A ⊗ B)

and n^{♯} from 1 to ♯1 by:

• n^{1} = 1 ⟶^{id_{1}} 1

• n^{⊤} = 1 ⟶^{∗_{1}} ⊤

• n^{id} = 1 ⟶^{id_{1}} 1

• n^{♯_{1}⊗♯_{2}} = 1 → 1 ⊗ 1 ⟶^{n^{♯_{1}}⊗n^{♯_{2}}} ♯_{1}1 ⊗ ♯_{2}1

• n^{♯_{1}&♯_{2}} = 1 ⟶^{Δ_{1}} 1 & 1 ⟶^{n^{♯_{1}}&n^{♯_{2}}} ♯_{1}1 & ♯_{2}1

C. Proof of Proposition 2.2.3

Proof. We first prove that b_{A}^{♯} belongs to coMON (C) by induction on the definition:

• b_{A}^{1} is comonoidal since w_{!A} is comonoidal and n is comonoidal.

• b_{A}^{⊤} is comonoidal since w_{!A} is comonoidal and q is comonoidal (by Lemma 2.1.6).

• b_{A}^{id} is comonoidal since id is comonoidal.

• b_{A}^{♯_{1}⊗♯_{2}} is comonoidal since c_{!A} is comonoidal, b_{A}^{♯_{1}} and b_{A}^{♯_{2}} are comonoidal by induction hypothesis and m_{♯_{1}A,♯_{2}A} is comonoidal.

• b_{A}^{♯_{1}&♯_{2}} is comonoidal since c_{!A} is comonoidal, b_{A}^{♯_{1}} and b_{A}^{♯_{2}} are comonoidal by induction hypothesis and p_{♯_{1}A,♯_{2}A} is comonoidal (by Lemma 2.1.6).

In the same way, we easily check naturality by properties of all the constructions involved in the definition of b^{♯}.

We finally prove the commutation of the two diagrams corresponding to the monoidality of the natural transformation:

\xymatrix{!A ⊗!B \ar[rr]^{m} \ar[d]_{b_{A}^{♯}⊗b_{B}^{♯}} &  & !(A ⊗ B) \ar[d]^{_{b{♯ \atop A⊗B}}} & 1 \ar[rr]^{n} \ar[dr]_{n} &  & !1 \ar[d]^{_{b{♯ \atop 1}}} \\ !♯A ⊗!♯B \ar[r]_{m} & !(♯A ⊗ ♯B) \ar[r]_{!m^{♯}} & !♯(A ⊗ B) &  & !1 \ar[r]_{!n^{♯}} & !♯1}

By induction on ♯ for the first diagram:

• If ♯ = 1, the following diagram commutes:

[figure: !A ⊗!B; m; b_{A}^{1}⊗b_{B}^{1}; w_{!A}⊗w_{!B}; !(A ⊗ B); _{w_{!(A⊗B)}}; _{b{1 \atop A⊗B}}; (b); (d); 1 ⊗ 1; (a); ≃; n⊗n; 1; (c); n; !1 ⊗!1; m; !(1 ⊗ 1); ≃; !1]

by (a) definition of b_{A}^{1}, (b) comonoidality of m, (c) definition of b_{A⊗B}^{1}, and (d) monoidality of !.

• If ♯ = ⊤, the following diagram commutes:

[figure: !A ⊗!B; m; b_{A}^{⊤}⊗b_{B}^{⊤}; w_{!A}⊗w_{!B}; !(A ⊗ B); _{w_{!(A⊗B)}}; _{b{⊤ \atop A⊗B}}; (b); (d); 1 ⊗ 1; (a); ≃; q⊗q; 1; (c); q; !⊤ ⊗!⊤; p; !(⊤ ⊗ ⊤); !∗; !⊤]

ON THE CATEGORICAL SEMANTICS OF ELEMENTARY LINEAR LOGIC  293

by (a) definition of b_{A}^{⊤}, (b) comonoidality of m, (c) definition of b_{A⊗B}^{⊤}, and (d) monoidality of !.

• If ♯ = id, the following diagram immediately commutes:

\xymatrix{!A ⊗!B \ar[rr]^{m} \ar[d]_{id⊗id} &  & !(A ⊗ B) \ar[d]^{id} \\ !A ⊗!B \ar[r]_{m} & !(A ⊗ B) \ar[r]_{!id} & !(A ⊗ B)}

• If ♯ = ♯_{1} ⊗ ♯_{2}, the following diagram commutes:

[figure: !A ⊗ !B; (b); c_{!A}⊗c_{!B}; (a); _{_{c}_{!A⊗!B}}; m; !(A ⊗ B); _{_{c}_{!(A⊗B)}}; !A ⊗ !A ⊗ !B ⊗ !B; ≃; b{♯_{1} \atop A} ⊗b{♯_{2} \atop A} ⊗b{♯_{1} \atop B} ⊗b{♯_{2} \atop B}; !A ⊗ !B ⊗ !A ⊗ !B; (d); m⊗m; b{♯_{1} \atop A} ⊗b{♯_{1} \atop B} ⊗b{♯_{2} \atop A} ⊗b{♯_{2} \atop B}; (c); !(A ⊗ B) ⊗ !(A ⊗ B); b{♯_{1} \atop A⊗B} ⊗b{♯_{2} \atop A⊗B}; !♯_{1}A ⊗ !♯_{2}A ⊗ !♯_{1}B ⊗ !♯_{2}B; (e); ≃; m⊗m; !♯_{1}A ⊗ !♯_{1}B ⊗ !♯_{2}A ⊗ !♯_{2}B; m⊗m; !(♯_{1}A ⊗ ♯_{1}B) ⊗ !(♯_{2}A ⊗ ♯_{2}B); (f); !m^{♯_{1}} ⊗!m^{♯_{2}}; m; !♯_{1}(A ⊗ B) ⊗ !♯_{2}(A ⊗ B); m; !(♯_{1}A ⊗ ♯_{2}A) ⊗ !(♯_{1}B ⊗ ♯_{2}B); m; !(♯_{1}A ⊗ ♯_{2}A ⊗ ♯_{1}B ⊗ ♯_{2}B); ≃; !(♯_{1}A ⊗ ♯_{1}B ⊗ ♯_{2}A ⊗ ♯_{2}B); !(m^{♯_{1}} ⊗m^{♯_{2}} ); !(♯_{1}(A ⊗ B) ⊗ ♯_{2}(A ⊗ B))]

by (a) definition of c_{!A⊗!B}, (b) comonoidality of m, (c) symmetry of ⊗, (d) induction hypothesis, (e) monoidality and symmetry of !, and (f) naturality of m.

• If ♯ = ♯_{1} & ♯_{2}, the diagram we want has the same first two lines as for ♯ = ♯_{1} ⊗ ♯_{2}. The last one becomes:

\xymatrix{!♯_{1}A ⊗ !♯_{2}A ⊗ !♯_{1}B ⊗ !♯_{2}B \ar[r]_{(a)}^{≃} \ar[d]_{p⊗p} & !♯_{1}A ⊗ !♯_{1}B ⊗ !♯_{2}A ⊗ !♯_{2}B \ar[r]_{m⊗m} & !(♯_{1}A ⊗ ♯_{1}B) ⊗ !(♯_{2}A ⊗ ♯_{2}B) \ar[r]_{(b)}_{!m♯1 ⊗!m♯2} \ar[d]^{p} & !♯_{1}(A ⊗ B) ⊗ !♯_{2}(A ⊗ B) \ar[d]^{p} \\ !(♯_{1}A & ♯_{2}A) ⊗ !(♯_{1}B & ♯_{2}B) \ar[r]_{m} & !((♯_{1}A & ♯_{2}A) ⊗ (♯_{1}B & ♯_{2}B)) \ar[r]_{!⟨proj1⊗proj1,proj2⊗proj2⟩} & !((♯_{1}A ⊗ ♯_{1}B) & (♯_{2}A ⊗ ♯_{2}B)) \ar[r]_{!(m♯1 &m♯2 )} & !(♯_{1}(A ⊗ B) & ♯_{2}(A ⊗ B))}

The square (b) commutes by naturality of p. We are going to prove the commutation of the hexagon (a). We have:

\xymatrix{ & !(A_{1} & A_{2}) ⊗ !(A_{1} & A_{2}) ⊗ !(B_{1} & B_{2}) ⊗ !(B_{1} & B_{2}) \ar[r]_{(b)}^{!proj_{1}⊗!proj_{2}⊗!proj_{1}⊗!proj_{2}} \ar[d]_{≃} & !A_{1} ⊗ !A_{2} ⊗ !B_{1} ⊗ !B_{2} \ar[d]^{≃} \\ !(A_{1} & A_{2}) ⊗ !(B_{1} & B_{2}) \ar[ur]_{(a)}_{(c)}^{c_{!(A_{1}&A_{2})}⊗c_{!(B_{1}&B_{2})}} \ar[r]_{_{_{c}_{!(A_{1}&A_{2})⊗!(B_{1}&B_{2})}}} \ar[d]_{m} & !(A_{1} & A_{2}) ⊗ !(B_{1} & B_{2}) ⊗ !(A_{1} & A_{2}) ⊗ !(B_{1} & B_{2}) \ar[r]_{(d)}^{!proj_{1}⊗!proj_{1}⊗!proj_{2}⊗!proj_{2}} \ar[d]_{m⊗m} & !A_{1} ⊗ !B_{1} ⊗ !A_{2} ⊗ !B_{2} \ar[d]^{m⊗m} \\ !((A_{1} & A_{2}) ⊗ (B_{1} & B_{2})) \ar[r]_{(e)}^{_{_{c}_{!((A_{1}&A_{2})⊗(B_{1}&B_{2}))}}} \ar[dr]_{!Δ} & !((A_{1} & A_{2}) ⊗ (B_{1} & B_{2})) ⊗ !((A_{1} & A_{2}) ⊗ (B_{1} & B_{2})) \ar[r]_{(f)}^{!(proj_{1}⊗proj_{1})⊗!(proj_{2}⊗proj_{2})} \ar[d]_{p} & !(A_{1} ⊗ B_{1}) ⊗ !(A_{2} ⊗ B_{2}) \ar[d]^{p} \\  & !((A_{1} & A_{2}) ⊗ (B_{1} & B_{2})) & ((A_{1} & A_{2}) ⊗ (B_{1} & B_{2})) \ar[r]_{!((proj_{1}⊗proj_{1})&(proj_{2}⊗proj_{2}))} & !((A_{1} ⊗ B_{1}) & (A_{2} ⊗ B_{2}))}

294  OLIVIER LAURENT

by (a) definition of c_{!(A_{1}&A_{2})⊗!(B_{1}&B_{2})}, (b) symmetry of ⊗, (c) comonoidality of m,

(d) naturality of m, (e) Property 3 of elementary Seely categories and (f) naturality of p. The last line is !⟨proj_{1} ⊗ proj_{1}, proj_{2} ⊗ proj_{2}⟩ and the first line pre-composed with p ⊗ p is the identity:

[figure: !(A_{1} & A_{2}) ⊗ !(B_{1} & B_{2}); (b); c!(A1&A2)⊗c!(B1&B2); id; !Δ⊗!Δ; (a); !(A_{1} & A_{2}) ⊗ !(A_{1} & A_{2}) ⊗ !(B_{1} & B_{2}) ⊗ !(B_{1} & B_{2}); !proj1⊗!proj2⊗!proj1⊗!proj2; !(A_{1} & A_{2} & A_{1} & A_{2}) ⊗ !(B_{1} & B_{2} & B_{1} & B_{2}); (c); !(proj1&proj2)⊗!(proj1&proj2); p−1⊗p−1; !A_{1} ⊗ !A_{2} ⊗ !B_{1} ⊗ !B_{2}; !(A_{1} & A_{2}) ⊗ !(B_{1} & B_{2}); p−1⊗p−1]

by (a) properties of products, (b) Property 3 of elementary Seely categories, and (c) naturality of p.

By induction on ♯ also for the second diagram:

• If ♯ = 1, the following diagram commutes:

\xymatrix{1 \ar[r]^{n} \ar[d]_{n} \ar[dr]_{_{id_{1}}} & !1 \ar[d]^{_{w_{!1}}} \\ !1 \ar[dr]_{!id_{1}} & 1 \ar[d]^{n} \\  & !1}

by comonoidality of n for the triangle and by properties of id for the square.

• If ♯ = ⊤, the following diagram commutes:

\xymatrix{1 \ar[r]^{n} & !1 \ar[r]^{^{w^{!1}}} \ar[dr]_{!∗_{1}} & 1 \ar[d]^{q} \\  &  & !⊤}

by Property 3 of elementary Seely categories.

• If ♯ = id, the following diagram commutes:

\xymatrix{1 \ar[r]^{n} \ar[d]_{n} & !1 \ar[d]^{_{id_{!1}}} \\ !1 \ar[r]_{!id_{1}} & !1}

• If ♯ = ♯_{1} ⊗ ♯_{2}, the following diagram commutes:

\xymatrix{ &  &  & !1 \ar[dr]_{(a)}^{_{c_{!1}}} \\  &  & 1 \ar[dddll]^{(d)}_{n} \ar[dl] \ar[ur]^{n} \ar[r] \ar[d]_{n} & 1 ⊗ 1 \ar[r]_{(e)}^{n⊗n} \ar[d]^{n⊗n} & !1 ⊗!1 \ar[d]^{b_{1}^{♯_{1}}⊗b_{1}^{♯_{2}}} \\  & 1 ⊗ 1 \ar[dr]_{(b)}^{(c)}_{n⊗1} & !1 \ar[r]_{_{c_{!1}}} & !1 ⊗!1 \ar[r]_{(g)}_{!n^{♯_{1}}⊗!n^{♯_{2}}} \ar[dd]^{_{m_{1,1}}} & !♯_{1}1 ⊗!♯_{2}1 \ar[dd]^{_{m_{♯_{1}1,♯_{2}1}}} \\  &  & !1 ⊗ 1 \ar[ur]_{(f)}_{!1⊗n} \\ !1 \ar[rrr] \ar[urr] &  &  & !(1 ⊗ 1) \ar[r]_{!(n^{♯_{1}}⊗n^{♯_{2}})} & !(♯_{1}1 ⊗ ♯_{2}1)}

by (a) comonoidality of n, (b) properties of monoidal categories, (c) comonoidality of n, (d) comonoidality of n, (e) induction hypothesis, (f) monoidality of ! and (g) naturality of m.

• If ♯ = ♯_{1} & ♯_{2}, the following diagram commutes:

\xymatrix{ & !1 \ar[dr]_{(a)}^{_{c_{!1}}} \\ 1 \ar[ur]_{(b)}^{n} \ar[r] \ar[d]_{n} & 1 ⊗ 1 \ar[r]_{(c)}^{n⊗n} \ar[d]^{n⊗n} & !1 ⊗!1 \ar[d]^{b_{1}^{♯_{1}}⊗b_{1}^{♯_{2}}} \\ !1 \ar[r]_{(d)}^{_{c_{!1}}} \ar[dr]_{!Δ_{1}} & !1 ⊗!1 \ar[r]_{(e)}_{!n^{♯_{1}}⊗!n^{♯_{2}}} \ar[d]^{_{p_{1,1}}} & !♯_{1}1 ⊗!♯_{2}1 \ar[d]^{_{p_{♯_{1}1,♯_{2}1}}} \\  & !(1 & 1) \ar[r]_{!(n^{♯_{1}}&n^{♯_{2}})} & !(♯_{1}1 & ♯_{2}1)}

by (a) comonoidality of n, (b) comonoidality of n, (c) induction hypothesis,

(d) Property 3 of elementary Seely categories, and (e) naturality of p.

D. Proof of Proposition 2.2.4

Proof.

• b_{A}^{id} = id_{!A} by definition.

• b ; b: by induction on ♯_{2}:

– if ♯_{2} = 1 or ♯_{2} = ⊤, we apply the definition of b_{♯_{1}A}^{♯_{2}} and we obtain the following commutative diagram:

\xymatrix{!A \ar[r]^{^{b{♯_{1} \atop A}}} \ar[dr]_{_{w_{!A}}} & !♯_{1}A \ar[d]^{_{w_{!♯_{1}A}}} \\  & 1 \ar[r]_{n/q} & !1/!⊤}

by comonoidality of b_{A}^{♯_{1}} (Proposition 2.2.3).

– if ♯_{2} = id, the result is immediate.

– if ♯_{2} = ♯_{2′} ⊗ ♯_{2′′} or ♯_{2} = ♯_{2′} & ♯_{2′′}, we apply the definition of b_{♯_{1}A}^{♯_{2}} and we obtain the following commutative diagram:

\xymatrix{!A \ar[r]^{^{b{♯_{1} \atop A}}} \ar[d]_{_{c_{!A}}} & !♯_{1}A \ar[d]^{_{c_{!♯_{1}A}}} \\ !A ⊗!A \ar[r]^{b_{A}^{♯_{1}}⊗b_{A}^{♯_{1}}} \ar[dr]_{b_{A}^{♯_{2′} ♯_{1}}⊗b_{A}^{♯_{2′′} ♯_{1}}} & !♯_{1}A ⊗!♯_{1}A \ar[d]^{b_{♯_{1}A}^{♯_{2′}}⊗b_{♯_{1}A}^{♯_{2′′}}} \\  & !♯_{2′}♯_{1}A ⊗!♯_{2′′}♯_{1}A \ar[r]_{m/p} & !♯_{2}♯_{1}A}

by comonoidality of b_{A}^{♯_{1}} (Proposition 2.2.3), and induction hypothesis.

• b_{A}^{⊤} = !∗_{A} by Property 3 of elementary Seely categories.

• b ; !proj: the following diagram commutes:

[figure: !A; (b); ^{b{♯_{1}&♯_{2} \atop A}}; ^{c^{!A}}; _{b{♯_{1} \atop A}}; !A ⊗!A; (c); (d); b_{A}^{♯_{1}}⊗b_{A}^{♯_{2}}; b_{A}^{♯_{1}}⊗w_{!A}; !♯_{1}A ⊗!♯_{2}A; (e); (a); p; id⊗w_{!♯_{2}A}; id⊗!∗_{♯_{2}A}; !(♯_{1}A & ♯_{2}A); !(id&∗_{♯_{2}A}); !♯_{1}A; ≃; !♯_{1}A ⊗ 1; id⊗q; !♯_{1}A ⊗!⊤; p; !(♯_{1}A & ⊤); ≃; (f)]

by (a) definition of b_{A}^{♯_{1}&♯_{2}}, (b) properties of the comonoid !A, (c) comonoidality of b_{A}^{♯_{2}}, (d) Property 3 of elementary Seely categories, (e) naturality of p and

finally (f) monoidality of !. We conclude by using !proj_{1} = !(♯_{1}A & ♯_{2}A) ⟶^{!(id&∗)}

!(♯_{1}A & ⊤) ⟶^{≃} !♯_{1}A.

E. Proof of Proposition 3.2.2

Starting from the ingredients given in [Bai00], we prove that SCOH satisfies all the axioms of elementary Seely categories.

E.0.1. Definition. [Category 𝕊COH] The category 𝕊COH is given by:

• objects: stratified coherent spaces

• morphisms: 𝕊COH(A, B) is the set of cliques of A ⊸ B

E.0.2. Lemma. 𝕊COH is a Seely category.

Proof. The categories COH and 𝕊COH are equivalent categories: the forgetful functor from 𝕊COH to COH (which maps a stratified coherent space A with depth d to the coherent space A^{d} and which maps a clique to itself) is full, faithful, surjective on objects (by considering constant stratified coherent spaces) and strictly preserves all the structures.

The visibility function V maps a clique to the sub-clique containing the visible elements.

A clique x of 𝕊COH(A, B) is right-handed if for any (a, b) ∈ x, if a is visible then b is visible and moreover V (x) is stratified. A clique x of 𝕊COH(A, B) is left-handed if for any (a, b) ∈ x, if b is visible then a is visible and moreover V (x) is stratified. A clique of 𝕊COH(A, B) is ambidextrous if it is both left-handed and right-handed.

It is immediate that stratified cliques are ambidextrous and that V is the identity on visible cliques (thus on stratified cliques).

E.0.3. Lemma. [Sub-categories of 𝕊COH] By keeping the same objects as in 𝕊COH and by restraining morphisms to left-handed, right-handed or ambidextrous cliques, one gets three sub-categories LHCOH, RHCOH and ACOH of 𝕊COH.

V defines a functor (objects are not modified) from any of LHCOH, RHCOH or ACOH to SCOH.

Proof. The identity is clearly ambidextrous and V (id) is the identity of SCOH [Bai00, Section 3.3].

If x ∈ 𝕊COH(A, B) and y ∈ 𝕊COH(B, C) are right-handed, if (a, c) belongs to x; y and if a is visible, then there exists b in B such that (a, b) ∈ x (so that b is visible) and (b, c) ∈ y thus c is visible. Moreover:

V (x; y) = V ({(a, c) | ∃b (a, b) ∈ x ∧ (b, c) ∈ y})
= {(a, c) | v(a) ∧ v(c) ∧ ∃b (a, b) ∈ x ∧ (b, c) ∈ y}
= {(a, c) | v(a) ∧ v(c) ∧ ∃b (a, b) ∈ x ∧ v(b) ∧ (b, c) ∈ y}
= {(a, c) | ∃b (a, b) ∈ V (x) ∧ (b, c) ∈ V (y)}
= V (x) ; V (y)

where v(a) means “a is visible”. This entails that V (x; y) is stratified [Bai00, Section 3.3] and that V is a functor.

In the same way, left-handed cliques and ambidextrous cliques compose, and functoriality of V holds.

To avoid confusion with the ! construction of SCOH, we use !_{m} for the usual multiset construction from COH (applied in 𝕊COH). As in [Bai00, Section 3.4], if x is a stratified clique, !x is defined by !x = V (!_{m}(x)).

The morphisms corresponding to the ⋆-autonomous structure of 𝕊COH are ambidextrous and the application of ! to them is also ambidextrous.

The morphisms corresponding to the finite products of 𝕊COH are ambidextrous. If x is a stratified clique, !_{m}x is right-handed [Bai00, Lemma 2]. The morphisms c_{!A} and w_{!A} are right-handed [Bai00, Section 3.4]. The morphism m_{A,B} is left-handed [Bai00, Section 3.4], and n = {(⋆, [⋆])} is ambidex-

trous.

The morphism p_{A,B} is ambidextrous [Bai00, Lemma 4], and q = {(⋆, [ ])} is ambidextrous.

We now turn to the proof of Proposition 3.2.2:

Proof. We are going to use V to show the commutation of the required diagrams in SCOH: if a commutative diagram deals with right-handed morphisms only in 𝕊COH, the corresponding diagram in SCOH also commutes (and the same with left-handed morphisms).

V strictly preserves all the multiplicative and additive constructions [Bai00, Section 3.4], thus SCOH is a ⋆-autonomous category with finite products. Let us give the example of naturality of the symmetry γ of ⊗ (which deals with ambidextrous morphisms only):

\xymatrix{A ⊗ B \ar[r]^{γ_{A,B}} \ar[d]_{x⊗y} & B ⊗ A \ar[d]^{y⊗x} \\ A′ ⊗ B′ \ar[r]_{γ_{A′,B′}} & B′ ⊗ A′}

In order to distinguish between constructions/morphisms in 𝕊COH and SCOH (when required), we use an exponent notation (.)^{0} for 𝕊COH. If x and y are stratified cliques, we have:

γ_{A,B} ; y ⊗ x = V (γ_{A,B}^{0}) ; V (y) ⊗ V (x)
= V (γ_{A,B}^{0}) ; V (y ⊗ x)
= V (γ_{A,B}^{0} ; y ⊗ x)
= V (x ⊗ y ; γ_{A′,B′}^{0})
= V (x ⊗ y) ; V (γ_{A′,B′}^{0})
= x ⊗ y ; γ_{A′,B′}

Concerning the exponential constructions, ! is an endofunctor [Bai00, Section 3.4]. (!A, c_{!A}, w_{!A}) is a symmetric ⊗-comonoid (the required diagrams use right-handed morphisms only), and if x is a stratified clique, !x is a comonoidal morphism [Bai00, Lemma 3].

m is a natural transformation [Bai00, Section 3.4] which defines comonoidal morphisms [Bai00, Lemma 3]. n is also a comonoidal morphism (the required diagrams use right-handed morphisms only). (!, m, n) is a symmetric monoidal functor since the additional required diagrams use left-handed morphisms only.

p_{A,B} is an isomorphism [Bai00, Lemma 4]. It defines a natural transformation since the required diagram uses right-handed morphisms only. We do it explicitly as an example:

\xymatrix{!A ⊗!B \ar[r]^{^{p^{A,B}}} \ar[d]_{!x⊗!y} & !(A & B) \ar[d]^{!(x&y)} \\ !A′ ⊗!B′ \ar[r]_{_{p_{A′,B′}}} & !(A′ & B′)}

we have:

p_{A,B} ; !(x & y) = V (p_{A,B}^{0}) ; V (!_{m}(x & y))
= V (p_{A,B}^{0} ; !_{m}(x & y))
= V (!_{m}x ⊗!_{m}y ; p_{A′,B′}^{0})
= V (!_{m}x ⊗!_{m}y) ; V (p_{A′,B′}^{0})
= V (!_{m}x) ⊗ V (!_{m}y) ; p_{A′,B′}
= !x ⊗!y ; p_{A′,B′}

q is also an isomorphism (ambidextrous morphisms only). (!, p, q) is a symmetric monoidal functor since the additional required diagrams use ambidextrous morphisms only.

Finally, the Condition 3 of the definition of elementary Seely categories is satisfied since it corresponds to diagrams using right-handed morphisms only.

References

[Bai00] Patrick Baillot. Stratified coherent spaces: a denotational semantics for light linear logic. Research Report EDI-INF-RR-0025, Laboratory for Foundations of Computer Science, Division of Informatics, University of Edinburgh, August 2000.

[Bai04] Patrick Baillot. Stratified coherent spaces: a denotational semantics for light linear logic. Theoretical Computer Science, 318(1–2):29–55, 2004.

[Ben94] Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models (extended abstract). In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, volume 933 of Lecture Notes in Computer Science, pages 121– 135. Springer, 1994.

[Bie95] Gavin Bierman. What is a categorical model of Linear Logic? In Mariangiola Dezani and Gordon Plotkin, editors, Typed Lambda Calculi and Applications ’95, volume 902 of Lecture Notes in Computer Science. Springer, April 1995.

[BT04] Patrick Baillot and Kazushige Terui. Light types for polynomial time computation in lambda-calculus. In Proceedings of the nineteenth annual symposium on Logic In Computer Science, pages 266–275. IEEE, IEEE Computer Society Press, 2004.

[DJ03] Vincent Danos and Jean-Baptiste Joinet. Linear logic and elementary time. Information and Computation, 183(1):123–137, May 2003.

[DLH05] Ugo Dal Lago and Martin Hofmann. Quantitative models and implicit complexity. In Proceedings of Foundations of Software Technology and Theoretical Computer Science, volume 3821 of Lecture Notes in Computer Science. Springer, 2005.

[Gir87] Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[Gir98] Jean-Yves Girard. Light linear logic. Information and Computation, 143(2):175–204, June 1998.

[GSS92] Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: a modular approach to polynomial time computability. Theoretical Computer Science, 97:1–66, 1992.

[JS93] André Joyal and Ross Street. Braided tensor categories. Advances in Mathematics, 102(1):20–78, November 1993.

[Laf04] Yves Lafont. Soft linear logic and polynomial time. Theoretical Computer Science, 318(1–2):163–180, June 2004.

[LTdF06] Olivier Laurent and Lorenzo Tortora de Falco. Obsessional cliques: a semantic characterization of bounded time complexity. In Proceedings of the twentyfirst annual symposium on Logic In Computer Science, pages 179–188, Seattle, August 2006. IEEE, IEEE Computer Society Press.

[Mel03] Paul-André Melliès. Categorical models of linear logic revisited. Prépublication électronique PPS//03/09//n^{∘}22 (pp), Laboratoire Preuves, Programmes et Systèmes, March 2003. To appear in Theoretical Computer Science.

[MO00] Andrzej Murawski and Luke Ong. Discreet games, light affine logic and PTIME computation. In Computer Science Logic, volume 1862 of Lecture Notes in Computer Science, pages 55–92. Springer, 2000.

[Red07] Brian Redmond. Multiplexor categories and models of soft linear logic. In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science (LFCS), volume 4514 of Lecture Notes in Computer Science, pages 472–485. Springer, June 2007.

[See89] Robert Seely. Linear logic, ⋆-autonomous categories and cofree coalgebras. Contemporary mathematics, 92, 1989.

Preuves Programmes Systèmes CNRS – Université Paris VII UMR 7126 – Case 7014 75205 Paris Cedex 13 – FRANCE

Email: Olivier.Laurent@ens-lyon.fr

This article may be accessed at http://www.tac.mta.ca/tac/ or by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/22/10/22-10.{dvi,ps,pdf}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available in .dvi, Postscript and PDF from the journal’s server at http://www.tac.mta.ca/tac/ and by ftp. It is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX2e strongly encouraged. Articles should be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor. Gavin Seal, McGill University: gavin seal@fastmail.fm

Transmitting editors.

Clemens Berger, Université de Nice-Sophia Antipolis, cberger@math.unice.fr Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown (at) btinternet.com Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Cuill Inc.: valeria@cuill.com Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Tom Leinster, University of Glasgow, T.Leinster@maths.gla.ac.uk Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca