Dual Intuitionistic Linear Logic

Andrew Barber

Department of Computer Science University of Edinburgh

September 23, 1996

Abstract: We present a new intuitionistic linear logic, Dual Intuitionistic Linear Logic, designed to reflect the motivation of exponentials as translations of intuitionistic types, and provide it with a term calculus, proving associated standard type-theoretic results. We give a sound and complete categorical semantics for the type-system, and consider the relationship of the new type-theory to the more familiar presentation found for example in [4].

1 Introduction and Motivation

1.1 Background

Linear Logic is a resource logic introduced by Girard in [7]. One focus of attention in this field has been the type theory of various intuitionistic versions of Linear Logic, which in general have as their term calculi resource-sensitive versions of the λ-calculus. For example, [4, 13, 14, 1] all propose systems of this form.

In this report, we will refer to [4] for a commonly used and well understood term calculus for Intuitionistic Linear Logic, ILL. We recall the most important rules of that system in a natural deduction form, with their term annotation:

Weakening Γ ⊢ t : B Δ ⊢ u :!A Γ, Δ ⊢ discard u in t : B Dereliction Γ ⊢ t :!A Γ ⊢ derelict(t) : A

Contraction

Γ, x :!A, y :!A ⊢ t : B Δ ⊢ u :!A
Γ, Δ ⊢ copy u as x, y in t : B

Promotion x_{1} :!A_{1}, …, x_{n} :!A_{n} ⊢ t : B {Δ_{i} ⊢ u_{i} :!A_{i}}_{i=1..n} Δ_{1}, …, Δ_{n} ⊢ promote u⃗ for x⃗ in t :!B

The reason for the complexity of these rules is that previous calculi [1] were not able to prove the following important substitution property:

Γ ⊢ t : A and Δ, x : A ⊢ u : B imply Γ, Δ ⊢ u[t/x] : B

Now in this presentation we can immediately see that in constrast to the normal situation of natural deduction, the !-connective has rules which do not fall easily into the introduction/elimination mould. In the term calculus, this has the consequence that we do not have a constructor and a destructor for the !, but instead we have four term constructs with a correspondingly high number of equalities.

We therefore introduce an alternative formulation of ILL, called Dual Intuitionistic Linear Logic (DILL), in which the exponential is seen as a way of translating from an intuitionistic context to a linear one. The name ‘Dual’ is intended to refer to the double context on the left, rather than any potential duality; the typing context of the logic is divided into two parts, one linear and one intuitionistic. A general sequent has the form Γ; Δ ⊢ A, which is interpreted as meaning that from intuitionistic assumptions in Γ and linear assumptions in Δ we can deduce A. This splitting of the context leads to an extra intuitionistic axiom form, but the remainder of the rules are very similar to their counterparts in ILL.

Having outlined the form of the logic, we can see that the term calculus will be different to those referenced above, because of the split context. The introduction and elimination rules for ! are reflected in two new term constructs, one !t :!A and the other let !x : A be u :!A in t, which are a constructor-destructor pair analogous to those familiar in term assignment systems.

1.2 Related Work

As mentioned above, linear term calculi for variants of intuitionistic linear logic are not rare. The features of this presentation are essentially the split context, and the form of the rules. The first of these seems originally to have been inspired by Girard [8], who used the idea in an all-encompassing system, LU. Then Miller remarked on the possibility of adapting the idea to Plotkin, who designed the system considered here [11]. In fact, DILL corresponds at the level of provability to the so-called “intuitionistic fragment” of LU, although it is not clear whether this holds at the level of proofs.

Wadler [15, 14] also adapted Girard’s idea to an intuitionistic framework, but with a slightly different syntax and development to ours. Another approach which is different in focus is Benton’s [2]; there, he develops a logic and term calculus for a particular set of categorical models of ILL, which we will mention later in the discussion on semantics. His logic is somewhat non-standard in that it has two notions of sequent, one to represent the intuitionistic case and one to represent the linear case. This is because his categorical models take the form of an adjunction between a cartesian closed category (CCC) and a symmetric monoidal closed category (SMCC).

We should note that the idea of using a SMCC with a monoidal adjunction to a CCC as a model of ILL is due to a number of researchers. In particular, this model is presented in Benton’s paper as cited above, and its motivation is presented in Bierman [6].

1.3 Structure of the Report

The structure of this report is as follows. Firstly, we present the logic, DILL and show some equivalences which are inherent in the rules. We then present the type-system associated with the logic, give the equality relation on the terms, and prove some fundamental typetheoretic results about the system. Having established the syntactic framework, we go on to consider categorical models, and prove that the term-system is sound and complete with respect to a certain class of categorical models.

We then consider the relationship between DILL and ILL. We map DILL into ILL and v.v., and show that the two mappings make DILL a conservative extension of ILL at the level of proofs, or equivalently terms. Finally, we give some category-theoretic consequences of this result and consider further work.

2 The Logic

We now introduce the logic. In order to make it more applicable, we incorporate primitive types and functions of one argument over those primitive types. We can express this information in the form of a graph.

A Base Graph of Objects and Arrows We assume that there exists a graph G of objects Ob(G) and arrows between them G(A, B) for A, B ∈ Ob(G) as a basis for the type system.

We will refer to the new logic as D(G)or simply DILL where no confusion is likely. We consider formulae:

A, B ::= Y ∈ Ob(G) | I | A−∘B | A ⊗ B | !A

A sequent in this system has the form: Γ; Δ ⊢ A, where we understand Γ to be a set of formulae (the intuitionistic assumptions), and Δ to be a multiset of formulae (the linear assumptions), with A a formula. Note that we use the “,” to mean either set union or multiset union as appropriate to the context.

2.1 The Rules

(Int − Ax) Γ, A; ⊢ A  (Lin − Ax) Γ; A ⊢ A
(Graph) {Γ; Δ ⊢ B \atop Γ; Δ ⊢ A} (if G(A, B) ≠ ∅)

(I − I) Γ; ⊢ I  (I − E) \begin{matrix}Γ; Δ_{1} ⊢ I & Γ; Δ_{2} ⊢ A \\ Γ; Δ_{1}, Δ_{2} ⊢ A \end{matrix}

(⊗ − I) \begin{matrix}Γ; Δ_{1} ⊢ A & Γ; Δ_{2} ⊢ B \\ Γ; Δ_{1}, Δ_{2} ⊢ A ⊗ B \end{matrix}  (⊗ − E) \begin{matrix}Γ; Δ_{1} ⊢ A ⊗ B & Γ; Δ_{2}, A, B ⊢ C \\ Γ; Δ_{1}, Δ_{2} ⊢ C \end{matrix}

(−∘I) {Γ; Δ, A ⊢ B \atop Γ; Δ ⊢ A−∘B}  (−∘E) \begin{matrix}Γ; Δ_{1} ⊢ A−∘B & Γ; Δ_{2} ⊢ A \\ Γ; Δ_{1}, Δ_{2} ⊢ B \end{matrix}

(! − I) {Γ; ⊢ A \atop Γ; ⊢!A}  (! − E) \begin{matrix}Γ; Δ_{1} ⊢!A & Γ, A; Δ_{2} ⊢ B \\ Γ; Δ_{1}, Δ_{2} ⊢ B \end{matrix}

As remarked in the introduction, we have replaced the four rules involving the !- connective in the original form of ILL with the introduction-elimination pair seen above. The contraction and weakening rules previously used are now derivable by virtue of the fact that we allow contraction and weakening in the intuitionistic side of the context.

It is also important to notice that in the rule !-I, we specify that a particular sequent use no linear assumptions. This is intuitively because we need to be able to use the sequent repeatedly.

2.2 The Cut Rules

Because we have a logic with two different regions on the left, there will be two cut rules, one in which the cut formula occurs to the left of the semicolon (the intuitionistic region) and one in which the cut formula occurs to the right of the semicolon (the linear region.

These are stated as follows:

(I − Cut) \begin{matrix}Γ, A; Δ ⊢ B & Γ; ⊢ A \\ Γ; Δ ⊢ B \end{matrix} (L − Cut) \begin{matrix}Γ; Δ_{1}, A ⊢ B & Γ; Δ_{2} ⊢ A \\ Γ; Δ_{1}, Δ_{2} ⊢ B \end{matrix}

Note that in the intuitionistic cut rule, the linear region of the sequent proving the cut formula is constrained to be empty. This is because the sequent using the cut formula as an intuitionistic assumption may use it arbitrarily many times (or none).

Cut-Elimination Having introduced these cut rules, we can immediately show that they are admissible in the system without cuts:

Lemma 2.1 (Intuitionistic Cut) If Γ, A; Δ ⊢ B and Γ; ⊢ A, then Γ; Δ ⊢ B without using cuts.

Lemma 2.2 (Linear Cut) If Γ; Δ_{1}, A ⊢ B and Γ; Δ_{2} ⊢ A, then Γ; Δ_{1}, Δ_{2} ⊢ B without using cuts.

We give the proofs of these lemmas in the typing section, where they will be restated as substitution lemmas.

2.3 Equivalences

We now go on to state a number of defining equivalences for the connectives, which confirm their behaviour as that familiar in a more conventional presentation of intuitionistic linear logic. The justification for this new system is based in large part on the fact that every proof using an exponential type is equivalent to one using an intuitionistic type (which is the base type of the exponential).

Lemma 2.3 (!-Equivalence) In the presence of the cut rules, the two-way proof rule:

{Γ, A; Δ ⊢ B \atop Γ; !A, Δ ⊢ B}

is equivalent in strength to the (! − I), (! − E) pair introduced earlier.

Proof If we have the two-way proof rule and the cut rules, then we can use the following deduction to give ! − I:

\begin{matrix}Γ; ⊢ A & {; !A ⊢!A \atop A; ⊢!A} \\ Γ; Δ ⊢!A \end{matrix}

Further, we can prove ! − E with the following derivation:

Γ; Δ_{1} ⊢!A {Γ, A; Δ_{2} ⊢ B \atop Γ; !A, Δ_{2} ⊢ B}
Γ; Δ_{1}, Δ_{2} ⊢ B

Going the other way, it is easy to derive both directions of the equivalence given the (! − I), (! − E) pair. The forward direction follows from one use of !-E, and the other direction is an instance of linear cut and derived weakening:

\begin{matrix}{Γ, A; ⊢ A \atop Γ, A; ⊢!A} & Γ, A; !A, Δ ⊢ B \\ Γ, A; Δ ⊢ B \end{matrix}

■

We give similar results for the other connectives:

Lemma 2.4 (Equivalences) In the presence of the linear cut rule:

• The two-way proof equivalence {Γ; Δ ⊢ C \atop Γ; Δ, I ⊢ C} is equal in strength to the I − I, I − E pair.

• The two way proof equivalence {Γ; Δ, A, B ⊢ C \atop Γ; Δ, A ⊗ B ⊢ C} is equal in strength to the ⊗−I, ⊗−E pair.

• The two way proof equivalence {Γ; Δ, A ⊢ B \atop Γ; Δ ⊢ A−∘B} is equal in strength to the −∘−I, −∘−E pair.

These are all proved in a similar way to that for !.

We also have:

Lemma 2.5 Γ; A, Δ ⊢ B implies Γ, A; Δ ⊢ B.

Proof This is also proved via a straightforward weakening and linear cut.

3 The Type System and its Basic Theory

We construct pre-terms as follows:

t ::= x | f(t) for f ∈ G(A, B) | ∗ | let ∗ be t in u | t_{1} ⊗ t_{2}
| let x ⊗ y : A ⊗ B be t in u | λx : A.t | tu | !t | let !x : A be t in u

where x ranges over a countably infinite set of variables. The notion of free variables of a pre-term t, written FV(t), is defined inductively over the structure of t as follows:

FV(x) = {x}
FV(f(t)) = FV(t)
FV(∗) = ∅
FV(let ∗ be u in t) = FV(u) ∪ FV(t)
FV(t ⊗ u) = FV(t) ∪ FV(u)
FV(let x ⊗ y be u in t) = FV(u) ∪ (FV(t) − {x, y})
FV(λx.t) = FV(t) − {x}
FV(tu) = FV(t) ∪ FV(u)
FV(let !x be u in t) = FV(u) ∪ (FV(t) − {x})
FV(!t) = FV(t)

We define substitution for free variables and hence α-conversion as normal, noting only that

(let x ⊗ y be t in u)[v/z] = let x ⊗ y be t[v/z] in u[v/z] if y ∉ {x, y})

and similarly for let !x be t in u.

Although we have defined pre-terms with type information incorporated, in the rest of this report we will omit the types for derivable terms, where they can be inferred from the derivation.

3.1 The Term Rules

Define a typing to be a pair x : A where x is a variable and A is a formula of the logic. We now define an environment to be a pair of sequences of typings in which no variable occurs twice. The intention is that the first sequence in the pair is the sequence of typings of ‘intuitionistic’ formulae (those to the left of the semicolon) and the second sequence in the pair is the sequence of typings of the ‘linear’ formulae.

We commonly write a type assignment in this system as Γ; Δ ⊢ t : A, where Γ; Δ is an environment. In the following, it is assumed that in addition (Γ_{1}; Δ_{1}) and (Γ_{2}; Δ_{2}) are environments.

(Int − Ax) Γ, x : A; ⊢ x : A  (Lin − Ax) Γ; x : A ⊢ x : A

(Graph) {Γ; Δ ⊢ t : A \atop Γ; ⊢ f(t):B} (f ∈G(A, B))

(I − I) Γ; ⊢ ∗ : I  (I − E) \begin{matrix}Γ; Δ_{1} ⊢ t : I & Γ; Δ_{2} ⊢ u : A \\ Γ; Δ_{1}, Δ_{2} ⊢ let ∗ be t in u : A \end{matrix}

(⊗ − I) \begin{matrix}Γ; Δ_{1} ⊢ t : A & Γ; Δ_{2} ⊢ u : B \\ Γ; Δ_{1}, Δ_{2} ⊢ t ⊗ u : A ⊗ B \end{matrix} (⊗−E) \begin{matrix}Γ; Δ_{1} ⊢ u:A⊗B & Γ; Δ_{2}, x : A, y : B ⊢ t:C \\ Γ; Δ_{1}, Δ_{2} ⊢ let x⊗y : A⊗B be u in t :C \end{matrix}

(−∘I) {Γ; Δ, x : A ⊢ t : B \atop Γ; Δ ⊢ (λx : A.t) : (A−∘B)}  (−∘E) \begin{matrix}Γ; Δ_{1} ⊢ u : A−∘B & Γ; Δ_{2} ⊢ t : A \\ Γ; Δ_{1}, Δ_{2} ⊢ (ut) : B \end{matrix}

(! − I) {Γ; ⊢ t : A \atop Γ; ⊢!t :!A}  (! − E) \begin{matrix}Γ; Δ_{1} ⊢ u :!A & Γ, x : A; Δ_{2} ⊢ t : B \\ Γ; Δ_{1}, Δ_{2} ⊢ let !x : A be u in t : B \end{matrix}

A term is a pre-term of the term calculus DILL over the graph G (which we will write D(G)) which can be shown to annotate the conclusion of a sequent using these rules. We will represent a term and the sequent which witnesses it as the typing Γ; Δ ⊢ t : A in general.

3.2 Results

We now give some easy type-theoretic results about this system, including weakening and strengthening (both in the intuitionistic assumptions) and prove subject reduction.

