Full Intuitionistic Linear Logic (Extended Abstract)

Martin Hyland Department of Pure Mathematics and Mathematical Statistics University of Cambridge

                         jmeh1@phx.cam.ac.uk

Valeria de Paiva Computer Laboratory University of Cambridge

                          vcvp@cl.cam.ac.uk

June 25, 1993

Introduction

In this paper we give a brief treatment of a theory of proofs for a system of Full Intuitionistic Linear Logic. Since Girard and Lafont’s original paper [13] on Intuitionistic Linear Logic it seems to have been generally assumed that the multiplicative disjunction, par, does not make sense outside the context of classical linear logic; in particular par was thought to present problems for an interpretation of proofs as functions as described in the first part of Abramsky [1]. However the connective par does have an entirely natural interpretation in models of the kind developed in de Paiva [7], and it is our intention to make good the claim that full intuitionistic is a significant dialect of linear logic.

We take as the main initial problem to be overcome the observation of Schellinx [22] that cut elimination fails outright for the system of logic considered by de Paiva. There seems to be a mismatch between this fact and the pleasing nature of the categorical semantics. Our response is to develop a term assignment system which gives an interpretation of proofs as some kind of non-deterministic function (which appears as a sequence of partial functions evaluated in parallel). In this way we find a system which does enjoy cut elimination. The system is a direct result of an analysis of the categorical semantics, though we make an effort to present the system as if it were purely a proof theoretic construction. Thus the proof-theorist that objects to category theory may safely skip the first section and still make sense of the paper.

In this paper we restrict attention to the so called multiplicative (and modality-free) fragment of Linear Logic as that is where the essential proof theoretic difficulty resides.

In the interests of clarity we build up to our system by considering subsystems of the multiplicative fragment. In all the subsystems we have a logic and its extension to a term assignment system (which gives an interpretation of the notion of proof), and both of these enjoy cut elimination (the term assignment system in a decorated sense that we shall discuss). For our full system however the term assignment system does essential work. It provides information in the dependence of formulae on the left and right of a sequent. The natural cut elimination procedure works for it, but it does not work for any obvious presentation of the pure logic.

In every case we equip the terms with a theory of equality which provides a term calculus corresponding to the ‘natural categorical model’. The equalities are needed to explain the extended sense of cut elimination, but this can be appreciated independently of the categorical motivation for the equations. We have suppressed discussion of the computational significance of the term calculus (in particular the relation with the reduction processes in Benton et al. [3]).

This paper is organised as follows. In Section 1 we give an overview of our categorical motivation. In Section 2 we present a simple term assignment for the tensor-implication fragment of Linear Logic as described Girard and Lafont [13], and discuss its categorical significance. In Section 3 we first introduce an eccentric system of par logic and the term assignment for the par fragment of Intuitionistic Linear Logic and then we discuss the system consisting of tensor and par alone. The heart of the paper is Section 4 where we show how to control the interaction between (linear) implication and par. Section 5 concludes the paper, describing some future and related work.

1 Categorical Motivation

For general discussion of the notion of a categorical model of classical or intuitionistic linear logic we refer the reader to the work of Seely [23], de Paiva [6], Benton et al. [3]. In this paper we are concerned only with the multiplicative fragment of Linear Logic without modalities and for that fragment we can give a succinct (preliminary) account:

• A categorical model of the multiplicative fragment of Classical Linear Logic consists of a ∗-autonomous category in the sense of Barr [2];

• A categorical model of the multiplicative fragment of Intuitionistic Linear Logic consists of a symmetric monoidal closed category in the sense of Eilenberg and Kelly [10].

Now in many cases of interest models of the multiplicative fragment of Intuitionistic Linear Logic (that is, symmetric monoidal closed categories) are in fact equipped with a second symmetric monoidal structure. Moreover this second monoidal structure (□, ⊥) is related to the original monoidal structure (⊗, I) by what we [16] (and Cockett and Seely [5], independently) have called a weak distributivity law: there is a comparison map

w_{A,B,C}: A⊗(B□C) → (A⊗B)□C

satisfying natural coherence conditions which involve commuting one operator past the other. (For details we refer the reader to Cockett and Seely [5]. As Joyal observed to us coherence conditions can be given a simple geometric explanation, whence the connection with braids.)

It seems reasonable to refer to a symmetric monoidal closed category equipped with this additional structure as a (weakly) distributive symmetric monoidal closed category; but that is a bit of a mouthful and so we have coined the term full multiplicative category. As observed also by Cockett and Seely the notion of weak distributivity on its own is the categorical counterpart of the tensor-par fragment of Linear Logic. (However as Cockett and Seely are mainly concerned with Classical Linear Logic, they have to add to this structure some extra maps.)

Thus we can add to the above account:

• A categorical model of the tensor-par fragment of Full Intuitionistic Linear Logic consists of a weakly distributive category.

• A categorical model of the multiplicative fragment of Full Intuitionistic Linear Logic consists of a full multiplicative category.

We now give three (families of) examples of full multiplicative categories and discuss them briefly.

