A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Preliminary Report)^{∗}

P. N. Benton^{†} University of Cambridge

Abstract

Intuitionistic linear logic regains the expressive power of intuitionistic logic through the ! (‘of course’) modality. Benton, Bierman, Hyland and de Paiva have given a term assignment system for ILL and an associated notion of categorical model in which the ! modality is modelled by a comonad satisfying certain extra conditions. Ordinary intuitionistic logic is then modelled in a cartesian closed category which arises as a full subcategory of the category of coalgebras for the comonad.

This paper attempts to explain the connection between ILL and IL more directly and symmetrically by giving a logic, term calculus and categorical model for a system in which the linear and non-linear worlds exist on an equal footing, with operations allowing one to pass in both directions. We start from the categorical model of ILL given by Benton, Bierman, Hyland and de Paiva and show that this is equivalent to having a symmetric monoidal adjunction between a symmetric monoidal closed category and a cartesian closed category. We then derive both a sequent calculus and a natural deduction presentation of the logic corresponding to the new notion of model.

∗A shorter version of this paper is to be presented at, and submitted to the proceedings of, the 1994 Annual Conference of the European Association for Computer Science Logic, Kazimierz, Poland.

†Author’s address: University of Cambridge, Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, United Kingdom. Email: Nick.Benton@cl.cam.ac.uk. Research supported by a SERC Fellowship and the EU Esprit project LOMAPS.

2

Contents

1 Introduction 5 1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.2 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

1.2.1 Functional Programming . . . . . . . . . . . . . . . . . . . . . . . . 5 1.2.2 Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.2.3 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

1.3 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

2 The Categorical Picture 9 2.1 An Isomorphism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2 The Comonad and Comparison with Linear Categories . . . . . . . . . . . . 15

2.2.1 LNL model Implies Linear Category . . . . . . . . . . . . . . . . . . 16 2.2.2 Linear Category Implies LNL model . . . . . . . . . . . . . . . . . . 22 2.2.3 Additives and the Seely Isomorphisms . . . . . . . . . . . . . . . . . 25

2.3 The Monad and Comparison with Let-CCCs . . . . . . . . . . . . . . . . . 27

2.3.1 Strong Monads . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.4 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

2.4.1 ω-complete Partial Orders . . . . . . . . . . . . . . . . . . . . . . . . 29 2.4.2 Abelian Groups . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

3 LNL Logic 31

3.1 Sequent Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.1.1 The First Wrong Way . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3.1.2 The Second Wrong Way . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.1.3 A Well-Behaved Sequent Calculus . . . . . . . . . . . . . . . . . . . 34 3.1.4 Cut Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 3.1.5 Cut Elimination and Semantic Equality . . . . . . . . . . . . . . . . 42 3.1.6 Variations: Introducing Additive Non-Linear Contexts . . . . . . . . 43 3.1.7 Variations: A Parsimonious Presentation . . . . . . . . . . . . . . . 45

3.2 Natural Deduction and LNL Terms . . . . . . . . . . . . . . . . . . . . . . . 47 3.2.1 The Natural Deduction Rules . . . . . . . . . . . . . . . . . . . . . . 47 3.2.2 Term Assignment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 3.2.3 Normalisation and Reduction . . . . . . . . . . . . . . . . . . . . . . 51

3.3 Translations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 3.3.1 ILL to LNL Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 3.3.2 LNL Logic to ILL . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 3.3.3 Further Results on the Translations . . . . . . . . . . . . . . . . . . 60

4 Conclusions and Further Work 62

5 Acknowledgements 63 4 CONTENTS

1 Introduction

1.1 Background

This paper concerns a variant of the intuitionistic fragment of Girard’s linear logic [Gir87]. As is well-known, linear logic does not contain the structural rules of weakening and contraction, but these are reintroduced in a controlled way via a unary operator, written ! and pronounced ‘of course’, ‘bang’ or ‘shriek’. The sequent calculus rules for ! are the following:

!Γ ⊢ A ; \overline{Promotion} ; !Γ ⊢!A  Γ, A ⊢ B ; \overline{Dereliction} ; Γ,!A ⊢ B

Γ,!A,!A ⊢ B ; \overline{Contraction} ; Γ,!A ⊢ B  Γ ⊢ B ; \overline{Weakening} ; Γ,!A ⊢ B

The rules above allow ordinary intuitionistic logic to be interpreted within intuitionisitic linear logic via (for example) the so-called ‘Girard translation’. In [BBHdP92, BBHdP93b, BBHdP93a], Benton, Bierman, Hyland and de Paiva formulated a natural deduction presentation of the multiplicative/exponential fragment of ILL, together with a term calculus (extending the propositions as types analogy to linear logic) and a categorical model (a linear category). In that work, the multiplicative (i.e. ⊗,−∘) part of the logic is modelled in a symmetric monoidal closed category (SMCC). That much is standard and well-understood. The ! modality is then modelled by a monoidal comonad on the SMCC which is required to satisfy certain extra (and non-trivial) conditions. These extra conditions are sufficient to ensure that the category of coalgebras for the comonad contains a full subcategory which is cartesian closed and thus models the interpretation of IL in ILL.

Whilst the view that linear logic is primary and that ordinary logic is merely a part of linear logic is appealing (particularly if one takes seriously the claims of linear logic to be “the logic behind logic”), it is not necessarily always the best way of seeing the situation. This paper tries to present a more symmetric view of the relationship between IL and ILL, starting from a model-theoretic perspective, and it seems worth trying to give some motivation for why this might be worth doing.

1.2 Motivation

1.2.1 Functional Programming

From a practical point of view, there are a number of reasons why the standard linear term calculus (LTC) of [BBHdP92] might be considered unsuitable as the basis of a linear functional programming language. Firstly, linear functional programming is verbose and unnatural – whilst the linear term calculus might well be a useful intermediate language for a compiler, it is not very appropriate as a language for everyday programming. If linearity is to be made visible to the programmer at all, it appears preferable to have some extension of a traditional non-linear language in which one could write the occasional linear function in order to deal with input/output, in-place update or whatever.

A second, more fundamental, problem is that, despite considerable research effort, the precise way in which a linear language can help with what we have deliberately referred to rather vaguely as ‘input/output, in-place update or whatever’ is still not clear. Most published proposals for using linear types to control or describe intensional features of functional programs are either unconvincing or use type systems which are only loosely inspired by linear logic. Systems in the last category can, pragmatically, be extremely successful; the most obvious example being the language CLEAN. The type system of CLEAN [BS93] incorporates a ‘uniqueness’ operator for (roughly) making non-linear types linear. This is in some sense dual to the ! of linear logic, which allows linear types to be treated non-linearly. Unique types in CLEAN are used to add destructive updates and I/O to the language in a clean (referentially transparent) way.

One (currently somewhat speculative) aim of the work described here is to provide a sound mathematical and logical basis for a type system like that of CLEAN. We are motivated and encouraged not only by the similarities between CLEAN and the calculus to be presented here (the LNL term calculus), but also by the fact that other researchers looking at practical implementations of linear languages have come up with systems which include aspects of the LNL term calculus. For example, Lincoln and Mitchell’s linear variant [LM92] of Fairbairn and Wray’s ‘three instruction machine’ [FW87] divides memory into two spaces corresponding to linear and non-linear objects. Similarly, Wadler’s ‘active and passive’ type system [Wad92] separates linear from non-linear types in an interesting way. It should also be mentioned that some of Wadler’s earliest attempts to define a linear type system for a functional language flagged linear types as the exception, rather than the rule [Wad90], although he later reverted to ‘belling the cat’ by annotating non-linear types.

Jacobs [Jac93] has independently described how a sequent calculus inspired by CLEAN’s uniqueness types may be interpreted using the linear categories of [BBHdP92] under some extra simplifying assumptions which are sufficient to make the whole Eilenberg-Moore category of coalgebras be cartesian closed. Jacobs’s logic turns out to be essentially the same as LNL logic, and we will discuss his work further in Section 3.1.7.

The logic described here is, in a fairly strong sense, equivalent to ordinary ILL. How then could such a system possibly lead to a better linear programming language? The first answer is that we refine ILL: there are distinct LNL terms which correspond to the same LTC term. The second answer is that logical systems which are denotationally equivalent may still have very different dynamic (proof-theoretic) behaviours. However, such speculations should only be viewed as motivation for studying the logic. We do not yet have any formal results concerning, for example, the memory graphs of programs written in a language based on the LNL term calculus.

1.2.2 Logic

From a more logical point of view, there has recently been much interest in Girard’s system LU [Gir93] and related systems in which the (multi)sets of formulae occuring in sequents are split into different zones. Formulae in some zones are treated classically, whilst those in other zones are treated linearly.

Intuitionistic logics inspired by LU have been proposed by Plotkin [Plo93] and Wadler [Wad93]. It is desirable to study the proof and model theory of such systems directly, rather than treating them as syntactic sugar for, for example, ordinary linear logic (if only to verify that it is possible to treat them as such syntactic sugar). The logic of this paper should turn out to be equivalent to a subsystem of LU, though there are some superficial differences of presentation such as the fact that LNL logic has no zones – the formulae themselves are either linear or conventional.^{1} 1.2.3 Semantics

1Though we, perhaps unwisely, abuse notation by writing a semicolon between formulae of different

From the categorical perspective, it seems natural to explore the more symmetric situation where one starts from an SMCC and a CCC with (adjoint) functors between them, rather than an SMCC with sufficient extra structure to ensure the existence of such a CCC. This is particularly true in the light of the fact that the definition of a linear category in [BBHdP92] was arrived at mostly from the proof theory of linear logic, but also (and this was something of a ‘hidden agenda’) from a desire to have enough structure to be able to derive an appropriate CCC from the model.^{2} It is also fair to say that the definition of a linear category is surprisingly complicated, so looking for simpler models, or simpler presentations of the same models, is a good idea. Pratt has also suggested that the comonad modelling ! might be less fundamental than the adjunctions from which it arises [Pra92].

1.3 Overview

The initial motivation for the present work comes from the categorical picture sketched in the previous section, and it is this which is explored first in Section 2. Once the definition has been made a little more precise, we shall show that such a situation leads to a comonad on the linear part of the model which automatically satisfies all the extra conditions required of a linear category, and thus gives a sound model of ILL including the ! operator. Furthermore, the converse holds – every linear category gives rise to such a pair of categories. Thus we have an alternative, simpler, definition of what constitutes a model for ILL. This can be seen as giving a purely category-theoretic reconstruction of !, in that a linear category (a model for ILL with !) is exactly what one obtains if one attempts directly to model an interpretation of IL in ILL without the !.

Another interesting feature of the model is that it gives rise to a strong monad on the CCC part. Thus one obtains a model not just of the lambda calculus, but of Moggi’s computational lambda calculus [Mog89, Mog91]. This may shed further light on the ‘monads versus comonads’ debate which has occasionally arisen in programming language theory. As we shall see, however, not all strong monads arise in this way, so the connection is not quite as neat as one might hope.

Section 3 then looks at the logic and term calculus which are associated with our new notion of model. After a brief description of two unsatisfactory versions of the logic, we formulate a sequent calculus presentation which satisfies cut-elimination and then give an equivalent natural deduction system. This then gives, by the Curry-Howard correspondence, an interesting term calculus which combines the usual simply-typed lambda calculus with a linear lambda calculus. We also consider translations in both directions between this new term calculus and the linear calculus introduced in [BBHdP92].

This paper is fairly self-contained and assumes only a basic knowledge of category theory (up to, say, adjunctions), some familiarity with linear logic and an understanding of typed lambda calculus and the Curry-Howard correspondence. A nodding acquaintance with previous work on the linear term calculus and categorical models of ILL is also desirable.

kinds.

2This is not to say that there is anything in the model which is not justifiable in terms of the proof theory (given a proper proof-theoretic account of η-rules), but merely that, given that a translation of IL proofs into ILL proofs exists, any correct model for ILL must be able to reflect the translation semantically.

This is a preliminary report, and doubtless contains errors and omissions. It certainly leaves plenty of obvious questions unanswered. Comments, questions and suggestions for improvement are welcome.

2 The Categorical Picture

Our aim is to present a logic/terms/categories correspondence, similar to that between intuitionistic logic, simply-typed lambda calculus and cartesian closed categories, in which the categorical vertex of the triangle consists of (essentially) the following:

1. a cartesian closed category (C, 1, ×, →);

2. a symmetric monoidal closed category (L, I, ⊗, −∘) and

3. a pair of functors G : L → C and F : C → L between them with F ⊣ G (i.e. F is the left adjoint to G).

Intuitively, the requirement that the two functors be adjoint should be understood as saying that there is an interpretation of IL (the CCC) into ILL (the SMCC).

We will, however, need our categorical model to satisfy some extra conditions before we can have any hope of it modelling a logic or term calculus. It is necessary for the two functors and the unit and counit of the adjunction to behave well with respect to the monoidal structures of the two categories. The reason for this is that we have to handle contexts correctly, and the multicategorical structure implied by the comma in a context will be represented by the appropriate tensor product. The need for such extra structure also arises in, for example, models of the computational lambda calculus (the monad must be strong) and linear categories (the comonad must be symmetric monoidal). The extra conditions which we shall impose are not ad hoc, but are just what is required to ensure coherence.^{3} Although the present paper gives all the definitions and proofs in an elementary form, it should be noted that morally we should regard everything as taking place in the 2-category of symmetric monoidal categories, in which context the extra monoidal conditions arise more naturally. Indeed, this view is an instance of a general principle concerning the categorical modelling of programming languages expressed by Moggi in [Mog91]^{4}

when studying a complex language the 2-category Cat of small categories, functors and natural transformations may not be adequate; however, one may replace Cat with a different 2-category, whose objects capture better some fundamental structure of the language, while less fundamental structure can be modelled by 2-categorical concepts.

Definition 1 A monoidal category is a category M equipped with a bifunctor ⊗ : M × M → M, and object I of M, and natural isomorphisms

α_{X,Y,Z} : (X ⊗ Y) ⊗ Z → X ⊗ (Y ⊗ Z)
l_{X} : I ⊗ X → X
r_{X} : X ⊗ I → X

3As has become traditional, however, we shall say very little about this important issue...

4Thanks to Ian Stark for bringing this quote to my attention.

which satisfy the following pair of coherence diagrams:

[figure: W ⊗ (X ⊗ (Y ⊗ Z)); (W ⊗ X) ⊗ (Y ⊗ Z); ((W ⊗ X) ⊗ Y) ⊗ Z; W ⊗ ((X ⊗ Y) ⊗ Z); (W ⊗ (X ⊗ Y)) ⊗ Z; α; α; α; α ⊗ 1; 1 ⊗ α]

[figure: (X ⊗ I) ⊗ Y; X ⊗ Y; X ⊗ (I ⊗ Y); α; r ⊗ 1; 1 ⊗ l]

and for which l_{I} = r_{I}.

Definition 2 A symmetric monoidal category (SMC) is a monoidal category (M, ⊗, I, α, l, r) together with a natural transformation σ_{X,Y} : X ⊗ Y → Y ⊗ X satisfying the following three coherence conditions:

[figure: (Y ⊗ X) ⊗ Z; Y ⊗ (X ⊗ Z); Y ⊗ (Z ⊗ X); (X ⊗ Y) ⊗ Z; X ⊗ (Y ⊗ Z); (Y ⊗ Z) ⊗ X; α; σ; σ ⊗ 1; α; α; 1 ⊗ σ]

[figure: Y ⊗ X; X ⊗ Y; X ⊗ Y; σ; σ; 1; I ⊗ X; X ⊗ I; X; σ; l; r]

Note that every cartesian category (i.e. with finite products) is an SMC.

Definition 3 A symmetric monoidal closed category (SMCC) is a symmetric monoidal category (M, ⊗, I, α, l, r, σ) such for each B ∈ M_{0} the functor − ⊗ B : M → M has a (specified) right adjoint. Thus there is for every A, C ∈ M_{0} an object (B −∘C) and a natural bijection

M(A ⊗ B, C) ≅ M(A, B −∘C)

Symmetric monoidal closed categories are also sometimes called autonomous categories.

Definition 4 A cartesian closed category (CCC) is an SMCC for which the tensor product is cartesian.

Whilst one might wish to consider functors between SMCs which preserve the structure on the nose or up to natural isomorphism, we shall take the class of functors between SMCs to be those preserving the structure up to a comparsion. We thus make the following definitions.

Definition 5 Given monoidal categories (M, ⊗, I, α, l, r) and (M′, ⊗′, I′, α′, l′, r′), a monoidal functor F : M → M′ is a functor from M to M′ equipped with a map m_{I} : I′ → F (I) in M′ and a natural transformation m_{X,Y} : F (X) ⊗′ F (Y) → F (X ⊗ Y) which satisfy the following coherence conditions:

[figure: F ((X ⊗ Y) ⊗ Z); F (X ⊗ Y) ⊗′ F (Z); (F (X) ⊗′ F (Y)) ⊗′ F (Z); F (X ⊗ (Y ⊗ Z)); F (X) ⊗′ F (Y ⊗ Z); F (X) ⊗′ (F (Y) ⊗′ F (Z)); α′; m ⊗′ 1; m; F (α); 1 ⊗′ m; m]