Lemma 3.1 (Typing Properties) We have the following in the type system DILL: Free Variables I If Γ; Δ ⊢ t : A, then FV(t) ⊆ dom(Γ) ∪ dom(Δ). Free Variables II If Γ; Δ, x : A ⊢ t : B, then x is free precisely once in t. Intuitionistic Weakening If Γ; Δ ⊢ t : A, then Γ, x : B; Δ ⊢ t : A. Intuitionistic Strengthening If x : A, Γ; Δ ⊢ t : B and x ∉ FV(t), then Γ; Δ ⊢ t : B. Environment Weakening If Γ; Δ, x : A ⊢ t : B, then Γ, x : A; Δ ⊢ t : B. Environment Strengthening If Γ, x : A; Δ ⊢ t : B and x occurs precisely once free, not

under a !-construct, in t, then Γ; Δ, x : A ⊢ t : B. !-Equivalence if Γ; x :!A, Δ ⊢ u : B, then

Γ, y : A; Δ ⊢ u[!y/x] : B

and if Γ, y : A; Δ ⊢ v : B, then

Γ; x :!A, Δ ⊢ let !y be x in v : B

Further, the maps u ↦ u[!y/x] and v ↦ let !y be x in v are inverse in both directions. Linear Cut If Γ; Δ_{1}, x : A ⊢ t : B and Γ; Δ_{2} ⊢ u : A, then Γ; Δ_{1}, Δ_{2} ⊢ t[u/x] : B. Intuitionistic Cut If Γ, x : A; Δ ⊢ t : B and Γ; ⊢ u : A, then Γ; Δ ⊢ t[u/x] : B.

As an example, we outline the proof of the linear cut lemma. That of the intuitionistic cut is similar. Proof: The proof proceeds by induction on the structure of t. Note that since x : A is a linear typing, x must be free in t, by our previous result. If t is y then y is x, since x is free in y, and hence the required sequent is the second

premise. If t is λy : B.v then we know that we must have a derivation:

{Γ, y : B; x : A′Δ_{1} ⊢ v : C \atop Γ; x : A, Δ_{1} ⊢ (λy : B.v) : B → C}

By the induction hypothesis on the premise, we now have:

Γ, y : B, Δ_{1}, Δ_{2} ⊢ v[u/x] : C

and the required sequent follows by one abstraction.

If t is let !z : c be w in v : B then we know that we have a derivation:

Γ, z : C; Δ_{1} ⊢ v : B Γ; Δ′_{1} ⊢ w :!C
Γ; Δ_{1}, Δ′_{1} ⊢ (let !z : C be w in v : B) : B

where x : A occurs in either Δ_{1} or Δ_{2}. In either case we can use the induction hypothesis to obtain the result required, since substitution commutes with the let construction by definition.

Other Cases The other cases proceed similarly.

Intuitionistic and Linear Free Variables In view of the first free-variable lemma above, we say that x ∈ FV(t) is a linear free variable of a derivation Γ; Δ ⊢ t : A if for some B we have x : B ∈ Δ. Correspondingly, x is an intuitionistic free variable if for some B we have x : B ∈ Γ.

3.3 Term Contexts

In order to present the type theory, we will need to define a notion of contexts, where these may be linear (ie, use their ‘argument’ linearly) or intuitionistic (eg, use their argument inside a !-construct).

We define a general context as follows:

[Contexts] A context C[ ] is an object constructed recursively as follows:

C[ ] := | let ∗ be C[ ] in t | let ∗ be t in C[ ] | t ⊗ C[ ] | C[ ] ⊗ t |

let x ⊗ y be C[ ] in t | let x ⊗ y be t in C[ ] | λx.C[ ] | C[ ]t | tC[ ] | !C[ ] | let !x be C[ ] in t | let !x be t in C[ ]

Note that this definition implies that there will be precisely one occurence of the symbol in every context.

We say that a context is linear if it is constructed from the above structure without the use of the clause !C[ ]. Further, a context binds a variable x if the context is constructed with the use of clauses let x ⊗ y be t in C[ ], let y ⊗ x be t in C[ ], λx.C[ ] or let !x be t in C[ ].

Now define C[t] for a given context C[ ] and term t to be the context C[ ] with the unique occurence of the symbol replaced by the term t. We can easily show by induction over contexts that C[t] is a pre-term.

3.4 The Term Equality

We present the equality we will use on the terms. An assertion of equality has the following form: Γ; Δ ⊢ t =_{A} u where this is well formed iff both t and u are typable of type A in the given environment Γ; Δ.

We first need to specify that the equality is reflexive, transitive and symmetric:

{Γ; Δ ⊢ t : A \atop Γ; Δ ⊢ t =_{A} t} \begin{matrix}Γ; Δ ⊢ t =_{A} u & Γ; Δ ⊢ u =_{A} v \\ Γ; Δ ⊢ t =_{A} v \end{matrix} {Γ; Δ ⊢ t =_{A} u \atop Γ; Δ ⊢ u =_{A} t}

Now we allow equality inside generic contexts C[ ].

Γ; Δ ⊢ t =_{A} u Γ; Δ′ ⊢ C[t] : B  Γ; Δ′ ⊢ C[u] : B
Γ; Δ, Δ′ ⊢ C[t] =_{B} C[u]

The β and η equalities are as follows:

(I_{β}) Γ; Δ ⊢ let ∗ be ∗ in t : A Γ; Δ ⊢ let ∗ be ∗ in t =_{A} t  (I_{η}) Γ; Δ ⊢ let ∗ be t in ∗ : I Γ; Δ ⊢ let ∗ be t in ∗ =_{I} t

(⊗_{β}) Γ; Δ ⊢ let x⊗y be v⊗u in t : C Γ; Δ ⊢ let x⊗y be v⊗u in t =_{C} t[v, u/x, y] (⊗_{η}) Γ; Δ ⊢ let x⊗y be v in x⊗y : A⊗B Γ; Δ ⊢ let x⊗y be v in x⊗y =_{A⊗B} t

(−∘_{β}) {Γ; Δ ⊢ (λx : A.t)u : A \atop Γ; Δ ⊢ (λx : A.t)u =_{A} t[u/x]}  (−∘_{η}) {Γ; Δ ⊢ λx : A.(tx) : A−∘B \atop Γ; Δ ⊢ λx : A.(tx) =_{A−∘B} t}

(!_{β}) Γ; Δ ⊢ let !x : A be !u in t : B Γ; Δ ⊢ let !x : A be !u in t =_{B} t[u/x]  (!_{η}) Γ; Δ ⊢ let !x : A be u in !x :!A Γ; Δ ⊢ let !x : A be u in !x =_{!A} u

Further to these equalities, we need some extra equalities which correspond to proof-rule permutations (the so-called commuting conversions). In other presentations of term calculi for ILL, the proof permutations are expressed as a large number of primitive equalities such as:

Γ; Δ ⊢ let x ⊗ y be t in u ⊗ v
Γ; Δ ⊢ u ⊗ (let x ⊗ y be t in v)

where x, y are not free in u.

We replace these by schematic versions where a general context is used to bring together the primitive equalities into classes. For example, the equality above would be an instance of our second equality rule, where the context C is v ⊗ .

• For linear contexts C:

Γ; Δ ⊢ let ∗ be t in C[u] : A
Γ; Δ ⊢ let ∗ be t in C[u] =_{A} C[let ∗ be t in u]

• For linear contexts C which do not bind x : A or y : B:

Γ; Δ ⊢ let x ⊗ y be t in C[u] : A
Γ; Δ ⊢ let x ⊗ y be t in C[u] =_{A} C[let x ⊗ y be t in u]

• For linear contexts C which do not bind x : A:

Γ; Δ ⊢ let !x be t in C[u] : A

Γ; Δ ⊢ let !x be t in C[u] =_{A} C[let !x be t in u]

Note that when we use these rules to prove an equality between two terms, because such an equality is only well-formed when both terms are typable, we must demonstrate that this is the case for our candidate terms. Fortunately, this is normally trivial and so we will freely omit these typings except where necessary.

Although there is an obvious way to give a rewrite system for this equality, we do not pursue this possibility here. Instead, we discuss this in the further work section of this report.

A Note on the Commuting Conversions of ! − E Notice that the restriction on the context in the !-commuting conversion rules out the following (well-typed) equality:

y :!A; ⊢!(let !x be y in x) =_{A} let !x be y in !x

This equality corresponds to imposing an extra requirement on models which cannot be motivated from the proof structure of linear logic.

3.5 A Definable Intuitionistic Function Space

We now briefly present a definable extension to the logic and term calculus given above. In order to make the syntax more useable, we show how we can define the types and terms associated with an intuitionistic arrow type purely in terms of the structures we already have.

Formulae and Types We define the formula A → B in our new system as the formula !A−∘B. Now we have the derived introduction/elimination pair:

(→ −I) {Γ, A; Δ ⊢ B \atop Γ; Δ ⊢ A → B} (→ −E) \begin{matrix}Γ; Δ ⊢ A → B & Γ; ⊢ A \\ Γ; Δ ⊢ B \end{matrix}

On terms, we define the abstraction and application as follows (where we use γ for the abstraction):

\begin{aligned}γx : A. t & = & λx′ :!A let !x be x′ in t \\ tu & = & t(!u) \end{aligned}

Now it can be proved that using the equalities already defined we have the following:

(→ β) {Γ; Δ ⊢ (γx : A.t)u : A \atop Γ; Δ ⊢ (γx : A.t)u =_{A} t[u/x]} (→ η) {Γ; Δ ⊢ γx : A.(tx) : A → B \atop Γ; Δ ⊢ γx : A.(tx) =_{A→B} t}

Hence this construct and its associated terms and equalities can be used as primitive without changing the development to follow. Other definitions of this function space are possible via more complex embeddings of intuitionistic logic into linear logic; for example see Benton [5] or Schellinx [12].

4 Categorical Semantics

We now show that DILL can be soundly and completely mapped into a class of models for linear logic. By this we mean that we can map proofs in the logic, as terms, to morphisms in the model in such a way that any two proofs are equal in the logic if and only if they are equal in every model of the class.

We start by presenting the class of models we will consider.

4.1 Linear-non-Linear Models

The models we will consider are called Linear-non-Linear models (commonly abbreviated to LNL-models) by Benton in his paper [2]. These are symmetric monoidal closed categories (SMCC’s) which have a monoidal adjunction to a cartesian closed category (CCC). The intention behind the construction is that the normal power of intuitionistic logic should be modelled in the CCC, with the intuitionistic linear logic being as usual modelled in the SMCC. This idea emerged in 1993 from discussions between a number of people, including Plotkin, Benton and Hyland. However, it was only during further work by Benton [2] that it became clear that it was necessary to impose the requirement that the adjunction be monoidal. In the referenced work by Benton there is an extensive comparison between these models and the previously proposed models [4]. We discuss further the connections between this work and ours at the end of this report.

4.2 Definitions

We now present the definition of LNL model, in stages. For brevity, we present the coherence diagrams in the form of equalities.

Symmetric Monoidal Closed Categories A Symmetric Monoidal Closed Category is a category C with a bifunctor ⊗ : C × C → C and natural isomorphisms

\begin{aligned}α_{A,B,C} : & (A ⊗ B) ⊗ C & → & A ⊗ (B ⊗ C) \\ ri_{A} : & I ⊗ A & → & A \\ li_{A} : & A ⊗ I & → & A \\ σ_{A,B} : & A ⊗ B & → & B ⊗ A \end{aligned}

s.t.

(α_{A,B,C} ⊗ id_{D}); α_{A,(B⊗C),D}; (id_{A} ⊗ α_{B,C,D}) = α_{(A⊗B),C,D}; α_{A,B,(C⊗D)}(1)
α_{A,I,B}; (id_{A} ⊗ il_{B}) = (ir_{A} ⊗ id_{B})  (2)
li_{I} = ri_{I}  (3)
(σ_{A,B} ⊗ id_{C}); α_{B,A,C}; l(id_{B} ⊗ σ_{A,C}) = α_{A,B,C}; σ_{A,(B⊗C)}; α_{B,C,A} (4)
σ_{A,B}^{−1} = σ_{B,A}  (5)
σ_{I,A}; il_{A} = ir_{A}  (6)

and s.t. ⊗ B ⊣ B−∘ , or

C(A ⊗ B, C) ≃ C(A, B−∘C)

where the isomorphism is natural in A and C.

Cartesian Closed Categories We assume familiarity with the standard definition of Cartesian Closed Categories (CCC’s henceforth). However, it is important to note that a CCC is merely a SMCC in which the tensor is Cartesian.

Symmetric Monoidal Functor We now need to define the concept of functor between two SMCCs. A symmetric monoidal functor

(F, m_{A,B}, m_{I}) : (C, ⊗, I, α, li, ri, σ) → (C′, ⊗′, I′, α′, li′, ri′, σ′)

is a functor F : C → C′ with a map m_{I} : I′ → F (I) and a natural transformation m_{A,B} : F (A) ⊗′ F (B) → F (A ⊗ B) s.t.

α′_{F A,F B,F C}; (id_{F A} ⊗′ m_{B,C}); m_{A,B⊗C} = (m_{A,B} ⊗′ id_{F C}); m_{A⊗B,C}; F (α_{A,B,C})(7)
ri′_{F A} = (m_{I} ⊗ id_{F A}); m_{I,A}; F (ri_{A})  (8)
σ′_{F A,F B}; m_{B,A} = m_{A,B}; F (σ_{A,B})  (9)

Under this definition it is easy to check that given two symmetric monoidal functors (F, m_{I}, m_{A,B}) and (G, n_{I′}, n_{A,B}) their compose is symmetric monoidal when equipped with maps:

(GF, (n_{I′}; G(m_{I})), (n_{F A,F B}; G(m_{A,B})))

Monoidal Natural Transformation A monoidal natural transformation from one symmetric monoidal functor (F, m_{I′}, m_{A,B}) to another (G, n_{I′}, n_{A,B}) is a natural transformation β : F → G s.t.

\begin{aligned}m_{A,B}; β_{A⊗B} & = (β_{A} ⊗′ β_{B}); n_{A,B} & (10) \\ m_{I′}; β_{I} & = n_{I′} & (11) \end{aligned}

4.2.1 LNL-Models

Now we define an LNL model to be a pair of categories (S, C) of which the first, S, is a SMCC and the second, C, is a CCC, with two symmetric monoidal functors F : C → S and G : S → C which are adjoint, G ⊢ F.

4.2.2 Contexts

We now make some definitions to simplify the interpretation. First, for a sequence of objects in the category S, A⃗ = A_{1}, A_{2}, … A_{n}, we define ⨂ A⃗ to be the left-bracketed tensor of this sequence, or:

⨂ A⃗ = (..(A_{1} ⊗ A_{2}) ⊗ … A_{n})

Now for a sequence of objects A⃗ = A_{1} … A_{n} we define F GA⃗ to be the sequence F GA_{1}, F GA_{2},… F GA_{n}. Also, for a sequence of types A_{1}, … A_{n}, we define !(A_{1}, … A_{n}) =!A_{1}, …!A_{n}.

4.3 Interpretation

We now define an interpretation [[ ]] : D(G) → (S, C) which takes the types and sequents of DILL over a graph G to a model M as follows:

Definition of [[ ]] on Types

