Categorical Models for Intuitionistic and Linear Type Theory

Maria Emilia Maietti, Valeria de Paiva and Eike Ritter^{⋆}

School of Computer Science, University of Birmingham Edgbaston, Birmingham B15 2TT, United Kingdom e-mail:{mem,vdp,exr}@cs.bham.ac.uk

Abstract. This paper describes the categorical semantics of a system of mixed intuitionistic and linear type theory (ILT). ILT was proposed by G. Plotkin and also independently by P. Wadler. The logic associated with ILT is obtained as a combination of intuitionistic logic with intuitionistic linear logic, and can be embedded in Barber and Plotkin’s Dual Intuitionistic Linear Logic (DILL). However, unlike DILL, the logic for ILT lacks an explicit modality ! that translates intuitionistic proofs into linear ones. So while the semantics of DILL can be given in terms of monoidal adjunctions between symmetric monoidal closed categories and cartesian closed categories, the semantics of ILT is better presented via fibrations. These interpret double contexts, which cannot be reduced to linear ones. In order to interpret the intuitionistic and linear identity axioms acting on the same type we need fibrations satisfying the comprehension axiom.

1 Introduction

This paper arises from the need to fill a gap in the conceptual development of the xSLAM project. The xSLAM project is concerned with the design and implementation of abstract machines based on linear logic. For xSLAM we initially developed a linear λ-calculus by adding explicit substitutions to Barber and Plotkin’s DILL [GdPR00]. We then considered the categorical models one obtains for both intuitionistic and linear logic with explicit substitutions on the style of Abadi et al. [GdPR99].

The DILL system [BP97] distinguishes between intuitionistic and linear variables: linear variables are used once during evaluation, intuitionistic ones arbitrarily often. This is a key feature for the optimisation which linear logic provides for the implementation of functional programming languages. But in DILL the intuitionistic implication is defined in terms of linear implication and the modality ! via the standard Girard translation, namely A → B = (!A)−∘B. This is not appropriate for implementations of functional languages. The reason is that in the translation of the simply-typed λ-calculus into DILL !’s occur only in types

⋆ Research supported by EPSRC-grant GR/L28296 under the title “The eXplicit Substitution Linear Abstract Machine”.

!A−∘B, and the linearity is in effect not used. Indeed, a function of this type is applied only to arguments with no free linear variables, and during the execution of the program these arguments will be substituted only for intuitionistic variables. Finally we want to detect immediately when a function is intuitionistic. Hence it is more appropriate to have both → and −∘ as primitive operations and disregard !. This leads to consideration of the mixed intuitionistic and linear type theory (henceforth named ILT) described by Plotkin [Plo93] and Wadler [Wad90] obtained from DILL by (i) adding intuitionistic implication, and (ii) removing the modality ! from the type operators.

The syntactic behaviour of ILT is very similar to that of DILL. But when it comes to semantics, the situation is a little more complicated. It is not obvious how to restrict the idea of a symmetric monoidal adjunction, so that we capture all the behaviour of intuitionistic implication, without at the same time, importing all the machinery for modelling the modality !. But if we step back and look at our models for calculi of explicit substitution, we can see that modelling intuitionistic logic using fibrations can be combined with modelling (intuitionistic) linear logic using symmetric monoidal closed categories, and in a way that does not bring in all the machinery for !.

The expert reader will note that the fibration modelling of intuitionistic logic is only necessary for dealing with predicates and/or dependent types; and this paper is only concerned with propositional intuitionistic logic. However, fibration modelling does provide a means of adding linear type theory to intuitionistic type theory in the required way. This is the main result we establish in this paper.

The paper is organised as follows. In the first section we describe the calculus ILT. In the next section we define IL-indexed categories and prove soundness and completeness of ILT with respect to them. In the third section we show that ILT is the internal language of (a suitable restriction of) IL-indexed categories. Finally in the fourth section we add exponentials to these IL-indexed categories and we prove the equivalence between them and the models given by a symmetric monoidal adjunction between a symmetric monoidal closed category with finite products and a cartesian closed category that is the co-Kleisli category with respect to the comonad induced by the adjunction.

2 Intuitionistic and Linear Type Theory

The system of mixed intuitionistic and linear logic that we model in this paper, to be called Intuitionistic and Linear Type Theory or ILT for short, borrows from Girard’s Logic of Unity the elegant idea of separating assumptions into two classes: intuitionistic, which can be freely duplicated (shared) or discarded (ignored); and linear, which are constrained to be used exactly once. Syntactically, this strict separation is achieved by maintaining judgements with double-sided (“dual”) contexts Γ | Δ ⊢ A, where, as a convention, Γ and Δ contain non-linear (intuitionistic) and linear assumptions, respectively. Another distinguishing feature of ILT is that it has both intuitionistic (A → B) and linear implications (A−∘B), as well as additive (A&B) and multiplicative (A⊗B) conjunctions with their units (1 and I), but no modality (or exponential) types !A. This system should not be confused with BI the logic of bunched implications proposed by O’Hearn and Pym [OP99], whose propositional fragment has the same operators, but with very different behaviour.

The system ILT closest relative is Barber and Plotkin’s DILL [BP97] and most of its syntactic properties can be easily derived from DILL’s properties. But semantics is a different story: DILL’s rather elegant semantics in terms of a monoidal adjunction between a symmetric monoidal closed category L and a cartesian closed category C is not suitable for ILT, as ILT has no terms (or morphisms) corresponding to the modality per se. For instance, ILT has no term corresponding to id: !A →!A. This section describes briefly the system ILT.