1. Domains and linear maps. As a simple example we consider the qualitative domains introduced by Girard [12]: these are essentially domains X which appear as subdomains of (P (|X|), ⊆), and we say that such a qualitative domain is on (the underlying set of tokens) |X|. A linear map (not necessarily stable) f : X → Y of qualitative domains is simply one which preserves all sups (unions) which exist in X; note that such a map is determined by a subset {(x, y)|y ∈ f({x})} of |X| × |Y |. If X and Y are qualitative domains, then X⊗Y is a qualitative domain on |X| × |Y | where a ∈ X⊗Y if and only if fst(a) ∈ X and snd(a) ∈ Y. If Y and Z are qualitative domains, then Y −∘Z is a qualitative domain on |Y |×|Z| where c ∈ Y −∘Z if and only if for all a ∈ Y the set {z|∃y ∈ a.(y, z) ∈ c} ∈ Z. It is easy to see that linear maps X⊗Y → Z are in bijective correspondence with linear maps X → Y −∘Z, and hence to check that the category of qualitative domains and linear maps has the structure of a monoidal closed category. But this category has also another (symmetric) monoidal structure. If X and Y are qualitative domains, then X□Y is a qualitative domain on |X| × |Y | where a ∈ X□Y if and only if fst(a) ∈ X or snd(a) ∈ Y. It is now easy to see that the weak-distributivity laws are satisfied, so that we have a full multiplicative category. In fact as the astute reader will realise, this example is a bit special; any qualitative domain has a comultiplication, so there is even a more familiar (non-linear) distributive law X⊗(Y □Z) → (X⊗Y)□(X⊗Z). However if we pass to more general domains we find that we still have a full multiplicative category of domains and linear maps, but without the non-linear distributivity. Also it is straightforward to extend this idea to categories of domains and stable linear maps, which again have the structure of full multiplicative categories.

2. The Dialectica categories GC. We recall that a family of (categorical) models of Intuitionistic Linear Logic and Classical Linear Logic have been provided by de Paiva [6, 9] with the generic title of Dialectica Categories. The dialectica categories^{1} are (parametric) constructions that one applies to a given category C to obtain other categories. In particular de Paiva describes the so called (Girard) categories GC where objects are relations in C, that is monics of the form A → U × X and morphisms are pairs of maps of C, f: U → V and F: Y → X such that a pullback condition is satisfied. Every category GC is a full multiplicative category and more they have finite products and coproducts (which model additives) and a comonad ‘!’ and a monad ‘?’ (which model the exponentials). An important point about the GC categories is that they were the first (non-syntactical) model of Linear Logic which distinguished between all operators and units of the logic.

1The Dialectica categories [9] got their name from Hyland’s insight that it was possible to use them to give an internal categorical characterization of Gödel’s Dialectica Interpretation [15].

3. Curien’s category of games. In a circulated email message Curien has drawn attention to a category based on Blass games [4] with partial strategies. In Blass games G and H between Friend (whom we prefer) and Foe, the players have to move alternately (so that there are no positions where both players may move). A Curien game is a Blass game in which Foe must move first. A map f: G → H of Curien games is a partial strategy for playing the game G−∘H which amounts to a partial strategy for playing the games G^{⊥} and H in parallel, according to the Blass par convention that only Friend may move from one game to the other. (Note that G^{⊥} is G with the roles of the players reversed, so it is not a Curien game!) There is a tensor product G⊗H of games, which corresponds to playing G and H in parallel according to the Blass tensor convention that only Foe may move from one game to the other; so in particular Foe chooses which game to start. The resulting category is symmetric monoidal closed with the internal-hom −∘ giving the closed structure corresponding to ⊗. However the category of Curien games also inherits a further (symmetric) monoidal structure (□, ⊥) defined by Blass. In the game G□H, Foe plays the first move in both G and H simultaneously and thereafter the games are played in parallel according to the Blass par convention. It is routine to define a weak distributivity law for ⊗ over □ so that the category of Curien games is naturally a full multiplicative category.

2 The tensor-implication fragment of Linear Logic

We recall the sequent calculus rules for the tensor-implication fragment of Intuitionistic Linear Logic in Figure 1. We refer to this fragment (which Girard, Scedrov and Scott [14] call rudimentary linear logic) as tensor-implication logic.

This is a familiar sequent calculus presentation for conjunction and implication with the feature (typical of linear logic) that there are no rules of weakening or contraction. Note the rule (Exchange); throughout this paper we are only concerned with commutative fragments of Linear Logic. On the left hand side of the turnstile we have a sequence of formulae and on the right-hand side a single formula.

The Cut rule is an eliminable rule of the system. Every derivation which uses the rule Cut can be transformed into a derivation without it. This ‘Cut Elimination Theorem’, a deep result in some contexts, is here more or less a triviality.

We can fill out the system of tensor-implication logic to an assignment of terms, as is done in Abramsky [1] and (in a very preliminary form) in Lafont [17]. We briefly sketch this material and consider its categorical significance.

Following Abramsky’s notation, we first define collections of patterns and of terms. Thus if X is a finite set of variables, define P_{X} the set of patterns with variables in X by:

∗ ∈ P_{∅} x ⊗ y ∈ P_{{x,y}}

\begin{aligned}& Identity \\ A ⊢ A \end{aligned}

Γ, A, B, Δ ⊢ C

\overline{Exchange}

Γ, B, A, Δ ⊢ C

Γ ⊢ B B, Δ ⊢ C
Cut
Γ, Δ ⊢ C
Γ ⊢ A ; (I_{L}) ; Γ, I ⊢ A  \begin{aligned}& (I_{R}) \\ ⊢ I \end{aligned}

Γ, A, B ⊢ C ; (⊗_{L}) ; Γ, A⊗B ⊢ C  Γ ⊢ A  Δ ⊢ B ; (⊗_{R}) ; Γ, Δ ⊢ A⊗B

Γ ⊢ A  Δ, B ⊢ C ; (−∘_{L}) ; Γ, Δ, A−∘B ⊢ C  Γ, A ⊢ B ; (−∘_{R}) ; Γ ⊢ A−∘B