\begin{aligned}[[X]] & = & I(X) for X ∈ Ob(G) \\ [[I]] & = & I \\ [[A ⊗ B]] & = & [[A]] ⊗ [[B]] \\ [[A−∘B]] & = & [[A]]−∘[[B]] \\ [[!A]] & = & F G([[A]]) \end{aligned}

We extend this firstly to lists by saying that for a list A_{1} … A_{n} of types, [[A_{1}, … A_{n}]] = ⨂([[A_{1}]], … [[A_{n}]]) Secondly, we extend the definition to contexts by saying that for a context A_{1}, … A_{n}; B_{1}, … B_{n},

[[A_{1}, … A_{n}; B_{1}, … B_{n}]] = [[!A_{1}, …!A_{n}, B_{1}, … B_{n}]]

Now in order to interpret the sequents of DILL over a graph G into a LNL-model (S, C), we will need a primitive interpretation function I : G → S such that I : G(A, B) → S([[A]], [[B]]) which tells us that we have enough morphisms in the category to model the primitive graph.

Context Manipulation Arrows We can now define some context-manipulation arrows, using the structure we have in the model.

Define

perm_{A⃗,B⃗,C⃗,D⃗} :([[A⃗]] ⊗ [[B⃗]]) ⊗ ([[C⃗]] ⊗ [[D⃗]]) → ([[A⃗]] ⊗ [[C⃗]]) ⊗ ([[B⃗]] ⊗ [[D⃗]])
der_{A} :[[!A]] → [[A]]
lcon_{Δ_{1},Δ_{2}} :[[Δ_{1}, Δ_{2}]] → [[Δ_{1}]] ⊗ [[Δ_{2}]]
dup_{A_{1},...A_{n}} :[[!(A_{1}, … A_{n})]] → [[!(A_{1}, … A_{n})]] ⊗ [[!(A_{1}, … A_{n})]]
str_{Γ,Δ_{1},Δ_{2}} :[[Γ; Δ_{1}Δ_{2}]] → [[Γ; Δ_{1}]] ⊗ [[Γ; Δ_{2}]]
disc_{A_{1},...A_{n}} :[[!(A_{1}, … A_{n})]] → I
prom_{Γ} :[[!(A_{1}, … A_{n})]] → [[!!(A_{1}, … A_{n})]]

as follows:

perm_{A⃗,B⃗,C⃗,D⃗} = α_{[[A⃗]],[[B⃗]],[[C⃗]]⊗[[D⃗]]}; (id_{[[A⃗]]} ⊗ α_{[[B⃗]],[[C⃗]],[[D⃗]]}^{−1}); (id_{[[A⃗]]} ⊗ (σ_{[[B⃗]],[[C⃗]]} ⊗ id_{[[D⃗]]}));
(id_{[[A⃗]]} ⊗ α_{[[C⃗]],[[B⃗]],[[D⃗]]}); α_{[[A⃗]],[[C⃗]],([[B⃗]]⊗[[D⃗]])}^{−1}
der_{A} = ϵ_{[[A]]}

lcon_{Δ_{1},Δ_{2}} = \begin{cases}(lcon_{Δ_{1},Δ′_{2}} ⊗ id_{[[A]]}); α_{[[Δ_{1}]],[[Δ′_{2}]],A}; \\ (id_{[[Δ_{1}]]} ⊗ lcon_{Δ′_{2},A}^{−1}) & where Δ_{1} ≠ and Δ_{2} = Δ′_{2}, A \\ ri_{[[Δ_{2}]]}^{−1} & if Δ_{1} = \\ li_{[[Δ_{1}]]}^{−1} & if Δ_{2} = \end{cases}

dup_{Γ} = \begin{cases}dup_{Γ′,A} ⊗ (F (c_{G[[B]]}); m_{G[[B]],G[[B]]}^{−1}); perm_{!(Γ′,A),!(Γ′,A),!B,!B} & if Γ = Γ′, A, B \\ F (c_{G[[A]]}); m_{G[[A]],G[[A]]}^{−1} & if Γ = A \\ ri_{I} & if Γ = \end{cases}

str_{Γ,Δ_{1},Δ_{2}} = lcon_{!Γ,(Δ_{1},Δ_{2})}; (dup_{Γ} ⊗ lcon_{Δ_{1},Δ_{2}}); perm_{!Γ,!Γ,Δ_{1},Δ_{2}}; (lcon_{!Γ,Δ_{1}}^{−1} ⊗ lcon_{!Γ,Δ_{2}}^{−1})

disc_{Γ} = \begin{cases}disc_{Γ′,B} ⊗ (F (d_{G[[A]]}); m_{1}^{−1}); ri_{I}^{−1} & if Γ = Γ′, B, A \\ F (d_{G[[A]]}); m_{1}^{−1} & if Γ = A \\ id_{I} & if Γ = \end{cases}

prom_{Γ} = \begin{cases}prom_{Γ′,B} ⊗ F (η_{G[[A]]}) & if Γ = Γ′, B, A \\ F (η_{G[[A]]}) & if Γ = A \\ id_{I} & if Γ = \end{cases}

Definition of [[ ]] on Sequents: The interpretation will take a sequent Γ; Δ ⊢ t : A to an arrow

[[Γ; Δ ⊢ t : A]] : [[Γ; Δ]] → [[A]]

in the LNL category.

[[ ]] is defined inductively over the structure of the derivation:

Linear Axiom Here we have:

[[Γ; x : A ⊢ x : A]] : [[Γ; A]] → [[A]]
= lcon_{!Γ,A}; (disc_{Γ} ⊗ id_{[[A]]}); ri_{[[A]]}

Intuitionistic Axiom Here, we have

[[Γ, x : A; ⊢ x : A]] : [[Γ, A; ]] → [[A]]
= lcon_{!Γ,!A}; (disc_{Γ} ⊗ der_{A}); ri_{[[A]]}

Primitive Arrow Rule We need to interpret the derivation:

{Γ; Δ ⊢ t : A \atop Γ; Δ ⊢ f(t); B} (for f ∈ G(A, B))

Given an arrow [[Γ; Δ ⊢ t : A]] : [[Γ; Δ]] → [[A]], all we do is take the arrow

[[Γ; Δ ⊢ t : A]]; I(f) : [[Γ; Δ]] → [[B]]

I-introduction Here we have:

[[Γ; ⊢ ∗ : I]] : [[Γ; ]] → [[I]]

= disc_{Γ}

I-elimination We need to interpret the derivation

Γ; Δ_{1} ⊢ t : I Γ; Δ_{2} ⊢ u : A

Γ; Δ_{1}, Δ_{2} ⊢ let ∗ be t in u : A

In this case, we have arrows

f : [[Γ; Δ_{1}]] → [[I]]
g : [[Γ; Δ_{2}]] → [[A]]

Hence we have

[[Γ; Δ_{1}, Δ_{2} ⊢ let ∗ be t in u : A]] : [[Γ; Δ_{1}, Δ_{2}]] → [[A]]
= str_{Γ,Δ_{1},Δ_{2}}; (f ⊗ g); ri_{[[A]]}

⊗-introduction The rule is:

\begin{matrix}Γ; Δ_{1} ⊢ t : A & Γ; Δ_{2} ⊢ u : B \\ Γ; Δ_{1}, Δ_{2} ⊢ t ⊗ u : A ⊗ B \end{matrix}

Using the premises, we already have arrows

f : [[Γ; Δ_{1}]] → [[A]]
g : [[Γ; Δ_{2}]] → [[B]]

Hence we have

[[Γ; Δ_{1}, Δ_{2} ⊢ t ⊗ u : A ⊗ B]] : [[Γ; Δ_{1}, Δ_{2}]] → [[A ⊗ B]]
= str_{Γ,Δ_{1},Δ_{2}}; (f ⊗ g)

⊗-Elimination The rule is

Γ; Δ_{1} ⊢ u : (A ⊗ B) Γ; Δ_{2}, x : A, y : B ⊢ t : C
Γ; Δ_{1}, Δ_{2} ⊢ let x ⊗ y be u in t : C

We have arrows:

f : [[Γ; Δ_{1}]] → [[A ⊗ B]]
g : [[Γ; Δ_{2}, A, B]] → [[C]]

Hence we have

[[Γ; Δ_{1}, Δ_{2} ⊢ let x ⊗ y be u in t : C]] :[[Γ; Δ_{1}, Δ_{2}]] → [[C]]

= str_{Γ,Δ_{1},Δ_{2}}; σ_{[[Γ;Δ_{1}]],[[Γ;Δ_{2}]]}; (id_{[[Γ;Δ_{2}]]} ⊗ f); α_{[[Γ;Δ_{2}]],[[A]],[[B]]}^{−1}; g

−∘-introduction The rule is as follows:

{Γ; Δ, x : A ⊢ t : B \atop Γ; Δ ⊢ λx.t : A−∘B}

so we have an arrow:

f : [[Γ; Δ, A]] → [[B]]

Hence we have

[[Γ; Δ ⊢ λx.t : A−∘B]] :[[Γ; Δ]] → [[A−∘B]]
= λ(lcon_{(!Γ,Δ),A}^{−1}; f)

−∘-elimination The rule is:

\begin{matrix}Γ; Δ_{1} ⊢ u : (A−∘B) & Γ; Δ_{2} ⊢ t : A \\ Γ; Δ_{1}, Δ_{2} ⊢ (ut) : B \end{matrix}

so we have arrows:

f : [[Γ; Δ_{1}]] → [[A−∘B]]
g : [[Γ; Δ_{2}]] → [[A]]

Hence we have

[[Γ; Δ_{1}, Δ_{2} ⊢ (ut) : B]] : [[Γ; Δ_{1}, Δ_{2}]] → [[B]]

= str_{Γ,Δ_{1},Δ_{2}}; (f ⊗ g); ap_{[[A]],[[B]]}

!-introduction The rule is:

{Γ; ⊢ t : A \atop Γ; ⊢!t :!A}

so we have an arrow:

f : [[Γ; ]] → [[A]]

Hence we have

[[Γ; ⊢!t :!A]] :[[Γ; ]] → [[!A]]
= prom_{Γ}; F G(f)

!-elimination The rule is:

Γ; Δ_{1} ⊢ u :!A Γ, x : A; Δ_{2} ⊢ t : B

Γ; Δ_{1}, Δ_{2} ⊢ let !x be u in t : B

Hence we have arrows:

f : [[Γ; Δ_{1}]] → [[!A]]
g : [[Γ, A; Δ_{2}]] → [[B]]

Hence we have

[[Γ; Δ_{1}, Δ_{2} ⊢ let !x be u in t : B]] : [[Γ; δ_{1}, Δ_{2}]] → [[B]]
= str_{Γ,Δ_{1},Δ_{2}}; (f ⊗ id_{[[Γ;Δ_{2}]]}); (id_{[[!A]]} ⊗ lcon_{!Γ,Δ_{2}});α_{[[!A]],[[!Γ]],[[Δ_{2}]]}^{−1}; (σ_{[[!A]],[[!Γ]]} ⊗ id_{[[Δ_{2}]]});
(lcon_{!Γ,!A}^{−1} ⊗ id_{[[Δ_{2}]]}); lcon_{(!Γ,A),Δ_{2}}^{−1}; g

4.4 Soundness

Having given the interpretation function [[ ]]M which takes terms of DILL into (the SMCC part of) the LNL-model M, we now need to show that the interpretation is sound. That is, we need to demonstrate that all the term equalities we have given in DILL are mapped to equalities in any LNL-model.

First we need to prove two technical lemmas, which show what the image of the two substitutions are in the model:

Lemma 4.1 If [[Γ; Δ ⊢ t : A]] = f and [[Γ; Δ′, x : A ⊢ u : B]] = g, then

[[Γ; Δ, Δ′ ⊢ u[t/x] : B]] = str_{Γ,Δ,Δ′};(f ⊗ id_{[[Γ;Δ′]]}); σ_{[[A]]),[[Γ;Δ′]]}; lcon_{(!Γ,Δ),A}^{−1}; g

Lemma 4.2 If [[Γ; ⊢ t : A]] = f and [[x : A, Γ; Δ ⊢ u : B]] = g, then

[[Γ; Δ ⊢ u[t/x] : B]] = str_{Γ, ,Δ};((prom_{Γ}; F G(f)) ⊗ id_{[[Γ;Δ]]}); (id_{[[!A]]} ⊗ lcon_{!Γ,Δ_{2}});
(σ_{[[!A]],[[!Γ]]} ⊗ id_{[[Δ_{2}]]}); (lcon_{!Γ,!A}^{−1} ⊗ id_{[[Δ_{2}]]}); lcon_{!(Γ,A),Δ_{2}}^{−1}; g

These lemmas are proved by induction over the structure of the first term. The proofs are again left to the reader.

Now we are able to prove soundness by considering the derivation of any equality in DILL.

Theorem 1 (Soundness) If Γ; Δ ⊢ t =_{A} u then

[[Γ; Δ ⊢ t : A]] = [[Γ; Δ ⊢ u : A]]

Proof

I − β In this case, we have

Γ; Δ ⊢ let ∗ be ∗ in t =_{A} t

The interpretation of the left hand side is the arrow

str_{Γ, ,Δ}; (disc_{Γ} ⊗ g); ri_{[[A]]}

but

str_{Γ, ,Δ}; (disc_{Γ} ⊗ id_{[[Γ;Δ]]}) = ri_{[[Γ;Δ]]}^{−1}

so this is just g by naturality of ri.

I − η In this case we have

Γ; Δ ⊢ let ∗ be t in ∗ =_{I} t

The interpretation of the left-hand side of this is the arrow

str_{Γ,Δ,} ; (f ⊗ disc_{Γ}); ri_{I}

but by a symmetric equality to that used above we have that this is

li_{[[Γ;Δ]]}^{−1}; (f ⊗ id_{I}); ri_{I}

but now since ri_{I} = li_{I} this is just f. ⊗ − η First, note that

[[Γ; x : A, y : B ⊢ x ⊗ y : A ⊗ B]] = str_{Γ,A,B}; ((lcon_{!Γ,A}; (disc_{Γ} ⊗ id_{[[A]]}); ri_{[[A]]})
⊗ (lcon_{!Γ,B}; (disc_{Γ} ⊗ id_{[[B]]}); ri_{[[B]]}))
= lcon_{!Γ,(A,B)}; (disc_{Γ} ⊗ id_{[[A⊗B]]}); ri_{[[A⊗B]]}

This means that

[[Γ; Δ ⊢ let x ⊗ y be t in x ⊗ y]] = str_{Γ, ,Δ}; (id_{[[Γ; ]]} ⊗ f); α_{[[Γ; ]],A,B}^{−1}; lcon_{!Γ,(AB)};
(disc_{Γ} ⊗ id_{A⊗B}); ri_{[[A]]})
= str_{Γ, ,Δ}; (id_{[[Γ; ]]} ⊗ f); (disc_{Γ} ⊗ id_{A⊗B}); ri_{A⊗B}
= str_{Γ, ,Δ}; (disc_{Γ} ⊗ f); ri_{A⊗B}
= f

! − β In this case,

