A syntax for linear logic^{⋆}

              Philip Wadler (wadler@dcs.glasgow.ac.uk)

Department of Computing Science, University of Glasgow, G12 8QQ, Scotland

Abstract. There is a standard syntax for Girard’s linear logic, due to Abramsky, and a standard semantics, due to Seely. Alas, the former is incoherent with the latter: different derivations of the same syntax may be assigned different semantics. This paper reviews the standard syntax and semantics, and discusses the problem that arises and a standard approach to its solution. A new solution is proposed, based on ideas taken from Girard’s Logic of Unity. The new syntax is based on pattern matching, allowing for concise expression of programs.

1 Introduction

Somewhere inside linear logic, there is a programming language struggling to get out. We wish to define an analogue of lambda calculus to solve the following equation:

\frac{lambda calculus}{intuitionistic logic} = \frac{?}{linear logic}

What does this language look like?

One would think the answer should be straightforward by now. There is the linear logic of Girard [Gir87], there is the syntax of Abramsky [Abr90], and there is the semantics of Seely [See89]. Each of these has become a standard.

Abramsky was inspired by the earlier work of Lafont [Laf88] and Holmström [Hol88], and in turn inspired related systems by Chirimar, Gunter, and Riecke [CGR92], Lincoln and Mitchell [LM92], Mackie [Mac91], Troelstra [Tro92], and Wadler [Wad90, Wad91].

Seely provided a categorical model, that subsumes other models such as coherence spaces [Gir87], event spaces [Pra91], games [LS91], and the Geometry of Interaction [AJ92].

Unfortunately, Abramsky’s syntax is incoherent with Seely’s semantics: different derivations of the same term may yield different semantics. The basic problem is that Promotion does not commute with substitution. All of the above syntaxes suffer from a similar problem in one form or another, meaning that it is difficult to assign them a meaning in any of the above models. (While the above rightly credits Abramsky’s influence, it would be wrong to burden him with too much blame. His syntax is coherent with the operational model he uses.)

⋆ In Brookes et al. editors, Mathematical Foundations of Programming Semantics, New Orleans, April 1993, Springer Verlag LNCS 802.

This difficulty was spotted previously by myself [Wad92]. Other researchers have not only observed the problem, but also proposed a solution in the form of a syntax that ‘boxes’ the Promotion rule, in much the same way that boxes are used in proof nets. Notable in this regard is the work of Benton, Bierman, de Paiva, and Hyland [BBdPH92], which provides a thorough introduction to natural deduction and sequent versions of linear logic, their categorical semantics, and the associated proof theory.

This paper presents a new syntax for linear logic that resolves the Promotion problem. The new syntax follows naturally from the idea of using patterns in sequents to represent destructors. It is closely related to Girard’s Logic of Unity, LU (though without the polarities) [Gir91]. Indeed, the syntax presented here is based on a suggestion from Jean-Yves Girard, who pointed out to me that the problems I had noted with the standard syntax are resolved in the syntax of LU. The syntax also bears a passing resemblance to Moggi’s calculus for monads [Mog89].

The syntax has been expressed in a way such that Dereliction and Promotion are made explicit, but Contraction and Weakening are left implicit. Even though linear logic is a ‘resource conscious’ logic, it seems adequate to be conscious of Dereliction and Promotion alone. The semantics introduces sufficient coherence properties so that the precise order in which Contraction and Weakening is applied is irrelevant. Such details may safely be omitted from the programme, yielding a more economic mode of expression. For those who truly desire to control all the details, a variant syntax that makes Contraction and Weakening explicit is given at the end.

Another approach to giving a syntax for linear logic based on LU appears in more recent work [Wad93]. That paper presents a more tutorial introduction: it is based on natural deduction rather than sequent calculus, so it takes less advantage of pattern matching, and it stresses the syntactic aspects of proof reduction while ignoring the semantics.

The remainder of this paper is organised as follows. Section 2 presents Abramsky’s syntax. Section 3 presents Seely’s semantics. Section 4 presents the new syntax. Section 5 compares the new syntax with Girard’s Logic of Unity. Section 6 sketches some variations on the new syntax.

2 Old syntax

For simplicity, we restrict ourself to the connectives ⊗ (tensor product), {− \atop ∘} (linear implication), & (product), and ! (of course). A type (or proposition) is built from these connectives and base types.

A, B, C ::= X | (A ⊗ B) | (A {− \atop ∘} B) | (A & B) | !A

Let A, B, C range over types, and X range over base types.

For each of these types, there are terms to construct and destruct values of that type.

t, u ::= x | (t, u) | (let (x, y) = t in u) | (λx. t) | (t u) |

⟨t, u⟩ | (let ⟨x, ⟩ = t in u) | (let ⟨ , y⟩ = t in u) |

!t | (let !x = t in u) | (let (x@y) = t in u) | (let = t in u)

Let t, u range over terms, and f , x, y, z range over variables. The use here of ‘let (x, y) = t in u’ in comparison with Abramsky’s ‘let t be x ⊗ y in u’ merely reflects a preference for the traditional notation, not any significant difference.

An assumption has the form x_{1} : A_{1} , …, x_{n} : A_{n} where all the variables are distinct, and n ≥ 0 . Let Γ and Δ range over assumptions. Write Γ, Δ for the catenation of two assumptions; whenever this appears it is assumed that the variables of Γ and Δ are disjoint. Finally, a judgement has the form Γ ⊢ t : A.