[figure: F (I) ⊗′ F (X); I′ ⊗′ F (X); F (I ⊗ X); F (X); l′; m ⊗′ 1; m; F (l); F (X) ⊗′ F (I); F (X) ⊗′ I′; F (X ⊗ I); F (X); r′; 1 ⊗′ m; m; F (r)]

Definition 6 If M and M′ above are symmetric monoidal, then F is a symmetric monoidal functor if it is monoidal and in addition satisfies the following coherence condition:

[figure: F (X ⊗ Y); F (X) ⊗′ F (Y); F (Y ⊗ X); F (Y) ⊗′ F (X); m; σ′; m; F (σ)]

In the definition of a symmetric monoidal functor, one of the coherence diagrams for l and r is redundant, as it follows from the other and the diagram for σ. Note also that the identity functor is (symmetric) monoidal and that (symmetric) monoidal functors can be composed in an obvious way – if (F, m) : M → M′ and (G, n) : M′ → M′′ then their composite is given by the usual composition of functors together with the comparison natural transformation p_{X,Y} : GF X ⊗′′ GF Y → GF (X ⊗ Y) where p_{X,Y} = G(m_{X,Y}) ∘ n_{F X,F Y} (and similarly for the nullary version). It is then routine to check that (GF, p) is indeed a (symmetric) monoidal functor, and that (symmetric) monoidal categories and (symmetric) monoidal functors form a category.

Definition 7 If (F, m) and (G, n) are monoidal functors from an MC M to an MC M′, then a monoidal natural transformation from (F, m) to (G, n) is a natural transformation f_{X} from F to G which is compatible with the comparison maps in the sense that the following two diagrams commute:

[figure: G(X) ⊗′ G(Y); F (X) ⊗′ F (Y); G(X ⊗ Y); F (X ⊗ Y); m; f_{X} ⊗′ f_{Y}; f_{X⊗Y}; n]

[figure: I′; F (I); G(I); f_{I}; m; n]

Definition 8 If M and M′ are (symmetric) monoidal categories then a (symmetric) monoidal adjunction between them is an ordinary adjunction in which both of the functors are (symmetric) monoidal functors and both the unit and the counit of the adjunction are monoidal natural transformations (with respect to the natural monoidal structure on the two composite functors, as defined above).

Having made the basic definitions, we are now in a position to define more precisely the categorical model sketched earlier.

Definition 9 A linear/non-linear model (LNL model) consists of

1. a cartesian closed category (C, 1, ×, →);

2. a symmetric monoidal closed category (L, I, ⊗, −∘) and

3. a pair of symmetric monoidal functors (G, n) : L → C and (F, m) : C → L between them which form a symmetric monoidal adjunction with F ⊣ G.

We shall usually use A, B, C to range over objects of L and X, Y, Z for objects of C. Spelling the definition out in a bit more detail, this means that we have a pair of natural transformations η : 1_{C}→^{·}GF and ε : F G→^{·}1_{L} which satisfy the triangle laws for an adjunction:

[figure: GA; GF GA; GA; η_{GA}; 1_{GA}; Gε_{A}; F X; F GF X; F X; F η_{X}; 1_{F X}; ε_{F X}]

That η and ε are monoidal natural transformations means that the following four diagrams commute:

[figure: GF (X × Y); X × Y; G(F X ⊗ F Y); GF X × GF Y; η_{X} × η_{Y}; η_{X×Y}; n_{F X,F Y}; G(m_{X,Y}); A ⊗ B; F GA ⊗ F GB; F (GA × GB); F G(A ⊗ B); ε_{A} ⊗ ε_{B}; m_{GA,GB}; F (n_{A,B}); ε_{A⊗B}]

[figure: 1; 1; GF (1); η_{1}; 1; G(m) ∘ n; F G(I); I; I; ε_{I}; F (n) ∘ m; 1]

2.1 An Isomorphism

An important consequence of the definition of an LNL model is that as well as the natural transformations

m_{X,Y} : F X ⊗ F Y → F (X × Y)
n_{A,B} : GA × GB → G(A ⊗ B)

and their nullary versions, the maps

m : I → F 1
n : 1 → GI

we have a family of maps

p_{X,Y} : F (X × Y) → F X ⊗ F Y

given by the transpose of n_{F X,F Y} ∘ η_{X} × η_{Y}:

[figure: F (X × Y); F (GF X × GF Y); F G(F X ⊗ F Y); F X ⊗ F Y; F (η_{X} × η_{Y}); F (n_{F X,F Y}); ε_{F X⊗F Y}]

and a map p : F 1 → I given by

[figure: F 1; F GI; I; F n; ε_{I}]

It is straightforward to check that the p_{X,Y} are the components of a natural transformation. We do not, however, get a collection of maps in the other possible direction, viz. from G(A ⊗ B) to GA × GB.

Proposition 1 In an LNL model (in fact for any monoidal adjunction), the maps m_{X,Y} are the components of a natural isomorphism with inverses p_{X,Y} and, furthermore, the map m is an isomorphism with inverse p:

F (X) ⊗ F (Y) ≅ F (X × Y)
I ≅ F (1)

Proof. We shall just prove the first of the isomorphisms above as the second is very similar. Firstly, we need to show that m_{X,Y} ∘ p_{X,Y} = 1_{F (X×Y)}:

[figure: F (X × Y); F (GF X × GF Y); F GF (X × Y); F G(F X ⊗ F Y); F (X × Y); F X ⊗ F Y; F (η_{X} × η_{Y}); 1; F (η_{X×Y}); F (n_{F X,F Y}); F G(m_{X,Y}); ε_{F X⊗F Y}; ε_{F (X×Y)}; m_{X,Y}]

The square on the right commutes by naturality of ε, whilst that on the left commutes as it is F applied to the earlier square which says that η is monoidal. The triangle on the bottom is one of the triangles for an adjunction and so the path up the left hand side, along the top and down the right hand side is equal to that along the bottom, as required.

Secondly, we claim that p_{X,Y} ∘m_{X,Y} = 1_{F X⊗F Y}, which follows from a similar diagram:

[figure: F X ⊗ F Y; F (X × Y); F GF X ⊗ F GF Y; F (GF X × GF Y); F X ⊗ F Y; F G(F X ⊗ F Y); m_{X,Y}; 1 ⊗ 1; F (η_{X}) ⊗ F (η_{Y}); F (η_{X} × η_{Y}); m_{GF X,GF Y}; F (n_{F X,F Y}); ε_{F X} ⊗ ε_{F Y}; ε_{F X⊗F Y}]

The square on the left commutes by naturality of m and that on the right because ε is monoidal. The triangle on the bottom commutes by two applications of one of the triangle laws for an adjunction and so the outer path is equal to that along the bottom, which is trivially equal to the identity. □

So F preserves the monoidal structure up to an isomorphism rather than merely up to a comparison. That is to say, F is a strong functor. This has a converse – given a strong functor with an adjoint, the adjoint (in fact the whole adjunction) has a unique monoidal structure. In our case, this means that instead of taking n as part of the definition of an LNL model and deriving p, we could equally well have started with p and defined n_{A,B} to be the composite

G(ε_{A} ⊗ ε_{B}) ∘ G(p_{GA,GB}) ∘ η_{GA×GB}

This fact will crop up again in Section 3.1.2.

There is, of course, a lot more interesting structure in an LNL model. To begin with, the adjunction induces a comonad on L and a monad on C. We discuss each of these below. Given one of the categories and the appropriate monad (triple) or comonad (cotriple), the other category and the adjunction arise as a resolution of the triple (cotriple). In contrast with some other proposed models of intuitionistic linear logic, we do not assume that this is initial or terminal in the category of all resolutions.

2.2 The Comonad and Comparison with Linear Categories

The comonad on L is (F G, ε : F G → 1, δ : F G → F GF G) where ε is the counit of the adjunction and δ is the natural transformation with components δ_{A} : F G(A) → F GF G(A) given by δ_{A} = F (η_{G(A)}). Writing ! for F G, we obtain the usual comonad diagrams:

[figure: !A; !A; !!A; !A; 1; δ_{A}; ε_{!A}; 1; !(ε_{A}); !!A; !A; !!!A; !!A; δ_{A}; δ_{A}; !(δ_{A}); δ_{!A}]

Lemma 2 The comonad (!, ε, δ) is symmetric monoidal, i.e. ! is a symmetric monoidal functor and ε and δ are monoidal natural transformations.

Proof. Clearly ! is a symmetric monoidal functor. The monoidal structure is given by a natural transformation q with components q_{A,B} :!A⊗!B →!(A ⊗ B) and a map q : I →!I whose definitions are

q_{A,B} = F (n_{A,B}) ∘ m_{GA,GB}
q = F (n) ∘ m

That ε is monoidal is part of the definition of an LNL model. The case of δ requires some easy checking. □

In [BBHdP92], we defined a model of the multiplicative/exponential fragment of intuitionistic linear logic as follows:

Definition 10 A linear category is specified by the following data:

1. A symmetric monoidal closed category (L, ⊗, I, −∘).

2. A symmetric monoidal comonad (!, ε, δ, q) on L.

3. Monoidal natural transformations^{5} with components

e_{A} :!A → I
d_{A} :!A →!A⊗!A

such that

(a) each (!A, e_{A}, d_{A}) is a commutative comonoid,

(b) e_{A} and d_{A} are coalgebra maps^{6}, and

(c) all coalgebra maps between free coalgebras preserve the comonoid structure.

2.2.1 LNL model Implies Linear Category

Now, any LNL model includes, by definition, part 1 of Definition 10, and we have just seen (Lemma 2) that it also satisfies part 2. Furthermore, there are plausible candidates for e_{A} and d_{A}:

e_{A} =^{def}p ∘ F (∗_{GA})

where ∗_{GA} is the unique map from GA to the terminal object 1 of C, and

d_{A} =^{def}p_{GA,GA} ∘ F (Δ_{GA})

where Δ_{GA} is the diagonal map from GA to GA × GA in C. We now embark on showing that these satisfy all the conditions which ensure that we have a linear category. The reader who is prepared to take this on trust may prefer to skip straight to Corollary 8.

Lemma 3 e_{A} and d_{A} as defined above are the components of natural transformations.

Proof. This is obvious as a result of general facts about composition of, and application of functors to, natural transformations. For example, we have to check that for any f : A → B,

[figure: !B; !A; !B⊗!B; !A⊗!A; !f; !f⊗!f; d_{A}; d_{B}]

5Note that this only makes sense because the functors A ↦ I and A ↦!A⊗!A are themselves (symmetric)

monoidal, but this is easily seen to be true. See the proof of Lemma 4 below for the details.

6Exactly what this means is spelled out in the proof of Lemma 6.

which expands to give

[figure: F GB; F GA; F (GB × GB); F GB ⊗ F GB; F (GA × GA); F GA ⊗ F GA; F (Δ_{GB}); p_{GB,GB}; F (Δ_{GA}); p_{GA,GA}; F Gf; F (Gf × Gf); F Gf ⊗ F Gf]

The left-hand square commutes by F applied to naturality of Δ and the other by naturality of p. Naturality of e is similar. □

Lemma 4 e and d are monoidal natural transformations.

Proof. We first have to make explicit the symmetric monoidal structure on the functors K : A ↦ I and D : A ↦!A⊗!A. For K we require a natural transformation s_{A,B} : K(A) ⊗ K(B) → K(A ⊗ B) and a map s : I → K(I). Clearly we can take s_{A,B} = l_{I} and s = 1_{I} and then verification of the coherence conditions showing that (K, s) is symmetric monoidal is trivial.

For D we need a natural transformation with components

t_{A,B} : (!A⊗!A) ⊗ (!B⊗!B) →!(A ⊗ B)⊗!(A ⊗ B)

together with a map t : I →!I⊗!I. We take t_{A,B} to be the composite

[figure: (!A⊗!A) ⊗ (!B⊗!B); (!A⊗!B) ⊗ (!A⊗!B); !(A ⊗ B)⊗!(A ⊗ B); iso; q_{A,B} ⊗ q_{A,B}]

where iso represents a combination of natural isomorphisms^{7} and t to be (q ⊗ q) ∘ l^{−1}. That t_{A,B} is natural and that the coherence conditions making D a symmetric monoidal functor are satisfied is trivial.

The lemma is thus the statement that the following four diagrams commute:

[figure: I ⊗ I; !A⊗!B; !(A ⊗ B); I; l_{I}; q_{A,B}; e_{A} ⊗ e_{B}; e_{A⊗B}; !I; I; I; q; e_{I}; 1] [figure: (!A⊗!A) ⊗ (!B⊗!B); !(A ⊗ B)⊗!(A ⊗ B); !A⊗!B; !(A ⊗ B); t_{A,B}; q_{A,B}; d_{A} ⊗ d_{B}; d_{A⊗B}] 7There is actually a choice here, but it doesn’t matter which iso we pick.

[figure: !I; I; !I⊗!I; q; d_{I}; t]

We will verify a couple of these. Firstly, the triangle for e expands and fills in as follows:

[figure: F GI; F 1; I; F 1; I; m; F (n); F (∗_{GI}); p; F (1); 1]

The triangle commutes because it is F applied to a triangle which commutes by the uniqueness of maps into 1. The square commutes because F is a functor and m = p^{−1} (Proposition 1).

The square for e expands and fills in like this (omitting subscripts on natural transformations):

[figure: F G(A ⊗ B); F (GA × GB); F GA ⊗ F GB; F 1; F (1 × 1); F 1 ⊗ F 1; F 1 ⊗ F 1; I ⊗ F 1; I; I; I ⊗ I; m; F (n); F (∗) ⊗ F (∗); F (∗ × ∗); F (∗); p ⊗ p; 1; m; F (l); 1 ⊗ m; m ⊗ 1; l; l; 1; m; p]

The top left square commutes by naturality of m, and the bottom left one by the fact that 1 is terminal. The triangle at the bottom of the right hand side and the quadrilateral at the top of the right hand side both commute because p = m^{−1}. The triangle in the middle at the left of the right hand side of the diagram commutes because F is a monoidal functor, and the remaining quadrilateral by naturality of l.

Filling in the two diagrams for d is left as an exercise in diagram chasing for the reader. They are rather larger, but fundamentally similar to those for e. □

Lemma 5 For any A, (!A, e_{A}, d_{A}) is a commutative comonoid.

Proof. This requires the following three diagrams to commute:

[figure: !A ⊗ I; !A⊗!A; !A; r^{−1}; d_{A}; 1_{!A} ⊗ e_{A}; !A; !A⊗!A; !A⊗!A; σ; d_{A}; d_{A}]

[figure: !A⊗!A; (!A⊗!A)⊗!A; !A ⊗ (!A⊗!A); !A; !A⊗!A; d_{A} ⊗ 1; α; d_{A}; d_{A}; 1 ⊗ d_{A}]

These are all fairly straightforward. For example, the first diagram can be expanded and filled in as follows:

[figure: F GA ⊗ F GA; F (GA × GA); F GA; F (GA × GA); F GA ⊗ F 1; F GA ⊗ F 1; F (GA × 1); F GA ⊗ I; F GA; 1; F (Δ); p; 1 ⊗ F (∗); 1 ⊗ p; r; 1; F (1 × ∗); m; 1; m; F (π_{1}); 1 ⊗ m]

Taking the regions clockwise from the top, the first is a consequence of obvious facts about cartesian products (in fact, that they give a commutative comonoid structure in C). The second commutes because F is a monoidal functor. The third and fifth because p = m^{−1}, and the fourth because m is a natural transformation.

The other two diagrams commute by similar reasoning. □

Lemma 6 e_{A} and d_{A} are coalgebra morphisms (with respect to the canonical coalgebra structures on I,!A and !A⊗!A, see Section 2.2.2).

Proof. We need the following pair of diagrams:

[figure: !!A; !A; !I; I; e_{A}; δ_{A}; !e_{A}; q; !A⊗!A; !A; !!A⊗!!A; !(!A⊗!A); !!A; δ_{A}; d_{A}; δ_{A} ⊗ δ_{A}; q_{!A,!A}; !d_{A}]

The second of these can be dealt with like this:

[figure: F GA ⊗ F GA; F (GA × GA); F GA; F GF GA ⊗ F GF GA; F (GA × GA); F (GF GA × GF GA); F GF (GA × GA); F G(F GA ⊗ F GA); F G(F GA ⊗ F GA); F GF GA; F (η); F (Δ); p; F (η) ⊗ F (η); m; F (n); 1; F GF (Δ); F G(p); F G(m); F (η); 1; F (η × η); m]

The large square on the left commutes by naturality of η. The two triangles both commute because p = m^{−1}. The region on the far right commutes by naturality of m, and that in the middle because η is monoidal.

The other diagram is similar. □

Lemma 7 Any coalgebra map f : (!A, δ_{A}) → (!B, δ_{B}) between free coalgebras preserves the comonoid structure given by e and d.

Proof. This means that for any such f, the following pair of diagrams commute:

[figure: I; !A; !B; e_{A}; e_{B}; f; !B; !A; !B⊗!B; !A⊗!B; d_{B}; d_{A}; f; f ⊗ f]

The second of these can be expanded out like this:

[figure: !B⊗!B; !(!B⊗!B); !!B⊗!!B; !!B; !B; !A⊗!A; !(!A⊗!A); !!A⊗!!A; !!A; !A; δ; d; q; ε; d; δ; d; q; ε; d; f; !f; !f⊗!f; !(f ⊗ f); f ⊗ f]

Taking the regions in the middle from the top, the first commutes by assumption (that f is a coalgebra morphism) and the second, third and fourth by naturality of d,q and ε respectively. The remaining two regions are both easily seen to commute, since they expand as follows:

[figure: F GA ⊗ F GA; F (GA × GA); F GA; F GF GA; F G(F GA ⊗ F GA); F (GF GA × GF GA); F GF GA ⊗ F GF GA; F (GF GA × GF GA); F (η); F (Δ); p; F (Δ); ε; p; m; F (n); 1; F (η × η)]

The triangle on the right commutes because p = m^{−1} and that on the top left by naturality of Δ. The middle region commutes simply because it is the definition of p. □

Taking the previous lemmas together, we have shown

Corollary 8 Any LNL model is a linear category. □

2.2.2 Linear Category Implies LNL model

In this section we sketch the proof of the converse to Corollary 8. Whilst this is largely a matter of recalling results which were proved in [BBHdP92] and [Bie94a], by doing this carefully we obtain a slightly better understanding of the situation.

Assume that L is a linear category as in Definition 10. We need to show that this gives rise to a CCC C and a symmetric monoidal adjunction between L and C as in Definition 9. Recall that the comonad on L gives rise to two categories of algebras:

• The Eilenberg-Moore category L^{!}. This has as objects all the !-coalgebras (A, h_{A} : A →!A) and as morphisms all the coalgebra morphisms.

• The (co-)Kleisli category L_{!}. This is the full subcategory of L^{!} which has as objects all the free !-coalgebras (!A, δ_{A} :!A →!!A). (This is not quite the most common definition of L_{!}, but the two definitions are equivalent.)

Each of these categories comes with a pair of adjoint functors F ⊣ G where G : A ↦ (!A, δ_{A}) and F : (A, h_{A}) ↦ A, thus (note that we are overloading F and G):

[figure: L; L^{!}; L_{!}; F; G; G; F; i]

where i : L_{!} ↪ L^{!} is the inclusion functor.

Lemma 9 If L is a linear category then L^{!} has finite products.

Proof. The terminal object is (I, q : I →!I). The unique map from (A, h_{A}) to the terminal object is e_{A} ∘h_{A}. The product of (A, h_{A}) and (B, h_{B}) is (A⊗B, q_{A,B} ∘(h_{A} ⊗h_{B})). Projections and diagonals are given by the following composites

π_{1} = [figure: A ⊗ B; A ⊗!B; A ⊗ I; A; 1 ⊗ h_{B}; 1 ⊗ e_{B}; r]
Δ_{A} = [figure: A; !A; !A⊗!A; A ⊗ A; h_{A}; d_{A}; ε_{A} ⊗ ε_{A}]

These are easily checked to satisfy the relevant conditions. □

In general, there is no reason why the Eilenberg-Moore category should be cartesian closed, since there is no reason why it should have an internal hom for arbitrary pairs of coalgebras. There are extra conditions which are sufficient to ensure that this does happen, such as requiring that L^{!} have equalisers of coreflexive pairs [Bie94a] or simply all equalisers [Jac93]. Although there are non-trivial examples in which such conditions hold, we shall not consider them further since we can find an appropriate CCC without them.

Lemma 10 In L^{!}, all the free coalgebras are exponentiable. That is, there is an internal hom into any free coalgebra (!B, δ_{B}). Furthermore, the internal hom is itself a free coalgebra.

Proof. We claim that

[(A, h_{A}), (!B, δ_{B})] =^{def} (!(A −∘B), δ_{A−∘B})

is an internal hom. This follows from the adjunction between F and G and from the closed structure on L, since for any coalgebra (C, h_{C}) there are bijections:

L^{!}((C, h_{C}), (!(A −∘B), δ_{A−∘B}))

= L(C, A −∘B)

= L(C ⊗ A, B)

= L^{!}((C ⊗ A, h_{C⊗A}), (!B, δ_{B}))

for any h_{C⊗A} giving C ⊗ A a coalgebra structure, in particular that arising from the product on L^{!}. So an instance of the last line is

L^{!}((C, h_{C}) × (A, h_{A}), (!B, δ_{B}))

as required. □

Now, notice that in any cartesian category, if an object X is exponentiable then so is [Y, X] for any Y, since we can take [Z, [Y, X]] to be [Z × Y, X]. Furthermore, the product of two exponentiable objects X and Y is exponentiable since we can take [Z, X × Y] to be [Z, X] × [Z, Y]. Taking this together with the previous lemma, we have:

Lemma 11 The full subcategory Exp(L^{!}) of the Eilenberg-Moore category having as objects the exponentiable coalgebras is cartesian closed and contains the Kleisli category L_{!}.

□

Note that the Kleisli category is not, in general, cartesian closed, since the product of two free coalgebras is not necessarily free. We shall consider a case in which this does happen in Section 2.2.3. In the general case, we do have the following, however:

Lemma 12 The full subcategory L_{!}^{∗} of Exp(L^{!}) consisting of finite products of free coalgebras is cartesian closed. □

The situation can be pictured thus:

[figure: L; Exp(L^{!}); L^{!}; L_{!}^{∗}; L_{!}; F; G; G; F; i; i; i]

We claim that either of these two CCCs will give rise to an LNL model.^{8} In what follows we let C stand for either Exp(L^{!}) or L_{!}^{∗}.

It is easy to see that F and G are still adjoint functors when regarded as going between C and L, so it merely remains to show that this is a symmetric monoidal adjunction.

Lemma 13 The forgetful functor F : C → L is symmetric monoidal.

Proof. We need a natural transformation with components m_{X,Y} : F (X) ⊗ F (Y) → F (X × Y) and a map m : I → F (1) satisfying certain conditions. But if X and Y are (A, h_{A}) and (B, h_{B}) respectively, this amounts to m_{X,Y} : A ⊗ B → A ⊗ B and m : I → I. Taking m_{X,Y} = 1_{A⊗B} and m = 1_{I} is then easily seen to work. □

Lemma 14 The free functor G : L → C is symmetric monoidal.

Proof. We need a natural transformation with components n_{A,B} : GA×GB → G(A⊗B) and a map n : 1 → GI satisfying some conditions. Spelling this out a bit, n_{A,B} is a coalgebra map:

n_{A,B} : (!A⊗!B, q_{A,B} ∘ (δ_{A} ⊗ δ_{B})) → (!(A ⊗ B), δ_{A⊗B})

Now the symmetric monoidal structure on ! gives a map between the underlying objects of these two coalgebras q_{A,B} :!A⊗!B →!(A ⊗ B), and that this is a coalgebra map follows immediately from the fact that δ is a monoidal natural transformation. The nullary case is similar. That this definition of n satisfies the conditions making (G, n) symmetric monoidal is then immediate from the fact that (!, q) is symmetric monoidal. □

Lemma 15 The unit of the adjunction η : 1_{C}→^{·}GF is a monoidal natural transformation.

8It may well be that there is a sensible definition of a category of ‘linear resolutions’ in which L_{!}^{∗} is initial and Exp(L^{!}) is terminal, but this idea has not yet been followed up.

Proof. This is also straighforward, though we have not so far made explicit what the definition of η_{(A,h_{A})} : (A, h_{A}) → (!A, δ_{A}) is. The answer is that it is just h_{A}, which is readily seen to be a coalgebra morphism by the definition of coalgebra and to be natural by the definition of coalgebra map. That h_{A} is monoidal is then completely trivial from the definition of the product of coalgebras. □

Lemma 16 The counit ε : F G→^{·}1_{L} of the adjunction is a monoidal natural transformation.

Proof. By assumption. □

Taking the preceding results together, we have:

Corollary 17 Any linear category gives rise to an LNL model, though it is not in general unique. □

Of course, given a linear category L, there may be many choices of C which lead to an LNL model other than the two given above. One could start with an arbitrary LNL model comprising some L and C together with the associated data, and then construct the linear category (L,!). In general, there is then no reason why C should be equivalent to either of L_{!}^{∗} or Exp(L^{!}), although in particular cases the distinction between some or all of these CCCs can collapse.

2.2.3 Additives and the Seely Isomorphisms

So far, we have concentrated on the relationship between the multiplicative ⊗, −∘ fragment of ILL and the ×, → fragment of IL. We now consider briefly what happens when an LNL model (or, equivalently, a linear category) also has the extra structure required to model the additive linear connectives &, ⊕ and the non-linear sum +.

The simplest case is when the SMCC part L of an LNL model also has finite products, modelling the additive connective ‘with’ (&). The functor G preserves limits because it is a right adjoint, and in particular

G(A&B) ≅ GA × GB
G1 ≅ 1

(note that we use 1 for the terminal object in both L and C). Taking this together with Proposition 1, we obtain the following natural isomorphisms:

!A⊗!B ≅ !(A&B)
I ≅ !1

These isomorphisms were central to Seely’s proposed model of ILL [See80], which also proposed interpreting IL in the Kleisli category. See [Bie94a] or [Bie94b] for a critique of Seely’s semantics; here we shall merely show that a linear category with products does indeed have a Kleisli category which is cartesian closed.

The isomorphisms ϕ_{A,B} :!(A&B) →!A⊗!B and ϕ :!1 → I can be given explicit definitions in terms of the data determining a linear category thus:

ϕ_{A,B} =^{def} [figure: !(A&B); !(A&B)⊗!(A&B); !A⊗!B; d_{A&B}; !π_{1}⊗!π_{2}]
ϕ =^{def} !1  I e^{1}

(Explicit definitions of the inverses are left as an exercise for the reader.)

Lemma 18 If a linear category has products then the product of two free !-coalgebras is a free coalgebra.

Proof. This amounts to checking the following diagram:

[figure: !!(A&B); !(A&B); !(!A⊗!B); !!A⊗!!B; !A⊗!B; δ_{A&B}; ϕ_{A,B}; !(ϕ_{A,B}); δ_{A} ⊗ δ_{B}; q_{!A,!B}]

which is an easy consequence of naturality and the fact that d is a coalgebra morphism. □

Corollary 19 If a linear category has products then the Kleisli category L_{!} is cartesian closed.

Proof. Lemma 18 says that L_{!} coincides with L_{!}^{∗}, which is cartesian closed by Lemma 12. □

Products were relatively easy to deal with – the correspondence between linear categories and LNL models extends trivially to one between linear categories with finite products and LNL models with products on the SMCC part. Coproducts are slightly more problematic. Whilst the appropriate extension of an LNL model seems obvious (just require both L and C to have finite coproducts), this does not correspond quite as simply as one might hope to linear categories with coproducts.

The difficulty is that, whilst an LNL model with coproducts certainly gives rise to a linear category with coproducts, the converse does not appear necessarily to be true. Assume L is a linear category with finite coproducts, then L^{!} also has finite coproducts as we can define the coproduct of (A, h_{A}) and (B, h_{B}) to be

(A + B, [!inl ∘ h_{A},!inr ∘ h_{B}])

and this is easily checked to satisfy the appropriate conditions. There seems no general reason, however, why either of the two CCCs which we have already identified as arising from L should be closed under this coproduct.

Fortunately, something can be salvaged. There are weak finite coproducts ⊕ in the Kleisli category, obtained by defining

(!A, δ_{A}) ⊕ (!B, δ_{B}) =^{def}(!(!A+!B), δ_{!A+!B})

with, for example, the left injection given by !inl ∘ δ_{A}. That this is a weak coproduct is easy to check.

2.3 The Monad and Comparison with Let-CCCs

The monad on C is (GF, η : 1 → GF, μ : GF GF → GF) where η is the unit of the adjunction and μ is the natural transformation with components μ_{X} : GF GF (X) → GF (X) given by μ_{X} = G(ε_{F X}). Writing T for GF, we obtain the usual monad diagrams:

[figure: T X; T X; T^{2}X; T X; 1; μ_{X}; η_{T X}; 1; T (η_{X}); T^{2}X; T X; T^{3}X; T^{2}X; μ_{X}; μ_{X}; T (μ_{X}); μ_{T X}]

It is then easy to see that (T, η, μ) is a symmetric monoidal monad, in that T is a symmetric monoidal functor and both η and μ are monoidal natural transformations (this is simply a monad in the 2-category of SMCs, SM functors and monoidal natural transformations [Str72]). Cartesian closed categories with (not necessarily symmetric) monoidal monads have recently been the focus of some interest, as they are the models for Moggi’s computational lambda calculus [Mog89, Mog91, BBdP93]. The definition is, however, more commonly given in terms of strong monads, for which we now make a brief digression. Most of the definitions and results about the various kinds of monads on various kinds of monoidal categories are due to Anders Kock; the interested reader should see [Koc71] and the further references cited there.

2.3.1 Strong Monads

Definition 11 If (M, ⊗, I, α, l, r) is a monoidal category, and (T, η, μ) is a monad on M, then T is a strong monad if there is a natural transformation τ (called the tensorial strength) with components

τ_{A,B} : A ⊗ T B → T (A ⊗ B)

such that the following four diagrams commute:

[figure: I ⊗ T A; T A; T (I ⊗ A); τ; l; T (l); A ⊗ B; T (A ⊗ B); A ⊗ T B; 1 ⊗ η; η; τ]

[figure: A ⊗ (B ⊗ T C); A ⊗ T (B ⊗ C); T (A ⊗ (B ⊗ C)); (A ⊗ B) ⊗ T C; T ((A ⊗ B) ⊗ C); τ; α; 1 ⊗ τ; τ; T (α)]

[figure: A ⊗ T B; A ⊗ T^{2}B; T (A ⊗ T B); T^{2}(A ⊗ B); T (A ⊗ B); 1 ⊗ μ; τ; T (τ); μ; τ]

If M above is symmetric monoidal (with symmetry σ), then there is a ‘twisted’ tensorial strength

τ′_{A,B} : T A ⊗ B → T (A ⊗ B)

given by

τ′_{A,B} = T (σ) ∘ τ_{B,A} ∘ σ

In this case we can also construct a pair of natural transformations Φ, Φ′ which have components

Φ_{A,B}, Φ′_{A,B} : T A ⊗ T B → T (A ⊗ B)

given by

Φ_{A,B} = μ_{A⊗B} ∘ T (τ′_{A,B}) ∘ τ_{T A,B}
Φ′_{A,B} = μ_{A⊗B} ∘ T (τ_{A,B}) ∘ τ′_{A,T B}

The monad is said to be commutative if Φ = Φ′.

Proposition 20 If M is a symmetric monoidal category and T is a strong monad on M, then

1. either of Φ or Φ′, together with the map η_{I} : I → T I, makes T into a monoidal functor;

2. both η and μ are monoidal natural transformations with respect to either of these monoidal structures on T;

3. T is a symmetric monoidal functor iff it is commutative.

□

Now, a model of the computational lambda calculus (what Crole and Pitts call a let-ccc [Cro92, CP90]) is a cartesian closed category with a strong monad. The above implies that an LNL model always has a strong monad on the CCC part of the model and thus includes a let-ccc. The monad is, however, always commutative (because T is a symmetric monoidal functor). It is not the case that all strong monads on CCCs are commutative; indeed, some very important monads arising in computer science are non-commutative, for example the free monoid monad (list, [·], flatten) on the category of sets. Thus it is certainly the case that not all, or even all interesting, let-ccc’s will arise from LNL models. Having said that, many of the most important monads arising in semantics, such as lifting and various flavours of powerset/powerdomain, are commutative, so the theory of commutative strong monads on CCCs is not without independent interest.

2.4 Examples

The preceding material is all rather abstract, so we now give a couple of concrete examples of LNL models. The first example is important from a computer science perspective and was a major motivation for the present work. The second arises from one of the most common (or at least, most commonly cited) ‘mathematical’ examples of a symmetric monoidal closed category.

2.4.1 ω-complete Partial Orders

Let L be the category of pointed ωcpos (ω-cocomplete partial orders with a least element) and strict (bottom preserving) continuous maps. This is a symmetric monoidal closed category with tensor product given by the so-called smash product, the identity for the tensor by the one-point space (which is also a biterminator) and internal hom by the strict continuous function space. In fact, L also has binary products and coproducts, given by cartesian product and coalesced sum respectively.

Given this choice of L, there are a couple of obvious choices for the CCC C which give an LNL model. One is to take C to be the category of pointed ω-cpos and continuous (not necessarily strict) maps, G to be the inclusion functor and F to be the lifting functor F : X → X_{⊥}. The monoidal structure m on F is given by the evident isomorphism X_{⊥} ⊗ Y_{⊥} ≅ (X × Y)_{⊥}. In this case, C is (equivalent to) the Kleisli category of the lifting comonad on L. Note that the cartesian closure of the Kleisli category follows from the fact that L has products. There are strong coproducts in L but only weak ones in C.

An alternative choice of C is the category of (not necessarily pointed) ω-cpos (these are sometimes called predomains) and continuous maps, again with inclusion and lifting functors. This is equivalent to the Eilenberg-Moore category of the lift comonad on L, so it has products and coproducts by our previous general arguments, but it also turns out to be cartesian closed.