Figure 1: Tensor-Implication Logic

Then define T_{X} the linear terms with set of free variables X, inductively as follows:

• x ∈ T_{{x}};

• ∗ ∈ T_{∅};

• t ∈ T_{X}, u ∈ T_{Y} , X ∩ Y = ∅ implies t ⊗ u ∈ T_{X∪Y};

• t ∈ T_{X}, p ∈ P_{Y} , e ∈ T_{Y ∪Z}, X ∩ Z = ∅, Y ∩ Z = ∅ implies (let t be p in e) ∈ T_{X∪Z};

• t ∈ T_{X}, u ∈ T_{Y} , X ∩ Y = ∅ implies tu ∈ T_{X∪Y};

• t ∈ T_{X∪{x}}, x ∉ X implies λx.t ∈ T_{X}.

The term assignment system for tensor-implication logic is displayed in Figure 2. Note that here, as throughout this paper, where substitutions are indicated it is assumed that the relevant variables actually appear.

Note that the new term constructor (let t be x⊗y in e) in rule (⊗_{L}) (and similarly for the rule (I_{L})) binds the variables x and y within the term e. The reader will see that here (as later) the term t and pattern p appear in (let t be p in e) in the opposite order to that traditional in functional programming where (let p = t in e) would be used. We find the non-standard order more intuitive when considering mathematical semantics, and apologize for any confusion this convention may cause.

Now we adopt the perspective from categorical logic where types correspond to objects of a category; terms correspond to maps (or arrows) and operations transforming proofs into proofs correspond (if possible) to natural transformations between appropriate homfunctors.

x : A ⊢ x : A
Γ, x : A, y : B, Γ′ ⊢ f : C

Exchange

Γ, y : B, x : A, Γ′ ⊢ f : C
Γ ⊢ e : A Δ, x : A ⊢ f : B

Cut

Γ, Δ ⊢ f[e/x] : B
Γ ⊢ e : A  Δ, x : B ⊢ f : C ; (−∘_{L}) ; Γ, g : A−∘B, Δ ⊢ f[(ge)/x] : C  Γ, x : A ⊢ e : B ; (−∘_{R}) ; Γ ⊢ λx.e : A−∘B
Γ ⊢ e : A
(I_{L})
Γ, x : I ⊢ let x be ∗ in e : A

\begin{aligned}& (I_{R}) \\ ⊢ ∗ : I \end{aligned}

Δ, x : A, y : B ⊢ f : C
(⊗_{L})
Δ, z : A⊗B ⊢ let z be x⊗y in f : C

Γ ⊢ e : A Δ ⊢ f : B ; (⊗_{R}) ; Γ, Δ ⊢ e⊗f : A⊗B

Figure 2: Term Assignment System for Tensor-Implication Logic

The analysis of the system just given is most clear if we take seriously the fact that we are dealing with sequents of the form Γ ⊢ t: A. The structural rules Identity and Cut then give a system corresponding to the notion of a multicategory (a recent reference is [18]); and adding (Exchange) gives rise to the notion of a symmetric multicategory. Then the rules for the logical connectives ⊗ and I provide a collection of terms suggesting that the connective ⊗ should be ‘the’ representing tensor product for the multimaps of the multicategory. In other words that we should have a (symmetric) monoidal multicategory in Lambek’s terminology. The rules for the connective linear implication suggest furthermore that the (symmetric) monoidal multicategory should be closed. Then a detailed analysis of the process of assigning terms to proofs, taking in consideration cut elimination as well as some simplifying extensionality assumptions (for a similar discusssion see the paper by Benton et al. [3]) provides us with some (extra) equations, similar to the β and η rules of standard lambda-calculus. These rules we collect in Figure 3.

The equality generated by (the typed version of) these rules gives us a theory which we refer to as the term calculus of tensor-implication logic. The categorical counterpart of this term calculus is the notion of a closed (symmetric) monoidal multicategory as is made precise shortly. Of course we can now suppress the multicategorical aspects: a closed (symmetric) monoidal multicategory is ‘essentially’ just a (symmetric) monoidal closed category. But this identification can only be made at the cost of introducing questions of coherence.

We now briefly explain the sense in which a closed (symmetric) monoidal (multi)category is the categorical counterpart of the term calculus. Given such a (multi)category one can inductively define an interpretation of the types and terms of the term assignment as objects and (multi)maps of the (multi)category. (Technically the induction is over the derivation of the sequent Γ ⊢ t : A but one can readily show that the interpretation is

let ∗ be ∗ in e  = e
let u be ∗ in f[∗/z]  = f[u/z]
let e⊗t be x⊗y in u  = u[e/x, t/y]
let u be x⊗y in f[x⊗y/z] = f[u/z]
(λx.t)e  = t[e/x]
λx.tx  = t

Figure 3: (Tensor-Implication) Categorical equalities

independent^{2} of the derivation.) In such an interpretation the (typed) equalities of Figure 3 hold. Furthermore the usual term model construction of categorical logic gives for any theory a (multi)category in which just the (typed) equalities of the theory hold. This in outline proves the following result.

Theorem 1 The (typed versions of the) equalities of Figure 3 are sound and complete for interpretations in symmetric monoidal closed categories.

We can now consider what becomes of the process of cut-elimination once terms have been added to the system. While cuts cannot be eliminated outright, they can be eliminated modulo the categorical equalities just introduced.