The rules for this version of linear logic are shown in Figure 1. Each rule has zero or more hypotheses above the horizontal line, and a conclusion below. There is one rule for each term form, with the exception of the two rules Exchange and Cut. The Exchange rule expresses that the order of assumptions is irrelevant. The Cut rule uses the notation u[t/x] to stand for the term derived from u by substituting t for all occurrences of x.

The rules are given in sequent calculus style, so constructors are represented by rules (such as ⊗-R) where the connective appears in the consequent of the conclusion (to the right of ⊢), and destructors are represented by rules (such as ⊗-L) where the connective appears in the antaceedent of the conclusion (to the left of ⊢). Promotion constructs a term with ‘of course’ type: it is a !-R rule. Dereliction uses a variable with ‘of course’ type once, Contraction duplicates it, and Weakening discards it: we refer to these collectively as !-L rules.

The {− \atop ∘}-L rule only allows one to apply a variable to a term. Readers may be more familiar with the application rule of Natural Deduction, which allows one to apply a term to a term.

{− \atop ∘}-E \frac{Γ ⊢ t : (A {− \atop ∘} B)  Δ ⊢ u : A}{Γ, Δ ⊢ (t u) : B}

This rule is derived as follows.

Γ ⊢ t : (A {− \atop ∘} B)  Δ ⊢ u : A  \overline{Id} ; y : B ⊢ y : B \overline{{− \atop ∘}-L} Δ, f : (A {− \atop ∘} B) ⊢ (f u) : B

\overline{Cut}

Γ, Δ ⊢ (t u) : B

Note the central role played here by Cut. Sequent and natural deduction versions of linear calculus are presented and shown equivalent by Lincoln and Mitchell [LM92]. Various mixtures of the two systems have been used by various researchers [BBdPH92, CGR92, Wad90, Wad91].

Id \overline{x : A ⊢ x : A}  Exchange \frac{Γ, x : A, y : B, Δ ⊢ t : C}{Γ, y : B, x : A, Δ ⊢ t : C}

Cut \frac{Γ ⊢ t : A  x : A, Δ ⊢ u : B}{Γ, Δ ⊢ u[t/x] : B}

⊗-R \frac{Γ ⊢ t : A  Δ ⊢ u : B}{Γ, Δ ⊢ (t, u) : (A ⊗ B)}  ⊗-L \frac{Γ, x : A, y : B ⊢ t : C}{Γ, z : (A ⊗ B) ⊢ (let (x, y) = z in t) : C}

{− \atop ∘}-R \frac{Γ, x : A ⊢ t : B}{Γ ⊢ (λx. t) : (A {− \atop ∘} B)}  {− \atop ∘}-L \frac{Γ ⊢ t : A  y : B, Δ ⊢ u : C}{Γ, f : (A {− \atop ∘} B), Δ ⊢ u[(f t)/y] : C}

&-R \frac{Γ ⊢ t : A  Γ ⊢ u : B}{Γ ⊢ ⟨t, u⟩ : (A & B)}

&-L \frac{Γ, x : A ⊢ t : C}{Γ, z : (A & B) ⊢ (let ⟨x, ⟩ = z in t) : C}  \frac{Γ, y : B ⊢ t : C}{Γ, z : (A & B) ⊢ (let ⟨ , y⟩ = z in t) : C}

Promotion \frac{x_{1} : !A_{1} , …, x_{n} : !A_{n} ⊢ t : B}{x_{1} : !A_{1} , …, x_{n} : !A_{n} ⊢ !t : !B}  Dereliction \frac{Γ, x : A ⊢ t : B}{Γ, z : !A ⊢ (let !x = z in t) : B}

Contraction \frac{Γ, x : !A, y : !A ⊢ t : B}{Γ, z : !A ⊢ (let (x@y) = z in t) : B}  Weakening \frac{Γ ⊢ t : B}{Γ, z : !A ⊢ (let = z in t) : B}

Fig. 1. Old syntax

Here are a few example judgements.

⊢ (λx. λy. let = y in x) : A {− \atop ∘}!B {− \atop ∘} A ⊢ (λr. λs. λx. let !f = r in let !g = s in let (y@z) = x in f y !(g z)) :

!(!A {− \atop ∘}!B {− \atop ∘} C ) {− \atop ∘}!(!A {− \atop ∘} B) {− \atop ∘}!A {− \atop ∘} C

⊢ (λx. let (y, z) = x in

!⟨let !r = y in let = z in r, let !s = z in let = x in s⟩) :

(!A ⊗!B) {− \atop ∘}!(A & B)

Because of the Cut rule, an unnerving property of this system is that terms do not uniquely encode derivations. For example, the judgement

z : !!A ⊢ !(let !x = z in x) : !!A

has the derivation

(∗)  \overline{Id} ; x : !A ⊢ x : !A \overline{Dereliction} z : !!A ⊢ (let !x = z in x) : !A \overline{Promotion} z : !!A ⊢ !(let !x = z in x) : !!A

and also the derivation

(∗∗) \overline{Id} ; x : !A ⊢ x : !A \overline{Dereliction} z : !!A ⊢ (let !x = z in x) : !A \overline{Id} ; y : !A ⊢ y : !A \overline{Promotion} y : !A ⊢ !y : !!A \overline{Cut} z : !!A ⊢ !(let !x = z in x) : !!A.

At first this may seem vaguely disturbing. We shall see shortly that it is profoundly disturbing, because each of these derivations is attached to a different semantics.

3 Semantics

This section presents Seely’s model of linear logic, restricted to the case of intuitionistic linear logic. Seely’s model is normally thought of as deriving from ∗-autonomous categories, but the dualising object ∗ is only required to model classical linear logic.