[[Γ; Δ ⊢ let !x be !t in u : B]] =str_{Γ, ,Δ}; ((prom_{Γ}; F G(f)) ⊗ id_{[[Γ;Δ]]}); (id_{[[!A]]} ⊗ lcon_{!Γ,Δ_{2}});
(σ_{[[!A]],[[!Γ]]} ⊗ id_{[[Δ_{2}]]}); (lcon_{!Γ,!A}^{−1} ⊗ id_{[[Δ_{2}]]}); lcon_{!(Γ,A),Δ_{2}}^{−1}; g

which is just the interpretation of u[t/x]. λ − β In this case, assuming that [[Γ; Δ_{1}, A ⊢ t : B]] = f and [[Γ; Δ_{2} ⊢ u : A]] = g, we have

[[Γ; Δ_{1}, Δ_{2} ⊢ (λx.t)u : B]] =str_{Γ,(Δ_{1},A),Δ_{2}}; (λ(lcon_{(!Γ,Δ_{1}),A}^{−1}; f) ⊗ g); ap_{[[A]],[[B]]}
=str_{Γ,Δ_{1},Δ_{2}}; (id_{[[Γ;Δ_{1}]]} ⊗ g); lcon_{!Γ,Δ_{1}}^{−1}; f
=[[Γ; Δ_{1}, Δ_{2} ⊢ t[u/x] : B]]

Reflexivity, Transitivity and Symmetry These cases are all trivial because categor-

ical equality is a congruence. Contexts It can be shown by induction over the structure of an arbitrary context that if

u = t, then [[C[u]]] = [[C[t]]], assuming this is a well-formed equality. This shows soundness. ■

4.5 Constructing the Term Model

The first stage in establishing completeness is to define the term model of DILL. It is clear that we will as normal construct the term category to form the SMCC part of the model, but we will need to use a somewhat more complex construction to provide the CCC part.

4.5.1 The Term Category

We define the term category T (G) for the graph G as follows:

• Ob(T (G) ) are the types of DILL over the graph G

• T (G) (A, B) = {[(x, t)]| ; x : A ⊢ t : B}, where [(x, t)] is the equivalence class of (x, t) over the equivalence ≡ defined by:

\begin{matrix}(x, t) ≡ (x, u) & if ; x : A ⊢ t =_{B} u \\ (x, t) ≡ (y, t[y/x]) \end{matrix}

Now define identities and substitution:

• id_{A} = [(x, x)]

• [(x, t)]; [(y, u)] = [(x, u[t/y])]

Now it is easily demonstrated that these definitions give a category, given primitive results on substitution proved earlier. Further, we certainly have an appropriate interpretation function I which interprets the graph G into T (G) ; it is defined as follows:

I(f) = (z, f(z)) : A → B

where f ∈ G(A, B).

The next step is to show that the term category is in fact a SMCC. First we define:

[(x, t)] ⊗ [(y, u)] = [(z, let x ⊗ y be z in t ⊗ u)]
ri_{A} : I ⊗ A → A = (z, let x ⊗ y be z in let ∗ be x in y)
ri_{A}^{−1} : A → I ⊗ A = (x, ∗ ⊗ x)
li_{A} : A ⊗ I → A = (z, let x ⊗ y be z in let ∗ be y in x)
li_{A}^{−1} : A → A ⊗ I = (x, x ⊗ ∗)
α_{A,B,C} : A ⊗ (B ⊗ C) → (A ⊗ B) ⊗ C = (w, let x ⊗ u be w in let y ⊗ z be u in (x ⊗ y) ⊗ z)
α_{A,B,C}^{−1} : (A ⊗ B) ⊗ C → A ⊗ (B ⊗ C) = (w, let u ⊗ z be w in let x ⊗ y be u in x ⊗ (y ⊗ z))
σ_{A,B} : A ⊗ B → B ⊗ A = (z, let x ⊗ y be z in y ⊗ x)
σ_{A,B}^{−1} : B ⊗ A → A ⊗ B = σ_{B,A}

4.5.2 ⨂ is a Functor

We need to show that the definition given above of the tensor is functorial. This amounts to showing that identities are preserved:

[(x, x)] ⊗ [(y, y)] = (w, let x ⊗ y be w in x ⊗ y)
=  (w, w)
=  id

and that composition is preserved. We show this in the second place of the functor, but the proof for the first place is analogous.

[(x, x)] ⊗ ([(y, t)]; [(z, u)])
=  [(w, let x ⊗ y be w in x ⊗ (u[t/z]))]
= [(w, let x ⊗ z be let x ⊗ y be w in x ⊗ t in x ⊗ u)]
=  ([(x, x)] ⊗ [(y, t)]); ([(x, x)] ⊗ [(z, u)])

4.5.3 Naturality Issues

A SMCC must have natural isomorphisms as given above for the tensor. We need to check the naturality squares of each of these transformations in each variable.

ri_{A} There is one diagram to check here for naturality, and two equalities for isomorphism.

ri_{A}; (x, t)
=  (z, t[let x′ ⊗ y′ be z in let ∗ be x′ in y/x])
=  (z, let x′ ⊗ y′ be z in let ∗ be x′ in t[y/x])
=  (z′, let x′′ ⊗ x be z′ in let ∗ be x′′ in t)
= (z′, let x′ ⊗ y′ be let x′′ ⊗ x be z′ in x′′ ⊗ t in let ∗ be x′ in y′)
=  (id_{I} ⊗ (x, t)); ri_{B}

This shows the naturality of ri. Now we check that it is a natural isomorphism; in one direction we have:

ri_{A}; ri_{A}^{−1} = (z, ∗ ⊗ let x ⊗ y be z in let ∗ be x in y)
=  (z, z)

and in the other we have:

ri_{A}^{−1}; ri_{A} = (w, let x ⊗ y be ∗ ⊗ w in let ∗ be x in y)
=  (w, w)

li_{A} The diagrams in this case are exactly analogous to the above ones, and hence are omitted. α_{A,B,C} We first check naturality for this arrow.

α_{A,B,C}; ((x, t) ⊗ (y, u)) ⊗ (z, v)
= (w, let x′ ⊗ z
be (let x′′ ⊗ w′′ be w in let y′′ ⊗ z′′ be w′′ in (x′′ ⊗ y′′) ⊗ z′′)
in let x ⊗ y be x′ in (t ⊗ u) ⊗ v)
= (w, let x ⊗ w′ be w in let y ⊗ z be w′′ in (t ⊗ u) ⊗ v)
= (w′′, let x′ ⊗ w′
be let x ⊗ w′′′ be w′′ in let y ⊗ z be w′′′ in t ⊗ (u ⊗ v)
in let y′ ⊗ z′ be w′ in (x′ ⊗ y′) ⊗ z′
= (x, t) ⊗ ((y, u) ⊗ (z, v)); α_{D,E,F}

The isomorphism is easily seen.

σ_{A,B} We need to show naturality:

(x, t) ⊗ (y, u); σ_{A,B}
= (z, let x′ ⊗ y′ be let x ⊗ y be z in t ⊗ u in y′ ⊗ x′)
=  (z, let x ⊗ y be z in u ⊗ t)
= (z, let y ⊗ x be let x′ ⊗ y′ be z in y′ ⊗ x′ in u ⊗ t)

Again, the isomorphism is easily seen.

4.5.4 Coherence Diagrams

Now we need to show that the coherence equalities given earlier hold in the term category. We check these by number based on the numbering given in the definition. Because the demonstration for larger equalities consists of equalities between huge terms of DILL, we check here only equalities 2,3,5 and 6.

(2) LHS =

(z, let u ⊗ v be let u′ ⊗ z′ be z in let x′ ⊗ y′ be u′ in x′ ⊗ (y′ ⊗ z′)
in u ⊗ (let x ⊗ y be v in let ∗ be x in y))
= (z, let u′ ⊗ z′ be z in let x′ ⊗ y′ be u′ in x′ ⊗ (let ∗ be y′ in z′))
= (z, let u′ ⊗ z′ be z in let x′ ⊗ y′ be u′ in let ∗ be y′ in (x′ ⊗ z′))
= (z, let u′ ⊗ z′ be z in (let x′ ⊗ y′ be u′ in let ∗ be y′ in x′) ⊗ z′)
= RHS

(3) LHS =

(z, let x ⊗ y be z in let ∗ be y in x)
= (z, let x ⊗ y be z in let ∗ be y in let ∗ be x in ∗)
= (z, let x ⊗ y be z in let ∗ be x in y)
= RHS

(5) We show this by demonstrating σ_{A,B}; σ_{B,A} = id.

LHS = (z, let x ⊗ y be let x′ ⊗ y′ be z in y′ ⊗ x′ in y ⊗ x)
= (z, z)

(6) LHS =

(z, let x ⊗ y be let x′ ⊗ y′ be z in y′ ⊗ x′ in let ∗ be y in x)
= (z, let x′ ⊗ y′ be z in let ∗ be x′ in y′)
= RHS

At this point we have shown that the term category is an SMC. It only remains to demonstrate that a suitable candidate exists for the right adjoint of the tensor.

4.5.5 Closedness of the SMC

Define D(G)(A, B) = {(x, t)| ; x : A ⊢ t : B}. Then we have that

T (G)(A, B) = {[(x, t)]|(x, t) ∈ D(G)(A, B)}

We have the following series of isomorphisms:

D(G)(A ⊗ B, C) defined  {(x, t)| ; x : A ⊗ B ⊢ t : C}
≃  {(y, z, u)| ; y : A, z : B ⊢ u : C}
≃  {(y, v)| ; y : A ⊢ v : B−∘C}
defines  D(G)(A, B−∘C)

Now T (G) (A ⊗ B, C) = {[(x, t)]|(x, t) ∈ D(G)(A ⊗ B, C)} but by the isomorphism, this is the same as

{[(x, t)]|(x, t) ∈ D(G)(A, B−∘C)}

which is the definition of T (G) (A, B−∘C)

Hence −∘ is the required right adjoint to the tensor and we have an SMCC.

Having shown that the term category is a SMCC, and hence forms part of an LNL model, we now need to find a suitable candidate for the CCC part of this model. To do this, we will need an intermediate construction.

4.6 A Multicategory Construction

We give a construction which for any closed multicategory gives us a CCC in a uniform way. We can then construct a suitable CCC part for the term category as the CCC corresponding to a multicategory induced by the intuitionistic part of the context of DILL.

4.6.1 Definition of Multicategories A Multicategory (as defined for example in [9]) is a structure M having:

• A set of base objects Ob(M).

• For each sequence of objects Ā and single object B, a set of morphisms M(Ā, B).

• A composition

;_{Ā,B̄,C} : (×_{B_{i}∈B̄}M(Ā, B_{i})) × M(B̄, C) → M(Ā, C)

which for f_{i} : M(Ā, B_{i}) and g : M(B̄, C), is written

< f_{i} >_{i=1..n}; g : M(Ā, C)

The composition is associative, by which we mean

< f̄; g_{i} >_{i=1..n}; h = f̄; (< g_{i} >_{i=1..n}; h)

for all morphisms of appropriate types.

• Identities id_{A} : M(< A >, A) for each object A which have the property that < f > ; id_{A} = f for all arrows f having domain A.

• Projections π_{i} : M(< A_{j} >_{j=1..n}, A_{i}) s.t. the following equations hold:

β < f_{i} >_{i=1..n}; π_{j} = f_{j} η < π_{i} >_{i=1..n}; f = f

This is the definition of multicategory with a cartesian-product-style interpretation of the sequence. There is a corresponding definition which interprets the sequence as a tensor-product; this has no projections.

We now define a closed multicategory. 4.6.2 Closed Multicategory A Closed Multicategory is a multicategory M whose objects are closed under the binary operation → such that:

M(ĀB; C) = M(Ā; B → C)

4.7 Closed Multicategory to CCC

We now make explicit the connection between closed multicategories and CCCs by defining a category M_{seq} based upon the closed multicategory M, which will be a CCC.

Let the objects of M_{seq} be sequences of objects of M, {< A_{i} >_{i=1..n} |A_{i} ∈ Ob(M)}. Now define the morphisms

M_{seq}(Ā, < B_{i} >_{i=1..n}) = {< f_{i} >_{i=1..n} |f_{j} ∈ M(Ā, B_{j})}

Now we define the identities on M_{seq}. Define id_{<A_{i}>} as follows:

• If < A_{i} > is the empty sequence, then the identity is the unique empty sequence of arrows.

• If < A_{i} > has length 1, then the identity is the sequence of length one containing just the identity arrow id_{A_{1}} :< A_{1} >→ A_{1} from the multicategory.

• If < A_{i} >_{i=1..n} has length greater than one, then id_{<A_{i}>} for i = 1..n is the sequence < π_{i} >_{i=1..n} of projections in the multicategory.

We define the composition of two morphisms < f_{i} >_{i=1..n} and < g_{j} >_{j=1..m} as follows:

< f_{i} >_{i=1..n}; < g_{j} >_{j=1..m}=< (f̄; g_{j}) >_{j=1..m}

Now we can show that M_{seq} is a category. The identity equations are satisfied by virtue of the projection equalities in the multicategory, and the associativity of composition follows from that of the multicategory composition.

CCC We now give the definitions required to turn this into a CCC. Define Ā× B̄ = ĀB̄. Then the projections are given by < π_{i} >:< A_{j} >_{j=1..n}→< A_{i} >, and the pairing of two arrows f̄ and ḡ is the concatenation of the sequences f̄ḡ.

The projections and pairing satisfy the equalities of a CCC by virtue of the projection equalities of the multicategory.

Define 1 = ⟨⟩. Then an arrow from any type to 1 is the by the empty sequence of arrows, which is necessarily unique. So we have: 1Ā = ⟨⟩ : Ā → 1

Define < A_{i} >_{i=1..n}→< B_{j} >_{j=1..m}=< A_{i} → (A_{2}.. → (A_{n} → B_{j})..) >_{j=1..m} Now we can show the Cartesian closedness of the category with this definition of →

since

M_{seq}(ĀB, < C_{i} >_{i=1..n})
definition  = {< f_{i} >_{i=1..n} |f_{j} ∈ M(ĀB; C_{j})}
multicategory closure ≃ {< f_{i} >_{i=1..n} |f_{j} ∈ M(Ā; B → C_{j})}
definition = M_{seq}(Ā, < B → C_{i} >_{i=1..n})
definition  = M_{seq}(Ā, < B >→< C_{i} >_{i=1..n})

So we have that M_{seq} is a CCC for any multicategory M.

CCC to Closed Multicategory In a straightforward way, given any CCC C it is possible to define a closed multicategory C_{mul}. We will not use this fact in the development, but we note that (M_{seq})_{mul} = M.

4.8 The Term Multicategory T M(G)

Now we can provide an appropriate CCC for the term LNL-model as T M_{seq} for a suitable closed multicategory T M. We define this multicategory as follows:

The objects of the multicategory T M(G)will be precisely the objects of the term category T (G) , which are the types of D(G).

Now the morphisms of T M(G) are as follows:

T M(G)(Ā, B) = {[(x̄, t)]|x_{1} : A_{1}, ..., x_{n} : A_{n}; ⊢ t : B}

where [(x̄, t)] is the equivalence class of pairs under the equivalence ≡_{M} defined:

(x̄, t) ≡_{M} (ȳ, u) iff x̄ : Γ; ⊢ t =_{A} u[x̄/ȳ]

Now we can give the identities, projections and composition on the multicategory:

\begin{matrix}id_{A} :< A >→ A = & [(< x >, x)] \\ π_{i} :< A_{j} >_{j=1..n}→ A_{i} = & [(< x_{j} >_{j=1..n}, x_{i})] if i ∈ 1..n \\ < [(x̄, t_{i})] >_{i=1..n}; [(< y_{i} >_{i=1..n}, u)] = & [(x̄, u[t_{i}/y_{i}]_{i=1..n})] \end{matrix}

Now we need to verify that these definitions satisfy the multicategory equations.

Associativity of Composition: The right-hand side of the equation is defined as follows, where we let f_{i} be (t_{i}, x̄), g_{i} be (u_{j}, ȳ) and h be (v, z̄)

[(x̄, t_{i})]; [(ȳ, v[u_{i}/z_{i}])] = [(x̄, v[u_{i}/z_{i}][t_{j}/y_{j}])]
= [(x̄, v[u_{i}[t_{j}/y_{j}]/z_{i}])]
= [(x̄, u_{j}[t_{i}/y_{i}])]; [(z̄, v)]

as required.

The β-product rule: The left-hand side of the rule is as follows, where we use [(ȳ, t_{j})]

for f_{j}:

[(ȳ, x_{i}[t_{j}/x_{j}])] = [(ȳ, t_{i})]

again as required.

The η-product rule: The left-hand side of the rule is as follows, where we use [(ȳ, t)] for

f:

[(x̄, t[x_{j}/y_{j}])] = [(ȳ, t)]

by α-conversion, as required.

Now we can show that the multicategory T M(G) is a closed multicategory; let the binary operation A → B be defined by !A−∘B over the objects of the multicategory.

To show that the closure property of the → is satisfied, observe that:

T M(G)(ĀB; C) = {[(x̄y, t)]|x̄ : Ā, y : B; ⊢ t : C}
= {[(x̄y, u′)]|x̄ : Ā; y :!B ⊢ u′ : C}
= {[(x̄, u′′)]|x̄ : Ā; ⊢ u′′ :!B−∘C}

But this is the definition of the operator → in the multicategory.

Hence we have established that T M(G) is indeed a multicategory, and hence using the multicategory to CCC result given earlier, we have a CCC T M(G)_{seq}.

Convention From now on, we will abbreviate an arrow

< [(< x_{i} >_{i=1..n}, t_{j})] >_{j=1..m}

as

[(< x_{i} >_{i=1..n}, < t_{j} >_{j=1..m})]

4.9 T (G) is monoidally adjoint to T M(G)_{seq}

In order to prove that the two categories we have given (T (G) and T M(G)_{seq}) form a LNL model, we need to demonstrate that there exists a monoidal adjunction between them.

4.9.1 Functors F and G

We define the functors G : T (G) → T M(G)_{seq} and F : T M(G)_{seq} → T (G) :

G(A)  =  < A >
G([(x, t)])  =  < [(< x >, t)] >
F (< A_{i} >_{i=1..n})  =  ⨂_{i=1..n}!A_{i}
F (< [(x̄_{j=1..m}, t_{i})] >_{i=1..n}) = [(z, let ∗ be z in ⨂_{i=1..n}!t_{i})] if m = 0
[(z, let ⊗_{j=1..m}y_{m} be z
in let !x̄_{j=1..m} be ȳ in ⨂_{i=1..n}!t_{i})] if w > 0

where ⨂_{i=1..0}!t_{i} = ∗ and ⨂_{i=1..0}!A_{i} = I.

We show that these definitions are functorial. It is easy to see that G preserves identities and composition, but more tricky for F. To show that it preserves identities:

F (id⟨⟩)
=  F (⟨⟩, ⟨⟩)
=  [(z, let ∗ be z in ⨂_{i=1..0}!t_{i})]
=  [(z, let ∗ be z in ∗)]
=  id_{I}
F (id_{<A_{i}>_{i=1..(n+1)}})
=  F (< π_{i=1..(n+1)} >)
= (z, let ⨂_{j=1..(n+1)} y_{j} be z in let !x̄_{j=1..(n+1)} be ȳ in (⨂_{i=1..(n+1)}!x_{i}))
=  (z, let ⨂_{j=1..(n+1)} y_{j} be z in ⨂_{i=1..(n+1)}(let !x_{i} be y_{i} in !x_{i}))
=  (z, let ⨂_{j=1..(n+1)} y_{j} be z in (⨂_{i=1..(n+1)} y_{i}))
=  (z, z)
=  id_{(⨂_{i=1..(n+1)}!A_{i})}

To show that it preserves composition, there are a number of cases:

• If [(< x_{i} >_{i=1..(n+1)}, ⟨⟩)] :< A_{i} >_{i=1..(n+1)}→ ⟨⟩ and

[(⟨⟩, < t_{j} >)]_{j=1..(m+1)} = g : ⟨⟩ →< B_{j} >_{j=1..(m+1)}

then

F (⟨⟩; g)
=  F ([(< x_{i} >, ⟨⟩)]; [(⟨⟩, < t_{j} >)])
=  F (< [(< x_{i} >, t_{j})] >)
= (z, let ⊗_{i=1..(n+1)}y_{i} be z in let !x̄ be ȳ in ⨂_{j=1..(m+1)}!t_{j})
=  (z, let ⊗_{i=1..(n+1)}y_{i} be z in let !x̄ be ȳ in ∗);
(z, let ∗ be z in ⨂_{j=1..(m+1)}!t_{j})
=  F (⟨⟩); F (g)

• If [(⟨⟩, < t_{i} >)] =< f_{i} >_{i=1..(n+1)}: ⟨⟩ →< A_{i} >_{i=1..(n+1)} and

[(< y_{i} >, < u_{j} >)] =< g_{j} >_{j=1..m}:< A_{i} >_{i=1..(n+1)}→< B_{j} >_{j=1..m}

then

F (< f_{i} >; < g_{j} >)

=  F (< [(⟨⟩, t_{i})] >; < [(< y_{i} >, u_{j})] >)
=  F (< [(⟨⟩, u_{j}[t̄/ȳ])] >)
=  (z, let ∗ be y in (⨂_{j=1..m}!u_{j}[t̄/ȳ]))
= (w, let ⊗z̄ be (let ∗ be w in ⨂!t_{i} in )let !ȳ be z̄ in ⨂!u_{j})
=  F ([(⟨⟩, < t_{i} >)]); F ([(ȳ, < u_{j} >)])
=  F (< f_{i} >); F (< g_{j} >)

• If

< [(x̄_{i=1..(n+1)}, t_{j})] >=< f_{j} >_{j=1..(m+1)}:< A_{i} >_{i=1..(n+1)}→< B_{j} >_{j=1..(m+1)} and

< [(< y_{j} >, u_{k})] >=< g_{k} >_{k=1..m}:< B_{j} >_{j=1..(m+1)}→< C_{k} >_{k=1..p}

then

F (< f_{j} >; < g_{k} >)
=  F (< [(x̄, t_{j})] >; < [(ȳ, u_{k})] >)
=  F (< [(x̄, u_{k}[t̄/ȳ])] >)
=  (z, let ⊗ȳ be z in let !x̄ be ȳ in ⨂!u_{k}[t̄/ȳ])
= (w, let ⊗v̄ be (let ⊗ȳ′ be w in let !x̄ be ȳ′ in ⨂!t_{j}) in let !ȳ be v̄ in ⨂!u_{k})
=  F (< [(x̄, t_{j})] >); F ([(ȳ, u_{k})])
=  F (< f_{j} >); F (< g_{k} >)

4.9.2 The Adjunction We need to establish that there is an adjunction between T (G) and T M(G)_{seq}.

T M(G)_{seq}(< A_{i} >_{i=1..n}, G(B)) =^{def}  T M(G)_{seq}(< A_{i} >_{i=1..n}, < B >)
=^{def}  {< f > |f ∈ T M(G)(< A_{i} >_{i=1..n}, B)}
=^{def} {< [(< x_{i} >_{i=1..n}, t)] > |x_{1} : A_{1}, ...x_{n} : A_{n}; ⊢ t : B}
≃  {< (y, u) > | ; y : ⨂_{i=1..n}!A_{i}) ⊢ u : B}
≃  {< f > |f ∈ T (G) (F (< A_{i} >_{i=1..n}), B)}
≃  T (G) (F (< A_{i} >_{i=1..n}), B)