2.4.2 Abelian Groups

Let L be the category of Abelian groups and group homomorphisms. This is symmetric monoidal closed with A ⊗ B the Abelian group generated by the set of tokens {a ⊗ b | a ∈ A, b ∈ B} subject to the relations

(a_{1} + a_{2}) ⊗ b = a_{1} ⊗ b + a_{2} ⊗ b
a ⊗ (b_{1} + b_{2}) = a ⊗ b_{1} + a ⊗ b_{2}

(More categorically, A ⊗ B can be defined by a homomorphism A × B → A ⊗ B which is universal amongst bilinear maps into Abelian groups.) The unit for ⊗ is the group of integers under addition, Z, and the internal hom A −∘B is the group of homomorphisms from A to B with the multiplication inherited from B. In fact L also has biproducts – the direct sum A⊕B is both a product and a coproduct and the trivial group is a biterminator.

Now let C be the category of sets, which is the prototypical example of a cartesian closed category, and F and G be the free and forgetful functors respectively. This gives an LNL model with the monoidal structures on the functors given (in what should be comprehensible notation) by

n_{A,B} : GA × GB → G(A ⊗ B)
: (a, b) ↦ [a ⊗ b]

n : 1 → GZ
: ∗ ↦ 1
m_{X,Y} : F X ⊗ F Y → F (X × Y)
: [Σ_{i}n_{i}x_{i} ⊗ Σ_{j}m_{j}y_{j}] ↦ Σ_{i,j}n_{i}.m_{j} (x_{i}, y_{j})
m : I → F 1
: n ↦ n.∗

It is fairly straightforward to check that this does indeed give an LNL model. The comonad on L takes an Abelian group to the free group on its underlying set. ε is ‘evaluation’ and η is the insertion of generators. This is another example of the situation described in Section 2.2.3, since C is equivalent to the Kleisli category of the comonad on L.

3 LNL Logic

LNL-models are, of course, supposed to be models of a logical system. Corollary 8 says that they are models for intuitionistic linear logic as defined by Girard, but the form of the definition of LNL-model suggests an interesting alternative presentation of the logic. The basic idea is that one starts with two independent logics, corresponding to the categories L and C and then adds operators which correspond in some way to the adjunction between the two categories. To do this and obtain a logic with a good proof theory is, however, not entirely straightforward.

Before attempting to be more precise about the rules of LNL-logic, we should perhaps say a little about what we are aiming for. Different researchers approach logic from many different backgrounds and with many different motivations, as is at least partly reflected by the question of whether one describes one’s work as logic, type theory or proof theory (or even categorical logic, or categorical proof theory). Of course, the very fact that such a confusion is possible is at the heart of what makes constructive logics exciting objects of study, but it does seem to lead to a certain lack of consensus about what constitutes a ‘good’ or ‘well-behaved’ system, and about which results are important.

We take propositional intuitionistic logic as our touchstone and the following properties of that system as our goals: Gentzen-style sequent calculus presentation with (preferably local) cut-elimination and subformula property; equivalent natural deduction system and term calculus with strong normalisation; natural class of categorical models which reflects accurately not just provability, but the equalities on proofs given by cut-elimination and proof normalisation. On the minus side, we are prepared to accept certain infelicities of syntax, such as commuting conversions in natural deduction, and we shall, at least in this paper, ignore Hilbert-style axiomatic presentations entirely. Furthermore we want a logic which contains both linear and non-linear propositions, treated in a way which reflects the symmetric presentation of the intended categorical models.

In keeping with our earlier conventions for naming objects of L and C, we will use A, B, C to range over linear propositions and X, Y, Z for conventional ones. We shall use Γ and Δ to range over linear contexts (finite multisets of linear propositions) and Θ and Φ for non-linear ones. We also decorate turnstiles with L or C to indicate which subsystem they belong to. Finally, if Θ is X_{1}, …, X_{n} then F Θ means F X_{1}, …, F X_{n}, and similarly for GΓ. The two classes of propositions with which we shall be dealing are defined by the following grammar:

A, B := A_{0} | I | A ⊗ B | A −∘B | F X
X, Y := X_{0} | 1 | X × Y | X → Y | GA

where A_{0} (resp. X_{0}) ranges over some unspecified set of atomic linear (resp. non-linear) propositions.

3.1 Sequent Calculus

Sequent calculus rules may be divided into three main classes: structural rules, such as weakening or exchange; the cut rule, which allows proofs to be composed, and logical rules. The logical rules are further divided into left and right rules for each connective. In a well-behaved sequent system there should be a certain symmetry between the left and right rules which leads to a cut elimination theorem. Furthermore, in many logics the cut rule is the only rule which can have a formula in the premises which is not a subformula of a formula in the conclusion. For such systems, a cut elimination theorem means that any provable sequent has a proof which only mentions subformulae of the conclusion, which has important implications for, for example, proof search.

The two logics with which we start are very familiar viz. the exponential-free, multiplicative fragment of propositional intuitionistic linear logic and the ×, → fragment of ordinary intuitionistic logic. These both have sequent presentations with all the properties we desire. How should the systems be enriched and combined to give LNL-logic? We shall approach this question by first outlining two unsatisfactory answers.

3.1.1 The First Wrong Way

The most obvious answer is to take the two familiar sequent calculi and add rules for the two functors and the unit and counit of the adjunction. Thus we have all the usual linear rules (including cut) for deducing sequents of the form Γ ⊢_{L} A and all the usual non-linear rules (including contraction, weakening and another cut rule) for deducing things of the form Θ ⊢_{C} X, together with the following four new rules:

Γ, A ⊢_{L} B ; \overline{F G-left} ; Γ, F GA ⊢_{L} B  Θ ⊢_{C} X ; \overline{F} ; F Θ ⊢_{L} F X

Θ ⊢_{C} X ; \overline{GF -right} ; Θ ⊢_{C} GF X  Γ ⊢_{L} A ; \overline{G} ; GΓ ⊢_{C} GA

Categorically we interpret proofs of conventional sequents

\begin{matrix}Π \\ X_{1}, …, X_{n} ⊢_{C} Y \end{matrix}

as maps

[[Π]] : [[X_{1}]] × ⋯ × [[X_{n}]] → [[Y]]

in C, and proofs of linear sequents

\begin{matrix}Σ \\ A_{1}, …, A_{m} ⊢_{L} B \end{matrix}

as maps

[[Σ]] : [[A_{1}]] ⊗ ⋯ ⊗ [[A_{m}]] → [[B]]

in L, where each of the logical connectives is interpreted as the obviously corresponding piece of categorical structure. (Thus [[A ⊗ B]] is [[A]] ⊗ [[B]] and so on. Henceforth we will omit semantic brackets whenever we think we can get away with it.)

The interpretations of the four new rules are as follows:

Γ ⊗ A⟶^{e}B

\overline{F G-left}

Γ ⊗ F GA⟶^{1⊗ε_{A}}Γ ⊗ A⟶^{e}B

X_{1} × ⋯ × X_{n}⟶^{e}Y

\overline{F}

F X_{1} ⊗ ⋯ ⊗ F X_{n}⟶^{m}F (X_{1} × ⋯ × X_{n})⟶^{F e}F Y

Γ⟶^{e}X

\overline{GF -right}

Γ⟶^{e}X⟶^{η_{X}}GF X

A_{1} ⊗ ⋯ ⊗ A_{n}⟶^{e}B

\overline{G}

GA_{1} × ⋯ GA_{n}⟶^{n}G(A_{1} ⊗ ⋯ ⊗ A_{n})⟶^{Ge}GB

Notice how the monoidal structure of the model is used to interpret the two functor rules. The coherence conditions on the model are sufficient to ensure that what we have rather glibly written as m and n above are in fact determined up to isomorphism, and we will in general be rather sloppy about including all the natural isomorphisms which should strictly be included in the categorical interpretations of logical rules. The interpretations of the remaining rules are completely standard, so we omit them for the moment, but note that the two cut rules are interpreted by composition in the two categories.

From the point of view of provability, this collection of rules is fine – it proves exactly the sequents we intend. From the point of view of proofs, however, things are not so good. Whilst the logic allows us to express each of the different intended proofs of a given sequent (i.e. morphisms in the free LNL-model), the equality of morphisms is not reflected by a good proof theory. This shows up most obviously in the fact that cut elimination fails for this formulation of the logic. We should not be too surprised that these rules are unsatisfactory, as their form is rather strange – the functor rules introduce a connective on both sides of the turnstile whilst the two other rules introduce two connectives at once. The failure of cut elimination can be seen by considering the sequent F X ⊢_{L} F X ⊗ F X. This sequent is certainly provable, but there is no rule which could be the last rule of a cut-free proof. This particular problem could be fixed in a slightly ad hoc way by adding contraction for linear assumptions of the form F X, but there are other problems, such as the following cut:

Θ ⊢_{C} X ; \overline{GF -right} ; Θ ⊢_{C} GF X  Γ, F X ⊢_{L} A ; \overline{G} ; GΓ, GF X ⊢_{C} GA
\overline{C-cut}
Θ, GΓ ⊢_{C} GA

This cut cannot, in general, be removed. (There is a rewrite which replaces the cut with a simpler L-cut, but it also introduces a new cut of the original form for each formula in Θ.)

3.1.2 The Second Wrong Way

The second set of rules which we shall consider looks even odder than the first, so the fact that it too fails to have a good proof theory is no surprise at all. The system is worth mentioning, however, because it is very simple and has a certain appeal from a categorical point of view. Like the first system, we start with the two separate logics but now we add just two rules, each of which is the inverse of the other:

F Θ ⊢_{L} A ; \overline{G-right} ; Θ ⊢_{C} GA  Θ ⊢_{C} GA ; \overline{F -left} ; F Θ ⊢_{L} A

These rules are, of course, syntax for the alternative presentation of the adjunction in the model in terms of a natural bijection between hom sets

L(F X, A) ; = ; C(X, GA)

and indeed it turns out that this system proves exactly the same sequents as the previous one. This is because each rule of one system is derivable (or admissible) in the other. For example, the G rule of the first system is admissible in the second system:

GA_{n} ⊢_{C} GA_{n} ; \overline{F -left} ; F GA_{n} ⊢_{L} A_{n}  GA_{1} ⊢_{C} GA_{1} ; \overline{F -left} ; F GA_{1} ⊢_{L} A_{1}  A_{1}, …, A_{n} ⊢_{L} B ; \overline{L-cut} ; F GA_{1}, A_{2}, …, A_{n} ⊢_{L} B ; \begin{matrix}· \\ · \\ · \\ · \end{matrix} ; F GA_{1}, …, F GA_{n−1}, A_{n} ⊢_{L} B
\overline{L-cut}
F GA_{1}, …, F GA_{n} ⊢_{L} B
\overline{G-right}
GA_{1}, …, GA_{n} ⊢_{C} GB

The reader may be surprised by the equivalence of these two systems. In particular, the way in which the monoidal structures on the two functors arise in the first presentation is clear, but the second system does not mention G on the left at all. Where, then, does the monoidal structure on G come from? The answer is in the remark made at the end of Section 2.1 – the categorical interpretation of the second system uses both m and m^{−1} (which we called p earlier), and this, together with the adjunction, is sufficient to ensure that G is monoidal too.

F X_{1} ⊗ ⋯ ⊗ F X_{n}⟶^{e}A

\overline{G-right}

X_{1} × ⋯ × X_{n}⟶^{η}GF (X_{1} × ⋯ × X_{n})⟶^{Gm^{−1}}G(F X_{1} ⊗ ⋯ ⊗ F X_{n})⟶^{Ge}GA

X_{1} × ⋯ × X_{n}⟶^{e}GA

\overline{F -left}

F X_{1} ⊗ ⋯ ⊗ F X_{n}⟶^{m}F (X_{1} × ⋯ × X_{n})⟶^{F e}F GA⟶^{ε}A

That the second systems fails to have cut-elimination may be seen by considering the following situation:

F Θ ⊢_{L} A ; \overline{G-right} ; Θ ⊢_{C} GA  F Θ′, F GA ⊢_{L} B ; \overline{G-right} ; Θ′, GA ⊢_{C} GB
\overline{C-cut}
Θ, Θ′ ⊢_{C} GB

or by trying to find a cut-free proof of F X ⊢_{L} F (X × X). Another reason for rejecting this second system is that even cut-free proofs do not have the subformula property.

3.1.3 A Well-Behaved Sequent Calculus

Fortunately, there is a way to present the logic which has a good proof theory. The trick is to allow conventional non-linear formulae to appear in the assumptions of a linear sequent. A typical linear sequent looks, therefore, like this:

X_{1}, …, X_{m}, A_{1}, …, A_{n} ⊢_{L} B

which is interpreted as a morphism in L of the form

F X_{1} ⊗ ⋯ ⊗ F X_{m} ⊗ A_{1} ⊗ ⋯ ⊗ A_{n} ⟶ B

Non-linear sequents are still constrained to have purely non-linear antecedents and are interpreted as morphisms in C as before.^{9}

We will usually abuse notation by writing linear sequents in the form Θ; Γ ⊢_{L} A, even though there is no need at all for the ‘;’ since linear and non-linear formulae can never be confused. It is important to understand that there is really just one kind of comma in the antecedent, and that the exchange rule (which we will supress) really allows linear and non-linear formulae to be mingled. Once this is understood, however, our potentially misleading notation seems rather less confusing than the alternative (to which we shall return) of introducing new metavariables ranging over arbitrary propositions and contexts. The sequent rules for LNL logic are shown in Figures 1 and 2.

There are several points to be noted about the rules. There are three cut rules according to the type of the cut formula and of the ultimate conclusion (there is no LC-cut rule because a linear formula cannot be cut into a non-linear sequent). Each of the non-linear left rules (including contraction and weakening) splits into two versions according to the type of the overall sequent. The rules for F and G look much pleasant than in the two unsatisfactory systems – each has one left and one right rule, neither of which affect the rest of the sequent. The annotations on the turnstiles are, strictly speaking, redundant as they are implicit in the consequent. The following is easy to verify:

Proposition 21 The sequent rules of LNL logic are equivalent in terms of provability to the two systems presented earlier. To be precise:

• Θ ⊢_{C} X in LNL logic iff Θ ⊢_{C} X in either of the earlier systems.

• Θ; Γ ⊢_{L} A in LNL logic iff F Θ, Γ ⊢_{L} A in either of the earlier systems.

□

The interpretation of LNL logic in an LNL-model is fairly straightforward, given what has gone before. We assume that the reader is familiar with the interpretation of the standard logical connectives and just give details of the interpretation of one of the cut rules and the four rules for F and G in Figure 3.

3.1.4 Cut Elimination

We now turn to the question of cut elimination in LNL logic. As usual, the proof describes a procedure in which the cuts in a proof are locally rewritten (making the proof, in general, much larger) so that they percolate up towards the leaves, where they eventually disappear. As is also usual, the fine details of making the induction go through are slightly delicate. In particular, we start by replacing the CL-cut and CC-cut rules with the following n-ary (n ≥ 0) variants, yielding an equivalent system which we call LNL^{+}:

Θ ⊢_{C} X X^{n}, Φ; Γ ⊢_{L} A
\overline{CL-cut_{n}}
Θ, Φ; Γ ⊢_{L} A

Θ ⊢_{C} X X^{n}, Φ ⊢_{C} Y ; \overline{CC-cut_{n}} ; Θ, Φ ⊢_{C} Y

where

X^{n} =^{def} \overbrace{X, …, X}^{n}

9The attempt to make a more symmetric system by allowing linear assumptions in conventional sequents gives yet another system without cut-elimination.

Axioms

A ⊢_{L} A L-axiom  X ⊢_{C} X C-axiom

Structural Rules

Θ, X, X; Γ ⊢_{L} A

L-contraction

Θ, X; Γ ⊢_{L} A

Θ, X, X ⊢_{C} Y

C-contraction

Θ, X ⊢_{C} Y

Θ; Γ ⊢_{L} A ; \overline{L-weakening} ; Θ, X; Γ ⊢_{L} A  Θ ⊢_{C} Y ; \overline{C-weakening} ; Θ, X ⊢_{C} Y

Cut Rules Θ ⊢_{C} X X, Φ; Γ ⊢_{L} A

\overline{CL-cut}
Θ, Φ; Γ ⊢_{L} A

Θ ⊢_{C} X X, Φ ⊢_{C} Y ; \overline{CC-cut} ; Θ, Φ ⊢_{C} Y

Θ; Γ ⊢_{L} A Φ; A, Δ ⊢_{L} B
\overline{LL-cut}
Θ, Φ; Γ, Δ ⊢_{L} B

×/1 Rules

Θ, X ⊢_{C} Z ; \overline{C-×-left1} ; Θ, X × Y ⊢_{C} Z  Θ, Y ⊢_{C} Z ; \overline{C-×-left2} ; Θ, X × Y ⊢_{C} Z

Θ, X; Γ ⊢_{L} A

\overline{L-×-left1}

Θ, X × Y; Γ ⊢_{L} A

Θ, Y; Γ ⊢_{L} A
\overline{L-×-left2}
Θ, X × Y; Γ ⊢_{L} A

Θ ⊢_{C} X Φ ⊢_{C} Y