Anticipating that objects will model types and assumptions, and that arrows will model terms, let A, B, C and Γ, Δ range over objects, and t, u, v range over arrows.

A model of intuitionistic linear logic is provided by a category with the following structure.

– It is symmetric monoidal closed, with unit object 1 , tensor ⊗, and internal hom {− \atop ∘}. The transpose of t : Γ ⊗ A → B is curry(t) : Γ → (A {− \atop ∘} B), and the counit is apply : (A {− \atop ∘} B) ⊗ A → B.

– It possesses finite products, with terminal ⊤ and product &. The unique arrow to the terminal is ⟨ ⟩ : Γ → ⊤, the mediating morphism of t : Γ → A and u : Γ → B is ⟨t, u⟩ : Γ → A&B, and the projections are fst : A&B → A and snd : A & B → B.

– It possesses a comonad !. The Kleisli operator of t : !A → B is kleisli(t) : !A → !B, and the counit is counit : !A → A.

– There are isomorphisms 1 ≃ !⊤ and !A ⊗ !B ≃ !(A & B). These induce a comonoid structure on each object !A that is natural in A, given by

!A ⟶^{discard} 1 = !A ⟶^{!⟨ ⟩} !⊤ ≃ 1 ,
!A ⟶^{duplicate} !A ⊗!A = !A ⟶^{!⟨id,id⟩} !(A & A) ≃ !A ⊗!A.

A categorical model is obtained by associating with each base type an object in our category, inducing a map from types to objects. Write A for both a type and its corresponding object. Each assumption Γ = x_{1} : A_{1} , …, x_{n} : A_{n} possesses a corresponding object Γ = A_{1} ⊗ ⋯ ⊗ A_{n}; the empty assumption corresponds to the unit object 1 .

Each judgement Γ ⊢ t : A corresponds to an arrow t : Γ → A. Figure 2 shows how each derivation induces an arrow which is its semantics.

Since a given judgement may have more than one derivation, we must verify that all possible derivations of a judgement assign it the same semantics. This

Id \overline{A ⟶^{id} A}  Exchange \frac{Γ ⊗ A ⊗ B ⊗ Δ ⟶^{t} C}{Γ ⊗ B ⊗ A ⊗ Δ ≃ Γ ⊗ A ⊗ B ⊗ Δ ⟶^{t} C}

Cut \frac{Γ ⟶^{t} A  A ⊗ Δ ⟶^{u} B}{Γ ⊗ Δ ⟶^{t⊗id} A ⊗ Δ ⟶^{u} B}

⊗-R \frac{Γ ⟶^{t} A  Δ ⟶^{u} B}{Γ ⊗ Δ ⟶^{t⊗u} A ⊗ B}  ⊗-L \frac{Γ ⊗ A ⊗ B ⟶^{t} C}{Γ ⊗ (A ⊗ B) ≃ Γ ⊗ A ⊗ B ⟶^{t} C}

{− \atop ∘}-R \frac{Γ ⊗ A ⟶^{t} B}{Γ ⟶^{curry(t)} (A {− \atop ∘} B)}

{− \atop ∘}-L \frac{Γ ⟶^{t} A  B ⊗ Δ ⟶^{u} C}{Γ ⊗ (A {− \atop ∘} B) ⊗ Δ ⟶^{t⊗id⊗id} A ⊗ (A {− \atop ∘} B) ⊗ Δ ≃ (A {− \atop ∘} B) ⊗ A ⊗ Δ ⟶^{apply⊗id} B ⊗ Δ ⟶^{u} C}

&-R \frac{Γ ⟶^{t} A  Γ ⟶^{u} B}{Γ ⟶^{⟨t,u⟩} (A & B)}

&-L \frac{Γ ⊗ A ⟶^{t} C}{Γ ⊗ (A & B) ⟶^{id⊗fst} Γ ⊗ A ⟶^{t} C}  \frac{Γ ⊗ B ⟶^{t} C}{Γ ⊗ (A & B) ⟶^{id⊗snd} Γ ⊗ B ⟶^{t} C}

Promotion \frac{!A_{1} ⊗ ⋯ ⊗!A_{n} ≃ !(A_{1} & ⋯ & A_{n}) ⟶^{t} B}{!A_{1} ⊗ ⋯ ⊗!A_{n} ≃ !(A_{1} & ⋯ & A_{n}) ⟶^{kleisli(t)} !B}

Dereliction \frac{Γ ⊗ A ⟶^{t} B}{Γ ⊗!A ⟶^{id⊗counit} Γ ⊗ A ⟶^{t} B}

Contraction \frac{Γ ⊗!A ⊗!A ⟶^{t} B}{Γ ⊗!A ⟶^{id⊗duplicate} Γ ⊗ (!A ⊗!A) ≃ Γ ⊗!A ⊗!A ⟶^{t} B}

Weakening \frac{Γ ⟶^{t} B}{Γ ⊗!A ⟶^{id⊗discard} Γ ⊗ I ≃ Γ ⟶^{t} B}

Fig. 2. Semantics

property is called coherence, and its importance was noted by Breazu-Tannen, Coquand, Gunter and Scedrov [BCGS91]. In our case, two derivations of a judgement can differ only in their use of the Exchange or Cut rules, since uses of all other rules are encoded in the term. Coherence is guaranteed for Exchange by the fact that ⊗ is symmetric monoidal.

Unfortunately, the Cut rule does indeed introduce incoherence, when used in conjunction with Promotion. The derivation (∗) given previously induces the semantics

(∗)  \overline{Id} ; !A ⟶^{id} !A \overline{Dereliction} !!A ⟶^{counit} !A \overline{Promotion} !!A ⟶^{kleisli(counit)} !!A.