The set of types we shall work with is

A ::= G | A−∘B | A → B | A ⊗ B | I | A&B | T

The syntax of preterms is defined inductively by

M, N ::= a | x | λa^{A}.M | λx^{A}.M | M _{i}N | M_{l}N
| M ⊗ N | let M be a ⊗ b in N | (M, N) | Fst(M) | Snd(M)
| ∘ | • | let M be • in N

where a and x range over countable sets of linear and intuitionistic variables, respectively. This distinction of variables is not strictly necessary, but we adopt it here to aid legibility. Because the two let-expressions behave so similarly we sometimes write let M be p in N to cover both, where p is either a ⊗ b or •. The typing rules for ILT are standard, see Table 1.

We have three kinds of equations, β and η-equations and commuting conversions. The last kind of equations, familiar in the setting of linear lambda-calculi, arise due to the form of η-rules for the tensor product and its unit. For the presentation of these equations we use contexts-with-holes, written C[ ]. They are given by the grammar

C[ ] ::= | λa^{A}.C[ ] | λx^{A}.C[ ] | C[ ]_{i}M | M_{i}C[ ] | C[ ]_{l}M | M_{l}C[ ]

| C[ ]⊗M | M⊗C[ ] | let C[ ] be p in N | let M be p in C[ ]

Note that this definition implies that there is exactly one occurrence of the symbol in a context-with-hole C[ ]. The term C[M] denotes the replacement of in C[ ] by M with the possible capture of free variables. This capture is the difference between the replacement of and substitution for a free variable: If C[ ] is the context-with-hole (λa^{A}. ), then C[a] = λa^{A}.a, whereas (λa^{A}.b)[a/b] = λc^{A}.a. The equations for ILT are given in Table 2.

Note that in ILT linear variables can move across the divisor of the context as expressed in the following lemma.

Lemma 1 For every ILT derivable judgement Γ | a_{1} : A_{1}, …, a_{n} : A_{n}, Σ ⊢ M : B we can derive Γ, x_{1} : A_{1}, …, x_{n} : A_{n} | Σ ⊢ M[x_{1}/a_{1}, … x_{n}/a_{n}] : B.

Γ | a : A ⊢ a : A Γ, x : A | ⊢ x : A

{Γ | Δ, a : A ⊢ M : B \atop Γ | Δ ⊢ λa^{A}.M : A−∘B}  {Γ | Δ_{1} ⊢ M : A−∘B Γ | Δ_{2} ⊢ N : A \atop Γ | Δ ⊢ M _{l}N : B}
{Γ, x : A | Δ ⊢ M : B \atop Γ | Δ ⊢ λx^{A}.M : A → B}  {Γ | Δ ⊢ M : A → B Γ | ⊢ N : A \atop Γ | Δ ⊢ M _{i}N : B}

{Γ | Δ_{1} ⊢ M : A Γ | Δ_{2} ⊢ N : B \atop Γ | Δ ⊢ M ⊗ N : A ⊗ B}

{Γ | Δ_{1} ⊢ M : A ⊗ B Γ | a : A, b : B, Δ_{2} ⊢ N : C \atop Γ | Δ ⊢ let M be a ⊗ b in N : B}

{Γ | Δ ⊢ M : A Γ | Δ ⊢ N : B \atop Γ | Δ ⊢ (M, N) : A&B} {Γ | Δ ⊢ M : A&B \atop Γ | Δ ⊢ Fst(M) : A} {Γ | Δ ⊢ M : A&B \atop Γ | Δ ⊢ Snd(M) : B}
Γ | ∅ ⊢ • : I  {Γ | Δ_{1} ⊢ M : I Γ | Δ_{2} ⊢ N : C \atop Γ | Δ ⊢ let M be • in N : C}
Γ | Δ ⊢ ∘ : 1

Where applicable Δ_{1}, Δ_{2} are disjoint and Δ is a permutation of Δ_{1}, Δ_{2}.

Table 1. The typing rules of ILT

β-equations:

(λx: A.M)_{i}N = M[N/x]  (λa: A.M)_{l}N = M[N/a]
let M⊗N be a⊗b in R = R[M/a, N/b] let • be • in M = M
Fst(M, N) = M  Snd(M, N) = N

η-equations:

λa : A.M_{l}a = M  λx : A.M_{i}x = M if x ∉ F V (M)
let a⊗b be M in a⊗b = M let • be M in • = M if Γ |Δ ⊢ M: 1
(Fst(M), Snd(M)) = M  ∘ = M

Commuting conversions:

                let M be ∗ in C[N] = C[let M be ∗ in N]

let M be a⊗b in C[N] = C[let M be a⊗b in N]

Table 2. The equations of ILT

3 Categorical semantics of ILT

The basis for our categorical model of ILT is Ehrhard’s notion of a D-category for modelling dependent types [Ehr88], which goes back to Lawvere’s idea of hyperdoctrines satisfying the comprehension axiom [Law70]. Hyperdoctrines model many-sorted predicative logic, where predicates are indexed over sorts or sets. A suitable adjunction allows the interpretation of the comprehension axiom, that is the creation of a subset defined by a predicate indexed over a set. Ehrhard generalized this idea in terms of fibrations introducing D-categories to interpret the Calculus of Constructions [Ehr88]. Here we adopt D-categories to model ILT. The fact of no having type dependencies will be clearly expressed by some restrictions that we will put on the particular D-categories we use to prove that ILT is their internal language.