\overline{×-right}

Θ, Φ ⊢_{C} X × Y

\overline{1-right} ; ⊢_{C} 1

⊗/I Rules

Θ; Γ, A, B ⊢_{L} C

\overline{⊗-left}

Θ; Γ, A ⊗ B ⊢_{L} C

Θ; Γ ⊢_{L} A Φ; Δ ⊢_{L} B
\overline{⊗-right}
Θ, Φ; Γ, Δ ⊢_{L} A ⊗ B

Θ; Γ ⊢_{L} A ; \overline{I-left} ; Θ; Γ, I ⊢_{L} A  \overline{I-right} ; ⊢_{L} I

Figure 1: Sequent calculus presentation of LNL logic (I)

3.1 Sequent Calculus 37 → Rules Θ ⊢_{C} X Y, Φ ⊢_{C} Z

\overline{C-→-left}

Θ, X → Y, Φ ⊢_{C} Z

Θ ⊢_{C} X Y, Φ; Γ ⊢_{L} A
\overline{L-→-left}
Θ, X → Y, Φ; Γ ⊢_{L} A

Θ, X ⊢_{C} Y ; \overline{→-right} ; Θ ⊢_{C} X → Y

−∘ Rules

Θ; Γ, A ⊢_{L} B

\overline{−∘-right}

Θ; Γ ⊢_{L} A −∘B

Θ, Γ ⊢_{L} A Φ; Δ, B ⊢_{L} C
\overline{−∘-left}
Θ, Φ; Γ, A −∘B, Δ ⊢_{L} C

F Rules

Θ ⊢_{C} X ; \overline{F -right} ; Θ ⊢_{L} F X Θ, X; Γ ⊢_{L} A \overline{F -left}

Θ; F X, Γ ⊢_{L} A

G Rules

Θ; B, Γ ⊢_{L} A
\overline{G-left}
Θ, GB; Γ ⊢_{L} A

Θ ⊢_{L} A ; \overline{G-right} ; Θ ⊢_{C} GA

Figure 2: Sequent calculus presentation of LNL logic (II)

Y_{1} × ⋯ × Y_{n}⟶^{e}X F X ⊗ F Φ ⊗ Γ⟶^{f}A

\overline{CL-cut}

(⨂_{i} F Y_{i}) ⊗ F Φ ⊗ Γ⟶^{m⊗1⊗1}F (∏_{i} Y_{i}) ⊗ F Φ ⊗ Γ⟶^{F e⊗1⊗1}F X ⊗ F Φ ⊗ Γ⟶^{f}A

X_{1} × ⋯ × X_{n}⟶^{e}X

\overline{F -right}

F X_{1} ⊗ ⋯ ⊗ F X_{n}⟶^{m}F (X_{1} × ⋯ × X_{n})⟶^{F e}F X

(F Θ ⊗ F X) ⊗ Γ⟶^{e}A

\overline{F -left}

F Θ ⊗ (F X ⊗ Γ)⟶^{e}A

F Θ ⊗ B ⊗ Γ⟶^{e}A

\overline{G-left}

F Θ ⊗ F GB ⊗ Γ⟶^{1⊗ε⊗1}F Θ ⊗ B ⊗ Γ⟶^{e}A

F X_{1} ⊗ ⋯ ⊗ F X_{n}⟶^{e}A

\overline{G-right}

∏_{i} X_{i}⟶^{η}GF (∏_{i} X_{i}) ⟶^{Gm^{−1}}G (⨂_{i} F X_{i}) ⟶^{Ge}GA

Figure 3: Categorical interpretation of LNL logic (sketch)

These rules are easily seen to be admissible in LNL, and it is also clear that cut-elimination for LNL^{+} implies cut-elimination for LNL.

Define the rank |A| (resp. |X|) of a linear (resp. non-linear) proposition to be the number of logical connectives in the proposition (so in particular, the rank of atomic propositions is 0). The cut rank c(Π) of a proof Π is one more than the maximum of the ranks of all the cut formulae in Π, and 0 if Π is cut-free. The depth d(Π) of a proof Π is the length of the longest path in the proof tree (so the depth of an axiom is 0). The key to the proof is the following lemma, which shows how to transform a single cut, either by removing it or by replacing it with one or more simpler cuts:

Lemma 22 (Cut Reduction)

1. If Π_{1} is an LNL^{+} proof of Θ ⊢_{C} X and Π_{2} is an LNL^{+} proof of X^{n}, Φ ⊢_{C} Y with c(Π_{1}), c(Π_{2}) ≤ |X| then there exists a proof Π of Θ, Φ ⊢_{C} Y with c(Π) ≤ |X|;

2. If Π_{1} is an LNL^{+} proof of Θ ⊢_{C} X and Π_{2} is an LNL^{+} proof of X^{n}, Φ; Γ ⊢_{L} A with c(Π_{1}), c(Π_{2}) ≤ |X| then there exists a proof Π of Θ, Φ; Γ ⊢_{L} A with c(Π) ≤ |X|;

3. If Π_{1} is an LNL^{+} proof of Θ; Γ ⊢_{L} A and Π_{2} is an LNL^{+} proof Φ; A, Δ ⊢_{L} B with c(Π_{1}), c(Π_{2}) ≤ |A| then there exists a proof Π of Θ, Φ; Γ, Δ ⊢_{L} B with c(Π) ≤ |A|.

Proof. The three parts are proved simultaneously by induction on d(Π_{1}) + d(Π_{2}). We consider cases according to the classes of the last rules used in each of the two proofs:

1. Both proofs end in logical rules which introduce the cut formula (so Π_{1} ends in a right rule and Π_{2} in a corresponding left rule). This is the most interesting case, and we consider each subcase in turn:

F -right/ F -left In this case we have

Π_{1} = \begin{matrix}π_{1} \\ Θ ⊢_{C} X \end{matrix} ; \overline{F -right} ; Θ ⊢_{L} F X Π_{2} = \begin{matrix}π_{2} \\ Φ, X; F X^{n}, Γ ⊢_{L} A \end{matrix} \overline{F -left} Φ; F X^{n+1}, Γ ⊢_{L} A

By the induction hypothesis applied to the proofs Π_{1} and π_{2} there exists a proof Π′ of Θ, Φ, X; Γ ⊢_{L} A with c(Π′) ≤ |F X| = |X| + 1. Then let Π be the following proof:

\begin{matrix}π_{1} \\ Θ ⊢_{C} X \end{matrix}  \begin{matrix}Π′ \\ Θ, Φ, X; Γ ⊢_{L} A \end{matrix}
\overline{CL-cut_{1}}

Θ, Θ, Φ; Γ ⊢_{L} A = Θ, Φ; Γ ⊢_{L} A

where the double line stands for a number of contractions. Π has cut rank max(|X| + 1, c(π_{1}), c(Π′)) which is equal to |X| + 1 = |F X| as required. Note that there is an obvious simplification in the case that n = 0 as we can then avoid an appeal to the induction hypothesis altogether by letting Π be simply

\begin{matrix}π_{1} \\ Θ ⊢_{C} X \end{matrix}  \begin{matrix}π_{2} \\ Φ, X; Γ ⊢_{L} A \end{matrix}
\overline{CL-cut_{1}}
Θ, Φ; Γ ⊢_{L} A

G-right/ G-left We have

Π_{1} = \begin{matrix}π_{1} \\ Θ ⊢_{L} A \end{matrix} ; \overline{G-right} ; Θ ⊢_{C} GA Π_{2} = \begin{matrix}π_{2} \\ Φ, GA^{n}; A, Γ ⊢_{L} B \end{matrix} \overline{G-left} Φ, GA^{n+1}; Γ ⊢_{L} B

By applying the induction hypothesis to Π_{1} and π_{2} we obtain a proof Π′ of Θ, Φ; A, Γ ⊢_{L} B with c(Π′) ≤ |GA| = |A| + 1. Now let Π be

\begin{matrix}π_{1} \\ Θ ⊢_{L} A \end{matrix}  \begin{matrix}Π′ \\ Θ, Φ; A, Γ ⊢_{L} B \end{matrix}
\overline{LL-cut}

Θ, Θ, Φ; Γ ⊢_{L} B = Θ, Φ; Γ ⊢_{L} B

The cut rank of Π is max(|A| + 1, c(π_{1}), c(Π′)) = |A| + 1 so we are done. Again, there is an obvious simplification when n = 0.

×-right/ C-×-left1 We have

Π_{1} = \begin{matrix}π_{1} \\ Θ_{1} ⊢_{C} X \end{matrix} \begin{matrix}π_{2} \\ Θ_{2} ⊢_{C} Y \end{matrix} \overline{×-right} Θ_{1}, Θ_{2} ⊢_{C} X × Y

and

Π_{2} = \begin{matrix}π_{3} \\ Φ, X, (X × Y)^{n} ⊢_{C} Z \end{matrix} ; \overline{C-×-left1} ; Φ, (X × Y)^{n+1} ⊢_{C} Z

Let Π′ be the result of applying the induction hypothesis to Π_{1} and π_{3}, so Π′ is a proof of Θ_{1}, Θ_{2}, Φ, X ⊢_{C} Z with c(Π′) ≤ |X × Y | = |X| + |Y | + 1. Now let Π be

\begin{matrix}π_{1} \\ Θ_{1} ⊢_{C} X \end{matrix}  \begin{matrix}Π′ \\ Θ_{1}, Θ_{2}, Φ, X ⊢_{C} Z \end{matrix}
\overline{CC-cut_{1}}

Θ_{1}, Θ_{1}, Θ_{2}, Φ ⊢_{C} Z = Θ_{1}, Θ_{2}, Φ ⊢_{C} Z

which has a cut rank of max(|X| + 1, c(π_{1}), c(Π′)) ≤ |X × Y |.

• The remaining subcases are similar and left to the reader.

2. The last rule used in Π_{1} is not a right logical rule. These are dealt with by simple permutations of the rules. We consider each remaining possibility for the last rule in Π_{1} and form of conclusion of Π_{2} in turn. A few representative cases:

C-contraction/ C sequent The situation is

Π_{1} = \begin{matrix}π_{1} \\ Θ, X, X ⊢_{C} Y \end{matrix} \overline{C-contraction} Θ, X ⊢_{C} Y \begin{matrix}Π_{2} \\ Y^{n}, Φ ⊢_{C} Z \end{matrix}

and by induction applied to π_{1} and Π_{2} there is a proof Π′ of Θ, X, X, Φ ⊢_{C} Z with c(Π′) ≤ |Y |. Let Π be

\begin{matrix}Π′ \\ Θ, X, X, Φ ⊢_{C} Z \end{matrix}

C-contraction

Θ, X, Φ ⊢_{C} Z

Clearly, c(Π) ≤ |Y | so we are done. CC-cut_{n}/ L sequent

Π_{1} = \begin{matrix}π_{1} \\ Θ ⊢_{C} X \end{matrix}  \begin{matrix}π_{2} \\ X^{n}, Φ ⊢_{C} Y \end{matrix} ; \overline{CC-cut_{n}} ; Θ, Φ ⊢_{C} Y  \begin{matrix}Π_{2} \\ Y^{m}, Φ′; Γ ⊢_{L} A \end{matrix}

By induction applied to π_{2} and Π_{2} we can form Π′ proving X^{n}, Φ, Φ′; Γ ⊢_{L} A with c(Π′) ≤ |Y |. Now let Π be

\begin{matrix}π_{1} \\ Θ ⊢_{C} X \end{matrix}  \begin{matrix}Π′ \\ X^{n}, Φ, Φ′; Γ ⊢_{L} A \end{matrix}
\overline{CL-cut_{n}}
Θ, Φ, Φ′; Γ ⊢_{L} A

By assumption, c(Π_{1}) ≤ |Y |, so in particular |X| + 1 ≤ |Y |. This means c(Π) = max(|X| + 1, c(π_{1}), c(Π′)) ≤ |Y | as required.

−∘-left/ L sequent

Π_{1} = \begin{matrix}π_{1} \\ Θ; Γ ⊢_{L} A \end{matrix}  \begin{matrix}π_{2} \\ Φ; B, Δ ⊢_{L} C \end{matrix} \overline{−∘-left} Θ, Φ; Γ, A −∘B, Δ ⊢_{L} C  \begin{matrix}Π_{2} \\ Θ′; C, Γ′ ⊢_{L} D \end{matrix}

By induction applied to π_{2} and Π_{2} there’s a proof Π′ of Φ, Θ′; B, Δ, Γ′ ⊢_{L} D with c(Π′) ≤ |C|. Let Π be

\begin{matrix}π_{1} \\ Θ; Γ ⊢_{L} A \end{matrix}  \begin{matrix}Π′ \\ Φ, Θ′; B, Δ, Γ′ ⊢_{L} D \end{matrix}
\overline{−∘-left}
Θ, Φ, Θ′; Γ, A −∘B, Δ, Γ′ ⊢_{L} D

and c(Π) = max(c(π_{1}), c(Π′)) ≤ |C| as required.

L-axiom/ L sequent This is one of the base cases for the induction. We have

Π_{1} = A ⊢_{L} A \begin{matrix}Π_{2} \\ Θ; A, Γ ⊢_{L} B \end{matrix}

and we simply let Π be Π_{2} (recall that c(Π_{2}) ≤ |A| by assumption).

3. The cut formula is a minor formula of the last rule in Π_{2}. These cases are also dealt with by fairly straightforward permutations and we omit them.

4. The last rule in Π_{2} is contraction on the cut formula. This is why we have the n-ary cut rules.

C-contraction

\begin{matrix}Π_{1} \\ Θ ⊢_{C} X \end{matrix} Π_{2} = \begin{matrix}π_{1} \\ X^{n+2}, Φ ⊢_{C} Y \end{matrix} \overline{C-contraction} X^{n+1}, Φ ⊢_{C} Y

By induction on Π_{1} and π_{1} there is a Π proving Θ, Φ ⊢_{C} Y with c(Π) ≤ |X| as required.

L-contraction Similar.

5. The last rule in Π_{2} is weakening introducing the cut formula.

L-weakening

Π_{1} Θ ⊢_{C} X \begin{matrix}π_{1} \\ X^{n}, Φ; Γ ⊢_{L} A \end{matrix}

\overline{L-weakening}
X^{n+1}, Φ; Γ ⊢_{L} A

By induction on Π_{1} and π_{1} there is a Π proving Θ, Φ; Γ ⊢_{L} A with c(Π) ≤ |X| as required. There is a simplification if n = 0, in which case Π is just

\begin{matrix}π_{1} \\ Φ; Γ ⊢_{L} A \end{matrix} ; = ; Θ, Φ; Γ ⊢_{L} A

where c(Π) = c(π_{1}) ≤ |X| by assumption.

C-weakening Similar.

6. Π_{2} is an axiom on the cut formula. Trivial.

□

Lemma 23 Let Π be an LNL^{+} proof of a sequent Θ ⊢_{C} X or Θ; Γ ⊢_{L} A such that c(Π) > 0. Then there is a proof Π′ of the same sequent with c(Π′) < c(Π).

Proof. Induction on d(Π). If the last inference of Π is not a cut then we simply apply the induction hypothesis. Assume then that the last inference is a cut on a formula A (the two cases of cuts on non-linear formulae are treated in just the same way). If c(Π) > |A| + 1 then we can apply the induction hypothesis. This leaves the case where the last rule is a cut on A and c(Π) = |A| + 1 so that

Π = \begin{matrix}Π_{1} \\ Θ; Γ ⊢_{L} A \end{matrix} \begin{matrix}Π_{2} \\ Φ; A, Δ ⊢_{L} B \end{matrix} \overline{LL-cut} Θ, Φ; Γ, Δ ⊢_{L} B

Clearly c(Π_{1}), c(Π_{2}) ≤ |A|+1, so by induction we can construct Π′_{1} proving Θ; Γ ⊢_{L} A and Π′_{2} proving Φ; A, Δ ⊢_{L} B with c(Π′_{1}), c(Π′_{2}) ≤ |A|. Then by Lemma 22, we can construct a Π′ proving Θ, Φ; Γ, Δ ⊢_{L} B with c(Π′) ≤ |A| as required. □

Theorem 24 (Cut Elimination) Let Π be a proof of a sequent Θ ⊢_{C} X or Θ; Γ ⊢_{L} A such that c(Π) > 0. Then there is an algorithm which yields a cut-free proof Π′ of the same sequent.

Proof. This follows immediately by induction on c(Π) and Lemma 23. □

It is very important to note that the proof of the cut elimination theorem says a lot more than that the theorem is true as stated. The proof gives a procedure for simplifying proofs by applying successive rewrites until a cut-free proof is reached. These rewriting steps are purely local and cut-free proofs also have the subformula property. Note that the algorithm described by the cut-elimination proof is non-deterministic – there is some freedom in choosing the order in which rewrites should be applied. On the other hand, the order in which transformations are applied is constrained rather more than is strictly necessary in order to make the induction work. In the present work we shall not, however, consider further the question of the extent to which cut elimination is strongly normalising.^{10}

3.1.5 Cut Elimination and Semantic Equality