The derivation (∗∗) given previously induces the semantics

(∗∗)  \overline{Id} ; !A ⟶^{id} !A \overline{Dereliction} !!A ⟶^{counit} !A  \overline{Id} ; !A ⟶^{id} !A \overline{Promotion} !A ⟶^{kleisli(id)} !!A \overline{Cut} !!A ⟶^{counit} !A ⟶^{kleisli(id)} !!A.

These are not necessarily equal. The arrow for (∗) is necessarily the identity, but the arrow for (∗∗) is not. We thus have the following.

Counterexample. The syntax of Figure 1 is not coherent with the semantics of Figure 2.

This problem arises only with the Promotion rule.

Theorem. The syntax of Figure 1 is coherent with the semantics of Figure 2 if Promotion is not used. If a term does not contain ! as a constructor, then all derivations of it will have the same semantics, even if they use Cut.

The proof is by examination of overlapping rules.

All of the variations of Abramsky’s syntax cited above suffer from this problem in one form or another. In a natural deduction system, this problem reveals itself in a failure of the Substitution Lemma: substitution does not commute with Promotion [Wad92]. The same difficulty is at the root of problems that Lincoln and Mitchell [LM92] and Chirimar, Gunter, and Riecke [CGR92] encountered with Subject Reduction theorems, forcing them to be restricted in various ways.

One way to fix the problems is to restrict the class of categorical models. In an earlier paper [Wad92], it was shown that substitution commutes with Promotion if and only if the categorical model satisfies counit; kleisli(id) = id. This is not very satisfactory, as none of the models cited at the beginning of this paper satisfy this restriction. Nonetheless, similar restrictions appears in the work of O’Hearn [O’He91] and Filinski [Fil92], and this may explain why.

Another fix is to revise the syntax of Promotion, so that it records explicitly what substitutions have occured. This suggestion has been made by Benton, Bierman, de Paiva, and Hyland [BBdPH92] and by Reddy [Red91]. The syntax of promotion is changed so that the term !t is replaced by ![u_{1} /x_{1} , …, u_{n}/x_{n}]t, where x_{1} , …, x_{n} are all the free variables of t. Here the square brackets are concrete syntax; this concrete syntax is chosen to resemble the meta-syntax for substitution, since the roles are similar. The revised Promotion rule is as follows.

Promotion′ \frac{x_{1} : !A_{1} , …, x_{n} : !A_{n} ⊢ t : B}{z_{1} : !A_{1} , …, z_{n} : !A_{n} ⊢ ![z_{1} /x_{1} , …, z_{n}/x_{n}]t : B}

After promotion, the free variables of the term are z_{1} , …, z_{n}, and any substitutions for these variables will be explicit in the term. By acting as a barrier to substitution, the new syntax performs much the same role that boxing does in proof nets [Gir87]. It is possible to show that this ‘boxed’ syntax is coherent: all derivations of a term have the same semantics.

Returning to our example, the first derivation becomes

(∗)  \overline{Id} ; x : !A ⊢ x : !A \overline{Dereliction} y : !!A ⊢ (let !x = y in x) : !A \overline{Promotion′} z : !!A ⊢ ![z/y](let !x = y in x) : !!A

and the second becomes

(∗∗) \overline{Id} ; x : !A ⊢ x : !A \overline{Dereliction} z : !!A ⊢ (let !x = z in x) : !A \overline{Id} ; y : !A ⊢ y : !A \overline{Promotion′} w : !A ⊢ ![w/y]y : !!A \overline{Cut} z : !!A ⊢ ![(let !x = z in x)/y]y : !!A.

Now the terms are different, so it is not a problem that they are assigned different semantics.

The key idea here is that there is a barrier around Promotion indicating what substitutions occur. The next section will reveal a different syntax that erects a similar barrier.

4 New syntax

The new syntax makes three significant changes. First, it introduces a notion of pattern. Whereas previously assumptions paired variables with types, now they will pair patterns with types. Second, the various instances of ‘let’ that appeared previously, associated with the ⊗-L, &-L, and !-L rules, are now all consolidated into a single ‘let’. Third, there is no explicit indication of Contraction or Weakening in the terms. (This third change is convenient but not essential, and we will see how to undo it in the next section.)

For each type, there is now a term to construct values of that type, and a pattern to destruct values of that type. The exception is {− \atop ∘}, which has terms for both construction and destruction. There is also a ‘let’ term.

p, q ::= x | (p, q) | ⟨p, ⟩ | ⟨ , q⟩ | !x
t, u ::= x | (t, u) | (λp. t) | (t u) | ⟨t, u⟩ | !t | (let p = t in u)

Let p, q range over patterns, t, u range over terms, and f , x, y, z range over variables. Note that patterns for the types ⊗ and & may be nested, but patterns for the type ! may not. We will see below that this system guarantees coherent semantics, but that if nested ! patterns were allowed then coherence would again be lost.

An assumption now has the form p_{1} : A_{1} , …, p_{n} : A_{n} where n ≥ 0 and no variable appears more than once in all of the patterns combined. Again, let Γ, Δ range over assumptions, and judgements have the form Γ ⊢ t : A.

The rules for this version of linear logic are shown in Figure 3. With the exception of the new rule Let, there is a one-to-one correspondence between rules in the old syntax and rules in the new syntax. The ⊗-L, &-L, and !-L rules now all introduce patterns rather than ‘let’ terms. The introduction of ‘let’ terms has been factored out into a separate Let rule. The three !-L rules all introduce the same pattern, so there is no explicit indication of Contraction or Weakening. The appearance of ! patterns in Contraction helps to explain the restriction to variables, since this makes the substitution associated with Contraction easier to express. Promotion is changed so that in addition to requiring that all types in the assumption begin with a !, all patterns in the assumption must also do so.