Theorem 2 If the sequent Γ ⊢ t : A is derivable then, for some \overline{t}, the equation t = \overline{t} is provable from the given categorical equalities (using typed equational logic) and Γ ⊢ \overline{t} : A is derivable without the Cut rule.

The proof of this theorem is an extension of the usual proof of cut elimination; one simply carries the terms along with one. At various points equational consequences of the categorical equalities are needed. These are all instances of the naturality equations displayed in Figure 4; the reader may like to check that the naturality equations are consequences of the categorical equalities of Figure 3. This seems to be related to the interesting

f[let u be ∗ in e/y] = let u be ∗ in f[e/y]
f[let u be x⊗y in g/w] = let u be x⊗y in f[g/w]

Figure 4: Naturality Equations

computational issues which arise if we regard the categorical equations as reduction (or computation) rules from left to right. We then do not have a confluent system, and application of a Knuth-Bendix algorithm leads to further reductions: ‘pushing-in’ rules like

2The reader is warned that this observation should be repeated (mutatis mutandis) for all the systems that we consider in this paper.

(let w be x ⊗ y in t) ⊗ w′ > let w be x ⊗ y in (t ⊗ w′)
w′ ⊗ (let w be x ⊗ y in t) > let w be x ⊗ y in (w′ ⊗ t)

and a rule (corresponding to associativity of composition) like:

let (let t be x ⊗ y in v) be x′ ⊗ y′ in u > let t be x ⊗ y in (let v be x′ ⊗ y′ in u)

all of which correspond to instances of the naturality equations. We believe that we do obtain a rewriting system with the Church-Rosser property, but have not written out all of the details.

3 Weakly Distributive Logic

As soon as we try to incorporate the multiplicative disjunction par into our logic we are forced to consider traditional sequents with many “hypotheses” and many “conclusions”. Our main innovation is to introduce a term assignment system and a term calculus in such circumstances. In an attempt to make the idea clear we first consider an eccentric system, that of the connective par alone.

3.1 The Par Logic

Since the multiplicative disjunction par is the least understood of the Linear Logic connectives we first present the logical system of par logic. We write par - Girard’s upside down ampersand - as a □ not only for typographical reasons, but also because it has different properties from Girard’s connective, for instance A□B in Full Intuitionistic Linear Logic is not the same as (A^{⊥} ⊗ B^{⊥})^{⊥}, as is the case in Classical Linear Logic. It is natural to formalize the par fragment of linear logic in an eccentric sequent calculus in which on the left-hand side of the turnstile we have exactly one formula, while on the right-hand side we have a sequence, Δ, of formulae. In other words we adopt a restriction dual to the one in Minimal Logic [21]. The sequent calculus rules for par logic are displayed in Figure 5. Note that this system is an exact dual of the system of tensor logic (tensor-implication logic without the rules for implication). In particular the Cut rule is certainly an eliminable rule of the system.

Now we describe a term assignment system for par logic. The duality that we have just drawn attention to breaks down completely: we hold on to a traditional interpretation of ‘proofs as functions’ by declaring a variable in the single hypothesis on the left of the turnstile, and presenting terms in each of the many conclusions on the right of the turnstile. (It may help the reader to think very roughly of the terms as denoting partial functions working in parallel, one of which should deliver a value.)

If X is a finite set of variables, we define P_{X} the set of patterns with set of variables X by:

x□− ∈ P_{{x}} − □y ∈ P_{{y}}

Now we define T_{X} the linear terms with set of free variables X, inductively as follows:

\begin{aligned}& Identity \\ A ⊢ A \end{aligned}

A ⊢ Δ, B, C, Δ′

\overline{Exchange}

A ⊢ Δ, C, B, Δ′

A ⊢ Δ, B, Δ′ B ⊢ Γ

Cut

A ⊢ Δ, Γ, Δ′

\begin{aligned}& (⊥_{L}) \\ ⊥ ⊢ \end{aligned}  A ⊢ Δ ; (⊥_{R}) ; A ⊢ Δ, ⊥

A ⊢ Δ  B ⊢ Δ′ ; (□_{L}) ; A□B ⊢ Δ, Δ′ A ⊢ Δ, B, C, Δ′ ; (□_{R}) ; A ⊢ Δ, B□C, Δ′

Figure 5: Par Logic

• x ∈ T_{{x}};

• ∘ ∈ T_{∅};

• t ∈ T_{X}, u ∈ T_{Y} implies t□u ∈ T_{X∪Y};

• t ∈ T_{X}, p ∈ P_{Y} , u ∈ T_{Y ∪Z}, X ∩ Z = ∅, Y ∩ Z = ∅ implies (let t be p in u) ∈ T_{X∪Z}.

(This definition is slightly more general than necessary for this section.)

We present the term assignment system for par logic in Figure 6.

To emphasise the fact that we are dealing with multiple conclusions we write the comma on the right-hand side of the turnstile as a vertical bar, a familiar notation in Computer Science for some kind of parallel process. A notational convenience is to write the sequence of formulae Γ as {C_{i}}_{i∈I} and Δ as {D_{i}}_{i∈I}. Also we would ideally write a sequent in the par term assignment system as

x : A ⊢ … | d_{i} : D_{i} | …

but to save space we omit the ‘dots’ (and bars) on either side of the formulae containing indices; the reader should take these as indicating sequences of term assignments (separated by our vertical line). The new term constructor (let t be p in e) also binds variables like the let for tensor, but they should not be confused.