The cut elimination process gives a notion of equality on sequent proofs, obtained by extending the one-step proof rewriting relation of the algorithm to a congruence (an equivalence relation which is compositional on proof trees). We intend this syntactic equality to be modelled soundly by equality in LNL models, and this is indeed the case:

Theorem 25 The cut-elimination procedure described in Section 3.1.4 is modelled soundly in any LNL model.

Proof. The basic idea is to show that whenever one proof is simplified to another then the interpretations of those two proofs are equal morphisms in the model. This is done by modifying the statement and proof of the cut reduction lemma (Lemma 22) to show that semantic equality is preserved. Rather than go into the tedious details, we just sketch one of the cases:

G-right/ G-left The cut reduction is

\begin{matrix}π_{1} \\ Θ ⊢_{L} A \end{matrix} \overline{G-right} Θ ⊢_{C} GA

\begin{matrix}π_{2} \\ Φ; A, Γ ⊢_{L} B \end{matrix}

\overline{G-left}

Φ, GA; Γ ⊢_{L} B

\overline{CL-cut}
Θ, Φ; Γ ⊢_{L} B

reduces to

Θ ⊢_{L} A Φ; A, Γ ⊢_{L} B
\overline{LL-cut}
Θ, Φ; Γ ⊢_{L} B

10One of the CSL referees asserted that cut elimination is strongly normalising, but I don’t see how to justify that without a lot more work.

Now, if Θ = X_{1}, …, X_{n}, [[π_{1}]] = f and [[π_{2}]] = g, then this corresponds categorically to the commutation of

[figure: (F X_{1} ⊗ ⋯ ⊗ F X_{n}) ⊗ F Φ ⊗ Γ; F (X_{1} × ⋯ × X_{n}) ⊗ F Φ ⊗ Γ; F GF (X_{1} × ⋯ × X_{n}) ⊗ F Φ ⊗ Γ; F G(F X_{1} ⊗ ⋯ ⊗ F X_{n}) ⊗ F Φ ⊗ Γ; F GA ⊗ F Φ ⊗ Γ; A ⊗ F Φ ⊗ Γ; B; A ⊗ F Φ ⊗ Γ; m ⊗ 1 ⊗ 1; F (η) ⊗ 1 ⊗ 1; F G(m^{−1}) ⊗ 1 ⊗ 1; F G(f) ⊗ 1 ⊗ 1; ε ⊗ 1 ⊗ 1; g; f ⊗ 1 ⊗ 1; g]

which is easily seen to follow using one of the triangle laws for the adjunction and naturality of ε.

□

3.1.6 Variations: Introducing Additive Non-Linear Contexts

There are a large number of possible variations on the sequent rules for LNL logic. One of the most natural is to treat the non-linear antecedents as additive rather than multiplicative (though linear antecedents are still multiplicative, of course). This also has the advantage of a closer correspondence to the natural deduction system which we shall introduce in Section 3.2 and is one of the reasons for our notational device of separating the linear and non-linear parts of the antecedents of linear sequents.

The additive variants of those rules which change are shown in Figure 4. The remaining rules remain unchanged. When we wish to distinguish the additively formulated sequent system from the multipliciative, we shall refer to LNL^{a} or to LNL^{m}.

Axioms

Θ; A ⊢_{L} A L-axiom  Θ, X ⊢_{C} X C-axiom

Cut Rules Θ ⊢_{C} X X, Θ; Γ ⊢_{L} A

\overline{CL-cut}
Θ, Γ ⊢_{L} A

Θ ⊢_{C} X X, Θ ⊢_{C} Y ; \overline{CC-cut} ; Θ ⊢_{C} Y

Θ; Γ ⊢_{L} A Θ; A, Δ ⊢_{L} B
\overline{LL-cut}
Θ; Γ, Δ ⊢_{L} B

×/1 Rules

Θ ⊢_{C} X Θ ⊢_{C} Y

\overline{×-right}
Θ ⊢_{C} X × Y

\overline{1-right} ; Θ ⊢_{C} 1

⊗/I Rules Θ; Γ ⊢_{L} A Θ; Δ ⊢_{L} B

\overline{⊗-right}
Θ; Γ, Δ ⊢_{L} A ⊗ B

\overline{I-right} ; Θ; ⊢_{L} I

→ Rules

Θ ⊢_{C} X Y, Θ ⊢_{C} Z ; \overline{C-→-left} ; Θ, X → Y ⊢_{C} Z Θ ⊢_{C} X Y, Θ; Γ ⊢_{L} A

\overline{L-→-left}
Θ, X → Y; Γ ⊢_{L} A

−∘ Rules

Θ, Γ ⊢_{L} A Φ; Δ, B ⊢_{L} C

\overline{−∘-left}
Θ, Φ; Γ, A −∘B, Δ ⊢_{L} C

Figure 4: Additive variations on LNL logic

The following facts concerning LNL^{a} are easily verified:

Proposition 26

1. The systems LNL^{a} and LNL^{m} are equivalent: each rule in one system is admissible in the other;

2. The weakening and contraction rules of LNL^{m} are admissible in LNL^{a} without weakening and contraction.

3. Cut elimination holds for LNL^{a}.

□

3.1.7 Variations: A Parsimonious Presentation

As we have already mentioned, there is another way of presenting the logic by using some new metavariables: let P, Q range over either linear or non-linear propositions and Υ over mixed contexts. We can then present LNL^{m} in a concise way as shown in Figure 5.

This presentation is equivalent to that shown in Figures 1 and 2. It has the disadvantage of obscuring the fact that there are really two distinct kinds of sequent. These rules are essentially the same as those given by Jacobs in [Jac93], which also contains good accounts of some examples of concrete categorical models. The description of the semantics in that paper is somewhat different from that given here, however. Jacobs starts with a linear category L satisfying extra conditions which make the category of !-coalgebras be cartesian closed. He then interprets all sequents as morphisms in L by applying F to the interpretation of non-linear formulae (in much the same way that we have interpreted linear sequents). This causes problems as it is not clear how to interpret →-right, for example. The solution is a mixture of syntax and semantics – one can verify that all provable sequents which only mention non-linear formulae satisfy what is called the conventional witness property. This means that they are interpreted by morphisms in L which are (up to m) the image under F of coalgebra morphisms. This property, which is necessary to complete the interpretation, is shown by induction on derivations. Interestingly, the proof given is incomplete unless one uses the following crucial (and easily verified) fact, which is never actually mentioned:

Lemma 27 Any provable parsimonious sequent with a non-linear consequent has only non-linear formulae in the anetecedent.

In fact, for the presentation of the logic given by Jacobs, the lemma above is only true because I is treated as a derived formula (it is defined to be F (1), cf. our Proposition 1). The left rule for ⊗ is given as

{Υ, A, B ⊢ P \atop Υ, A ⊗ B ⊢ P}

but it just so happens that the conclusion P will always be a linear formula C. This would cease to be true if the left rule for I were given explicitly as the nullary version of that for ⊗:

{Υ ⊢ P \atop Υ, I ⊢ P}

for then one could introduce linear antecedents to non-linear formulae and the proof theory would break down. A slightly subtle point is that the above rule for I appears at first 46 3 LNL LOGIC

Axiom

P ⊢ P

Structural Rules

Υ, X, X ⊢ P ; \overline{Contraction} ; Υ, X ⊢ P Υ ⊢ P ; \overline{Weakening} ; Υ, X ⊢ P

Cut Rule

Υ ⊢ P P, Υ′ ⊢ Q

\overline{Cut}

Υ, Υ′ ⊢ Q

×/1 Rules

Υ, X ⊢ P ; \overline{×-left1} ; Υ, X × Y ⊢ P Υ, Y ⊢ P ; \overline{×-left2} ; Υ, X × Y ⊢ P

Θ ⊢ X Φ ⊢ Y

\overline{×-right}

Θ, Φ ⊢ X × Y

\overline{1-right} ; ⊢ 1

⊗/I Rules

Υ, A, B ⊢ C ; \overline{⊗-left} ; Υ, A ⊗ B ⊢ C Υ ⊢ A Υ′ ⊢ B

\overline{⊗-right}
Υ, Υ′ ⊢ A ⊗ B
Υ ⊢ A ; \overline{I-left} ; Υ, I ⊢ A \overline{I-right} ; ⊢ I

→ Rules Θ ⊢ X Y, Υ ⊢ P

\overline{→-left}

Θ, X → Y, Υ ⊢ P

Θ, X ⊢ Y ; \overline{→-right} ; Θ ⊢ X → Y

−∘ Rules Υ ⊢ A B, Υ′ ⊢ C

\overline{−∘-left}

Υ, A −∘B, Υ′ ⊢ C

Υ, A ⊢ B ; \overline{−∘-right} ; Υ ⊢ A −∘B

F Rules

Υ, X ⊢ A ; \overline{F -left} ; Υ, F X ⊢ A Θ ⊢ X ; \overline{F -right} ; Θ ⊢ F X

G Rules

Υ, B ⊢ A ; \overline{G-left} ; Υ, GB ⊢ A Θ ⊢ A ; \overline{G-right} ; Θ ⊢ GA

Figure 5: Parsimonious presentation of LNL logic sight to be valid in the semantics given by Jacobs, though it would actually cause the conventional witness property to fail and thus prevent the interpretation of →.

In any case, once one has observed the importance of the previous lemma, it seems rather more natural to interpret sequents with non-linear consequents as morphisms in the cartesian closed category in the first place, as we have done here.

3.2 Natural Deduction and LNL Terms

In this section we will present a natural deduction formulation of LNL logic and a procedure for normalising deductions. By applying the Curry-Howard correspondence, we then derive a term assignment system and a set of reduction rules, i.e. a mixed linear/non-linear lambda calculus.

3.2.1 The Natural Deduction Rules

The usual way to present natural deductions is as trees, each of which has assumptions at the leaves and a conclusion at the root. Whilst such a presentation of LNL logic is possible, we shall just give a ‘sequent style’ natural deduction system. The reason for this is that, mainly for reasons to do with term assignment, we wish to give the natural deduction analogue of LNL^{a} (rather than LNL^{m}), and the mixture of shared and distinct assumption sets which this involves is more clearly shown in the sequent style presentation. The natural deduction system is characterised by having introduction and elimination rules for each logical connective, rather than the left and right rules of the sequent calculus.

The natural deduction rules are shown in Figure 6. We will call this inference system ND.

Note that

• The elimination rule for F, like that for ⊗, builds in some substitution.

• The introduction and elimination rules for G are exact inverses.

• The G-introduction rule corresponds to promotion in ordinary linear logic. The restriction that the assumptions in the premiss be all non-linear corresponds to the restriction on the promotion rule. We do not, however, need to build any substitution into the G-introduction rule.

• None of the natural deduction rules split into L and C versions, so the natural deduction formulation is automatically ‘parsimonious’.

An important fact about the natural deduction system is that it satisfies the substitution property. This essentially means that the cut rules from the sequent calculus presentation are admissible in natural deduction:

Lemma 28 The following three rules are admissible in the natural deduction formulation of LNL logic:

Θ ⊢_{C} X X, Θ; Γ ⊢_{L} A
\overline{CL-subs}
Θ, Γ ⊢_{L} A

Θ ⊢_{C} X X, Θ ⊢_{C} Y ; \overline{CC-subs} ; Θ ⊢_{C} Y

Θ; Γ ⊢_{L} A Θ; A, Δ ⊢_{L} B

\overline{LL-subs}

Θ; Γ, Δ ⊢_{L} B

Θ; A ⊢_{L} A  Θ, X ⊢_{C} X

Θ ⊢_{C} X Θ ⊢_{C} Y

\overline{×-intro}

Θ ⊢_{C} X × Y

\overline{1-intro} ; Θ ⊢_{C} 1

Θ ⊢_{C} X × Y ; \overline{×-elim1} ; Θ ⊢_{C} X  Θ ⊢_{C} X × Y ; \overline{×-elim2} ; Θ ⊢_{C} Y

Θ; Γ ⊢_{L} A Θ; Δ ⊢_{L} B

\overline{⊗-intro}

Θ; Γ, Δ ⊢_{L} A ⊗ B Θ; Γ ⊢_{L} A ⊗ B Θ; Δ, A, B ⊢_{L} C

\overline{⊗-elim}

Θ; Γ, Δ ⊢_{L} C

\overline{I-intro} ; Θ ⊢_{L} I Θ; Γ ⊢_{L} I Θ; Δ ⊢_{L} A

\overline{I-elim}

Θ; Γ, Δ ⊢_{L} A

Θ, X ⊢_{C} Y ; \overline{→-intro} ; Θ ⊢_{C} X → Y  Θ ⊢_{C} X → Y  Θ ⊢_{C} X ; \overline{→-elim} ; Θ ⊢_{C} Y

Θ; Γ, A ⊢_{L} B

\overline{−∘-intro}

Θ; Γ ⊢_{L} A −∘B Θ; Γ ⊢_{L} A −∘B Θ; Δ ⊢_{L} A

\overline{−∘-elim}

Θ; Γ, Δ ⊢_{L} B

Θ ⊢_{C} X ; \overline{F -intro} ; Θ ⊢_{L} F X Θ; Γ ⊢_{L} F X Θ, X; Δ ⊢_{L} A \overline{F -elim}

Θ; Γ, Δ ⊢_{L} A

Θ ⊢_{L} A ; \overline{G-intro} ; Θ ⊢_{C} GA  Θ ⊢_{C} GA ; \overline{G-elim} ; Θ ⊢_{L} A

Figure 6: Natural deduction presentation of LNL logic 3.2 Natural Deduction and LNL Terms 49

Proof. Induction on the derivation of the right-hand premiss. □

We will also need: Lemma 29 The weakening rules of the sequent calculus are admissible in the natural deduction system. □

Using the previous lemmas, we can establish a connection between the sequent calculus and natural deduction formulations of the logic: Proposition 30 There are functions S : ND → LNL^{a} and N : LNL^{a} → ND which map a proof in one system to a proof of the same sequent in the other system. Furthermore, for any natural deduction Σ, N S(Σ) is equal to Σ. Proof. This is all fairly obvious induction. We start by looking at the definition of S:

• The axioms map to axioms.

• Introduction rules become right rules. For example,

\begin{matrix}Σ_{1} \\ Θ ⊢_{C} X \end{matrix}  \begin{matrix}Σ_{2} \\ Θ ⊢_{C} Y \end{matrix}
\overline{×-intro}
Θ ⊢_{C} X × Y

maps to

\begin{matrix}S(Σ_{1}) \\ Θ ⊢_{C} X \end{matrix}  \begin{matrix}S(Σ_{2}) \\ Θ ⊢_{C} Y \end{matrix}
\overline{×-right}
Θ ⊢_{C} X × Y

• Elimination rules become combinations of left rules with cuts. For example

\begin{matrix}Σ_{1} \\ Θ; Γ ⊢_{L} A ⊗ B \end{matrix}  \begin{matrix}Σ_{2} \\ Θ; Δ, A, B ⊢_{L} C \end{matrix}
\overline{⊗-elim}
Θ; Γ, Δ ⊢_{L} C

maps to

S(Σ_{1}) Θ; Γ ⊢_{L} A ⊗ B \begin{matrix}S(Σ_{2}) \\ Θ; Δ, A, B ⊢_{L} C \end{matrix} \overline{⊗-left}

Θ; Δ, A ⊗ B ⊢_{L} C
\overline{LL-cut}
Θ; Γ, Δ ⊢_{L} C

The function N mapping sequent proofs to natural deductions is also fairly straightforward:

• Axioms are translated by axioms.

• Instances of cut rules are translated by the appropriate admissible substitution rules (Lemma 28).

• Right rules become introductions.

• Left rules become eliminations modulo some structural fiddling. For example:

\begin{matrix}Σ \\ Θ, X ⊢_{C} Z \end{matrix}

\overline{C-×-left1}

Θ, X × Y ⊢_{C} Z

maps to

Θ, X × Y ⊢_{C} X × Y \overline{×-elim1} Θ, X × Y ⊢_{C} X \begin{matrix}N (Σ) \\ Θ, X ⊢_{C} Z \end{matrix}

\overline{C-weakening}
Θ, X × Y, X ⊢_{C} Z
\overline{CC-subs}
Θ, X × Y ⊢_{C} Z

Similarly, the proof

\begin{matrix}Σ \\ Θ, X; Γ ⊢_{L} A \end{matrix}

\overline{F -left}

Θ; F X, Γ ⊢_{L} A

maps to

Θ; F X ⊢_{L} F X \begin{matrix}N (Σ) \\ Θ, X; Γ ⊢_{L} A \end{matrix}

\overline{F -elim}
Θ; F X, Γ ⊢_{L} A

That N ∘ S is the identity can then be verified by induction. The proof is most easily obtained with the assistance of the term calculus which we are about to introduce. □

Clearly, there is an categorical interpretation of natural deduction proofs in any LNL model. One way to obtain the interpretation is to apply the S translation and then the interpretation of sequent proofs which we gave earlier, but it is fairly easy to write down directly (and one does indeed get the same answer!). Some of the clauses of this direct interpretation are shown in Figure 7.

3.2.2 Term Assignment