This last change is the critical step – the ! patterns will act as a barrier to substitution, just as the ‘boxed’ syntax at the end of the last section did. What was written ![u_{1} /x_{1} , …, u_{n}/x_{n}]t in the boxed syntax is here written

let !y_{1} = u_{1} in ⋯ let !y_{n} = u_{n} in t[!y_{1} /x_{1} , …,!y_{n}/x_{n}].

Note that ![u_{i}/x_{i}]t is concrete syntax, whereas t[!y_{i}/x_{i}] is meta-syntax for substitution. Although here the new syntax appears less compact than the boxed syntax, in practice the new syntax will often be more compact because of pattern matching, and because Contraction and Weakening are not explicitly indicated.

The Let rule has no logical content, as erasing the terms from the hypothesis or the conclusion gives the same logical judgement, Γ, A ⊢ B. Indeed, the Let rule can be simply considered a convenient abbreviation, as it can be derived from the {− \atop ∘} rules and Cut.

Γ, p : A ⊢ u : B

\overline{{− \atop ∘}-R}

Γ ⊢ (λp. u) : (A {− \atop ∘} B)

\overline{Id} ; x : A ⊢ x : A  \overline{Id} ; y : B ⊢ y : B

\overline{{− \atop ∘}-L}

f : (A {− \atop ∘} B), x : A ⊢ (f x) : B

\overline{Cut}

Γ, x : A ⊢ ((λp. u) x) : B

Thus, we can take (let p = x in u) as an abbreviation for ((λp. u) x).

Id \overline{x : A ⊢ x : A}  Exchange \frac{Γ, p : A, q : B, Δ ⊢ t : C}{Γ, q : B, p : A, Δ ⊢ t : C}

Cut \frac{Γ ⊢ t : A  x : A, Δ ⊢ u : B}{Γ, Δ ⊢ u[t/x] : B}  Let \frac{Γ, p : A ⊢ u : B}{Γ, x : A ⊢ (let p = x in u) : B}

⊗-R \frac{Γ ⊢ t : A  Δ ⊢ u : B}{Γ, Δ ⊢ (t, u) : (A ⊗ B)}  ⊗-L \frac{Γ, p : A, q : B ⊢ t : C}{Γ, (p, q) : (A ⊗ B) ⊢ t : C}

{− \atop ∘}-R \frac{Γ, p : A ⊢ t : B}{Γ ⊢ (λp. t) : (A {− \atop ∘} B)}  {− \atop ∘}-L \frac{Γ ⊢ t : A  y : B, Δ ⊢ u : C}{Γ, f : (A {− \atop ∘} B), Δ ⊢ u[(f t)/y]) : C}

&-R \frac{Γ ⊢ t : A  Γ ⊢ u : B}{Γ ⊢ ⟨t, u⟩ : (A & B)}

&-L \frac{Γ, p : A ⊢ t : C}{Γ, ⟨p, ⟩ : (A & B) ⊢ t : C}  \frac{Γ, q : B ⊢ t : C}{Γ, ⟨ , q⟩ : (A & B) ⊢ t : C}

Promotion \frac{!x_{1} : !A_{1} , …, !x_{n} : !A_{n} ⊢ t : B}{!x_{1} : !A_{1} , …, !x_{n} : !A_{n} ⊢ !t : !B}  Dereliction \frac{Γ, z : A ⊢ t : B}{Γ, !z : !A ⊢ t : B}

Contraction \frac{Γ, !x : !A, !y : !A ⊢ t : B}{Γ, !z : !A ⊢ t[z/x, z/y] : B}  Weakening \frac{Γ ⊢ t : B}{Γ, !z : !A ⊢ t : B}

Fig. 3. New syntax

The rules in Figure 2 for assigning a semantics to the derivation of a term still apply. The Let rule assigns the judgement in the conclusion the same semantics as the judgement in the hypothesis.

Theorem. The syntax of Figure 3 is coherent with the semantics of Figure 2.

The proof is by examining the possible overlaps between rules.

Here are the example judgements of Section 2 revisited.

⊢ (λx. λ!y. x) : A {− \atop ∘}!B {− \atop ∘} A

⊢ (λ!f . λ!g. λ!x. f !x !(g !x)) : !(!A {− \atop ∘}!B {− \atop ∘} C ) {− \atop ∘}!(!A {− \atop ∘} B) {− \atop ∘}!A {− \atop ∘} C ⊢ (λ(!r,!s).!⟨r, s⟩) : (!A ⊗!B) {− \atop ∘}!(A & B)

The new syntax is considerably more compact.

Returning to our main example, the first derivation becomes

(∗)  \overline{Id} ; z : !A ⊢ z : !A \overline{Dereliction} !z : !!A ⊢ z : !A \overline{Promotion} !z : !!A ⊢ !z : !!A.

The second derivation is no longer valid. The Promotion rule no longer applies, because it contains patterns not in the proper form. In order to obtain the same semantics as previously, the derivation must be rewritten. The old use of the Id rule, which yielded x : !A ⊢ x : !A, is replaced with a use of Id, Dereliction, and Promotion, which yields !y : !A ⊢ !y : !A. Both derivations have the same semantics (the identity arrow), but further promotion is only possible for the latter.