Though this system is in no immediate sense dual to the term assignment system for tensor logic, there is a kind of translation which we do not have space to describe here, but whose nature should be clear from the categorical semantics. Categorically the system consisting only of the structural rules (Identity, Exchange and Cut) corresponds to the dual of a (symmetric) multicategory. (It does not seem worth coining a name for this notion. Recall that unlike the notion of a category, the notion of a multicategory is not self-dual.) Hence as before we expect the full system with the logical rules for par to correspond to the dual of a (symmetric) tensor multicategory. Again if we suppress the multicategorical aspects we deal simply with a symmetric monoidal category. x : A ⊢ Δ | t : B | Δ′ y : B ⊢ f_{i} : C_{i}

Cut

x : A ⊢ Δ | f_{i}[t/y] : C_{i} | Δ′
\begin{aligned}& (⊥_{L}) \\ x : ⊥ ⊢ \end{aligned} x : A ⊢ Δ ; (⊥_{R}) ; x : A ⊢ ∘ : ⊥ | Δ
x : A ⊢ d_{i} : C_{i} y : B ⊢ f_{j} : D_{j}

(□_{L})

z : A□B ⊢ let z be x□ − in d_{i} : C_{i} | let z be − □y in f_{j} : D_{j}

x : A ⊢ Δ | e : A | f : B
(□_{R})
x : A ⊢ Δ | e□f : A□B

Figure 6: Term Assignment System for Par Logic

As for tensor-implication logic we need some equations to make the tie up between the syntactic calculus and the expected semantics. The categorical equations are given in Figure 7. Note that in this system there is no ‘β-rule’ for the conective ⊥. The first equation is the ‘η-rule’ for ⊥, the next two constitute the ‘β-rule’ for □ abd the final equation the ‘η-rule’ for □. Figure 8 contains the two naturality equations associated with the connective par, which as in the case of ⊗ follow from the categorical equations of Figure 7.

u = ∘
let u□v be x□ − in t = t[u/x]
let u□v be − □y in t = t[v/y]

(let u be x□ − in x)□(let u be − □y in y) = u

Figure 7: (Par) categorical equations

let t be x□ − in f[u/x] = f[let t be x□ − in u/x]

let t be − □y in f[v/y] = f[let t be − □y in v/y]

Figure 8: (Par) naturality equations

Since we do not intend that par logic should be taken too seriously on its own it does not seem worth stating formally the soundness and completeness theorem nor the decorated cut-elimination theorem for it. As for the term calculus for tensor-implication logic, interesting questions arise when we read our equations as rewrite rules, but we shall not consider these here.

3.2 The tensor-par fragment of Linear Logic

Suppose that we now consider a system of logic for tensor and par. We have to use traditional two-sided sequents, but since there is little difficulty in giving the logic in this form, we shall proceed to the term assignment system. We take patterns and terms given by the clauses of previous sections (except that the connective linear implication is not dealt with) and we present the term assignment system for this fragment of Linear Logic, called tensor-par logic, in Figure 9.

\begin{aligned}& Identity \\ x : A ⊢ x : A \end{aligned}

Γ ⊢ Δ | t : A | Δ′ y : A, Γ′ ⊢ f_{i} : B_{i}

Cut

Γ, Γ′ ⊢ Δ | f_{i}[t/y] : B_{i} | Δ′

Γ, x : A, y : B, Γ′ ⊢ Δ ; Exchange_{L} ; Γ, y : B, x : A, Γ′ ⊢ Δ  Γ ⊢ Δ | f : A | g : B | Δ′ ; Exchange_{R} ; Γ ⊢ Δ | g : B | f : A | Δ
Γ ⊢ e_{i} : A_{i}

(I_{L})

Γ, x : I ⊢ let x be ∗ in e_{i} : A_{i}

\begin{aligned}& (I_{R}) \\ ⊢ ∗ : I \end{aligned}

Γ, x : A, y : B ⊢ f_{i} : C_{i}
(⊗_{L})
Γ, z : A⊗B ⊢ let z be x⊗y in f_{i} : C_{i}

Γ ⊢ e : A | Δ Γ′ ⊢ f : B | Δ′

(⊗_{R})

Γ, Γ′ ⊢ e⊗f : A⊗B | Δ | Δ′

\begin{aligned}& (⊥_{L}) \\ x : ⊥ ⊢ \end{aligned}  Γ ⊢ Δ ; (⊥_{R}) ; Γ ⊢ ∘ : ⊥ | Δ

Γ, x : A ⊢ d_{i} : C_{i} Γ′, y : B ⊢ f_{j} : D_{j}
(□_{L})

Γ, Γ′, z : A□B ⊢ let z be x□ − in d_{i} : C_{i} | let z be − □y in f_{j} : D_{j}

Γ ⊢ e : A | f : B | Δ
(□_{R})
Γ ⊢ e□f : A□B | Δ

Figure 9: Term Assignment System for Tensor-Par Logic

The question of a categorical model provides us with more of a problem. First we have to understand what is needed to model the structural rules. Essentially this induces the notion of a polycategory, introduced many years ago by Szabo [24]. Now the term assignment suggests that we must have representing objects for operations on multimaps and comultimaps as forced by the categorical equations. But there is a bit more to it than that, as we always have two-sided sequents. Recall that in Intuitionistic Logic one has conjunction ∧ and disjunction ∨ and the rules of the logic are reflected exactly in the structure of a distributive lattice (or category). In Linear Logic we keep a vestige of that distributivity, a weak form of distributivity between tensor and par given by natural maps

w: A ⊗ (B□C) → (A ⊗ B)□C
w′: (A□B) ⊗ C → A□(B ⊗ C)