Just as the simply typed lambda calculus arises as a notation for proofs in a natural deduction system for ordinary intuitionistic propositional logic, we can annotate proofs in our system ND to derive a mixed linear and non-linear term calculus. The term assignment system is shown in Figure 8. We use a, b, c for linear variables, e, f, g, h for linear terms, w, x, y, z for non-linear variables and s, t, u, v for non-linear terms. Distinct linear contexts are assumed to mention disjoint sets of linear variable names.

As should be obvious, the two of the forms of let and the two kinds of λ are variablebinding constructs. We refrain from giving a detailed definition of free and bound variables and capture-avoiding substitution as the reader should be able to work them out without difficulty.

Lemma 31 Terms encode deductions uniquely – if Θ ⊢_{C} s: X or Θ; Γ ⊢_{L} e: A is derivable then the derivation is uniquely determined by the term. □

Lemma 32 If Θ; Γ ⊢_{L} e: A is derivable then each linear variable in the context (i.e. each variable in Γ) has exactly one free occurence in the term e.

Non-linear variables in the context may appear any number of times (including zero) in a well-typed term. □

X_{1} × ⋯ × X_{n}⟶^{s}Y

\overline{F -intro}

F X_{1} ⊗ ⋯ ⊗ F X_{n}⟶^{m}F (X_{1} × ⋯ × X_{n})⟶^{F (s)}F Y

F Θ ⊗ Γ⟶^{e}F X F Θ ⊗ F X ⊗ Δ⟶^{f}A

\overline{F -elim}

F Θ ⊗ Γ ⊗ Δ⟶^{dup⊗1⊗1}F Θ ⊗ F Θ ⊗ Γ ⊗ Δ⟶^{1⊗e⊗1}F Θ ⊗ F X ⊗ Δ⟶^{f}A

where if Θ = X_{1}, …, X_{n}, dup : F Θ → F Θ ⊗ F Θ is

⨂_{i} F X_{i}⟶^{m}F (∏_{i} X_{i}) ⟶^{F (Δ)}F ((∏_{i} X_{i}) × (∏_{i} X_{i})) ⟶^{m^{−1}} (⨂_{i} F X_{i}) ⊗ (⨂_{i} F X_{i})

F X_{1} ⊗ ⋯ ⊗ F X_{n}⟶^{e}A

\overline{G-intro}

X_{1} × ⋯ × X_{n}⟶^{η}GF (X_{1} × ⋯ × X_{n})⟶^{G(m^{−1})}G(F X_{1} ⊗ ⋯ ⊗ F X_{n})⟶^{G(e)}GA

X_{1} × ⋯ × X_{n}⟶^{s}GB

\overline{G-elim}

F X_{1} ⊗ ⋯ ⊗ F X_{n}⟶^{m}F (X_{1} × ⋯ × X_{n})⟶^{F (s)}F GB⟶^{ε}B

Figure 7: Categorical interpretation of natural deductions (sketch)

Lemma 28 can now be restated to include the terms:

Lemma 33 (Substitution) The following three rules are admissible in the LNL term calculus:

Θ ⊢_{C} s: X x: X, Θ; Γ ⊢_{L} e: A
\overline{CL-subs}
Θ, Γ ⊢_{L} e[s/x]: A
Θ ⊢_{C} s :: X x: X, Θ ⊢_{C} t: Y
\overline{CC-subs}
Θ ⊢_{C} t[s/x]: Y
Θ; Γ ⊢_{L} e: A Θ; a: A, Δ ⊢_{L} f: B
\overline{LL-subs}
Θ; Γ, Δ ⊢_{L} f[e/a]: B
□

It should be noted that the term calculus contains the usual simply typed lambda calculus as a subsystem. Note also that, in contrast to the term assignment system for intuitionistic linear logic, there is no explicit syntax for weakening or contraction in the calculus.

3.2.3 Normalisation and Reduction

We now look at the process of normalisation on natural deduction proofs in our logic, and at the associated reductions on terms. The fundamental kind of normalisation step is the removal of a ‘detour’ in the deduction, which consists of an introduction rule immediately followed by the corresponding elimination. There is thus a normalisation step for each intro/elim pair, and we consider each of these in turn:

Θ; a: A ⊢_{L} a: A  Θ, x: X ⊢_{C} x: X

{Θ ⊢_{C} s: X  Θ ⊢_{C} t: Y \atop Θ ⊢_{C} (s, t): X × Y}  Θ ⊢_{C} (): 1

{Θ ⊢_{C} s: X × Y \atop Θ ⊢_{C} fst(s): X}  {Θ ⊢_{C} s: X × Y \atop Θ ⊢_{C} snd(s): Y}

{Θ; Γ ⊢_{L} e: A Θ; Δ ⊢_{L} f: B \atop Θ; Γ, Δ ⊢_{L} e ⊗ f: A ⊗ B} Θ; Γ ⊢_{L} e: A ⊗ B Θ; Δ, a: A, b: B ⊢_{L} f: C

Θ; Γ, Δ ⊢_{L} let a ⊗ b = e in f: C

Θ ⊢_{L} ∗: I

Θ; Γ ⊢_{L} e: I Θ; Δ ⊢_{L} f: A
Θ; Γ, Δ ⊢_{L} let ∗ = e in f: A

{Θ, x: X ⊢_{C} s: Y \atop Θ ⊢_{C} (λx: X.s): X → Y}  {Θ ⊢_{C} s: X → Y  Θ ⊢_{C} t: X \atop Θ ⊢_{C} s t: Y}

{Θ; Γ, a: A ⊢_{L} e: B \atop Θ; Γ ⊢_{L} (λa: A.e): A −∘B}  {Θ; Γ ⊢_{L} e: A −∘B  Θ; Δ ⊢_{L} f: A \atop Θ; Γ, Δ ⊢_{L} e f: B}

{Θ ⊢_{C} s: X \atop Θ ⊢_{L} F(s): F X} Θ; Γ ⊢_{L} e: F X Θ, x: X; Δ ⊢_{L} f: A

Θ; Γ, Δ ⊢_{L} let F(x) = e in f: A

{Θ ⊢_{L} e: A \atop Θ ⊢_{C} G(e): GA} Θ ⊢_{C} s: GA

Θ ⊢_{L} derelict(s): A

Figure 8: LNL term assignment system • The deduction

\begin{matrix}Σ_{1} \\ Θ ⊢_{C} X \end{matrix}  \begin{matrix}Σ_{2} \\ Θ ⊢_{C} Y \end{matrix}
\overline{×-intro}
Θ ⊢_{C} X × Y
\overline{×-elim1}
Θ ⊢_{C} X

normalises to

\begin{matrix}Σ_{1} \\ Θ ⊢_{C} X \end{matrix}

• The case of ×-intro followed by ×-elim2 is similar.

• The deduction

\begin{matrix}Σ_{1} \\ Θ; Γ_{1} ⊢_{L} A \end{matrix}  \begin{matrix}Σ_{2} \\ Θ; Γ_{2} ⊢_{L} B \end{matrix}
\overline{⊗-intro}
Θ; Γ_{1}, Γ_{2} ⊢_{L} A ⊗ B

Σ_{3} Θ; Γ_{3}, A, B ⊢_{L} C
\overline{⊗-elim}
Θ; Γ_{1}, Γ_{2}, Γ_{3} ⊢_{L} C

normalises to the deduction denoted by

Σ_{1} Θ; Γ_{1} ⊢_{L} A \begin{matrix}Σ_{2} \\ Θ; Γ_{2} ⊢_{L} B \end{matrix}  \begin{matrix}Σ_{3} \\ Θ; Γ_{3}, A, B ⊢_{L} C \end{matrix} \overline{LL-subs}

Θ; Γ_{2}, Γ_{3}, A ⊢_{L} C
\overline{LL-subs}
Θ; Γ_{1}, Γ_{2}, Γ_{3} ⊢_{L} C

Note that this is not as asymmetric as it appears – the subs rule is only an admissible rule, and the actual deduction intended by the above shorthand is exactly the same as the one obtained by substituting the derivation of A first.

•

\overline{I-intro} ; Θ ⊢_{L} I  \begin{matrix}Σ \\ Θ; Γ ⊢_{L} A \end{matrix}
\overline{I-elim}
Θ; Γ ⊢_{L} A

normalises to

\begin{matrix}Σ \\ Θ; Γ ⊢_{L} A \end{matrix}

•

\begin{matrix}Σ_{1} \\ Θ, X ⊢_{C} Y \end{matrix} ; \overline{→-intro} ; Θ ⊢_{C} X → Y  \begin{matrix}Σ_{2} \\ Θ ⊢_{C} X \end{matrix}
\overline{→-elim}
Θ ⊢_{C} Y

normalises to

\begin{matrix}Σ_{2} \\ Θ ⊢_{C} X \end{matrix}  \begin{matrix}Σ_{1} \\ Θ, X ⊢_{C} Y \end{matrix}
\overline{CC-subs}
Θ ⊢_{C} Y

•

\begin{matrix}Σ_{1} \\ Θ; Γ_{1}, A ⊢_{L} B \end{matrix}

\overline{−∘-intro}

Θ; Γ_{1} ⊢_{L} A −∘B

Σ_{2} Θ; Γ_{2} ⊢_{L} A
\overline{−∘-elim}
Θ; Γ_{1}, Γ_{2} ⊢_{L} B

normalises to

\begin{matrix}Σ_{2} \\ Θ; Γ_{2} ⊢_{L} A \end{matrix}  \begin{matrix}Σ_{2} \\ Θ; Γ_{1}, A ⊢_{L} B \end{matrix}
\overline{LL-subs}
Θ; Γ_{1}, Γ_{2} ⊢_{L} B

•

\begin{matrix}Σ_{1} \\ Θ ⊢_{C} X \end{matrix} ; \overline{F -intro} ; Θ ⊢_{L} F X  \begin{matrix}Σ_{2} \\ Θ, X; Γ ⊢_{L} A \end{matrix}
\overline{F -elim}
Θ; Γ ⊢_{L} A

normalises to

\begin{matrix}Σ_{1} \\ Θ ⊢_{C} X \end{matrix}  \begin{matrix}Σ_{2} \\ Θ, X; Γ ⊢_{L} A \end{matrix}
\overline{CL-subs}
Θ; Γ ⊢_{L} A

•

\begin{matrix}Σ \\ Θ ⊢_{L} A \end{matrix} ; \overline{G-intro} ; Θ ⊢_{C} GA

\overline{G-elim}

Θ ⊢_{L} A

normalises to

\begin{matrix}Σ \\ Θ ⊢_{L} A \end{matrix}

The normalisation steps on natural deductions induce β-reductions on the associated terms. These are shown in Figure 9.

As often happpens with natural deduction systems, there is also a secondary class of reductions – the commuting conversions, which are caused by rules which have a ‘parasitic formula’. In LNL logic there are three such rules, the elimination rules for ⊗, I and F. Such a rule can artificially prevent an introduction/elimination pair from reacting unless we explicitly add certain commutations. The basic pattern is that a natural deduction looking like

⋮  ⋮ ; C ; \overline{r} ; C ; any-elim ; D

fst(s, t) →_{β} s
snd(s, t) →_{β} t
let a ⊗ b = e ⊗ f in g →_{β} g[e/a, f/b]
let ∗ = ∗ in e →_{β} e
(λx: X.s) t →_{β} s[t/x]
(λa: A.e) f →_{β} e[f/a]
let F(x) = F(s) in e →_{β} e[s/x]
derelict(G(e)) →_{β} e

Figure 9: Term calculus β-reductions

where r is a rule with parasitic formula C and any-elim is any elimination rule, commutes to

⋮  ⋮ ; C ; any-elim ; D
\overline{r}
D

In the case of LNL logic, the parasitic formula C is always linear, so any-elim can only be the elimination of one of the four linear connectives ⊗, I, −∘ and F. This means that we have 3 × 4 = 12 commuting conversions. Rather than give the conversions explicitly on proofs, we merely list the induced commutations on terms in Figure 10. The proofs are easily reconstructed by Lemma 31.^{11}

The reduction relations →_{β} and →_{c} are defined as the precongruence closures of the clauses given in Figures 9 and 10 respectively. We write →_{β,c} for →_{β} ∪ →_{c}. As we have avoided all mention of raw terms (sometimes also known as preterms), the following is almost a complete triviality:

Proposition 34 (Subject Reduction) Reduction is well-typed:

• If Θ; Γ ⊢_{L} e: A and e →_{β,c} e′ then Θ; Γ ⊢_{L} e′: A.

• If Θ ⊢_{C} s: X and s →_{β,c} s′ then Θ ⊢_{C} s′: X.

□

Somewhat more interesting is the fact that when a term is reduced its categorical interpretation remains unchanged (cf. Theorem 25).

Theorem 35 Both the β-reductions and the commuting conversions are soundly modelled by the interpretation of the natural deduction system in any LNL model.

11A small technicality is that the conversion for F -elim against itself is not an entirely local rewrite, but uses the admissible weakening rule. This would not be the case for an entirely multiplicative formulation of the natural deduction system, however.

let a ⊗ b = (let ∗ = e in f) in g →_{c} let ∗ = e in (let a ⊗ b = f in g)
let ∗ = (let ∗ = e in f) in g →_{c} let ∗ = e in (let ∗ = f in g)
(let ∗ = e in f) g →_{c} let ∗ = e in (f g)
let F (x) = (let ∗ = e in f) in g →_{c} let ∗ = e in (let F (x) = f in g)
let a ⊗ b = (let c ⊗ d = e in f) in g →_{c} let c ⊗ d = e in (let a ⊗ b = f in g)
let ∗ = (let a ⊗ b = e in f) in g →_{c} let a ⊗ b = e in (let ∗ = f in g)
(let a ⊗ b = e in f) g →_{c} let a ⊗ b = e in (f g)
let F (x) = (let a ⊗ b = e in f) in g →_{c} let a ⊗ b = e in (let F (x) = f in g)
let a ⊗ b = (let F (x) = e in f) in g →_{c} let F (x) = e in (let a ⊗ b = f in g)
let ∗ = (let F (x) = e in f) in g →_{c} let F (x) = e in (let ∗ = f in g)
(let F (x) = e in f) g →_{c} let F (x) = e in (f g)
let F (y) = (let F (x) = e in f) in g →_{c} let F (x) = e in (let F (y) = f in g)

Figure 10: Term calculus commuting conversions

• If Θ; Γ ⊢_{L} e: A and e →_{β,c} e′ then

[[Θ; Γ ⊢_{L} e: A]] = [[Θ; Γ ⊢_{L} e′: A]]

• If Θ ⊢_{C} s: X and s →_{β,c} s′ then

[[Θ ⊢_{C} s: X]] = [[Θ ⊢_{C} s′: X]]
□

3.3 Translations

We already know from Section 2 that LNL models and linear categories are equivalent. What we have not yet done is show any direct relationship between provability (or proofs) in LNL logic and in ordinary ILL. Such questions could be approached from the semantic point of view if we had a completeness result for LNL models, but for the moment we shall just argue proof-theoretically.^{12} In this section we will relate LNL logic to ILL, restricting attention to the natural deduction formulations (equivalently, the term assignment systems). Comparable translations for the sequent calculus are straightforward to obtain, but omitted.

We begin by recalling in Figure 11 the linear term calculus (LTC) which corresponds to the natural deduction presentation of ILL [BBHdP92].

12I conjecture that the natural completeness theorem is true, and see no particular reason why the proof should not be by a standard term-model construction – I just haven’t done it yet. The first step is to list all the term equalites given by the category theory. These comprise the β, c equalities from the proof theory together with a number of naturality and η (uniqueness) equalities.

a : A ⊢ a : A (Ax)

Γ, a : A ⊢ e : B ; (−∘_{I}) ; Γ ⊢ (λa: A.e) : A −∘B  Γ ⊢ e : A −∘B  Δ ⊢ f : A ; (−∘_{E}) ; Γ, Δ ⊢ ef : B

⊢ ∗ : I (I_{I})

Γ ⊢ e : A Δ ⊢ f : I
(I_{E})
Γ, Δ ⊢ let f = ∗ in e : A

Γ ⊢ e : A Δ ⊢ f : B ; (⊗_{I}) ; Γ, Δ ⊢ e ⊗ f : A ⊗ B Γ ⊢ e : A ⊗ B Δ, a : A, b : B ⊢ f : C

(⊗_{E})
Γ, Δ ⊢ let e = a ⊗ b in f : C

Δ_{1} ⊢ e_{1} :!A_{1} ⋯ Δ_{n} ⊢ e_{n} :!A_{n} a_{1} :!A_{1}, …, a_{n} :!A_{n} ⊢ f : B

\overline{Promotion}

Δ_{1}, …, Δ_{n} ⊢ promote e_{1}, …, e_{n} for a_{1}, …, a_{n} in f :!B

Γ ⊢ e :!A Δ, a :!A, b :!A ⊢ f : B

\overline{Contraction}

Γ, Δ ⊢ copy e as a, b in f : B

Γ ⊢ e :!A Δ ⊢ f : B

\overline{Weakening}

Γ, Δ ⊢ discard e in f : B

Γ ⊢ e :!A

\overline{Dereliction}

Γ ⊢ derelict(e) : A

Figure 11: The linear term calculus (LTC)

3.3.1 ILL to LNL Logic

The translation of ILL into LNL logic is not particularly difficult. If A is an ILL proposition, define the linear LNL proposition A^{∘} inductively as follows:

A_{0}^{∘} = A_{0} (A_{0} atomic)
(A ⊗ B)^{∘} = A^{∘} ⊗ B^{∘}
(A −∘B)^{∘} = A^{∘} −∘B^{∘}
I^{∘} = I
(!A)^{∘} = F G(A^{∘})

Theorem 36 If Γ ⊢ e: A in ILL, then there is an e^{∘} such that Γ^{∘} ⊢_{L} e^{∘}: A^{∘}.

Proof. This is done by induction on the derivation in ILL (that is, on the structure of the linear term e). The exponential-free rules are completely straightforward, so we just detail the translations of the one introduction and three elimination rules for !. The easiest way to present the translations is just to give the translation from terms to terms, as that determines the translation of proofs.

Promotion The (−)^{∘} translation of

promote e_{1}, …, e_{n} for a_{1}, …, a_{n} in f

is

let F (y_{1}) = e_{1}^{∘} in let F (y_{2}) = e_{2}^{∘} in … F G(f^{∘}[F (y_{i})/a_{i}])

where the y_{i} are fresh. One might be tempted to simplify the translation to

F G(f^{∘}[e_{i}/a_{i}])

but a moment’s consideration reveals that this latter expression is not well-typed. It is interesting to note how the ‘boxing’ behaviour of the promotion rule is thus maintained by its translation into LNL logic, even though neither of the introduction rules for F and G themselves involve a change of variable names. Note also that the translation makes use of an admissible substitution rule.

Dereliction

(derelict(e))^{∘} = let F (x) = e^{∘} in derelict(x)

where x is fresh. (Which version of derelict() is meant should usually be clear from context.)

Weakening

(discard e in f)^{∘} = let F (x) = e^{∘} in f^{∘}

where x is fresh. Contraction

(copy e as a, b in f)^{∘} = let F (x) = e^{∘} in f^{∘}[F (x)/a, F (x)/b]

where x is fresh. Again, note that this is not just f^{∘}[e^{∘}/a, e^{∘}/b].

□

So we can translate ILL into the linear-only part of LNL logic in such a way that provability is preserved. That it is also reflected will follow from the translation from LNL logic to ILL which we are about to give.

3.3.2 LNL Logic to ILL

This direction is more interesting. The basic idea is to translate the linear part of LNL logic essentially unchanged and to translate the non-linear part by using a variant of the Girard translation. There is a small technicality concerning atomic propositions, in that LNL logic has both linear and non-linear atoms. We will thus translate into an ILL theory which has an extra atomic proposition A_{X_{0}} for each non-linear atomic proposition X_{0} in the LNL theory. Given this, we can define the ILL proposition A^{∗} or X^{∗} for each LNL proposition A or X inductively as follows

A_{0}^{∗} = A_{0} (A_{0} atomic)
(A ⊗ B)^{∗} = A^{∗} ⊗ B^{∗}
I^{∗} = I
(A −∘B)^{∗} = A^{∗} −∘B^{∗}
(F X)^{∗} = !(X^{∗})
X_{0}^{∗} = A_{X_{0}} (X_{0} atomic)
(X × Y)^{∗} = !(X^{∗})⊗!(Y^{∗})
1^{∗} = I
(X → Y)^{∗} = !(X^{∗}) −∘Y^{∗}
(GA)^{∗} = A^{∗}

Note that what is usually called ‘the Girard translation’ of IL to ILL uses the & connective (‘with’) to translate conjunction in IL, but we have not done this as we are dealing only with the multiplicative fragment of ILL at the moment. Were we to include additives, then obviously an alternative translation would be possible.

Theorem 37

1. If Θ ⊢_{C} s: X in LNL logic, then there is an LTC term s^{∗} such that

!Θ^{∗} ⊢ s^{∗}: X^{∗}

2. If Θ; Γ ⊢_{L} e: A in LNL logic, then there is an LTC term e^{∗} such that

!Θ^{∗}, Γ^{∗} ⊢ e^{∗}: A^{∗}

Proof. This is proved by induction on the LNL derivation. The translation is slightly more complicated than it might be because of the fact that we have treated the conventional parts of LNL contexts in an additive way, and this does not easily match the purely multiplicative contexts used in ILL. For this reason, as well as the way in which the translation depends upon context, we will present this translation on derivations in the logic rather than on terms. The reader should be able easily to supply the missing term annotations so as to prove the theorem as stated.

• The translation of an axiom

Θ, X ⊢_{C} X

is

!X^{∗} ⊢!X^{∗} ; \overline{Dereliction} ; !X^{∗} ⊢ X^{∗}

= Weakening*

!Θ^{∗},!X^{∗} ⊢ X^{∗}

• The translation of an axiom

Θ; A ⊢_{L} A

is A^{∗} ⊢ A^{∗}

= Weakening*
!Θ^{∗}, A^{∗} ⊢ A^{∗}

• If the LNL derivation ends in

Θ ⊢_{C} X Θ ⊢_{C} Y
\overline{×-intro}
Θ ⊢_{C} X × Y

where Θ = Y_{1}, …, Y_{n}, then by induction we have ILL derivations of !Θ^{∗} ⊢ X^{∗} and !Θ^{∗} ⊢ Y^{∗} so that we can form the following (omitting rule names for reasons of space):

\begin{matrix}{!Y_{1}^{∗} ⊢!Y_{1}^{∗} ⋯!Y_{n}^{∗} ⊢!Y_{n}^{∗}  !Θ^{∗} ⊢ X^{∗} \atop !Y_{1}^{∗}, …,!Y_{n}^{∗} ⊢!X^{∗}} & {!Y_{1}^{∗} ⊢!Y_{1}^{∗} ⋯!Y_{n}^{∗} ⊢!Y_{n}^{∗}  !Θ^{∗} ⊢ Y^{∗} \atop !Y_{1}^{∗}, …,!Y_{n}^{∗} ⊢!Y^{∗}} \\ !Θ^{∗},!Θ^{∗} ⊢!X^{∗}⊗!Y^{∗} \end{matrix}
= Contraction*
!Θ^{∗} ⊢!X^{∗}⊗!Y^{∗}

• If the LNL derivation ends in

Θ ⊢_{C} X → Y Θ ⊢_{C} X

\overline{→-elim}
Θ ⊢_{C} Y

where Θ = Y_{1}, …, Y_{n},then by induction we have ILL derivations of !Θ^{∗} ⊢!X^{∗} −∘Y^{∗} and !Θ^{∗} ⊢ X^{∗} so we can form

!Θ^{∗} ⊢!X^{∗} −∘Y^{∗}  !Y_{1}^{∗} ⊢!Y_{1}^{∗} ⋯ !Y_{n}^{∗} ⊢!Y_{n}^{∗}  !Θ^{∗} ⊢ X^{∗} \overline{Promotion} !Y_{1}^{∗}, …,!Y_{n}^{∗} ⊢!X^{∗}
\overline{−∘-elim}
!Θ^{∗},!Θ^{∗} ⊢ Y^{∗}
= Contraction*
!Θ^{∗} ⊢ Y^{∗}

• If the LNL derivation ends with

Θ ⊢_{C} X ; \overline{F -intro} ; Θ ⊢_{L} F X

where Θ = Y_{1}, …, Y_{n}, then by induction there is a derivation of !Θ^{∗} ⊢ X^{∗} so we can

form !Y_{1}^{∗} ⊢!Y_{1}^{∗} ⋯ !Y_{n}^{∗} ⊢!Y_{n}^{∗} !Θ^{∗} ⊢ X^{∗}

\overline{Promotion}

!Y_{1}^{∗}, …,!Y_{n}^{∗} ⊢!X^{∗}

as required.

• Because of the fact that the G operator of LNL logic translates to nothing in ILL, the translation of both the G-introduction and G-elimination rules is the identity.

• The remaining rules are similar.

□

3.3.3 Further Results on the Translations

We now have translations both ways between LNL logic and ILL which preserve provability. There are probably other translations one could use, but these two seem to be the most natural.

Clearly, if one starts with a judgement of LNL logic and translates it to ILL and then back to LNL logic, one will not, in general, get back to the original judgement. This is because the final judgment will be in the purely linear fragment of LNL logic. Going around the cycle the other way, however, is the identity:

Theorem 38 For any ILL judgement Γ ⊢ A, the result of translating it into LNL logic and then back to ILL, viz.

Γ^{∘}^{∗} ⊢ A^{∘}^{∗}

is equal to the original judgement. As a corollary, the (−)^{∘} translation of ILL into LNL logic reflects, as well as preserves, provability in that

Γ ⊢ A

is provable in ILL iff

Γ^{∘} ⊢_{L} A^{∘}

is provable in LNL logic.

Proof. A trivial induction shows that for all ILL formulae A, A = A^{∘}^{∗}, from which the first part of the theorem is immediate. The second part then follows by Theorems 36 and 37. □

A natural question is whether the previous result extends to proofs (rather than just to provability). It is certainly not the case that the result of mapping an ILL proof into LNL logic and back again is syntactically identical to the original proof, but it turns out that it is equal to the original proof under the equality on ILL proofs given by linear categories. The easiest way to state and prove this result is by using the linear term calculus:

Theorem 39 If Γ ⊢ e: A in LTC, then not only is Γ ⊢ e^{∘}^{∗}: A provable, but e ≈ e^{∘}^{∗} where ≈ is the categorical equality relation on LTC terms given in [BBHdP92, Figure 11, page 40].

Proof. This is an induction on the structure of e, but we omit the rather hairy details (which in any case would require the repetition of too much material from the earlier work). One first has to fill in the missing terms in the proof of Theorem 37 and then prove a number of lemmas concerning the way in which the (−)^{∗} translation behaves with respect to the admissible rules of weakening, contraction and substitution in the LNL term calculus (because these rules are used in defining the (−)^{∘} translation). The terms arising directly from the composite translation (−)^{∘}^{∗} are in general very large, but, given a certain amount of care over variable names, they simplify fairly easily. □

4 Conclusions and Further Work

We have given a new and intuitively appealing characterisation of categorical models of intuitionistic linear logic. We then used this presentation of the models as the basis for defining a new logic which unifies ordinary intuitionistic logic with intuitionistic linear logic. The natural deduction presentation of the new logic then gave, by the Curry-Howard correspondence, a mixed linear and non-linear lambda calculus.

At first sight, one might be tempted to regard LNL logic as “a logical atrocity without interest” [GLT89]. I hope, however, that I have shown that this is not the case. LNL logic has a very natural class of categorical models and a well-behaved proof theory in both its sequent calculus and natural deduction formulations. Given this, and the links with other research which were mentioned in the introduction, LNL logic certainly seems to merit further study.

On the theoretical side, much remains to be done. We have not proved a completeness theorem, nor have we proved that the LNL term calculus is strong normalising. The strong normalisation proof should be relatively easy to do via a translation argument like that which we have previously used for the linear term calculus [Ben95] and the computational lambda calculus [BBdP93]. It would be nice to have better (that is, less degenerate) examples of concrete models and one might well find such examples by looking at some of the categories arising in game semantics.

The connections between LNL logic and other work on LU and related systems should be looked at more closely. As well as the references cited in the introduction, Schellinx’s work [Sch94] on decorating conventional proofs to give linear ones seems particularly interesting in this respect.

It should be noted that although the translations between ILL and LNL logic behave well with respect to equality, we have not claimed anything concerning the translations and reduction. I do not yet have any definitive results on whether, for example, reduction is preserved under either of the translations, but it certainly seems that any positive results will involve commuting conversions as well as the more conventional β rules.

There are also many obvious extensions to the system discussed here. The first of these is to consider the additive connectives on the linear side, and disjunction (coproducts) on the conventional side. We touched briefly on this in Section 2.2.3, but more remains to be done; this should be relatively straightforward, although, as we have already seen, there is some complication regarding coproducts in LNL models compared with coproducts in linear categories. Beyond that, one could consider adding inductive or coinductive datatypes or second-order quantification to the logic. This seems particularly worthwhile in the light of Plotkin’s work on parametricity and recursion in a logic rather like ours [Plo93].

On the practical side, we should investigate whether or not the LNL term calculus lends itself more readily to efficient implementation than does the linear term calculus. The hope is that one can arrange an implementation with two memory spaces, corresponding to the two subsystems of LNL logic. The non-linear space would be garbage collected in the usual way, whereas the linear space would contain objects satisfying some useful memory invariant (such as having only one pointer to them at all times) which could be exploited to reduce the space usage of programs. Previous experience, however, shows that turning such intuitively plausible hopes into provably correct implementations is a non-trivial task.

5 Acknowledgements

I should like to thank my collaborators Gavin Bierman, Martin Hyland and Valeria de Paiva for innumerable discussions about logic, terms and categories. Thanks also to Gordon Plotkin for making a remark which led directly to the work described here, and to Barney Hilken for several useful conversations. John Reynolds’s diagram macros and Paul Taylor’s proof tree macros were used to typeset the paper.

References

[BBdP93] P. N. Benton, G. M. Bierman, and V. C. V. de Paiva. Computational types from a logical perspective. Preprint, 1993.

[BBHdP92] P. N. Benton, G. M. Bierman, J. M. E. Hyland, and V. C. V. de Paiva. Term assignment for intuitonistic linear logic. Technical Report 262, Computer Laboratory, University of Cambridge, August 1992.

[BBHdP93a] P. N. Benton, G. M. Bierman, J. M. E. Hyland, and V. C. V. de Paiva. Linear lambda calculus and categorical models revisited. In E. Börger et al., editor, Selected Papers from Computer Science Logic ’92, volume 702 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

[BBHdP93b] P. N. Benton, G. M. Bierman, J. M. E. Hyland, and V. C. V. de Paiva. A term calculus for intuitionistic linear logic. In M. Bezem and J. F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

[Ben95] P. N. Benton. Strong normalisation for the linear term calculus. Journal of Functional Programming, 1995. To appear. Also available as Technical Report 305, University of Cambridge Computer Laboratory, July 1993.

[Bie94a] G. M. Bierman. On intuitionistic linear logic (revised version of PhD thesis). Technical Report 346, Computer Laboratory, University of Cambridge, August 1994.

[Bie94b] G. M. Bierman. What is a categorical model of intuitionistic linear logic? Technical Report 333, Computer Laboratory, University of Cambridge, April 1994.

[BS93] E. Barendsen and S. Smetsers. Conventional and uniqueness typing in graph rewrite systems. Technical Report CSI-R9328, Katholieke Universiteit Nijmegen, December 1993.

[CP90] R. L. Crole and A. M. Pitts. New foundations for fixpoint computations: FIX-hyperdoctines and the FIX-logic. Technical Report 204, Computer Laboratory, University of Cambridge, August 1990.

[Cro92] R. L. Crole. Programming Metalogics with a Fixpoint Type. PhD thesis, Computer Laboratory, University of Cambridge, February 1992. Available as Technical Report 247.

[FW87] J. Fairbairn and S. Wray. TIM: A simple, lazy abstract machine to execute supercombinators. In G. Kahn, editor, Proceedings of the 1987 Conference on Functional Langauges and Computer Architecture. LNCS 274, Springer-Verlag, 1987.

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

[Gir93] J.-Y. Girard. On the unity of logic. Annals of Pure and Applied Logic, 59:201–217, 1993.

[GLT89] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[Jac93] B. Jacobs. Conventional and linear types in a logic of coalgebras. Preprint, University of Utrecht, April 1993.

[Koc71] A. Kock. Bilinearity and cartesian closed monads. Math. Scand., 29:161–174, 1971.

[LM92] P. Lincoln and J. C. Mitchell. Operational aspects of linear lambda calculus. In Proceedings of the 7th Annual Symposium on Logic in Computer Science. IEEE, 1992.

[Mog89] E. Moggi. Computational lambda-calculus and monads. In Proceedings of the 4th Annual Symposium on Logic in Computer Science, Asiloomar, CA, pages 14–23, 1989.

[Mog91] E. Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

[Plo93] G. D. Plotkin. Type theory and recursion (abstract). In Proceedings of 8th Conference on Logic in Computer Science. IEEE Computer Society Press, 1993.

[Pra92] V. Pratt. Message to the ‘categories@mta.ca’ electronic mailing list 27th November, 1992.

[Sch94] H. Schellinx. The Noble Art of Linear Decorating. PhD thesis, University of Amsterdam, 1994.

[See80] R. A. G. Seely. Linear logic, *-autonomous categories and cofree coalgebras. In Conference on Categories in Computer Science and Logic, volume 92 of AMS Contemporary Mathematics, June 1980.

[Str72] R. Street. The formal theory of monads. J. Pure and Applied Algebra, 2:149–168, 1972.

[Wad90] P. Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, Programming Concepts and Methods. North Holland, 1990.

[Wad92] P. Wadler. There’s no substitute for linear logic (projector slides). In G. Winskel, editor, Proceedings of the CLICS Workshop (Part I), March 1992, Aarhus, Denmark, May 1992. Available as DAIMI PB-397-I Computer Science Department, Aarhus University.

[Wad93] P. Wadler. A taste of linear logic. In A. M. Borzyszkowski and S. Sokolowski, editors, Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, number 711 in Lecture Notes in Computer Science, pages 185–210, 1993.