(∗∗)  \overline{Id} ; z : !A ⊢ z : !A \overline{Dereliction} !z : !!A ⊢ z : !A  \overline{Id} ; x : A ⊢ x : A \overline{Dereliction} !x : !A ⊢ x : A \overline{Promotion} !x : !A ⊢ !x : !A \overline{Promotion} !x : !A ⊢ !!x : !!A \overline{Let} w : !A ⊢ let !x = w in !!x : !!A \overline{Cut} !z : !!A ⊢ (let !x = z in !!x) : !!A.

The new (∗) and (∗∗) have the same semantics as the old. As with the boxed semantics, we now have distinct terms yielding distinct semantics. Every old derivation carries into a new derivation with the same semantics; the only change needed may be to replace some uses of Id with Id, Dereliction, and Promotion, as above; and to add some uses of Let.

If nested ! patterns were allowed, the coherence property would again be lost. Consider the (illegal) judgement !!x : !!A ⊢ !x : !A. There are two different proof trees that yield this judgement. The first applies rules in the order Id, Derelict, Promote, Derelict and has semantics counit; kleisli(counit), which simplifies to counit. The second applies rules in the order Id, Derelict, Derelict, Promote and has semantics kleisli(counit; counit), which does not simplify to counit. Hence the restriction that ! patterns cannot be nested. There is no similar problem for ⊗ or & patterns.

Since there are no longer explicit terms for Contraction and Weakening, these must be checked for coherence. Coherence here is guaranteed by the fact that discard and duplicate form a comonoid: duplicating and then discarding is the same as the identity; two duplications in different orders have the same meaning, and so on. The situation is very similar to that for Exchange, and indeed there appears to be no more reason for textually indicating each use of Contraction or Weakening than there is for indicating each use of Exchange.

The new syntax satisfies a pleasing number of equivalences. In the case where the ‘let’ is simply binding a variable, it can be replaced by substitution. Further, whenever a constructor meets a corresponding destructor, it can be substituted out. Finally, ‘let’ satisfies a pair of familiar laws. All these points are summarised in the following.

Theorem. The following equations hold for the syntax of Figure 3 with the semantics of Figure 2.

(1 )  (let x = t in u) = u[t/x]
(2 )  (let (p, q) = (t, u) in v) = (let p = t in (let q = u in v))
(3 )  ((λp. u) t) = (let p = t in u)
(4 )  (let ⟨p, ⟩ = ⟨t, u⟩ in v) = (let p = t in v)
(5 )  (let ⟨ , q⟩ = ⟨t, u⟩ in v) = (let q = u in v)
(6 )  (let !x = !t in u) = u[t/x]
(7 )  (let p = t in p) = t
(8 ) (let q = (let p = t in u) in v) = (let p = t in (let q = u in v))

These laws assume no collision of bound variables; e.g., in law (2), the free variables of u must not be bound in p.

Law (1) is immediate from coherence. Laws (2)–(6) and (8) follow immediately from the categorical semantics. Law (7) is proved by induction on the pattern.

Here are equations (6)–(8) again, with the last two instantiated to the special case of ! patterns.

(let !x = !t in u) = u[t/x]
(let !x = t in !x) = t
(let !y = (let !x = t in u) in v) = (let !x = t in (let !y = u in v))

These are reminiscent of the three equations satisfied by Moggi’s calculus for monads [Mog89]. For our syntax the first equation depends on the right counit law for comonads and the second equation depends on the left counit law for comonads; while for Moggi’s calculus the first equation depends on the left unit law for monads, and the second equation depends on the right unit law for monads. However, the analogy goes awry with the third equation. Moggi’s last equation depends on the associative law for monads, while our last equation has nothing to do with the associative law for comonads. (However, the associative laws for comonads is important in verifying the coherence of the new syntax.)

5 Logic of Unity

The system described here is closely related to Girard’s Logic of Unity (LU) [Gir91]. Indeed, it was inspired by it: the trick that avoids coherence problems was stolen from LU. To clarify the relation, this section present an appropriately simplified version of LU. Major differences from Girard’s LU are that this version is restricted to the intuitionistic fragment, and there are no polarities.

In this variant of LU, there are two sorts of assumptions, linear and intuitionistic. Linear assumptions pair patterns with types, so they have the form p_{1} : A_{1} , … p_{n} : A_{n}, while intuitionistic assumptions pair variables with types, so they have the form x_{1} : A_{1} , … x_{n} : A_{n}. Linear assumptions may not be contracted or weakened, while intuitionistic assumptions may. The Contraction rule is much more neatly expressed in terms of variables because it involves substitution, which partly explains the restriction to variables in intuitionistic assumptions. Let Γ, Δ range over linear assumptions, and Φ, Ψ range over intuitionistic assumptions. A judgement has the form Γ; Φ ⊢ t : A, where the linear and intuitionistic assumptions are separated by a semicolon.

The rules for this variant of LU are shown in Figure 4. There is a close correspondence with our new syntax of Figure 3, here called LL for short. The previous Id rule is split into two rules, Id and Id-Int, the first dealing with a linear assumption and the second dealing with an intuitionistic one. Similarly, the previous Exchange rule is split into Exchange and Exchange-Int. The logical rules for ⊗ and {− \atop ∘} deal with linear assumptions. Promotion and Deriliction are logical rules of ! and deal with the relation between the two sorts of assumptions, while Contraction and Weakening have metamorphosed from logical rules of ! to structural rules dealing with intuitionistic assumptions.

Id \overline{x : A; ⊢ x : A}  Id-Int \overline{; x : A ⊢ x : A}

Exchange \frac{Γ, p : A, q : B, Δ; Φ ⊢ t : C}{Γ, q : B, p : A, Δ; Φ ⊢ t : C}  Exchange-Int \frac{Γ; Φ, x : A, y : B, Ψ ⊢ t : C}{Γ; Φ, y : B, x : A, Ψ ⊢ t : C}