4.9.3 Monoidality We now need to check that the adjunction is monoidal. This involves various steps.

Monoidal Functors We need to show that both F and G are monoidal functors. This involves giving natural transformations:

(⟨⟩, < ∗ >) = m⟨⟩^{G} : ⟨⟩ → G(I)
(< x, y >, < x ⊗ y >) = m_{A,B}^{G} : G(A)G(B) → G(A ⊗ B)
(z, z) = m_{I}^{F} : I → F (⟨⟩)
(z, z)  = m_{A,B}^{F} : F (Ā) ⊗ F (B̄) → F (ĀB̄)
for Ā ≠ ⟨⟩ ≠ B̄
li_{F Ā}  = m_{Ā,⟨⟩}^{F} : F (Ā) ⊗ F (⟨⟩) → F (Ā)
ri_{F Ā}  = m_{⟨⟩,Ā}^{F} : F (⟨⟩) ⊗ F (Ā) → F (Ā)

We must now check naturality and certain coherence conditions. We first observe that naturality is trivial for the identity.

Naturality of m^{G} Assume that f = (x, < t >) and that g = (y, < u >). Then

LHS = (G(f) × G(g)); m^{G}
= (< xy >, < tu >); (< xy >, < x ⊗ y >)
= (< xy >, t ⊗ u)
= (< xy >, < x ⊗ y >); (< z >, < let x ⊗ y be z in t ⊗ u >)
= m^{G}; G(f ⊗ g)
= RHS

(8) for m^{F} Since m^{F} is the identity, this equality is trivial by definition.

(9) for m^{F}

LHS = (z, let x ⊗ y be z in y ⊗ x)
= (z, let x′ ⊗ y′ be z in let ! < xy > be < x′y′ > in !y⊗!x)
= F (< xy >, < yx >)
= RHS

(8) for m^{G} LHS =

(< x >, < x >)

= (< x >, < ∗ ⊗ x >); (< z >, < let x ⊗ y be z in let ∗ be x in y >)
= (< x >, < ∗x >); (xy, < x ⊗ y >);
G(z, let x ⊗ y be z in let ∗ be x in y)
= RHS

(9) for m^{G}

LHS = (< xy >, < yx >); (< xy >, < x ⊗ y >)
= (< xy >, < y ⊗ x >)
= (< xy >, < x ⊗ y >); (< z >, < let x ⊗ y be z in y ⊗ x >)
= (< xy >, < x ⊗ y >); G(z, let x ⊗ y be z in y ⊗ x)
= RHS

Monoidal Adjunction We also need to show that the adjunction is monoidal, ie that the unit and counit of the adjunction are monoidal natural transformations. We give the unit and counit, and the composite monoidality maps for F G and GF:

(z, let !x be z in x)  : ϵ_{A} : F GA → A
(< x_{i} >_{i=1..n}, < ⨂_{i=1..n}!x_{i} >)  : ηĀ : Ā → GF (Ā)
(z, let ∗ be z in !∗)  : m_{I}^{F G} : I → F GI
(z, let x ⊗ y be z in
let ! < x′y′ > be < xy > in !(x ⊗ y)) : m_{A,B}^{F G} : F GA ⊗ F GB → F G(A ⊗ B)
(⟨⟩, < ∗ >)  : m⟨⟩^{GF} : ⟨⟩ → GF (⟨⟩)
(< x̄ȳ >), (< xy >, < x ⊗ y >) : m_{Ā,B̄}^{GF} : GF ĀGF B̄ → GF (ĀB̄)

We now need to check certain coherence conditions:

(10) for ϵ

LHS
=  (z, let x ⊗ y be z in let !x′ be x in x′ ⊗ let !y′ be y in y′)
=  (z, let x ⊗ y be z in let ! < x′y′ > be < xy > in x′ ⊗ y′)
=  (z, let !x′′ be let x ⊗ y be z in let ! < x′y′ > be < xy > in !(x′ ⊗ y′) in x′′)
= (z, let x ⊗ y be z in let ! < x′y′ > be < xy > in !(x′ ⊗ y′)); (z, let !x′′ be z in x′′)
=  RHS

(11) for ϵ

LHS = (z, let ∗ be z in !∗); (z, let !x be z in x)
= (z, z)
= RHS

(10) for η

LHS
= (< x_{i}, y_{j} >_{i=1..n,j=1..m}, < ⨂_{i=1..n}!x_{i}, ⨂_{j=1..m}!y_{j} >); (< xy >, < x ⊗ y >)
= (< x_{i}, y_{j} >_{i=1..n,j=1..m}, < ⨂_{i=1..n,j=1..m}!x_{i}, y_{j} >)
= RHS

(11) for η

LHS = (⟨⟩, < ⨂_{i=1..0}!x_{i} >)
= (⟨⟩, < ∗ >)
= RHS

We have now demonstrated that T (G) is monoidally adjoint to T M(G)_{seq}, and hence this pair forms a term LNL-model, as originally required.

4.10 Completeness

We now have a term model of D(G) which is an LNL model. In order to prove completeness, it now suffices to prove a lemma:

Lemma 4.3 [[x̄ : Γ; ȳ : Δ ⊢ t : A]] = (w, let z̄ȳ be w in let !x̄ be z̄ in t) in the SMCC part of the term model.

Proof We prove this lemma by induction over the structure of the term.

Now completeness is easy:

Theorem 2 (Completeness) For terms t and u provable in the same context Γ; Δ:

Γ; Δ ⊢ t =_{A} u if and only if [[Γ; Δ ⊢ t : A]] = [[Γ; Δ ⊢ u : A]] in every LNL model of D(G).

Proof We have the forward direction of the implication as soundness proved earlier. As for the other direction, assume that [[t]] = [[u]]. Then since the term model is an LNL model we have by the lemma that

(w, let z̄ȳ be w in let !x̄ be z̄ in t) = (w, let z̄ȳ be w in let !x̄ be z̄ in u)

and hence we have

; w : ⨂_{A∈!Γ,Δ}(A) ⊢ let z̄ȳ be w in let !x̄ be z̄ in t =_{B} let z̄ȳ be w in let !x̄ be z̄ in t

But now it follows that if we substitute ⨂!x̄, ȳ for w in both terms we still have an equality. However, under this substitution, we have:

let z̄ȳ be (⨂!x̄, ȳ) in let !x̄ be z̄ in t =_{βη−cc} t

and hence

Γ; Δ ⊢ t =_{B} u

as required. ■

5 Relating DILL and ILL

We now show that DILL is a conservative extension of ILL, by which we mean that we give a translation from DILL to ILL and one in the reverse direction, such that two terms are equal in ILL if and only if their images are equal in DILL. Further, we show that the sub type-system of DILL consisting of terms t derivable with no intuitionistic assumptions, ; Δ ⊢ t : A, is isomorphic to the type system ILL.

5.1 The System ILL

We give the equalities and rules for the exponential part of the system of ILL we will use in the appendix. Wherever numbers are used to refer to particular equalities, those numbers are as given in the appendix.