In order to make more explicit the structure we need to interpret our calculus we recall the definition of D-categories in terms of indexed categories, which are categorically equivalent to fibrations. A D-category is a split indexed category E: B^{op}→Cat^{1} where the base category B models contexts and the fibre over an object Γ models terms whose free variables are contained in the context modelled in Γ. We require both B and each fibre E(Γ), for Γ in B, to have a terminal object ⊤. We also require that for every f morphism in the base category E(f) preserves the terminal object. The fibration associated to this indexed category is the projecting functor p : Gr(E)→B, where Gr(E) is the Grothendieck completion (see also page 107 of [Jac99]). We recall that the objects of the Grothendieck completion of E are the couples (Γ, A) where Γ is an object of B and A is an object of E(Γ). The morphisms of Gr(E) between (Γ, A) and (Δ, C) are couples (f, h) where f : Γ → Δ is a morphism in B and h : A → E(f)(C) is a morphism in E(Γ). For every object Γ in B the category E(Γ) is said the fibre of p under the object Γ.

The key construction of a D-category to interpret contexts and substitutions is the requirement called the “comprehension property” i.e. the requirement that the terminal object functor T : B→Gr(E) has got a right adjoint G: Gr(E)→B. Recall that the functor T is defined as follows: for every object Γ in the base category B, T (Γ) ≡ (Γ, ⊤) and for every morphism f, T (f) ≡ (f, Id). Actually T is an embedding functor of the base category B into the fibres of E. The right adjoint to T assures that every object, which for example interprets a sequent Γ ⊢ A in the fibre over the object interpreting the context Γ, can be put in correspondence to a context, in the example Γ, A, in the base category. Moreover by T a morphism in the fibre corresponds to a morphism in the base category and this allows to model substitution by the re-indexing functor.

The idea for the model of ILT is to modify this setting to capture the separation between intuitionistic and linear variables in ILT (with their corresponding substitutions) and simultaneously to model the two identity axioms, i.e. the assumptions of intuitionistic and linear variables, acting on the same types. The

1 Note that from now on when we refer to indexed categories we mean split indexed categories, i.e. the pseudofunctor towards Cat is actually a functor.

base category B models only the intuitionistic contexts of ILT, i.e., objects in B model contexts (Γ | ). Each fibre over an object in B modelling a context Γ | models terms Γ | Δ ⊢ M: A for any context Δ. We require a terminal object in B. The fibres are now symmetric monoidal closed categories with finite products (SMCP categories) and model the linear constructions of ILT. The functors between the fibres have to preserve the SMCP structure.

Since we no longer require each fibre to have a terminal object, we replace the right adjoint to the terminal object functor T by a right adjoint G to the unit functor U: B→Gr(E), assigning to each object Γ in B the object (Γ, I). This right-adjoint G is the comprehension functor. In this way we obtain that morphisms in the base correspond to morphisms with domain I in the fibre, i.e., terms with no free linear variables.

Now we can model substitution for intuitionistic variables by reindexing along morphisms in the base as usual: this adjunction U ⊣ G enforces the restriction that only terms with no free linear variables can be substituted for intuitionistic variables. Intuitionistic function spaces are modelled in the standard way by the right adjoint to weakening.

Definition 2 Let B be a category with a terminal object ⊤. An IL-indexed category is a functor E: B^{op}→Cat such that the following conditions are satisfied. (Note that we write f ∗ (−) for the application of the functor E to f, for any morphism f in B.)

(i) E(Γ) is a symmetric monoidal category with finite products, i.e. a SMCP category, for each object Γ of B. Moreover for each morphism f in B, the functor f^{∗} preserves this SMCP structure on the nose, i.e. it is a SMCP functor. For every object Γ in B, we denote the terminal object of E(Γ) by ⊤, the unique map towards ⊤ from every object C of E(Γ) by ter_{C}, the product of two objects A and B by A × B, the projections by π_{1} and π_{2} and the unique map from A to B × C given two maps t and s from A to B and A to C respectively by < t, s >.

(ii) For each object Γ of B the functor U: B→Gr(E), given by U(Γ) ≡ (Γ, I) and U(f) ≡ (f, Id) has a right adjoint G: Gr(E)→B. The object G(Γ, A) is abbreviated Γ.A in the sequel and the morphism G(f, h) is written f.h. Furthermore (Fst, Snd): (Γ.A, I)→(Γ, A) denotes the counit of this adjunction. The natural isomorphism between Hom_{Gr(E)}((−, I), (−, A)) and Hom_{B}(−, −.A) is denoted by [−, −].

(iii) For every object Γ of B and A of E(Γ), the functor Fst_{A}^{∗}: E(Γ)→E(Γ.A) has a right adjoint Π_{A}: E(Γ.A)→E(Γ). We will write in the sequel Cur^{I} for the natural isomorphism between Hom_{E(Γ.A)}(Fst_{A}^{∗}(B), C) and Hom_{E(Γ)}(B, Π_{A}(C)) and App_{I} for its counit.