Cut \frac{Γ; Φ ⊢ t : A  x : A, Δ; Ψ ⊢ u : B}{Γ, Δ; Φ, Ψ ⊢ u[t/x] : B}  Let \frac{Γ, p : A; Φ ⊢ u : B}{Γ, x : A; Φ ⊢ (let p = x in u) : B}

⊗-R \frac{Γ; Φ ⊢ t : A  Δ; Ψ ⊢ u : B}{Γ, Δ; Φ, Ψ ⊢ (t, u) : (A ⊗ B)}  ⊗-L \frac{Γ, p : A, q : B; Φ ⊢ t : C}{Γ, (p, q) : (A ⊗ B); Φ ⊢ t : C}

{− \atop ∘}-R \frac{Γ, p : A; Φ ⊢ t : B}{Γ; Φ ⊢ (λp. t) : (A {− \atop ∘} B)}  {− \atop ∘}-L \frac{Γ; Φ ⊢ t : A  y : B, Δ; Ψ ⊢ u : C}{Γ, f : (A {− \atop ∘} B), Δ; Φ, Ψ ⊢ u[(f t)/y]) : C}

&-R \frac{Γ; Φ ⊢ t : A  Γ; Φ ⊢ u : B}{Γ; Φ ⊢ ⟨t, u⟩ : (A & B)}

&-L \frac{Γ, p : A; Φ ⊢ t : C}{Γ, ⟨p, ⟩ : (A & B); Φ ⊢ t : C}  \frac{Γ, q : B; Φ ⊢ t : C}{Γ, ⟨ , q⟩ : (A & B); Φ ⊢ t : C}

Promotion \frac{; Φ ⊢ t : B}{; Φ ⊢ !t : !B}  Dereliction \frac{Γ, !z : !A; Φ ⊢ t : B}{Γ; z : A, Φ ⊢ t : B}

Contraction \frac{Γ; Φ, x : A, y : A ⊢ t : B}{Γ; Φ, z : A ⊢ t[z/x, z/y] : B}  Weakening \frac{Γ; Φ ⊢ t : B}{Γ; Φ, z : A ⊢ t : B}

Fig. 4. A version of the Logic of Unity

It is possible to translate LU into LL. A judgement of the form Γ; Φ ⊢ t : A in LU corresponds to a judgement Γ, !Φ ⊢ t : A in LL, where if Φ is x_{1} : A_{1} , …, x_{n} : A_{n} then !Φ is !x_{1} : !A_{1} , …, !x_{n} : !A_{n}.

Each rule in LU corresponds to the rule of the same name in LL, with two spectacular exceptions. Id-Int in LU translates to a combination of Id and Dereliction in LL.

Id-Int \overline{; x : A ⊢ x : A}  ↦  \overline{Id} ; x : A ⊢ x : A \overline{Dereliction} !x : !A ⊢ x : A

On the other hand, both the hypothesis and conclusion of the Dereliction rule of LU translate to the same judgement of LL.

Dereliction \frac{Γ, !z : !A; Φ ⊢ t : B}{Γ; z : A, Φ ⊢ t : B}  ↦  Γ, !z : !A, !Φ ⊢ t : B

Thus Id-Int in LU corresponds to Dereliction in LL, while Dereliction in LU corresponds to nothing at all!

The translation induces the obvious semantics: the semantics of a judgement in LU is the the same as the semantics of the corresponding judgement in LL. Analogues of the theorems of Section 4 hold.

There are a number of rules which one would expect of LU, which can be derived from the rules given here. The most important of these is Cut-Int.

Cut-Int \frac{; Φ ⊢ t : A  Δ; x : A, Ψ ⊢ u : B}{Δ; Φ, Ψ ⊢ (let !x = !t in u) : B}

This rule is derived as follows.

; Φ ⊢ t : A \overline{Promotion} ; Φ ⊢ !t : !A

Δ; x : A, Ψ ⊢ u : B

\overline{Dereliction}

Δ, !x : !A; Ψ ⊢ u : B

\overline{Let}

Δ, y : !A; Ψ ⊢ let !x = y in u : B

Δ; Φ, Ψ ⊢ (let !x = !t in u) : B

Observe that the semantics of (let !x = !t in u) is identical to the semantics of u[t/x], which may offer further scope for simplification.

6 Variations

Many programmers are unfamiliar with the {− \atop ∘}-L rule of the sequent calculus, and may find the {− \atop ∘}-E rule of natural deduction more natural. On the other hand, the use of sequent calculus seems to naturally capture the pattern matching in the ⊗ and & rules, so there may be some value in exploring a hybrid of the two systems. One variation would simply replace the {− \atop ∘}-L rule by {− \atop ∘}-E. This might be easier for programmers to follow, though important logical properties such as cut-elimination would be lost.

The work presented here extends straightforwardly to handle sums.

⊕-I \frac{Γ ⊢ t : A}{Γ ⊢ (inl t) : (A ⊕ B)}  \frac{Γ ⊢ u : B}{Γ ⊢ (inr u) : (A ⊕ B)}

⊕-E \frac{Γ ⊢ z : (A ⊕ B)  Δ, p : A ⊢ t : C  Δ, q : B ⊢ u : C}{Γ, Δ ⊢ (case z of \{inl p → t; inr q → u\}) : C}