Vector Notation We use a vector notation in order to reduce the complexity of the rules. We take t⃗ to represent a sequence of terms t_{1}, t_{2}..t_{n} for some n, and denote the empty vector by ⟨⟩. This construction, and in particular the case where all the terms t_{i} are variables (denoted x_{1}, x_{2}...x_{n} for some n) is used in the promote construct. Also, following Benton, we use the form (discard t⃗ in u) to abbreviate (discard x_{1} in discard x_{2} in... in u). We also use (copy t⃗ for x⃗, y⃗ in u) to abbreviate (copy t_{1} for x_{1}, y_{1} in copy t_{2} for x_{2}, y_{2} in .... in u). Further, when we come to define the translations, we will use the analogous abbreviation (let !x⃗ be u⃗ in t) to indicate the term

let !x_{1} be u_{1} in let !x_{2} be u_{2} in ...t

in DILL type theory.

We use a subscript on the turnstile to differentiate between proof systems where necessary, so that for example the statement of lemma 5.1.1 below is to be read:

If Δ ⊢ t : A in the type system ILL, then ; Δ ⊢ Φ(t) : A in the type system DILL

5.2 The Translations

We will define two translations, having types:

Φ : ILL → DILL
Ψ_{V} : DILL → ILL

The subscript V in the translation Ψ is a vector indicating which variables are to be regarded as intuitionistic. This is necessary since we use the same global variable set for both types of environment.

These translations will be the identity on types, further reinforcing the intuition that the type constructors of DILL are those familiar in ILL. We summarise their crucial properties here; we will prove:

Lemma 5.1 (Properties of the Translations) The following are properties of Φ and Ψ:

1. If Δ ⊢ILL t : A, then ; Δ ⊢DILL Φ(t) : A

2. If x⃗ : Γ; Δ ⊢DILL u : A, then x⃗ :!Γ, Δ ⊢ILL Ψx⃗(u) : A

3. If Δ ⊢ILL t =_{A} u, then ; Δ ⊢DILL Φ(t) =_{A} Φ(u)

4. If x⃗ : Γ; Δ ⊢DILL t =_{A} u, then x⃗ :!Γ, Δ ⊢ILL Ψx⃗(t) =_{A} Ψx⃗(u)

5. If Δ ⊢ILL t : A, then Δ ⊢ILL Ψ⟨⟩(Φ(t)) =_{A} t

6. If ; Δ ⊢DILL t : A, then ; Δ ⊢DILL Φ(Ψ⟨⟩(t)) =_{A} t

Given these lemmas, we can prove:

Theorem 3 (Conservative Extension) • Δ ⊢ILL t =_{A} u iff ; Δ ⊢DILL Φ(t) =_{A} Φ(u)

• ; Δ ⊢DILL t =_{A} u iff Δ ⊢ILL Ψ⟨⟩(t) =_{A} Ψ⟨⟩(u)

Proof The two proofs are almost identical. Consider the first case. We already have the implication

Δ ⊢ILL t =_{A} u implies ; Δ ⊢DILL Φ(t) =_{A} Φ(u)

Now assume ; Δ ⊢DILL Φ(t) = Φ(u). By lemma 5.1.4, we have that Δ ⊢ILL Ψ⟨⟩(Φ(t)) =_{A} Ψ⟨⟩(Φ(u)), but we also have by lemma 5.1.5 that Δ ⊢ILL Ψ⟨⟩(Φ(t)) =_{A} t, and hence the other direction of the implication holds.

The proof of the second case uses the analogous results in lemma 5.1.3 and 5.1.6 ■

We now proceed to prove lemma 5.1, and hence the results of theorem 3 hold. Those readers not wishing to examine the somewhat complex term manipulations which these proofs consist of can readily skip to the end of this section.

5.3 From Intuitionistic Linear Logic to DILL

Now we can define the translation of terms Φ from intuitionistic linear type theory ILL to DILL. In order to make this definition, we need to assume that we are using ILL over the same graph G of primitive types and arrows.

5.3.1 Definition of Φ

On Types we define Φ to be the identity, since every type in DILL is intended to have the same interpretation as the corresponding type of ILL.

On Terms we define Φ as follows:

Φ(x)  =  x
Φ(f(t))  =  f(Φ(t))
Φ(∗)  =  ∗
Φ(let ∗ be t in u)  =  let ∗ be Φ(t) in Φ(u)
Φ(t ⊗ u)  =  Φ(t) ⊗ Φ(u)
Φ(let x ⊗ y : A ⊗ B be t in v) = let x ⊗ y : A ⊗ B be Φ(t) in Φ(v)
Φ(λx : A.t)  =  λx : A.Φ(t)
Φ(tu)  =  Φ(t)Φ(u)
Φ(discard t in u)  =  let !z be Φ(t) in Φ(u)
Φ(copy t for x :!A, y :!A in u) = let !z : A be Φ(t) in Φ(u)[!z/x, y]
Φ(derelict(t)) = let !z be Φ(t) in z
Φ(promote t⃗ for x⃗ : !A in u) = let !z⃗ : A⃗ be Φ⃗(t) in !(Φ(u)[!z⃗/x⃗])

where in the last four rules z is taken from an infinite set of fresh free variables. Now we need to prove the lemma.

Lemma 5.1.1 If Δ ⊢ILL t : A, then ; Δ ⊢DILL Φ(t) : A.

Proof This proof is by induction over the structure of the term t. We give a summary proof only.

Axiom Instance: In this case, we have x : A ⊢ x : A, so that the translation is ; x : A ⊢ x : A, which is derivable.

Primitive arrow, Unit-I and Unit-E: In these cases there is almost nothing to show, as the corresponding typing rules in DILL are analogous. We note the requirement that we have the same primitive arrows in each type theory.

⊗-Introduction: We present this case as an example of these simple cases. We have the

derivation

\begin{matrix}Δ_{1} ⊢ v : A & Δ_{2} ⊢ u : B \\ Δ_{1}, Δ_{2} ⊢ v ⊗ u : A ⊗ B \end{matrix} (⊗ − I)

By the inductive hypothesis, we have ; Δ_{1} ⊢ Φ(v) : A, and ; Δ_{2} ⊢ Φ(u) : A, so we have ; Δ_{1}, Δ_{2} ⊢ Φ(v) ⊗ Φ(u) : A ⊗ B via the ⊗-introduction rule of DILL. But Φ(v ⊗ u) = Φ(v) ⊗ Φ(u), so we are done.

⊗-E,−∘-I and −∘-E: Again these rules in ILL are exactly parallelled in DILL.

Weakening Rule: In this case, we have the derivation Δ_{1} ⊢ t : B Δ_{2} ⊢ u :!A

Δ_{1}, Δ_{2} ⊢ discard u in t : B

By intuitionistic weakening and our inductive hypothesis, we have z : A; Δ_{1} ⊢ Φ(t) : B. Now by one application of our !-E rule gives us ; Δ_{1}, Δ_{2} ⊢ let !z be Φ(u) in Φ(t) : B, which is precisely Φ(discard u in t).

Contraction: In this case, we have the derivation in ILL:

Δ ⊢ u :!A Γ, x :!A, y :!A ⊢ v : B
Δ, Γ ⊢ copy u for x, y in v : B

Now by the inductive hypothesis, we have the derivations:

; Δ ⊢ Φ(u) :!A

and

; Γ, x :!A, y :!A ⊢ Φ(v) : B

in DILL. But now, using the substitution lemmas of DILL and the !-I,E pair, we have the following derivation:

; Γ, Δ ⊢ let !z be Φ(u) in Φ(v)[!z/x, y]

which proves the case.

Dereliction: In this case we have the derivation

Γ ⊢ t :!A

Γ ⊢ derelict t : A

in ILL. Using the inductive hypothesis, we have in DILL that

; Γ ⊢ Φ(t) :!A

so using one instance of !-E we have

; Γ ⊢ let !z be Φ(t) in z : A

as required.

Promotion Rule: The derivation here is

Δ_{i} ⊢ t_{i} :!A_{i} {x_{i} :!A_{i}}_{i∈I} ⊢ u : B
Δ_{i} ⊢ promote t⃗ for x⃗ in u : B

By our remark, and the inductive hypothesis, we have {z_{i} : A_{i}}_{i∈I}; ⊢ Φ(u)[!z⃗/x⃗] : B. Hence, by the promotion rule of DILL, we have

{z_{i} : A_{i}}_{i∈I}; ⊢!Φ(u)[!z⃗/x⃗] :!B

We also have ; Δ_{i} ⊢ Φ(t_{i}) :!A_{i} for each i ∈ I. Hence, by I applications of the !-E rule, we have

; Δ_{i} ⊢ let !z be Φ⃗(t) in !Φ(u)[!z⃗/x⃗] : B

since we understand let !z be in to be a sequence of let constructions. This is precisely what is given in the translations. ■

We now give one auxiliary lemma:

Lemma 5.2 We have that for terms t : B and u : A of ILL, where t has a free variable x : A,

Φ(t[u/x]) = Φ(t)[Φ(u)/x]

This is easily proved by induction over the first term, t, and we leave them to the reader.

Another important lemma is as follows:

Lemma 5.1.3 If Δ ⊢ILL t =_{A} u, then ; Δ ⊢DILL Φ(t) =_{A} Φ(u).

Proof This is proved by induction over the derivation of the equality t =_{A} u in ILL. First we consider all the one-step derivations, ie those consisting of basic equalities. However, since there are a large number of these, most of which are identical to the equalities already given in DILL, we give the proof only for the substantially different ones, that is those equalities concerning the ! term constructs which are summarised in the appendix. We also need to mention the basic logical rules for equality, which we have assumed are presented in the same way for ILL as we have presented them for DILL. Having said that, the reflexivity, transitivity and congruence of the image of the equality on ILL is easy to show. The numbers refer to the numbering of the equalities in the appendix.

1): In this case, Φ(t) is

let !w be (let !z be Φ⃗(e) in !Φ(t)[!z⃗/x⃗]) in w

This is equivalent by a commuting conversion (since w and z_{i} are fresh) to

let !z be Φ⃗(e) in (let !w be !Φ(t)[!z⃗/x⃗] in w)

In this term, (let !w be !Φ(t)[!z⃗/x⃗] in w) is β-equal to Φ(t)[!z⃗/x⃗]. This gives us

(let !z be Φ⃗(e) in (Φ(t)[!z⃗/x⃗]))

Now by using commuting conversions and η-equality, this reduces to Φ(t)[Φ⃗(e)/x⃗], which is Φ applied to the right-hand side.

2): In this case, Φ(t) is

let !w be (let !z be Φ⃗(e) in !Φ(t)[!z⃗/x⃗]) in Φ(u)

This is equivalent by a commuting conversion (since w and z_{i} are fresh) to

let !z be Φ⃗(e) in (let !w be !Φ(t)[!z⃗/x⃗] in Φ(u))

We know, however, that w does not occur in Φ(u), as it is fresh, so this is equal to (let !z be Φ⃗(e) in Φ(u)), which is precisely Φ applied to the right-hand side.

3): In this case we have that the image of the left hand side is let !w be Φ(u) in Φ(C)[Φ(v)]. Now by the fact that the context in ILL is linear, and the translation of the linear context C[ ] to DILL is linear, we have by commuting conversions that this is equal to

Φ(C)[let w be Φ(u) in Φ(v)]

which is precisely the image of the right-hand side.

4): This case is analogous to the previous one, since this is another commuting conversion.

5): In this case, Φ(t) is

let !w_{1} be z in !(let !w_{2} be x in w_{2})[!w_{1}/x]

This is

let !w_{1} be z in !(let !w_{2} be !w_{1} in w_{2})

which β-reduces to

let !w_{1} be z in !w_{1}

which is η-equal to z, which is Φ(z).

6): In this case, the image of the left-hand side is:

let !w be Φ(e) in Φ(u)[!w/x, y]

which is easily seen to be the image of the right-hand side since we are using a multiple substitution (substitution of a term simultaneously for a set of variables).

7): In this case the image of the left-hand side is

let !w_{1} be Φ(e) in (let !w_{2} be x in Φ(u))[!w_{1}/x, y]

which is equal to

let !w_{1} be Φ(e) in (let !w_{2} be !w_{1} in Φ(u))[!w_{1}/y]

but by one β-equality this is

let !w_{1} be Φ(e) in Φ(u)[!w_{1}/y]

so we can now see that via commuting conversions and an η-equality this is the image of the right-hand side, ie Φ(v)[Φ(e)/y]

8): In this case the left hand side of the equality has image

let !w_{1} be Φ(e) in (let !w_{2} be w in Φ(u)[!w_{2}/y, z])[!w_{1}/x, w]

but this is equal to

let !w_{1} be Φ(e) in (let !w_{2} be !w_{1} in Φ(u)[!w_{2}/y, z])[!w_{1}/x]

However, by a β-equality this is equal to

let !w_{1} be Φ(e) in Φ(u)[!w_{1}/x, y, z]

and by a similar process we can see that the image of the right-hand side is also equal to this term.

9): In this case, Φ(t) is

let !w_{1},!w⃗_{2} be Φ(f), Φ⃗(e) in !(let !w_{3} be y in Φ(v))[!w_{1},!w⃗_{2}/y, x⃗]

which is

let !w_{1},!w⃗_{2} be Φ(f), Φ⃗(e) in !(let !w_{3} be !w_{1} in Φ(v))[!w⃗_{2}/x⃗]

which is β-equal to

let !w_{1},!w⃗_{2} be Φ(f), Φ⃗(e) in !Φ(v)[w_{1},!w⃗_{2}/w_{3}, x⃗]

This is

let !w_{1} be Φ(f) in (let !w⃗_{2} be Φ⃗(e) in !Φ(v)[w_{1},!w⃗_{2}/w_{3}, x⃗])

but we know that w_{3} does not occur in Φ(v), so this is

let !w_{1} be Φ(f) in (let !w⃗_{2} be Φ⃗(e) in !Φ(v)[!w⃗_{2}/x⃗])

which is Φ(u). 10): In this case, Φ(t) is

let !w_{1} be (let !w_{2} be Φ⃗(e) in !Φ(t)[!w⃗_{2}/x⃗]) in Φ(u)[!w_{1}/y, z]

This is equivalent, again by a commuting conversion, to

let !w_{2} be Φ⃗(e) in (let !w_{1} be !Φ(t)[!w⃗_{2}/x⃗] in Φ(u)[!w_{1}/y, z])

Now this is β-equal to

let !w_{2} be Φ⃗(e) in (!Φ(u)[!Φ(t)[!w⃗_{2}/x⃗]/y, z])

But !Φ(u)[!Φ(t)[!w⃗_{2}/x⃗]/y, z] is β-equal to !Φ(u)[let !w⃗_{3} be !w⃗_{2} in !Φ(t)[!w⃗_{3}/x⃗]/_{y,z}] And this in turn is the same as

!Φ(u)[(let !w⃗_{3} be x⃗′ in !Φ(t)[!w⃗_{3}/x⃗]), (let !w⃗_{3} be x⃗′′ in !Φ(t)[!w⃗_{3}/x⃗])/_{y,z}][!w⃗_{2}/x⃗′, x⃗′′] which is

Φ(u[(promote x⃗′ for x in t), (promote x⃗′′ for x in t)/y, z][!w⃗_{2}/x⃗′, x⃗′′]) Therefore,

Φ(t) =_{β} let !w⃗_{2} be Φ⃗(e) in

(Φ(u[(promote x⃗′ for x in t), (promote x⃗′′ for x in t)/y, z][!w⃗_{2}/x⃗′, x⃗′′])) But this is precisely