(iv) The Beck-Chevalley-condition for the adjunctions Fst_{A}^{∗} ⊢ Π_{A} is satisfied in the strict sense, i.e. the equation f^{∗}(Cur_{A}^{I}(t)) = Cur_{A}^{I}((f.Id)^{∗}(t)) holds for every f: Δ→Γ, A ∈ E(Γ), B ∈ E(Γ.A).

Next, we define the interpretation of the ILT-calculus, which is the minimal ILT-theory corresponding to the notion of IL-indexed category.

Definition 3 Given any IL-indexed category E: B^{op}→Cat we define a map [[ ]] from types to objects in E(⊤), from intuitionistic contexts Γ to objects in B, from linear contexts Δ to objects in E(⊤), from double contexts to objects of suitable fibres and from terms Γ | Δ ⊢ M: A to morphisms [[M]]: [[Δ]]→[[A]] in E([[Γ]]) by induction over the structure:

(i) On intuitionistic and linear contexts respectively:

[[ ]] = ⊤ [[Γ, x: A]] = [[Γ]].[[A]]  [[ ]] = I [[Δ, a: A]] = [[Δ]]⊗[[A]]

where I is the tensor-unit in the category E(⊤) and also [[Δ]] and [[A]] are objects of E(⊤). On double contexts: [[Γ | Δ]] = Fst_{[[Γ]]}^{∗}([[Δ]]) because [[Δ]] being a linear context is an object of E(⊤).

(ii) On types:

\begin{aligned}[[A → B]] & = & Π_{[[A]]}.[[B]] & [[A−∘B]] & = & [[A]]−∘[[B]] & [[A⊗B]] & = & [[A]]⊗[[B]] \\ [[I]] & = & I & [[A&B]] & = & [[A]] × [[B]] & [[1]] & = & ⊤ \end{aligned}

(iii) On terms (assuming that Γ = x_{1}: A_{1}, …, x_{n}: A_{n}):

[[Γ, x: A | ⊢ x: A]] = Snd  [[Γ |a: A ⊢ a: A]] = Id
\begin{matrix}[[Γ ⊢ M: A]] = t \\ [[Γ, x: B ⊢ M: A]] = Fst ∗ t \end{matrix}  [[Γ | Δ ⊢ ∘ : 1]] = ter_{[[Δ]]}

\begin{matrix}[[Γ, x: A | Δ ⊢ M: B]] = t \\ [[Γ | Δ ⊢ λx^{A}.M: A → B]] = Cur^{I}(t) \end{matrix} \begin{matrix}[[Γ | Δ ⊢ M: A → B]] = t [[Γ | ⊢ N: A]] = s \\ [[Γ | Δ ⊢ M_{I}N: B]] = ⟨Id, s⟩ ∗ (App_{I} · t) \end{matrix}

\begin{matrix}[[Γ | Δ ⊢ M: A]] = t [[Γ | Δ ⊢ N: B]] = s \\ [[Γ | Δ ⊢ (M, N): A × B]] =< t, s > \end{matrix}

\begin{matrix}[[Γ | Δ ⊢ M: A × B]] = t \\ [[Γ | Δ ⊢ Fst(M): A]] = π_{1}(t) \end{matrix}  \begin{matrix}[[Γ | Δ ⊢ M: A × B]] = t \\ [[Γ | Δ ⊢ Snd(M): B]] = π_{2}(t) \end{matrix}

\begin{matrix}[[Γ | Δ_{1} ⊢ M: A]] = t [[Γ | Δ_{2} ⊢ N: B]] = s \\ [[Γ | Δ ⊢ M⊗N: A ⊗ B]] = (t ⊗ s) · π \end{matrix}

[[Γ | Δ_{1} ⊢ M: A × B]] = m [[Γ | Δ_{2}, a: A, b: B ⊢ N: C]] = n

[[Γ | Δ ⊢ let M be a ⊗ b in N: C]] = n · (Id ⊗ m) · π

[[Γ | ∅ ⊢ • : I]] = Id  [[Γ | Δ_{1} ⊢ M: I]] = m [[Γ | Δ_{2} ⊢ N: C]] = n [[Γ | Δ ⊢ let M be • in N: C]] = n · ψ · (Id ⊗ m) · π

where ψ is one part of the isomorphism between [[Δ_{2}]] and [[Δ_{2}]] ⊗ I

\begin{matrix}[[Γ | Δ, a: A ⊢ M: B]] = t \\ [[Γ | Δ ⊢ λa^{A}.M: A−∘B]] = Cur^{L}(t) \end{matrix}

where Cur^{L} is the corresponding natural transformation for the adjunction between (−)⊗[[A]] and [[A]]−∘(−) in E([[Γ]])

\begin{matrix}[[Γ | Δ_{1} ⊢ M: A−∘B]] = t [[Γ | Δ_{2} ⊢ N: A]] = s \\ [[Γ | Δ ⊢ M_{L}N: B]] = App_{L} · (t⊗s) · π \end{matrix}

where App_{L} is the counit of the right adjoint to tensor and π is the canonical morphism from [[Δ]] to [[Δ_{1}]]⊗[[Δ_{2}]].

Next, we turn to the soundness of this categorical semantics. As always, the key lemmata concern substitution. In particular they are needed to prove the validity of introduction and elimination rules regarding intuitionistic implication and of all the conversion rules involving substitution. As we have two kinds of substitution, we have to show two substitution lemmata, namely for substitution of intuitionistic and linear variables.