Here we have I and E rules rather than R and L rules. These rules do not exploit the power of pattern matching as thoroughly as one might hope. For instance, patterns of the form (inl p) and (inr q) cannot appear nested inside other patterns. An open question is whether there is a different approach that allows for such nested patterns. One path in this direction is indicated by the work of Breazu-Tannen, Kesner, and Puel [BTKP93].

Another variation is to include patterns to indicate Contraction and Weakening. The grammar of patterns is divided into patterns and of-course patterns, the former being a superset of the latter.

p, q ::= x | (p, q) | ⟨p, ⟩ | ⟨ , q⟩ | o
o, r ::= (o@r) | | !x

Let p, q range over patterns, and o, r range over of-course patterns. The new rules are as follows.

Promotion \frac{o_{1} : !A_{1} , …, o_{n} : !A_{n} ⊢ t : B}{o_{1} : !A_{1} , …, o_{n} : !A_{n} ⊢ !t : !B}  Dereliction \frac{Γ, z : A ⊢ t : B}{Γ, !z : !A ⊢ t : B}

Contraction \frac{Γ, o : A, r : A ⊢ t : B}{Γ, (o@r) : A ⊢ t : B}  Weakening \frac{Γ ⊢ t : B}{Γ, : !A ⊢ t : B}

Dereliction, Contraction, and Weakening introduce the three different sorts of of-course pattern, while Promotion allows any of-course pattern. This variation is included simply to illustrate that the approach used here does not preclude the use of specific patterns to indicate Contraction and Weakening. However, in practice there does not seem to be much value in including such detailed information.

Acknowledgements. I am grateful to Jean-Yves Girard, Samson Abramsky, Robert Seely, Martin Hyland, Valeria de Paiva, and Uday Reddy for their insights into linear logic. One of the MFPS referees made detailed and valuable suggestions for improvement.

References

[Abr90] S. Abramsky, Computational interpretations of linear logic. Presented at Workshop on Mathematical Foundations of Programming Language Semantics, 1990. To appear in Theoretical Computer Science.

[AJ92] S. Abramsky and R. Jagadeesan, New foundations for the geometry of interaction. In 7’th Symposium on Logic in Computer Science, IEEE Press, Santa Cruz, California, June 1992.

[Bar79] M. Barr, ∗-Autonomous Categories. Lecture Notes in Mathematics 752, Springer Verlag, 1979.

[BBdPH92] N. Benton, G. Bierman, V. de Paiva, and M. Hyland, Type assignment for intuitionistic linear logic. Technical report 262, Computing Laboratory, University of Cambridge, August 1992.

[BCGS91] V. Breazu-Tannen, T. Coquand, C. A. Gunter, and A. Scedrov, Inheritance as explicit coercion. Information and Compututation, 93:172–221, 1991. (An earlier version appeared in Symposium on Logic in Computer Science, IEEE Press, Asilomar, California, June 1989.)

[BTKP93] V. Breazu-Tannen, D. Kesner, L. Puel, A typed pattern calculus. In 8’th Symposium on Logic in Computer Science, Montreal, June 1993.

[CGR92] J. Chirimar, C. A. Gunter, and J. G. Riecke. Linear ML. In Symposium on Lisp and Functional Programming, ACM Press, San Francisco, June 1992.

[Fil92] A. Filinski, Linear continuations. In Symposium on Principles of Programming Languages, ACM Press, Albuquerque, New Mexico, January 1992.

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

[Gir91] J.-Y. Girard, On the unity of logic. Manuscript, 1991.

[Hol88] S. Holmström, A linear functional language. Draft paper, Chalmers University of Technology, 1988.

[Laf88] Y. Lafont, The linear abstract machine. Theoretical Computer Science, 59:157–180, 1988.

[LM92] P. Lincoln and J. Mitchell, Operational aspects of linear lambda calculus. In 7’th Symposium on Logic in Computer Science, IEEE Press, Santa Cruz, California, June 1992.

[LS91] Y. Lafont and T. Streicher. Game semantics for linear logic. In 6’th Symposium on Logic in Computer Science, IEEE Press, Amsterdam, July 1991.

[Mac91] I. Mackie, Lilac: a functional programming language based on linear logic. Master’s Thesis, Imperial College London, 1991.

[Mog89] E. Moggi, Computational lambda-calculus and monads. In 4’th Symposium on Logic in Computer Science, IEEE Press, Asilomar, California, June 1989.

[O’He91] P. W. O’Hearn, Linear logic and interference control. In Conference on Category Theory and Computer Science, Paris, September 1991. LNCS, Springer Verlag.

[Pra91] V. Pratt, Event spaces and their linear logic. In AMAST ’91: Algebraic Methodology And Software Technology, Iowa City, Springer Verlag LNCS, 1992.

[Red91] U. Reddy, Acceptors as Values. Manuscript, December 1991.

[See89] R. A. G. Seely, Linear logic, ∗-autonomous categories, and cofree coalgebras. In Categories in Computer Science and Logic, June 1989. AMS Contemporary Mathematics 92.

[Tro92] A. S. Troelstra, Lectures on Linear Logic. CSLI Lecture Notes, 1992.

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

[Wad91] P. Wadler, Is there a use for linear logic? In Conference on Partial Evaluation and Semantics-Based Program Manipulation (PEPM), New Haven, Connecticut, ACM Press, June 1991.

[Wad92] P. Wadler, There’s no substitute for linear logic. Presented at Workshop on Mathematical Foundations of Programming Language Semantics, Oxford, April 1992.

[Wad93] P. Wadler, A taste of linear logic. In Mathematical Foundations of Computer Science, Gdansk, Poland, LNCS, Springer Verlag, August 1993.

This article was processed using the LaTEX macro package with LLNCS style