satisfying appropriate coherence conditions. (As we assume symmetry we do not really need the dual w′.) Hence the categorical model for the tensor-par calculus is a (symmetric) weakly distributive (bi)tensor polycategory. As before we can suppress completely the polycategorical structure and deal with (symmetric) weakly distributive categories.

Putting together the categorical equations for tensor and par we obtain Figure 10. As before the equality generated by these rules gives us a term calculus. We can inductively define an interpretation of types and terms of the term assignment system as objects and maps of the (symmetric) weakly distributive category. A sequent

\overline{x} : Γ → f_{i} : Δ

is interpreted as a (poly)map

C_{1}⊗ … ⊗C_{n} → D_{1}□ … □D_{m}

And we can state the result.

let ∗ be ∗ in e  = e
let u be ∗ in f[∗/z]  = f[u/z]
let e⊗t be x⊗y in u  = u[e/x, t/y]
let u be x⊗y in f[x⊗y/z]  = f[u/z]
let u□v be x□ − in t  = t[u/x]
let u□v be − □y in t  = t[v/y]
(let u be x□ − in x)□(let u be − □y in y) = u

Figure 10: (Tensor-Par) categorical equations

Theorem 3 The (typed versions of the) equalities of Figure 10 are sound and complete for interpretations in (symmetric) weakly distributive categories.

Again if we consider what becomes of the process of cut elimination for the the tensorpar term assignment system we get the following result.

Theorem 4 If the sequent Γ ⊢ t_{i}: D_{i} is derivable then for some terms \overline{t_{i}}, \overline{t_{i}} = t_{i} in the term calculus and the sequent Γ ⊢ \overline{t_{i}}: D_{i} is derivable without the Cut rule.

The proof is again routine, simply follow the steps of the standard process of cut elimination carrying the terms.

We note that the logical system of tensor-par logic has been independently considered in Cockett and Seely ([5]); indeed they coined the term weakly distributive category. They take a more general view of the categorical semantics (in that they do not presupose symmetry), and they present (in their setting) the coherence conditions.

4 The multiplicative fragment of Full Intuitionistic Linear Logic

First we give a brief account of the problem, a solution to which is sketched in this section. Suppose that we take a system of logic incorporating tensor, linear implication and par. We would have to use traditional sequents to handle par, and the non-obvious feature is the treatment of the rules for linear implication. A natural guess, based on experience with Intuitionistic Logic (see, for example, Takeuti [25]) is that we need simply restrict the rule (−∘_{R}) to the case where there is just one formula to the right of the turnstile. This is the choice made in de Paiva [6] and it seems a good one at least in as much as it is justified by the models. The proposed system is sound for the models while an unrestricted system (in which for example (A□B −∘ A)□B is valid) is not sound.

However, again as suggested by experience with Intuitionistic Logic, there are considerable problems with a system of this kind. It appears to lack some computational significance in that the natural process of cut elimination breaks down. Of course the cut rule may still be redundant as in the case of the multiple conclusion formulation of Intuitionistic Logic (we have not got round to checking this). But that always seems something of a cheat. Even more tellingly, there is a definite negative result to contend with. For Schellinx has shown [22] that in a system including the additives, there are valid sequents for which there is no cut-free proof. There the cut elimination theorem fails.

We solve these problems (here) by concentrating on an appropriate term assignment system.

4.1 Term Assignment for multiplicative Full Intuitionistic Linear Logic

We take the collection of patterns and terms generated by the clauses from previous sections. Then our proposed term assignment system for the multiplicative fragment of Full Intuitionistic Linear Logic is presented in Figure 11.

The crucial rule is linear implication on the right (−∘_{r}) where the side condition is motivated by the categorical semantics, which we now describe.

Suppose that we have a full multiplicative category, that is a symmetric monoidal closed category which is weakly distributive. We first need a definition.

Definition 1 Suppose that we have a map of the form

f: A⊗B → C□D

in a weakly distributive category C. We say that C is independent of B (for f) iff there exists an object E of C and maps g: A → C□E and h: E⊗B → D such that the composite

A⊗B −g⊗1 ; \begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ (C□E)⊗B −w ; \begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ C□(E⊗B) −1□h ; \begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ C□D

is equal to f: A⊗B → C□D

\begin{aligned}& Identity \\ x : A ⊢ x : A \end{aligned}

Γ ⊢ t : A | Δ y : A, Γ′ ⊢ f_{i} : B_{i}

Cut
Γ, Γ′ ⊢ Δ | f_{i}[t/y] : B_{i}
Γ, x : A, y : B, Γ′ ⊢ Δ ; Exchange_{L} ; Γ, y : B, x : A, Γ′ ⊢ Δ Γ ⊢ Δ | f : A | g : B | Δ′ ; Exchange_{R} ; Γ ⊢ Δ | g : B | f : A | Δ′

Γ ⊢ e_{i} : A_{i}

(I_{L})

Γ, x : I ⊢ let x be ∗ in e_{i} : A_{i}

\begin{aligned}& (I_{R}) \\ ⊢ ∗ : I \end{aligned}

Γ, x : A, y : B ⊢ f_{i} : C_{i}

(⊗_{L})

Γ, z : A⊗B ⊢ let z be x⊗y in f_{i} : C_{i}

Γ ⊢ e : A | Δ Γ′ ⊢ f : B | Δ′
(⊗_{R})
Γ, Γ′ ⊢ e⊗f : A⊗B |Δ | Δ′
\begin{aligned}& (⊥_{L}) \\ x : ⊥ ⊢ \end{aligned} Γ ⊢ Δ ; (⊥_{R}) ; Γ ⊢ ∘ : ⊥ | Δ