Φ(copy e⃗ for x⃗′, x⃗′′ in u[(promote x⃗′ for x⃗ in t), (promote x⃗′′ for x⃗ in t)/_{y,z}]) so we are done.

11): In this case, Φ(t) is

let !w_{1},!w⃗_{2} be Φ(f), Φ⃗(e) in !(let !w_{3} be w in Φ(v)[!w_{3}/x, y])[!w_{1},!w⃗_{2}/w, z⃗] This is

let !w_{1},!w⃗_{2} be Φ(f), Φ⃗(e) in !(let !w_{3} be !w_{1} in Φ(v)[!w_{3}/x, y,!w⃗_{2}/z⃗]) which is β-equal to

let !w_{1},!w⃗_{2} be Φ(f), Φ⃗(e) in !(Φ(v)[!w_{1}/x, y,!w⃗_{2}/z⃗])

and this is η-equal to

let !w_{1} be Φ(f) in (let !w⃗_{2} be Φ⃗(e) in !(Φ(v)[!w_{1}/x, y,!w⃗_{2}/z⃗]))

But this is η-equal to the translation of the right-hand side. 12): The image of the left-hand side of this equality is

let !w_{1},!w⃗_{2} be (let !w⃗_{3} be z⃗ in !Φ(f)[!w⃗_{3}/z⃗]), w⃗ in !Φ(g)[!w_{1},!w⃗_{2}/y, y⃗] By commuting conversions this is equal to

let !w⃗_{3} be z⃗ in (let !w_{1},!w⃗_{2} be !Φ(f)[!w⃗_{3}/z⃗], w⃗ in !Φ(g)[!w_{1},!w⃗_{2}/y, y⃗]) This then is η-equal to

let !w⃗_{3} be z⃗ in (let !w⃗_{2} be w⃗ in !Φ(g)[!Φ(f)[!w⃗_{3}/z⃗],!w⃗_{2}/y, y⃗])

This is abbreviated to

let !w⃗_{3},!w⃗_{2} be z⃗, w⃗ in (!Φ(g)[!Φ(f)[!w⃗_{3}/z⃗],!w⃗_{2}/y, y⃗])

But by an η-equality this is equal to

let !w⃗_{3},!w⃗_{2} be z⃗, w⃗ in (!Φ(g)[(let !w⃗_{4} be !w⃗_{3} in !Φ(f)[!w⃗_{4}/z⃗]),!w⃗_{2}/y, y⃗])

and this can be written as

let !w⃗_{3},!w⃗_{2} be z⃗, w⃗ in (!Φ(g)[let !w⃗_{4} be !z⃗′ in !Φ(f)[!w⃗_{4}/z⃗]/y])[!w⃗_{3},!w⃗_{2}/z⃗′, y⃗]

But now this is the image of the right-hand side.

■

5.4 From DILL to Intuitionistic Linear Logic

There is a slight complication to the translation from DILL to ILL, because we need to make a distinction between variables which annotate types in the intuitionistic segment and those which annotate variables in the linear segment. Hence we annotate the mapping Ψ with a subscripted vector V which indicates those variables supposed to annotate intuitionistic assumptions.

5.4.1 Definition of Ψ

Again, we need to assume that we are using the same graph of primitive type and functions in both systems.

Define Ψ_{V} on types as the identity.

Define Ψ_{V} on terms as follows.

Ψy⃗(x : A) = discard y⃗ in x if x ∉ y⃗
Ψ_{y⃗x}(x : A) = discard y⃗ in derelict x
Ψy⃗(f(t)) = f(Ψy⃗(t))
Ψy⃗(∗) = discard y⃗ in ∗
Ψy⃗(let ∗ be t in u) = copy y⃗ for y⃗_{1}, y⃗_{2} in (let ∗ be Ψy⃗_{1}(t[y⃗_{1}/y⃗]) in Ψy⃗_{2}(u[y⃗_{2}/y⃗]))
Ψy⃗(t ⊗ u) = copy y⃗ for y⃗_{1}, y⃗_{2} in Ψy⃗_{1}(t[y⃗_{1}/y⃗]) ⊗ Ψy⃗_{2}(u[y⃗_{2}/y⃗])
Ψy⃗(let x ⊗ z : A ⊗ B be t in u) = copy y⃗ for y⃗_{1}, y⃗_{2} in p_{1}
where p_{1} = (let x ⊗ z : A ⊗ B be Ψy⃗_{1}(t[y⃗_{1}/y⃗]) in Ψy⃗_{2}(u[y⃗_{2}/y⃗]))
Ψy⃗(λx : A.t) = λx : A.Ψy⃗(t)
Ψy⃗(tu) = copy y⃗ for y⃗_{1}, y⃗_{2} in Ψy⃗_{1}(t[y⃗_{1}/y⃗])Ψy⃗_{2}(u[y⃗_{2}/y⃗])
Ψy⃗(!t) = promote y⃗ for y⃗_{1} in Ψy⃗_{1}(t[y⃗_{1}/y⃗])
Ψy⃗(let !x : A be t in u) = copy y⃗ for y⃗_{1}, y⃗_{2} in Ψ_{y⃗_{2},x}(u[y⃗_{2}/y⃗])[Ψy⃗_{1}(t[y⃗_{1}/y⃗])/x]

where y⃗_{1} and y⃗_{2} are vectors of variables taken from the infinite set of unused variables. Now we prove the first, and fundamental, lemma about this translation:

Lemma 5.1.2 If y⃗; Γ; Δ ⊢DILL t : A, then y⃗ :!Γ, Δ ⊢ILL Ψy⃗(t) : A.

Proof This is proved by induction over the first derivation. We leave most of this proof, as it is routine, but we consider the tensor introduction as a sample case, and also the rules for ! as they are significantly different.

Axioms, Unit Rules and Primitive Arrow: These cases are all essentially trivial, and we leave them here.

Tensor Introduction We have in this case that there is a deduction in DILL

\begin{matrix}y⃗ : Γ; Δ_{1} ⊢ u : A & y⃗ : Γ; Δ_{2} ⊢ v : B \\ y⃗ : Γ; Δ_{1}, Δ_{2} ⊢ u ⊗ v : A ⊗ B \end{matrix}

By the inductive hypothesis we have that there exist derivations in ILL (using some α-conversion):

y⃗_{1} :!Γ, Δ_{1} ⊢ Ψy⃗_{1}(u[y⃗_{1}/y⃗]) : A ⊗ B

and

y⃗_{2} :!Γ, Δ_{2} ⊢ Ψy⃗_{2}(v[y⃗_{2}/y⃗]) : A ⊗ B

Now we have by the tensor introduction in ILL

y⃗_{1} :!Γ, y⃗_{2} :!Γ, Δ_{1}, Δ_{2} ⊢ Ψy⃗_{1}(u[y⃗_{1}/y⃗]) ⊗ Ψy⃗_{2}(v[y⃗_{2}/y⃗]) : A ⊗ B

But by a sequence of copies, we can now obtain:

y⃗ :!Γ, Δ_{1}, Δ_{2} ⊢ copy y⃗ for y⃗_{1}, y⃗_{2} in Ψy⃗_{1}(u[y⃗_{1}/y⃗]) ⊗ Ψy⃗_{2}(v[y⃗_{2}/y⃗]) : A ⊗ B

which is precisely the image of the tensor. In fact, the technique of modelling the shared intuitionistic context with repeated contractions accounts for all of the copy constructs in the definition of Ψ.

!-Introduction In this case, we have the following deduction in DILL:

{y⃗ : Γ; ⊢ t : A \atop y⃗ : Γ; ⊢!t :!A}

By the inductive hypothesis, we have a derivation in ILL (using some α-conversion)

y⃗′ :!Γ ⊢ Ψy⃗′(t[y⃗′/y⃗]) : A

Now by one use of promotion, we have

y⃗ :!Γ ⊢ promote y⃗ for y⃗′ in Ψy⃗′(t[y⃗′/y⃗]) :!A

wehich is precisely the image of !t under Ψ.

!-Elimination In This case, we have the following derivation in DILL.

y⃗ : Γ; Δ_{1} ⊢ t :!A y⃗ : Γ, x : A; Δ_{2} ⊢ u : B
y⃗ : Γ; Δ_{!}, Δ_{2} ⊢ let !x be t in u : B