Lemma 4 (i) Assume [[Γ, x: A | Δ ⊢ M: B]] = t and [[Γ | ⊢ N: A]] = s. Then

[[Γ | Δ ⊢ M[N/x]: B]] = ⟨Id, s⟩ ∗ t. (ii) Assume [[Γ | Δ_{1}, a: A ⊢ M: B]] = t and [[Γ | Δ_{2} ⊢ N: A]] = s. Then

[[Γ | Δ ⊢ M[N/a]: B]] = t · (Id⊗s) · π, where π is the canonical morphism from [[Δ]] to [[Δ_{1}⊗Δ_{2}]].

Proof. Induction over the structure of M.

The soundness proof is now routine.

Theorem 5 Given an IL- indexed category E: B^{op} → Cat under the above interpretation [[]] the following facts hold.

(i) Assume Γ | Δ ⊢ M: A. Then [[Γ | Δ ⊢ M: A]] is a morphism from [[Δ]] to [[A]] in E([[Γ]]);

(ii) Assume Γ | Δ ⊢ M = N: A. Then [[Γ | Δ ⊢ M: A]] = [[Γ | Δ ⊢ N: A]].

Now we turn to the completeness theorem.

Theorem 6 If [[Γ | Δ ⊢ M: A]] = [[Γ | Δ ⊢ N: A]] where [[]] is the above defined interpretation, for every IL- indexed category E: B^{op} → Cat and for every derived sequents Γ | Δ ⊢ M: A and Γ | Δ ⊢ N: A then we can derive in ILT Γ | Δ ⊢ M = N: A.

Proof. As usual the proof is based on the construction of a term model out of ILT. Since the interpretation of ILT in the syntactic model turns out to be the identity then the completeness immediately follows. First recall that in order to prove that two functors U : B → Gr(E) and G : Gr(E) → B define a right adjunction U ⊣ G, we give two data: firstly, a natural transformation α_{D} : Hom(U(−), D)→ Hom(−, G(D)) for each object D in Gr(E), and secondly the co-unit, that is a natural transformation ϵ : U · G→1 such that for every object C in B and every f in Hom(U(C), D) we have ϵ_{D} · U(α_{D}(f)) = f.

Now we proceed by defining the syntactic IL-indexed category starting from an ILT-theory, based on the ILT-calculus and possibly some ground types with the corresponding terms.

Definition 7 Given an ILT-theory T with any set of ground types G we define the syntactic IL- indexed category F (T ) in the following way. The base category:

– Objects of the base category B(T ) are lists of types (A_{1}, …, A_{n}). The terminal object is the empty context [ ].

– Morphisms from (A_{1}, …, A_{n}) to (B_{1}, …, B_{m}) are lists of terms (M_{1}, …, M_{m}) such that x_{1}: A_{1}, …, x_{n}: A_{n} | ⊢ M_{i}: B_{i} for some intuitionistic variables x_{1}, …, x_{n}. We will write A⃗ for (A_{1}, …, A_{n}) whenever convenient.

– Two morphisms (M_{1}, …, M_{m}) and (N_{1}, …, N_{m}) from (A_{1}, …, A_{n}) to (B_{1}, …, B_{m}) supposing that x_{1}: A_{1}, …, x_{n}: A_{n} | ⊢ M_{i}: B_{i} and y_{1}: A_{1}, …, y_{n}: A_{n} | ⊢ N_{i}: B_{i} are equal if we derive x_{1}: A_{1}, …, x_{n}: A_{n} ⊢ M_{i} = N_{i}[x⃗/y⃗]: B_{i}. We will write (M⃗) for (M_{1}, …, M_{m}) whenever convenient.

– The identity morphism on (A⃗) is the list (x⃗);

– Composition is given by intuitionistic substitution: given morphisms (M_{1}, …, M_{m}) from (A_{1}, …, A_{n}) to (B_{1}, …, B_{m}) with x_{1}: A_{1}, …, x_{n}: A_{n} | ⊢ M_{i}: B_{i} and (N_{1}, …, N_{n}) from (C_{1}, …, C_{k}) to A⃗ such that y_{1}: C_{1}, …, y_{k}: C_{k} | ⊢ N_{j}: A_{j}, we define M⃗ · N⃗ to be (M_{1}[N⃗/x⃗], …, M_{m}[N⃗/x⃗]).

The fibres:

– The objects of the fibres of E(A⃗) are types A.

– A morphism from A to B in E(A⃗) is a term M such that x_{1}: A_{1}, …, x_{n}: A_{n} | a: A ⊢ M: B. Two morphisms M and N from A to B in E(A⃗) such that x_{1}: A_{1}, …, x_{n}: A_{n} | a: A ⊢ M: B and y_{1}: A_{1}, …, y_{n}: A_{n} | b: A ⊢ N: B are equal if we derive x⃗: A⃗ | a: A ⊢ M = N[x⃗/y⃗, a/b]: B.

– For any morphism M⃗ from A⃗ to B⃗, the functor E(M⃗) is the identity on the objects and transforms any morphism M with y⃗: B⃗ | a: A ⊢ M: B to M[M⃗/y⃗].

The structure in a fibre is given in the following.

– The tensor product of two objects A and B in the fibre E(A⃗) is the type A⊗B. The tensor product of two morphisms M and N in E(A⃗) is the term let a⊗b be z in M⊗N if x_{1}: A_{1}, …, x_{n}: A_{n} | a: A ⊢ M: B and y_{1}: A_{1}, …, y_{n}: A_{n} | b: A ⊢ N: B.