Γ, x : A ⊢ d_{i} : C_{i} Γ′, y : B ⊢ f_{j} : D_{j}

(□_{L})

Γ, Γ′, z : A□B ⊢ let z be x□ − in d_{i} : C_{i} | let z be − □y in f_{j} : D_{j}

Γ ⊢ Δ | e : A | f : B | Δ′

(□_{R})
Γ ⊢ Δ | e□f : A□B | Δ′

Γ ⊢ e : A | Δ Δ′, x : B ⊢ f_{i} : C_{i}

(−∘_{L})

Γ, g : A−∘B, Δ ⊢ f_{i}[(ge)/x] : C_{i} | Δ

Γ, x : A ⊢ e : B | Δ

if x ∉ Δ(−∘_{R})

Γ ⊢ λx.e : A−∘B | Δ

Figure 11: Term Assignment System for Full Intuitionistic Linear Logic

Then we need a couple of lemmas.

Lemma 1 Suppose we have a map f: A⊗B → C□D in a full multiplicative category C. If C is independent of B for f then there exists an \overline{f}: A → C□(B−∘D).

Thus in the case that C is closed we have a preferred object B−∘D in C which is an instance of the object E referred to in the definition above. Now we show that the operation

f ↦ \overline{f}

preserves other independences.

Lemma 2 Suppose we have a map f: A⊗B⊗C → D□E□F in a full multiplicative category C. Suppose also that D□E is independent of C for f so that we have a map

A⊗B −\begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ D□E□(C−∘F)

Then:

• If F is independent of B for f then C−∘F is independent of B for \overline{f}.

• If E is independent of B for f then E is independent of B for \overline{f}.

We use these two lemmas in the course of the inductive definition of the interpretation of a sequent Γ ⊢ t_{i} : D_{i} in Full Intuitionistic Linear Logic as a map

C_{1}⊗C_{2}⊗ … ⊗C_{n} −\begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ D_{1}□D_{2}□ … □D_{m}

in a full multiplicative category. In addition we need a lemma relating the categorical structure with the syntactic condition on the (⊗_{R}) rule. Suppose in a sequent like the above we want to abstract the variable x_{i} in the term t_{j} that is we want to form λx_{i}.t_{j}. We can show inductively that:

Lemma 3 If the variable x_{i} : C_{i} does not appear in {□D_{k}|k ≠ j} then {□D_{k}|k ≠ j} is independent of C_{i} in the interpretation

C_{1}⊗C_{2}⊗ … ⊗C_{n} −\begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ D_{1}□D_{2}□ … □D_{m}

This lemma justifies the restriction on the (⊗_{R}) rule. Note that no new equations are introduced by this restriction. Hence we can state:

Theorem 5 The equalities of Figure 3 and Figure 7 are sound and complete for interpretations in full multiplicative categories.

4.2 Cut Elimination

Our main result is that the cut elimination theorem holds for the term assignment system we have presented for (the multiplicative fragment of) Full Intuitionistic Linear Logic.

Theorem 6 If the sequent Γ ⊢ t_{i}: D_{i} is derivable in the multiplicative fragment of Full Intuitionistic Linear Logic then for some \overline{t_{i}}, \overline{t_{i}} = t_{i} in the term calculus and the sequent Γ ⊢ \overline{t_{i}}: D_{i} is derivable without the rule Cut.

Proof. We give an outline of a typical step in the cut elimination procedure in the troublesome case. Suppose that we have a derivation of the following form:

Γ ⊢ A, B  Δ, B, C ⊢ D ; (−∘_{R}) ; Δ, B ⊢ C−∘D
\overline{Cut}
Γ, Δ ⊢ A, C−∘D

We can easily arrange things so that in the cut elimination procedure we transform this to

Γ ⊢ A, B Δ, B, C ⊢ D
\overline{Cut}
Γ, Δ, C ⊢ A, D
(−∘_{R})
Γ, Δ ⊢ A, C−∘D

But the latter is not a valid derivation in the system of de Paiva [7] as the use of the rule (−∘_{R}) is only permitted when there is just one formula on the right hand side of the sequent. However, if we add terms we get

\overline{x} : Γ ⊢ r : A, s : B  \overline{z} : Δ, y : B, w : C ⊢ t : D ; (−∘_{R}) ; \overline{z} : Δ, y : B ⊢ λw.t : C−∘D
\overline{Cut}
\overline{x} : Γ, \overline{z} : Δ ⊢ r : A | λw.t : C−∘D

and we may transform this into

\overline{x} : Γ ⊢ r : A | s : B \overline{z} : Δ, y : B, w : C ⊢ t : D
\overline{Cut}
\overline{x} : Γ, \overline{z} : Δ, w : C ⊢ r : A | t : D
(−∘_{R})
\overline{x} : Γ, \overline{z} : Δ ⊢ r : A | t : C−∘D

which is valid in our system as w does not appear (free) in r.

The cut elimination process can now be pushed through in a standard way. □

We do not know whether the cut elimination theorem holds in the weak sense for the multiplicative fragment in the formulation of de Paiva [7]; that is it may be that every derivable sequent has a cut-free derivation even though the cut elimination process is blocked (after all this is what happens in the usual formulation of multiple-succedent Intuitionistic Logic). However Schellinx [22] shows that even this does not hold once one includes the additive constant 0.

5 Conclusions