Hence again by the inductive hypothesis we have the following derivations in ILL (using some α-conversion:

y⃗_{1} :!Γ, Δ_{1} ⊢ Ψy⃗_{1}(t[y⃗_{1}/y⃗]) :!A

and

y⃗_{2} :!Γ, x :!A, Δ ⊢ Ψy⃗_{2}(u[y⃗_{2}/y⃗]) : B

Now by the admissible cut rule in ILL we have

y⃗_{1} :!Γ, y⃗_{2} :!Γ, Δ_{1}, Δ_{2} ⊢ Ψy⃗_{2}(u[y⃗_{2}/y⃗])[Ψy⃗_{1}(t[y⃗_{1}/y⃗])/x] : B

Now by the familiar series of contractions, we have

y⃗ :!Γ, Δ_{1}, Δ_{2} ⊢ copy y⃗ for y⃗_{1}, y⃗_{2} in Ψy⃗_{2}(u[y⃗_{2}/y⃗])[Ψy⃗_{1}(t[y⃗_{1}/y⃗])/x] : B
■

We now give auxiliary lemmas relating intuitionistic and linear substitions in DILL to substitution in ILL.

Lemma 5.3 (Linear Substitution) If we consider the substitution:

y⃗ : Γ; Δ_{1}, x : A ⊢DILL t : B y⃗ : Γ; Δ_{2} ⊢DILL u : A
y⃗ : Γ; Δ_{1}, Δ_{2} ⊢DILL t[u/x] : B

then

Ψy⃗(t[u/x]) = copy ȳ for ȳ_{1}, ȳ_{2} in Ψy⃗_{1}(t[ȳ_{1}/x̄])[Ψ(u)y⃗_{2}[ȳ_{2}/x̄]/x]

Lemma 5.4 (Intuitionistic Substitution) If we consider the substitution:

y⃗ : Γ, x : A; Δ ⊢DILL t : B y⃗ : Γ; ⊢DILL u : A
y⃗ : Γ; Δ ⊢DILL t[u/x] : B

then we have that

Ψy⃗(t[u/x]) = copy ȳ for ȳ_{1}, ȳ_{2} in Ψ_{y⃗_{1},x}(t[ȳ_{1}/ȳ])[promote ȳ_{2} for ȳ_{3} in Ψy⃗_{3}(u[ȳ_{3}/ȳ])/x]

These are both routine inductions over the structure of the first term, and are left to the reader.

Now we can prove the equality lemma:

Lemma 5.1.4 If y⃗ : Γ; Δ ⊢DILL t =_{A} u, then y⃗ :!Γ, Δ ⊢ILL Ψy⃗(t) =_{A} Ψy⃗(u)

Proof This is proved again by induction over the length of the derivation of equality in DILL. We consider only the exponential equalities, as it is easy but time-consuming to show that the other components of the equality rule system over DILL correspond to equalities on ILL.

!-β This equality is:

y⃗ : Γ; Δ ⊢ let !x be !u in v =_{A} v[u/x]

The left-hand side of this translates into ILL as the following:

copy y⃗ for y⃗_{1}, y⃗_{2} in Ψy⃗_{1}(v[y⃗_{1}/y⃗])[promote y⃗_{2} for y⃗_{3} in Ψy⃗_{3}(u[y⃗_{3}/y⃗]/x])

But this is just the image of intuitionistic substitution in ILL.

!-η This equality is

y⃗ : Γ; Δ ⊢ let !x be t in !x =_{!A} t

The image of the left-hand side is

copy y⃗ for y⃗_{1}, y⃗_{2} in (discard y⃗_{2} in promote x for x′ in derelict x′ )[Ψy⃗_{1}(t[y⃗_{1}/y⃗])/x]

By equality (5) of ILL we have that this is precisely

copy y⃗ for y⃗_{1}, y⃗_{2} in (discard y⃗_{2} in Ψy⃗_{1}(t[y⃗_{1}/y⃗]))

However, using equality (7) this is just Ψy⃗(t)

Commuting Conversions are dealt with easily, as they translate to the commuting conversions in ILL.

■

Lemma 5.1.5 For any term Δ ⊢ILL t : A of ILL, Δ ⊢ILL Ψ⟨⟩(Φ(t)) =_{A} t.

Proof We note first that the translation Φ is effectively the identity on terms other than those containing the exponential constructors. Moreover, since Φ translates sequents to sequents derivable from no intuitionistic assumptions, applying Ψ to these sequents gives the identity (as we need no copy or discard constructs). Hence we know that Ψ(Φ(t)) is the identity except perhaps on terms involving the exponential constructors.

We prove that the translation satisfies the property above by consideration of the structure of t. We consider only the exponential cases.

derelict: In this case, we have that t has the form derelict(u), and hence that Φ(t) has the form let !z be Φ(u) in z. This must have the following derivation in DILL:

z : A; ⊢ z : A ; Δ ⊢ Φ(u) :!A
; Δ ⊢ let !z be Φ(u) in z : A

The translation Ψ takes this derivation to

z :!A ⊢ derelict (z) : A Δ ⊢ Ψ⟨⟩(Φ(u)) :!A
Ψ(Δ) ⊢ derelict (z)[Ψ⟨⟩(Φ(u))/z] : Ψ(A)

which is derelict(Ψ⟨⟩(Φ(u))), but this is βη-equal to derelict (u) by the inductive hypothesis.

discard: In this case, t has the form discard u in v, so that Φ(t) is let !z be Φ(u) in Φ(v). This must have the following derivation in DILL:

z : A; Δ_{1} ⊢ Φ(v) : B ; Δ_{2} ⊢ Φ(u) :!A
; Δ_{1}, Δ_{2} ⊢ let !z be Φ(u) in Φ(v) : B

Ψ applied to this derivation gives the following:

z :!A, Δ_{1} ⊢ discard z in Ψ⟨⟩(Φ(v)) : B Δ_{2} ⊢ Ψ⟨⟩(Φ(u)) :!A
Δ_{1}, Δ_{2} ⊢ discard z in (Ψ⟨⟩(Φ(v)))[Ψ⟨⟩(Φ(u))/z] : B

but since z does not occur in Φ(v) and hence in Ψ⟨⟩(Φ(v)), this is precisely discard Ψ⟨⟩(Φ(u)) in (Ψ⟨⟩(Φ(v))) which is βη-equal to discard u in v by hypothesis. copy: Here, Φ(t) has the form let !z be Φ(u) in Φ(v)[!z/x, y], and therefore has the deriva-

tion:

z : A; Δ_{1} ⊢ Φ(v)[!z/x, y] : B ; Δ_{2} ⊢ Φ(u) :!A
; Δ_{1}, Δ_{2} ⊢ let !z be Φ(u) in Φ(v)[!z/x, y] : B

Under Ψ, this derivation becomes

z :!A, Δ_{1} ⊢ copy z for x, y in Ψ⟨⟩(Φ(v)) : B Δ_{2} ⊢ Ψ⟨⟩(Φ(u)) :!A
Δ_{1}, Δ_{2} ⊢ copy z for x, y in Ψ⟨⟩(Φ(v))[Ψ⟨⟩(Φ(u))/z] : B

which is copy Ψ⟨⟩(Φ(u)) for x, y in Ψ⟨⟩(Φ(v)), which is by hypothesis equal to copy u for x, y in v, or t.

promote: In this case, t has the form promote u⃗ for x⃗ in v. Hence we know that Φ(t) is let !z⃗ be Φ(u⃗) in !Φ(v)[!z⃗/x⃗].

This has the derivation

z⃗ : A⃗; ⊢!Φ(v)[!z⃗/x⃗] : B ; Δ_{i} ⊢ Φ(u_{i}) :!A_{i}
; Δ⃗ ⊢ let !z⃗ be Φ⃗(u) in !Φ(v)[!z⃗/x⃗] : B

When Ψ is applied, this becomes

z⃗ : !A ⊢ promote z⃗ for x⃗ in Ψ⟨⟩(Φ(v)) : B Δ_{i} ⊢ Ψ⟨⟩(Φ(u_{i})) :!A_{i}
Δ⃗ ⊢ (promote z⃗ for x⃗ in Ψ⟨⟩(Φ(v)))[Ψ⃗⟨⟩(Φ(u))/z⃗] : B

but this final term is just promote Ψ⃗⟨⟩(Φ(u)) for x⃗ in Ψ⟨⟩(Φ(v)), which is equal to the original term.

We can prove an analogous lemma for the alternative direction:

Lemma 5.1.6 For any term ; Δ ⊢ t : A of DILL, ; Δ ⊢ Φ(Ψ⟨⟩(t)).

This is easily proved in the same manner as the previous lemma. Now by virtue of the proof at the beginning of this section, we have the results:

Theorem 3.1 Δ ⊢ILL t =_{A} u iff ; Δ ⊢DILL Φ(t) =_{A} Φ(u)

Theorem 3.2 ; Δ ⊢DILL t =_{A} u iff Δ ⊢ILL Ψ⟨⟩(t) =_{A} Ψ⟨⟩(u)

6 Further Category-Theoretic Issues

6.1 Implications of Completeness

Our proof of completeness above has certain easy corollaries. Firstly, since we have shown that the term system ILL together with its βη-cc equality is isomorphic to a subsystem of DILL, with its βη-cc equality, we know that the models of DILL wil be very closely related to models of ILL. We give some results which are easily proved.

Lemma 6.1 (Interpretation for ILL) If Δ ⊢ILL t : A, then we have an arrow [[ ; Δ ⊢ Φ(t) : A]] : [[Δ]] → [[A]] in the SMCC part of any LNL model.

This is obvious from the form of the maps [[ ]] and Φ.

Corollary 3.1 (Soundness for ILL) If Δ ⊢ILL t =_{A} u, then the arrows [[ ; Δ ⊢ Φ(t) : A]] and [[ ; Δ ⊢ Φ(u) : A]] are equal in the SMCC part of any LNL model.

This follows from the fact that Φ preserves equalities, and from the fact that [[ ]] is sound.

Corollary 3.2 (Completeness for ILL) For terms t and u provable in the same context Δ, Δ ⊢ t =_{A} u if and only if

[[ ; Δ ⊢ Φ(t) : A]] = [[ ; Δ ⊢ Φ(u) : A]]

in the SMCC part of every LNL model.

Proof Assume that the interpretation of two ILL terms t and u are equal in every LNL model. Then it follows that via completeness for [[ ]] the two DILL terms Φ(t) and Φ(u) are βη-cc equal unless they have different contexts. But then it follows by the correspondence results proved earlier that the two ILL terms t and u are βη-cc equal unless they have different contexts. This shows completeness, when taken with the earlier soundness result.

Hence we have shown that ILL in its original formulation is complete for LNL models. We can also give a corresponding result in the reverse direction:

Corollary 3.3 If ILL has a complete model C with an interpretation function Θ_{C} : ILL → C in the same sense as previously used, ie

For terms t and u provable in ILL in the same context Δ, Δ ⊢ILL t =_{A} u iff Θ_{C}(t) = Θ_{C}(u) in C.

then for terms t and u provable in DILL in the same context Γ; Δ, Γ; Δ ⊢DILL t =_{A} u iff Θ_{C}(Ψ(t)) = Θ_{C}(Ψ(u)) in C.

Proof Working with terms t and u of DILL provable in the context Γ; Δ, we have:

Γ; Δ ⊢DILL t =_{A} u iff !Γ, Δ ⊢ILL Ψ(t) =_{A} Ψ(u) iff Θ_{C}(Ψ(t)) = Θ_{C}(Ψ(u)) in C

Hence the result is shown. ■

This demonstrates that models DILL and models of ILL are essentially the same.

6.2 Relating LNL models and Cambridge Models

We now recall that together with the original presentation of ILL, in [4], a categorical model was given based on a SMCC with a comonoidal comonad. These models were referred to as linear categories, or sometimes as Cambridge categories. It is natural to ask how this model of Linear Logic relates to the LNL models we have used, and indeed this question has been raised in detail by Benton in [2]. We summarise his results in this area.

Lemma 6.2 (Benton, [2], Corollary 8) Any LNL model has as its SMCC part a linear category.

Lemma 6.3 (Benton, [2], Corollary 17) Any linear category is the SMCC part of at least one LNL model.

This last lemma is of particular interest because the construction of a suitable CCC part to make the LNL model can be accomplished in a variety of ways. This is precisely the point which was made when we constructed a term-multicategory to form the CCC part of our term LNL-model; it was conceivable that there would be other possible choices of CCC which would satisfy the adjunction requirements.

We can make this more concrete by giving a lemma.

Lemma 6.4 If we have a Cambridge category C, then we can use a multicategory construction having the following arrows:

M(C)(< A_{i} >_{i=1..n}, B) = C(( ⨂_{i=1..n}!A_{i}), B)

to give us a CCC M(C)_{seq}. Further, the pair C and M(C)_{seq} form a LNL model.

We will not prove this here; however, the proof is straightforward, and is largely similar to the equivalent proof for the particular case when the Cambridge category C is taken to be the term category.

It is an open question as to which of Benton’s two constructions this syntactic construction corresponds to, if either.

We can now prove the following lemma, which neatly confirms the claim made in [3]:

Theorem 4 (Completeness of ILL for Cambridge Categories) For two terms t and u of ILL provable in the same context Δ, Δ ⊢ILL t =_{A} u iff

[[ ; Δ ⊢ Φ(t) : A]] = [[ ; Δ ⊢ Φ(u) : A]]

in the Cambridge category.

6.2.1 Proof

First observe that for any Cambridge category, by Benton’s lemma there is a LNL model which has the Cambridge category as its SMCC part. This justifies the fact that we are using our function [[ ]] to map into a Cambridge category, since the co-domain of this function is the SMCC part of the LNL model.

Soundness We can prove this direction by observing that as previously, since Φ and [[ ]] preserve the relevant equality, their compostion must do.

Completeness For this direction, assume that every Cambridge category makes [[Φ(t)]] and [[Φ(u)]] equal. Then observe that since the SMCC part of the term LNL-model is a Cambridge category, [[Φ(t)]] and [[Φ(u)]] are equal in the term LNL-model. However, we have previously shown that this implies Δ ⊢ILL t =_{A} u if both terms are provable in context Δ. Hence we have the result. ■

7 Further Work

7.1 Additives

We might wish to extend the syntax of DILL with the additive constructs of Linear Logic.

The Product Adding the product construct is simply a matter of introducing the term constructs π_{1,2} and < t, u > as normal, and augmenting the given equality with the β and η rules for these connectives. We have proved that the results on the translations between ILL and DILL still hold with this extension. The situation with the categorical semantics is less definite; results of Benton (op. cit.) and Bierman [6] have shown that in the case where the Cambridge category has products, the co-Kleisli category is a CCC and is the unique CCC which makes the pair a LNL model. This then means that Cambridge categories with products and LNL models with the SMCC part having products are isomorphic, and we would expect therefore that DILL with these product constructions would be complete for that class of models. However, this has not been proved as yet.

The co-Product Adding the co-product is again simple at the level of terms, since we need only to add the constructs (inl t), (inr t) and (case t of x in u or y in v). Again, we have shown that adding this to DILL makes it isomorphic to ILL with the equivalent construct added in the same sense as previously shown. However, the category theory is less clear; certainly it is not obviously the case that a Cambridge model with co-products gives rise to a LNL model, since it not obvious whether there is a suitable CCC having coproducts.

7.2 Rewriting

In considering linear λ-calculi, it is traditional to adopt the reductions of λ-calculus as far as possible, although of course it is not clear what direction if any should be assigned to the commuting conversions. We have disregarded this here in favour of a uniform treatment, since it is well known also that standard theorems such as strong normalisation are difficult to prove even in the simple case having just the connectives I, ⊗ and −∘. However, one virtue of DILL is that the treatment of ! enables us to give convincing orientations to all the equalities save the commuting conversions, and indeed this is reflected in our choice of presentation when the equalities were first given. Unfortunately, with these obvious directions assigned to the equalities, DILL fails to be confluent, as can be seen by considering the term let ∗ be x in ∗ ⊗ ∗ which has two reductions, to ∗ ⊗ x and x ⊗ ∗ respectively. We note that this problem will stop any term calculus with this treatment of the tensor unit from being confluent, which includes the majority of term calculi. The fact that this problem occurs with such a blameless connective shows that at a very basic level there is a problem with our representation of linear logic in a term calculus way, at least with respect to the dynamics. For this reason I am presently working on a new style of syntax for linear logic, to provide a good account of the dynamics as well as the semantics.

8 Acknowledgements

The system presented in this report was suggested by my supervisor, Gordon Plotkin, in [10]. I have benefited greatly from discussions with him and also with Philippa Gardner and Alex Simpson.

References

[1] Samson Abramsky. Computational Interpretations of Linear Logic. Journal of Theoretical Computer Science, 111:3–57, 1993. Earlier version appeared as Imperial College Technical Report DOC 90/20, October 1990.

[2] N. Benton. A mixed linear and non-linear logic; proofs, terms and models. In Proceedings of Computer Science Logic ’94, number 933 in LNCS. Verlag, June 1995. 15 page version.

[3] N. Benton, G. Bierman, V. de Paiva, and J.M.E. Hyland. Linear lambda-calculus and categorical models revisited. In Computer Science Logic ’92, Selected Papers, pages 61–84. Springer LNCS, vol. 702, 1993.

[4] N. Benton, G. Bierman, V. de Paiva, and M. Hyland. A term calculus for intuitionistic linear logic. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, number 664 in LNCS. Springer-Verlang, 1993.

[5] N. Benton and P. Wadler. Linear logic, monads and the lambda calculus. In Proceedings of LICS ’96, 1996.

[6] G. Bierman. What is a categorical model of intuitionistic linear logic? In Proceedings of the Second International Conference on Typed Lambda Calculus, number 902 in LNCS. Springer Verlag, April 1995.

[7] Jean-Yves Girard. Linear Logic. Theoretical Computer Science, 50(1):1–102, 1987.

[8] Jean-Yves Girard. On the unity of logic. Annals of Pure and Applied Logic, 59:201– 217, 1993.

[9] Joachim Lambek. Multicategories revisited. In J. W. Gray and A. Scedrov, editors, Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, pages 217–240, 1989.

[10] G. Plotkin. Second-order propositional intuitionistic linear logic. Unpublished Notes, 1993.

[11] G. Plotkin. Type theory and recursion. In Proceedings of the Eigth Symposium of Logic in Computer Science, Montreal, page 374. IEEE Computer Society Press, 1993. (Abstract).

[12] H. Schellinx. The Noble Art of Linear Decorating. PhD thesis, Institute of Logic, Language and Computation, University of Amsterdam, 1994. ILLC-Dissertation Series, 1994-1.

[13] Philip Wadler. There’s no substitute for linear logic. In Eighth International Conference on the Mathematical Foundations of Programming Semantics, Oxford, April 1992.

[14] Philip Wadler. A syntax for linear logic. In Ninth International Coference on the Mathematical Foundations of Programming Semantics, volume 802 of LNCS. Springer Verlag, April 1993.

[15] Philip Wadler. A taste of linear logic. In LNCS 711, volume LNCS 711 of Mathematical Foundations of Computer Science, Gdansk, August 1993. Springer Verlag.

A The System ILL

As mentioned in the introduction, we will follow closely the term assignment and presentation of [4], for the fragment of the logic containing the same connectives as those of DILL, namely I, ⊗, −∘ and !. The rules for the exponential ! in that presentation are moderately familiar, and are presented at the beginning of this report. However, we gather the significant term rules and equality rules of the system together here for convenience.

A.1 The Exponential Rules

Weakening

Γ ⊢ t : B Δ ⊢ u :!A

Γ, Δ ⊢ discard u in t : B Dereliction

Γ ⊢ t :!A

Γ ⊢ derelict(t) : A

Contraction

Γ, x :!A, y :!A ⊢ t : B Δ ⊢ u :!A
Γ, Δ ⊢ copy u as x, y in t : B

Promotion x_{1} :!A_{1}, …, x_{n} :!A_{n} ⊢ t : B {Δ_{i} ⊢ u_{i} :!A_{i}}_{i=1..n} Δ_{1}, …, Δ_{n} ⊢ promote u⃗ for x⃗ in t :!B

The rules for the other connectives are essentially those for the corresponding parts of DILL with the omission of the intutionistic environment Γ.

A.2 The Equality

We assume that a suitable system of rules for equality including reflexivity, transitivity and congruence has been presented, together with a definition of linear and binding contexts, all in a similar manner to those given earlier for the DILL type theory. Further, we assume that one-step equalities on the familiar non-exponential constructors have been given, analogously to those of DILL. In that context, the one step equalities for the exponential presented here should be understood as abbreviations for their corresponding one-step equality rules.

derelict (promote e⃗ for x⃗ in t) = t[e⃗/x⃗]  (1)
discard (promote e⃗ for x⃗ in t) in u = discard e⃗ in u  (2)
discard u in C[v] = C[discard u in v]  (3)
copy u for x, y in C[v] = C[copy u for x, y in v]  (4)
promote t for x in derelict (x) = t  (5)
copy e for x, y in u = copy e for y, x in u  (6)
copy e for x, y in (discard x in u) = u[e/y]  (7)
copy e for x, w in copy w for y, z in u = copy e for w, z in copy w for x, y in u (8)
promote e, e⃗ for x, x⃗ in (discard x in t) = discard e in (promote e⃗ for x⃗ in t) (9)
copy (promote e⃗ for x⃗ in t) for y, z in u = copy e⃗ for x⃗′, x⃗′′ in u[p_{1}, p_{2}/y, z]  (10)

where p_{1} = promote x⃗′ for x⃗ in t

and p_{2} = promote x⃗′′ for x⃗ in t

promote e, e⃗ for x, x⃗ in (copy x for y, z in t) = copy e for y′, z′ in p_{3}  (11)

where p_{3} = promote e⃗, y′, z′ for x⃗, y, x in t

promote (promote z⃗ for x⃗ in f), w⃗ for y, y⃗ in g = promote z⃗, w⃗ for z⃗′, y⃗ in g[p_{4}/y]  (12)

where p_{4} = promote z⃗′ for x⃗ in f

where equation (3) is subject to the side condition that C is linear and binds none of the free variables of the u_{i}, and equation (4) is subject to the side condition that C is linear, does not bind any of the free variables of u, and does not contain x or y free.