– The unit of the category E(A⃗) is given by the type I.

– The product and terminal object in E(A⃗) are given by the products and the type 1 in the syntax in the standard way.

– The right adjoint to the tensor product in E(A⃗) is given by the natural transformation mapping the morphism M from C⊗A to B to λa: A.M[c⊗a/b] where x⃗: A⃗ | b: C⊗A ⊢ M: B; the co-unit is the natural transformation whose component at the object B is given by the morphism let a⊗b be c in ab with x⃗: A⃗ | c: A−∘B⊗A ⊢ let a⊗b be c in ab: B.

The comprehension property:

– The right adjoint G to the functor U is given by

G(((A_{1}, … A_{n}), A)) = (A_{1}, …, A_{n}, A)
G(((M_{1}, … M_{n}), M)) = (M_{1}, …, M_{n}, M[x/a])

if x⃗: A⃗ | a: A ⊢ M: B, since by lemma 1 we can derive x⃗: A⃗, x: A | ⊢ M[x/a]: B. For any morphism ((M_{1}, … M_{n}), M) with x⃗: A⃗ | a: I ⊢ M: B the natural isomorphism [M⃗, M] is (M_{1}, …, M_{n}, M[•/a]). The co-unit for the object ((A_{1}, …, A_{n}), A) is the morphism ((x_{1}, …, x_{n}), let ∗ be a in x).

The intuitionistic function space:

– The right adjoint to Fst^{∗}: E(A⃗)→E((A⃗, A)) is the functor Π_{A}(−): E((A⃗, A))→E(A⃗) which maps every object C of E((A⃗, A)) to A → C and every morphism M in E((A⃗, A)) to λx^{A}.M. The natural transformation Cur^{I} maps the morphism M from C to B in E(A⃗, A) to λx: A.M if x⃗: A⃗, x: A | ⊢ M: B; the co-unit is the natural transformation whose component at the object B is given by the term ax where x⃗: A⃗, x: A | a: A → B ⊢ ax: B.

Note the subtle difference in the definition of the base category and the fibre: we define objects in the base category to be lists of types, whereas objects in the fibre are singleton types. Having products in the calculus, we could have chosen a uniform definition and defined the objects of B to be types rather than lists of types. However, this means we would need to use projections in the syntax to access the components of the product, which is rather cumbersome. In contrast we have no choice for the definition of the fibres but to use types as objects. The reason is that with the other choice there is no way of turning the fibre into a symmetric monoidal closed category, as there is no way of defining C−∘A⊗B in terms of C−∘A and C−∘B. This is not problem for a cartesian closed category, as in this case we have C → A × B ≡ (C → A) × (C → B).

The key part of the completeness theorem is the following proposition, whose proof is a routine verification:

Proposition 8 For any ILT-theory T the syntactic IL-indexed category F (T ) is an IL-indexed category.

The syntactic IL-indexed category allow us to prove completeness for ILT with respect to IL-indexed categories.

4 ILT as an internal language

Starting from the above soundness and completeness theorems we want to see if ILT is actually an internal language of IL-indexed categories. To this purpose we define the following categories TH(ILT) and IL-ind.

Definition 9 The objects of TH(ILT) are the ILT-theories, i.e. type theories whose inference rules include the ILT ones. The morphisms are translations that send types to types so as to preserve I, ⊤, ⊗, &, −∘, →. They send terms to terms so as to preserve the introduction and elimination constructors corresponding to the above types and they send intuitionistic (linear) variables to intuitionistic (linear) variables respecting their typability such that the typability judgement and equality between terms are preserved.

Definition 10 The objects of the category IL-ind are IL-indexed categories and the morphisms between E: B^{op} → Cat and E′: B^{′op} → Cat are given by a functor H : B → B′ preserving the terminal object and a natural transformation α : E ⇒ E′ · H such that for every object Δ in B α_{Δ} : E(Δ) → E′(H(Δ)) is a SMCP-functor. Finally the comprehension adjunction is preserved and the intuitionistic function spaces too as expressed by the conditions described in the following (where we differentiate the structure of E from that one of E′ with the prime).

1. For every object Δ in B and A in E(Δ), and for every morphism (f, t) : (Δ, A) → (Γ, C) in Gr(E) we have H(G(Δ, A)) = G′(H(Δ), α_{Δ}(A)) and H(G(f, t)) = G′(H(f), α_{Δ}(t)).

2. For every (f, t) : (Δ, I) → (Γ, C) H([f, t]) = [(H(f), α_{Δ}(t))]′

3. For every object Δ in B, A in E(Δ) and C in E(Δ.A) and every morphism f in E(Δ.A) we have that α_{Δ}(Π_{A}(C)) = Π_{α_{Δ}(A)}(α_{Δ.A}(C)) and α_{Δ}(Cur^{I}(f)) = Cur^{I}′(α_{Δ.A}(f)).

Formally the fact that ILT is the internal language of our IL-indexed categories is proved by providing an equivalence between the category of ILT-theories TH(ILT) and that one of IL-indexed categories IL-ind. But we can prove the above equivalence only if we put some restrictions on the IL-indexed categories.

Definition 11 An IL-indexed category E: B^{op} → Cat, is a restricted IL-indexed category if the following conditions hold:

1. for every object Δ ∈ Ob(B), meaning with ι_{Δ} : Δ → ⊤ the unique map towards the terminal object ⊤ in B, the functor E(ι_{Δ}) : E(⊤) → E(Δ) is bijective on the objects;

2. the right adjoint G restricted to the fibres of ⊤ corresponding to E(⊤) is bijective on the objects;

Finally we call rIL-ind the full subcategory of IL-ind whose object are restricted IL-indexed categories. Now we are ready to prove the following:

Proposition 12 There exist two functors L : TH(ILT) → rIL-ind and F : rIL-ind → TH(ILT) that give rise to an equivalence between TH(ILT) and rIL-ind.

Proof. Given an ILT-theory T we define F (T ) in an analogous way to the definition of the syntactic ILT-category in Definition 7, but we take B(T ) to be the category whose objects are the ILT-types and whose morphisms between the types A and C are x : A | ⊢ c : C. Hence we define G((A, B)) ≡ A&B. We can easily see that F (T ) is a restricted IL-indexed category. We can obviously lift any translation to become a morphism between IL-indexed categories. Given an IL-indexed category E: B^{op} → Cat we now define an ILTtheory L(E) out of it in the following way:

Definition 13 The language of L(E) is defined as follows:

1. the types of L(E) are the objects of the fibre E(⊤);

2. the preterms of L(E) are the morphisms of E(Δ) for every object Δ of B;

3. The inference rules are defined as the interpretation function in the Definition 3. Note that two typed terms represented by two morphisms in the same fibre are equal if they are equal as morphisms.

The functor L can be easily extended on the morphisms of IL-indexed categories to define translations. What remains to be checked is that the two compositions L · F and F · L are naturally isomorphic to the corresponding identity functors. For every ILT-theory T it is easy to check that L(F (T )) can be translated into T via a natural isomorphism.

For every restricted IL-indexed category E: B^{op} → Cat we prove that F (L(E)) is equivalent to E by the added requirements on IL-indexed categories. The base category B is equivalent to the B(F (L(E))) since by the comprehension adjunction with respect to E together with the first requirement we can build a faithful, full and surjective functor from B(F (L(E))) towards B. The natural transformation on each fibre is given by the projecting functors on the objects and by the identity on morphisms. The components of this natural transformations are really isomorphisms by the second requirement on the restricted indexed category.

Note that the internal language could be naturally enriched with explicit substitutions on terms to represent the composition in the fibre by explicit substitutions of linear variables and the morphism assignment of E by explicit substitutions of intuitionistic variables. But if we want to interpret explicit substitution operations on contexts in a different way from those on terms, then we need to add another fibration to each SMCP fibre in the style of [GdPR99], passing to a complicated doubly indexed category.

Moreover, observe that every categorical model defined by Benton [Ben95] given by a symmetric monoidal adjunction F ⊢ K with F : C → S, C a cartesian closed category, S a symmetric monoidal closed category with finite products, provides an IL-indexed category, by taking as a base the cartesian closed category C and as the fibre over an object C of the base the symmetric monoidal closed category with finite products whose objects are those of S but whose morphism from A to B are the S-morphism F (C)⊗A−∘B. The intuitionistic space between A and B is given by the usual F (A)−∘B. Then, if the adjunction F ⊢ K satisfies the requirement that C is the co-Kleisli category with respect to the comonad induced by the adjunction and K the embedding functor via the counit, the above IL-indexed category is also restricted.

5 The connection to the exponentials

In this section we show how to regain exponentials. We characterise exponentials by a universal construction, namely as the left adjunction to the functor which replaces all linear variables in a term by the intuitionistic ones. Note that since ILT is the internal language of a restricted IL-indexed category, its base category is actually cartesian closed so we can give the following definition to get exponentials:

Definition 14 An rIL-indexed category with exponentials is a restricted IL-indexed category E: B^{op}→Cat such that the functor I: E(⊤)→B given by I(A) = ⊤.A, I(t) = id.t has a symmetric monoidal left adjoint to form a symmetric monoidal adjunction. We write ! for the left adjoint.

Note that I is a monoidal functor by using the internal language. It is also possible to define the exponentials by the condition Hom_{E(Γ)}(!^{∗}A, B) ≅ Hom_{E(Γ ·A)}(I, B) plus a Beck-Chevalley-condition [HS99]. It is easy to see that these two definitions are equivalent: if you specialise the second condition to the case Γ = ⊤ and use the adjunction between B and Gr(E) putting !(⊤.A) ≡!^{∗}(A), you obtain the first condition by the first requirement of restricted indexed categories. The converse argument goes as follows:

Hom_{E(Γ)}(!^{∗}A, B) ≅ Hom_{E(Γ)}(I,!^{∗}A−∘B) ≅ Hom_{B}(Γ, ⊤.(!^{∗}A−∘B)) ≅ Hom_{E(T)}(!Γ,!^{∗}A−∘B) ≅ Hom_{E(T)}(!Γ ⊗!^{∗}A, B) ≅ Hom_{E(T)}(!(Γ × (⊤.A)), B) ≅ Hom_{B}(Γ.A, ⊤.B) ≅ Hom_{E(Γ ·A)}(I, B)

where the second-but-last equivalence uses the fact that the adjunction between E(⊤) and B is monoidal.