We would not wish to overplay the conclusions to be drawn from the work presented here. However one phenomenon seems worth drawing attention to. A number of proof theorists have been drawn to decorate sequents with additional information in order to enable them to give a satisfactory presentation of a logic. Simple examples of such use include Zucker [26] and Pottinger [20]. More extensive examples are Gabbay [11] and recently Parigot [19]. Our use of terms can be seen in this light. Our term assignment system essentially does nothing more than provide additional information by keeping track of those formulae to the right of the turnstile which are in some sense independent of a given formula to the left. What we would like to stress is the novel (and, if so wished, hidden) use of categorical logic here; the additional information is derived from (the syntax for) a categorical semantics.

We note that there is a presentation of Intuitionistic Logic with two-sided sequents analogous to our system for Full Intuitionistic Linear Logic. For this system, the natural cut elimination procedure goes through (for more details see [8]). The resulting term calculus may of interest to some as it provides a unified syntax for cartesian closed and distributive categories, both of which have been used as the basis for approaches to functional programming.

It still remains to give a satisfactory intuitive account of the computational meaning of the term calculus for Full Intuitionistic Linear Logic. With other colleagues we have been trying to give an interpretation in terms of processes, but we rather hope that a number of different interpretations will emerge. We should like to end by recording our belief in the significance of Full Intuitionistic Linear Logic. It seems to provide a context for considering different interpretations of functional programming, and as such to deserve further attention.

Acknowledgements

We would like to thank the members of the CLICS group at the Computer Laboratory, University of Cambridge and, in particular, Gavin Bierman, for many useful discussions on the topic of this paper.

References

[1] Samson Abramsky. Computational interpretations of linear logic. Technical Report 90/20, Department of Computing, Imperial College, London, October 1990.

[2] M. Barr. *-Autonomous Categories, volume 752 of Lecture Notes in Mathematics. Springer-Verlag, 1979.

[3] Nick Benton, Gavin Bierman, Valeria de Paiva, and Martin Hyland. Term assignment for intuitionistic linear logic. Technical Report 262, University of Cambridge Computer Laboratory, August 1992.

[4] A. Blass. A game semantics for linear logic. Annals of Pure and Applied Logic, 56:183–220, 1992.

[5] Robin Cockett and Robert Seely. Weakly distributive categories. In Applications of Categories in Computer Science - Proc. of the LMS Symposium, Durham 1991, pages 45–66, 1992.

[6] Valeria de Paiva. The dialectica categories. In Conference on Categories in Computer Science and Logic, volume 92 of AMS Contemporary Mathematics, pages 47–62, June 1989.

[7] Valeria de Paiva. A dialectica-like model of linear logic. In Category Theory in Computer Science, volume 389 of Lecture Notes in Computer Science, pages 341–356, September 1989.

[8] Valeria de Paiva and Luiz Carlos Pereira. A new proof system for intuitionistic logic. Abstract accepted for the Logic Colloquium’93, Keele, England, April 1993.

[9] Valeria C.V. de Paiva. The Dialectica Categories. PhD thesis, Department of Pure Mathematics and Mathematical Statistics, University of Cambridge, 1988. Published as Computer Laboratory Technical Report 213, 1990.

[10] S. Eilenberg and G. M. Kelly. Closed categories. In Proceedings of Conference on Categorical Algebra, La Jolla, 1966.

[11] Dov M. Gabbay. Labelled deductive systems, part 1. Technical Report 90-22, CIS– Munchen, 1991.

[12] Jean-Yves Girard. The system F of variable types fifteen years later. Theoretical Computer Science, 45:159–192, 1986.

[13] Jean-Yves Girard and Yves Lafont. Linear logic and lazy computation. In Proceedings of TAPSOFT’87, vol. 2, volume 250 of Lecture Notes in Computer Science, pages 52– 66, 1987.

[14] Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic (a modular approach to polynomial time computability). In Mathematical Sciences Institute Workshop on Feasible Mathematics, pages 195–209, June 1989.

[15] Kurt Gödel. Collected Works. Oxford University Press, 1990. Edited by S. Feferman.

[16] Martin Hyland and Valeria de Paiva. Lineales. Talk given at the Montreal International Category Theory Meeting, 1991.

[17] Yves Lafont. Logiques, Catégories et Machines. PhD thesis, Université de Paris 7, 1988.

[18] J. Lambek. Multicategories revisited. In Categories in Computer Science and Logic, volume 92 of AMS Contemporary Mathematics, pages 217–239, June 1989.

[19] M. Parigot. λμ-calculus: an algorithmic interpretation of classical natural deduction. Draft, 1992.

[20] Garrel Pottinger. Normalization as a homomorphic image of cut-elimination. Annals of Mathematical Logic, 12:323–357, 1977.

[21] Dag Prawitz. Natural Deduction, volume 3 of Stockholm Studies in Philosophy. Almqvist and Wiksell, 1965.

[22] H. Schellinx. Some syntactical observations on linear logic. Journal of Logic and Computation, 1(4):537–559, 1991.

[23] R.A.G. Seely. Linear logic, *-autonomous categories and cofree algebras. In Conference on Categories in Computer Science and Logic, volume 92 of AMS Contemporary Mathematics, pages 371–382, June 1989.

[24] M. E. Szabo. Polycategories. Communications in Algebra, 3:663–689, 1975.

[25] G. Takeuti, editor. Proof Theory, volume 81 of Studies in logic and the foundations of mathematics. North-Holland, Amsterdam, 1975.

[26] J. Zucker. The correspondence between cut-elimination and normalization. Annals of Mathematical Logic, 7(1):1–112, 1974.