It is instructive to examine the relation between a rIL-indexed category and certain Benton’s linear-nonlinear categories as expressed in the following.

Definition 15 The category Ben_{r} has as objects Benton’s models F ⊢ K [Ben95], i.e. a symmetric monoidal adjunction between a cartesian closed category C and a symmetric monoidal closed category with finite products S where F : C → S, such that C is the co-Kleisli category with respect to the comonad induced by the adjunction and K is the embedding functor via the counit. The morphisms between F ⊣ K and F′ ⊢ K′, with F : C → S and F′ : C′ → S′, are functors M : S → S′ preserving the SMCP structure and the symmetric monoidal comonad.

We recall that the category Ben of Benton’s models and couples of functors (H_{1}, H_{2}) with H_{1} : S → S′, H_{2} : C → C′ commuting with the adjoints and preserving the monoidal adjunction has Ben_{r} as a co-reflective subcategory:

[figure: Ben_{r}; I; Ben; R]

assigning to each Benton’s model the corresponding one given by the monoidal adjunction with the co-Kleisli category. Morever note that the category Ben_{r} is equivalent to the category Bier of Bierman’s models (see [?]) with functors preserving the relevant structure.

Definition 16 The category rIL-indE has restricted IL-indexed categories as objects and as morphisms IL-morphisms preserving the adjunction that define exponentials, i.e. a morphism between E: B^{op} → Cat and E′: B^{′op} → Cat is a rIL-ind morphism given by H : B → B′ and α : E ⇒ E′ · H such that it also satisfies the following conditions:

– for every object Δ in B, !H(Δ) = α_{⊤}(!Δ);

– for every object Δ in B and A in E(⊤) and for every morphism t : Δ → I(A) in B, ϕ′(H(t)) = α_{⊤}(ϕ(t)), where ϕ′ and ϕ are the bijections of the corresponding adjunctions.

Proposition 17 The category Ben_{r} of suitable Benton’s models is equivalent to the category rIL − indE.

Proof. We already saw how every linear-nonlinear category in Ben_{r} gives rise to an rIL-indexed category in section 4. The exponentials in Benton’s setting satisfy the universal property for exponentials in a rIL-indexed category with exponentials. Conversely, any rIL-indexed category with exponentials E : B→Cat gives rise to a linear-nonlinear category: the symmetric monoidal closed category is E(⊤), and the cartesian closed category is the base category B, which we prove to be cartesian closed by means of its internal language ILT. Now we can observe by the internal language that the adjunction ! ⊢ I gives rise to a symmetric monoidal adjunction between E(⊤) and B. Using the equivalence between the two definitions of exponentials given above one shows that these functors define an equivalence.

By the above proposition we conclude that we can embed the category Ben into the category IL-ind through the reflection into Ben_{r}, as an alternative to the embedding into IL-ind obtained by taking the cartesian closed category of a Benton’s model as the base category of the indexed category.

[figure: Bier; ≃; Ben_{r}; ≃; I; Ben; R; rIL−indE; rIL−ind; IL−ind]

Here we could also prove that rIL-indE is a reflective subcategory of rIL-ind, whose reflection is given by freely adding the ! modality to the internal language of a rIL-indexed category and then considering the syntactic category associated.

In the context of Benton’s model, once the SMCP category S is fixed one is free to choose a functor F : C → S to represent exponentials. In the context of rIL-indexed categories with exponentials the choice of F is determined by the choice of the indexed category E, that is the substitution along intuitionistic variables.

6 Conclusion

We have produced a sound and complete model for the type theory ILT. Moreover we showed that, with a suitable restriction, IL-categories are the internal language for this type theory. The reasons for developing ILT are of a pragmatic nature: in applications within linear functional programming, it seems a good idea to have both intuitionistic and linear implication co-existing, instead of having intuitionistic implication a derived operation, obtained from Girard’s translation.

We hope to find a good representation in terms of one-dimensional categories for IL-indexed categories. Maybe in order to achieve this we need to extend ILT with a connective reflecting the logical role of the operation “|” acting on ILTcontexts.

References

[Ben95] Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Proceedings of Computer Science Logic ’94, Kazimierz, Poland. Lecture Notes in Computer Science No. 933, Berlin, Heidelberg, New York, 1995.

[BP97] A. Barber and G. Plotkin. Dual intuitionistic linear logic. Technical report, LFCS, University of Edinburgh, 1997.

[Ehr88] Th. Ehrhard. A categorical semantics of constructions. In Computer Science Press, editor, Logic in Computer Science, IEEE, pages 264–273, 1988.

[GdPR99] Neil Ghani, Valeria de Paiva, and Eike Ritter. Categorical models of explicit subsitutions. In Proc. of FoSSaCS’99, volume 1578 of Lecture Notes in Computer Science, 1999.

[GdPR00] N. Ghani, V. de Paiva, and E. Ritter. Linear explicit substitutions. Journal of the IGPL, to appear 2000.

[HS99] Martin Hofmann and Thomas Streicher. Personal communication, 1999.

[Jac99] B. Jacobs. Categorical Logic and Type Theory., volume 141 of Studies in Logic. Elsevier, 1999.

[Law70] F.W. Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. Proc. Sympos. Pure Math., XVII:1–14, 1970.

[OP99] P. O’Hearn and D.J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215–244, 1999.

[Plo93] G.D. Plotkin. Type theory and recursion. In Proc. of Logic in Computer Science, 1993.

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