Linear Logic, Monads and the Lambda Calculus^{∗}

Nick Benton University of Cambridge Computer Laboratory New Museums Site Pembroke Street

Cambridge CB2 3QG, UK

Nick.Benton@cl.cam.ac.uk

Philip Wadler University of Glasgow

Department of Computing Science

Lilybank Gardens Glasgow G12 8QQ, UK

 wadler@dcs.glasgow.ac.uk

Abstract

Models of intuitionistic linear logic also provide models of Moggi’s computational metalanguage. We use the adjoint presentation of these models and the associated adjoint calculus to show that three translations, due mainly to Moggi, of the lambda calculus into the computational metalanguage (direct, call-by-name and call-by-value) correspond exactly to three translations, due mainly to Girard, of intuitionistic logic into intuitionistic linear logic. We also consider extending these results to languages with recursion.

1. Introduction

Two of the most significant developments in semantics during the last decade are Girard’s linear logic [10] and Moggi’s computational metalanguage [14]. Any student of these formalisms will suspect that there are significant connections between the two, despite their apparent differences. The intuitionistic fragment of linear logic (ILL) may be modelled in a linear model – a symmetric monoidal closed category with a comonad ! which satisfies some extra conditions relating it to the monoidal structure [6]. Moggi’s computational metalanguage may be modelled in a monad model – a cartesian closed category with a monad T satisfying some different conditions relating it to the cartesian structure. The situations are tantalisingly close to dual: ! is almost, but not quite, entirely like T.

Benton has given an alternative presentation of models of ILL (adjoint models), based on a cartesian closed category C and a symmetric monoidal closed category L connected by functors F : C → L and G : L → C, with F left adjoint to G. Again there is additional structure, which is pleasingly easy to describe: the adjunction must be symmetric monoidal [4]. Taking ! = F G makes L a linear model, while taking T = GF makes C a monad model. Further, every linear model arises in this way, as do all the members of a significant class of monad models.

Each of the three models corresponds to both a logic and an associated term calculus. The logic associated with monad models and the computational metalanguage is an intuitionistic modal logic, dubbed CL-logic in [5]. Associated with linear models and ILL are several proposals for linear term calculi, such as those of [6], [18], [11]. Here we choose to work with the calculus of [6]. Corresponding to adjoint models are the LNL term calculus (here referred to as the adjoint calculus) and LNL logic of [4].

Girard proposed two mappings of intuitionistic logic (or, equivalently, the simply typed lambda calculus) into ILL (or, equivalently, the linear term calculus), labelled ∘ and ∗ [10]. The connection between the ∘ translation and call-by-name (CBN) lambda calculus, and between the ∗ translation and call-by-value (CBV) lambda calculus has previously been noted in [12, 13]. Moggi also proposed two translations, clearly labelled as call-by-value and call-by-name [14], of the lambda calculus into his computational metalanguage; Wadler discusses these further in [17].

In this paper we start with three source calculi with identical syntax but different semantics: the direct calculus λ is the usual simply typed lambda calculus, the lifted calculus λ_{⊥} is a typed version of Abramsky and Ong’s lazy lambda calculus [1], and the call-by-value calculus λ_{v} is typed version of Plotkin’s calculus of that name [16]. Each of these calculi is given two interpretations in an adjoint model via two translations – one into the monadic calculus, yielding a semantics in C, and one into the linear calculus, yielding a semantics in L. For λ we use a trivial mapping into the monadic calculus and Girard’s ∘ translation into the linear calculus. For λ_{⊥}, we use Moggi’s CBN translation and a slight variant of Girard’s ∘ translation. For λ_{v} we use Moggi’s CBV translation and Girard’s ∗ translation. The central result of the paper is that for each of the three calculi, the two interpretations are essentially the same, in that they are mates across the adjunction between C and L. Thus, for instance, Girard’s ∗ translation, first published in 1987, corresponds exactly to Moggi’s call-by-value translation, first published in 1989, and we can finally see that this is the case in 1996.

∗In 11’th IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, July 1996.

2. Categorical models

In this section we recall the central semantic definitions from [4], [14] and [6] and some results which we shall need later.

Definition 2.1 An adjoint model is specified by

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

2. a symmetric monoidal closed category

(L, I, ⊗, {− \atop ∘}), and

3. a  symmetric  monoidal  adjunction

(F, G, η, ϵ, m, n) from C to L.

We will use A, B, C and e, f, g range over objects and arrows in L, and X, Y, Z and s, t, u to range over objects and arrows in C.

Particularly important examples of adjoint models arise from the operation of lifting on categories of complete partial orders. Let L be the category of pointed ω-cpos (domains) and strict continuous maps. This is an SMCC with tensor product given by smash product and internal hom by the strict continuous function space. We can take C to be either the category of ωcpos and continuous maps (predomains) or the category of pointed ω-cpos and continuous maps. In both cases we obtain an adjoint model by taking G to be the inclusion functor and F to be the lifting functor F: X ↦ X_{⊥}. The monoidal structure on F is given by the isomorphism X_{⊥} ⊗ Y_{⊥} ≅ (X × Y)_{⊥}.

Later, we will exploit the following isomorphisms:

Lemma 2.2 In any adjoint model,

1. F (X × Y) ≅ F X ⊗ F Y and

2. X → GB ≅ G(F X {− \atop ∘} B).

□

Definition 2.3 A monad model is specified by

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

2. a strong monad (T, η, μ, τ) on C.

The relation between adjoint models and monad models is given by the following two propositions:

Proposition 2.4 If (C, L, F, G, η, ϵ) is an adjoint model, then (C, GF, η, GϵF) is a monad model with a commutative monad. □

Proposition 2.5 If (C, T, η, μ) is a monad model with a commutative monad and in addition C has equalisers and C^{T}, the Eilenberg-Moore category, has coequalisers of reflexive pairs, then C^{T} is symmetric monoidal closed and (C, C^{T} , F, G, η, ϵ) is an adjoint model, where G and F are the forgetful and free functors, respectively. □

Definition 2.6 A linear model is specified by

1. a symmetric monoidal closed category

(L, I, ⊗, {− \atop ∘}),

2. a symmetric monoidal comonad (!, ϵ, δ, q) on L, and

3. monoidal natural transformations with components disc_{A}: !A → I and dupl_{A}: !A → !A ⊗ !A such that

(a) each (!A, disc_{A}, dupl_{A}) is a commutative comonoid,

(b) disc_{A} and dupl_{A} are coalgebra maps, and

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

The relation between adjoint models and linear models is given by the following two propositions:

Proposition 2.7 If (C, L, F, G, η, ϵ) is an adjoint model, then (L, F G, ϵ, F ηG) is a linear model. □

Proposition 2.8 Any linear model gives rise to an adjoint model in which C is a full subcategory of the Eilenberg-Moore category L^{!} of coalgebras; though it is not, in general, unique. □

An adjoint or linear model may also have finite products (1, &) in L. This is essential for the direct translation but not for the call-by-name and call-by-value translations. The correspondence between adjoint and linear models is maintained in the presence of such products.

3. Term calculi

The syntax and type rules of our three source calculi λ,λ_{⊥} and λ_{v} are just those of the usual simply typed lambda calculus with pairing and a unit type. Briefly, the difference between these calculi is that they have different equational theories: λ satisfies the usual β and η rules, λ_{⊥} just satisfies the β rules and λ_{v} satisfies the restricted β_{v} and η_{v} laws [16].

The computational metalanguage, λ_{m}, extends the simply typed calculus with a new unary type constructor T:

X, Y, Z ::= 1 | X × Y | X → Y | T X

and adds the following introduction and elimination forms to the syntax:

T -I \frac{Θ ⊢ t : X}{Θ ⊢ [t] : T X}
T -E \frac{Θ ⊢ s : T X  Θ, x : X ⊢ u : T Y}{Θ ⊢ let x ← s in u : T Y}

The types of the linear term calculus λ_{l} are given by

A, B, C ::= I | A ⊗ B | 1 | A & B | A {− \atop ∘} B |!A

and the syntax is shown in Figure 1. We adopt the conventions that distinct linear contexts mention disjoint sets of variable names and that any variable name occuring only in the RHS of a definition, or in the conclusion of an inference rule, is chosen fresh. Which constructs bind variables, and hence how capture-avoiding substitution is defined, should be obvious from the typing rules.

We are using the syntax of [6], which is now fairly standard and well-known, although this does make the terms associated with the translations rather large and unwieldy. The alternative would have been to use the DILL (for ‘dual intuitionistic linear logic’) syntax due to Wadler [18] and, independently, to Plotkin and Barber [3]. Using DILL makes two of the term translations appear more elegant, but makes the connection with the commonest presentations of ILL a little more indirect. It should be stressed that everything works equally well with either syntax. We omit the standard details of the interpretation of linear and monadic calculi in their respective models.

4. Translations

Before presenting the translations into the monadic and linear calculi, we note, without giving the details, that there are two natural erasures |-|_{m}: λ_{m} → λ and |-|_{l}: λ_{l} → λ which map the monadic and linear calculi into our source calculi. For each of the translations which we shall present, following the translation by the appropriate erasure is the identity on source calculus typing judgements, which can be used to show that each translation not only preserves, but also reflects, typing judgements.

From now on, we assume that we are working in an given adjoint model (L, C, …), with the linear calculus interpreted in L and the monadic calculus in C.

4.1. Direct translations

The direct translation •: λ → λ_{m} is just the trivial inclusion of the simply typed lambda calculus into the computational metalanguage which makes no use of the computation type constructor. The corresponding translation ∘: λ → λ_{l} into the linear calculus is usually known as ‘the Girard translation’, and is shown in Figure 2.

That the two translations ∘ and • give equivalent semantics is hardly surprising, as it was one of motivations for Girard’s original formulation of linear logic and has subsequently been a touchstone in the formulation of various categorical models. However, the details are often glossed over (a notable exception being [8]). Firstly we observe that GX^{∘} ≅ X^{•} for each source type X. For the unit type this follows because G preserves limits, whilst for compound types it follows from a little inductive calculation: G(X × Y)^{∘}

=  { def’n ∘ }
G(X^{∘} & Y^{∘})
≅  { G + limits }
GX^{∘} × GY^{∘}
≅  { induction }
X^{•} × Y^{•}
=  { def’n • }
(X × Y)^{•},

G(X → Y)^{∘}

=  { def’n ∘ }

G(F GX^{∘} {− \atop ∘} Y^{∘})

≅  { Lemma 2.2 }

GX^{∘} → GY^{∘}

≅  { induction }

X^{•} → Y^{•}

=  { def’n • }

(X → Y)^{•}.

Now write φ for the top-to-bottom composite of the following chain of natural bijections between homsets:

hom_{C}(X_{1}^{•} × ⋯ × X_{n}^{•}, X^{•})
≅  { relation of X^{•} to X^{∘} }
hom_{C}(GX_{1}^{∘} × ⋯ × GX_{n}^{∘}, GX^{∘})
≅  { adjunction }
hom_{L}(F (GX_{1}^{∘} × ⋯ × GX_{n}^{∘}), X^{∘})
≅  { Lemma 2.2 }
hom_{L}(F GX_{1}^{∘} ⊗ ⋯ ⊗ F GX_{n}^{∘}, X^{∘})

The relation between the translations is the following:

Proposition 4.1 If Θ ⊢ t: X in λ then

φ([[Θ^{•} ⊢ t^{•} : X^{•}]]) = [[!Θ^{∘} ⊢ t^{∘} : X^{∘}]].

Id \overline{a : A ⊢ a : A}  I-I \overline{⊢ ∗: I}  I-E \frac{Γ ⊢ e: I Δ ⊢ f: A}{Γ, Δ ⊢ let ∗ = e in f: A}

⊗-I \frac{Γ ⊢ e: A Δ ⊢ f: B}{Γ, Δ ⊢ e ⊗ f: A ⊗ B}  ⊗-E \frac{Γ ⊢ e: A ⊗ B Δ, a: A, b: B ⊢ f: C}{Γ, Δ ⊢ let a ⊗ b = e in f: C}

&-I \frac{Γ ⊢ e: A Γ ⊢ f: B}{Γ ⊢ (e, f): A & B}  &-E \frac{Γ ⊢ e: A & B}{Γ ⊢ fst e: A}  \frac{Γ ⊢ e: A & B}{Γ ⊢ snd e: B}

1-I \overline{Γ ⊢ (): 1}  {− \atop ∘}-I \frac{Γ, a: A ⊢ e: B}{Γ ⊢ λa: A. e: A {− \atop ∘} B}

{− \atop ∘}-E \frac{Γ ⊢ e: A {− \atop ∘} B  Δ ⊢ f: A}{Γ, Δ ⊢ e f: B}  Der \frac{Γ ⊢ e: !A}{Γ ⊢ derelict e: A}

Weak \frac{Γ ⊢ e: !A  Δ ⊢ f: B}{Γ, Δ ⊢ discard e in f: B}  Contr \frac{Γ ⊢ e: !A  Δ, a: !A, b: !A ⊢ f: B}{Γ, Δ ⊢ copy e as a, b in f: B}

Promote \frac{Δ_{1} ⊢ e_{1}: !A_{1} ⋯ Δ_{n} ⊢ e_{n}: !A_{n}  a_{1}: !A_{1}, …, a_{n}: !A_{n} ⊢ f: B}{Δ_{1}, …, Δ_{n} ⊢ promote e_{1}, …, e_{n} for a_{1}, …, a_{n} in f: !B}

Figure 1. Linear lambda calculus (λ_{l})

Translation ∘ : λ → λ_{l}

1^{∘} = 1
(X × Y)^{∘} = X^{∘} & Y^{∘}
(X → Y)^{∘} = !X^{∘} {− \atop ∘} Y^{∘}
(Θ ⊢ t : X)^{∘} = !Θ^{∘} ⊢ t^{∘} : X^{∘}
(x⃗_{i}: Θ, x: X ⊢ x: X)^{∘} = x⃗_{i}: !Θ^{∘}, x: !X^{∘} ⊢ discard x⃗_{i} in derelict x: X^{∘}
(Θ ⊢ (): 1)^{∘} = !Θ^{∘} ⊢ (): 1
(Θ ⊢ (s, t): X × Y)^{∘} = !Θ^{∘} ⊢ (s^{∘}, t^{∘}): X^{∘} & Y^{∘}
(Θ ⊢ fst s: X)^{∘} = !Θ^{∘} ⊢ fst s^{∘}: X^{∘}
(Θ ⊢ snd s: Y)^{∘} = !Θ^{∘} ⊢ snd s^{∘}: Y^{∘}
(Θ ⊢ λx: X. s: X → Y)^{∘} = !Θ^{∘} ⊢ λx: X^{∘}. s^{∘}: !X^{∘} {− \atop ∘} Y^{∘}
(x⃗_{i}: Θ ⊢ s t: Y)^{∘} = x⃗_{i}: !Θ^{∘} ⊢ copy x⃗_{i} as a⃗_{i}, b⃗_{i} in (s^{∘}[a⃗_{i}/x⃗_{i}]) (promote b⃗_{i} for x⃗_{i} in t^{∘}): Y^{∘}

Figure 2. The direct translation ∘ Proof. Induction on t. One can use the categorical semantics to perform the calculations directly, but it is more convenient to use the adjoint calculus, which is the internal language of adjoint models. We describe the adjoint calculus in Section 5. □

4.2. Lifted translations

The translations associated with the lifted call-by-name calculus λ_{⊥}, shown in Figure 3 are †: λ_{⊥} → λ_{m}, which is Moggi’s CBN translation, and ‡: λ_{⊥} → λ_{l}, which is a slight variant of the Girard translation which appears to be new. The ‡ translation adds an extra ! to the translations of products and function spaces compared with the ∘ translation (note that the ‘Seely isomorphisms’ I ≅!1 and (!A⊗!B) ≅!(A & B) hold in any linear category with products). By similar reasoning to that which we used for the direct translation, we can then calculate that GX^{‡} ≅ GF X^{†} for each λ_{⊥} type X and that there is a natural bijection

\begin{matrix}ϕ : hom_{C}(GF X_{1}^{†} × ⋯ × GF X_{n}^{†}, GF X^{†}) → \\ hom_{L}(F GX_{1}^{‡} ⊗ ⋯ ⊗ F GX_{n}^{‡}, X^{‡}). \end{matrix}

We can then use induction on t to show

Proposition 4.2 If Θ ⊢ t: X in λ_{⊥} then

ϕ([[T Θ^{†} ⊢ t^{†} : T X^{†}]]) = [[!Θ^{‡} ⊢ t^{‡} : X^{‡}]].

□

4.3. Call-by-value translations

The call-by-value translations are ⋆: λ_{v} → λ_{m}, which is Moggi’s CBV translation [14], and ∗: λ_{v} → λ_{l} which is another translation due to Girard [10]. (Interestingly, although the CBV translation is central to Moggi’s work, Girard thought his ∗ translation was “not of much interest”.) These translations are shown in Figure 4.

The terms given in Figure 4 for the ∗ translation make use of a family of auxiliary macros P_{X}(·), indexed by the types of λ_{v}, which correspond to admissible rules of ILL. This complexity, which also arises if one uses the DILL syntax, is caused by the fact that the types of translated free variables are not all explicitly !-ed in this translation, so they cannot be directly weakened or contracted. For each λ_{v} type X, however, we can define a macro P_{X}(·) such that a: X^{∗} ⊢ P_{X}(a): !X^{∗}, which does enable values of that type to be copied and discarded. We need that ∀a: X^{∗}. derelict (P_{X}(a)) = a, though the other equation which would make P_{X}(·) a coalgebra structure map does not seem to be necessary.

P_{1}(a) = let ∗ = a in promote − for − in ∗
P_{X×Y} (a) = let b ⊗ c = a in promote P_{X}(b), P_{Y} (c)

for b′, c′ in derelict b′ ⊗ derelict c′

P_{X→Y} (a) = promote a for b in b

A simple inductive calculation shows that for any type X of λ_{v}, X^{∗} ≅ F X^{⋆} and thus that there is a natural bijection

\begin{matrix}ψ : hom_{C}(X_{1}^{⋆} × ⋯ × X_{n}^{⋆}, GF X^{⋆}) → \\ hom_{L}(X_{1}^{∗} ⊗ ⋯ ⊗ X_{n}^{∗}, X^{∗}). \end{matrix}

such that the relation between the two translations is

Proposition 4.3 If Θ ⊢ t: X in λ_{v} then

ψ([[Θ^{⋆} ⊢ t^{⋆} : T X^{⋆}]]) = [[Θ^{∗} ⊢ t^{∗} : X^{∗}]].
□

It is worth remarking that if we wished to extend the ∗ translation to incorporate other base types in the source language, then for each base type B, B^{∗} has to be a linear type on which we can define an appropriate P_{B}(·). The easiest way to ensure this is to take B^{∗} to be !L_{B} for some L_{B} so that we can use the free coalgebra structure. In general, however, there may other definitions of P_{B}(·), possibly involving extralogical constants, which work. Of course, if we also wished Proposition 4.3 to remain true, we should have to check that the linear and monadic translations of each base type and constant symbol were appropriately related, but this is necessary for any of our translation pairs.

5. The adjoint calculus

In this section we sketch the adjoint calculus λ_{a} of [4] and describe the translations of λ_{l} and λ_{m} into λ_{a} which were used to prove the main results presented here. The adjoint calculus includes both linear types and terms, corresponding to objects and arrows of L, and non-linear types and terms, corresponding to objects and arrows of C. The syntax of the adjoint calculus is shown in Figure 5.

Note that non-linear terms only have non-linear free variables, but that linear terms may have both linear and non-linear free variables. Corresponding to each judgement x_{1}: X_{1}, …, x_{m}: X_{m} ⊢_{C} s: Y is an arrow X_{1}× ⋯ × X_{m} ⟶^{s} Y in C and corresponding to each judgement x_{1}: X_{1}, …, x_{m}: X_{m}, a_{1}: A_{1}, …, a_{n}: A_{n} ⊢_{L} e: B is

an arrow F (X_{1} × ⋯ × X_{m}) ⊗ A_{1} ⊗ ⋯ ⊗ A_{n} ⟶^{e} B in

L. Further details of both the semantics and the proof theory of λ_{a} may be found in [4].

Translation † : λ_{⊥} → λ_{m}

1^{†} = 1
(X × Y)^{†} = (T X^{†} × T Y^{†})
(X → Y)^{†} = T X^{†} → T Y^{†}
(Θ ⊢ t : X)^{†} = T Θ^{†} ⊢ t^{†} : T X^{†}
(Θ, x: X ⊢ x: X)^{†} = T Θ^{†}, x: T X^{†} ⊢ x: T X^{†}
(Θ ⊢ (): 1)^{†} = T Θ^{†} ⊢ [()]: T 1
(Θ ⊢ (s, t): X × Y)^{†} = T Θ^{†} ⊢ [(s^{†}, t^{†})]: T (T X^{†} × T Y^{†})
(Θ ⊢ fst s: X)^{†} = T Θ^{†} ⊢ let z ← s^{†} in fst z: T X^{†}
(Θ ⊢ snd s: Y)^{†} = T Θ^{†} ⊢ let z ← s^{†} in snd z: T Y^{†}
(Θ ⊢ λx: X. s: X → Y)^{†} = T Θ^{†} ⊢ [(λx: T X^{†}. s^{†})]: T (T X^{†} → T Y^{†})
(Θ ⊢ s t: Y)^{†} = T Θ^{†} ⊢ let z ← s^{†} in z t^{†}: T Y^{†}

Translation ‡ : λ_{⊥} → λ_{l}

1^{‡} = I
(X × Y)^{‡} = !X^{‡} ⊗!Y^{‡}
(X → Y)^{‡} = !(!X^{‡} {− \atop ∘} Y^{‡})
(Θ ⊢ t : X)^{‡} = !Θ^{‡} ⊢ t^{‡} : X^{‡}
(x⃗_{i}: Θ, x: X ⊢ x: X)^{‡} = x⃗_{i}: !Θ^{‡}, x: !X^{‡} ⊢ discard x⃗_{i} in derelict x: X^{‡}
(x⃗_{i}: Θ ⊢ (): 1)^{‡} = x⃗_{i}: !Θ^{‡} ⊢ discard x⃗_{i} in ∗: I

(x⃗_{i}: Θ ⊢ (s, t): X × Y)^{‡} = x⃗_{i}: !Θ^{‡} ⊢ copy x⃗_{i} as a⃗_{i}, b⃗_{i} in (promote a⃗_{i} for x⃗_{i} in s^{‡})⊗

(promote b⃗_{i} for x⃗_{i} in t^{‡}) :!X^{‡}⊗!Y^{‡}
(Θ ⊢ fst s: X)^{‡} = !Θ^{‡} ⊢ let a ⊗ b = s^{‡} in discard b in derelict a: X^{‡}
(Θ ⊢ snd s: Y)^{‡} = !Θ^{‡} ⊢ let a ⊗ b = s^{‡} in discard a in derelict b: Y^{‡}
(x⃗_{i}: Θ ⊢ λx: X. s: X → Y)^{‡} = x⃗_{i}: !Θ^{‡} ⊢ promote x⃗_{i} for a⃗_{i} in (λx: !X^{‡}. s^{‡})[a⃗_{i}/x⃗_{i}]: !(!X^{‡} {− \atop ∘} Y^{‡})

(x⃗_{i}: Θ ⊢ s t: Y)^{‡} = x⃗_{i}: !Θ^{‡} ⊢ copy x⃗_{i} as a⃗_{i}, b⃗_{i} in (derelict s^{‡}[a⃗_{i}/x⃗_{i}])

(promote b⃗_{i} for x⃗_{i} in t^{‡}) : Y^{‡}

Figure 3. Lifted call-by-name translations

Both the linear and the monadic calculi may be translated into the adjoint calculus. These translations are shown in Figure 6, where we have omitted some entirely obvious clauses, such as that which states that ⊗-introduction in λ_{l} is translated as ⊗-introduction in λ_{a}. Both of these translations preserve semantics in the sense that for any linear term e, the interpretation of e^{♯} in the adjoint model (L, C, …) is equal to the one-step interpretation of e in L qua linear model, and similarly for monad calculus terms.

The equational axioms for the adjoint calculus are shown in Figure 7. So, for example, the proof of Proposition 4.2 may be obtained by showing that if Θ ⊢ t: X in λ_{⊥} then ϕ((t^{†})^{♭}) = (t^{‡})^{♯} using the rules of Figure 7 (plus the usual rules for equality, including congruence), where ϕ is an a macro corresponding to the bijection between homsets.

6. Coproducts

A linear category with binary coproducts models the extension of λ_{l} which includes the additive sum ⊕. Similarly a monad model with binary coproducts models the extension of λ_{m} with binary sums. Thus we are led to consider adjoint models with binary coproducts in both L and C. The correspondence of Proposition 2.8 is not quite maintained when we add coproducts, since an adjoint model (L, C, …) derived from a linear category (L, …) with coproducts has, in general, only weak coproducts in C. This happens in the concrete domain theoretic case when C is the category of domains and continuous maps (the Kleisli category of the lift comonad on L). Rather than work with weak coproducts, however, we choose to assume that we are working in a adjoint model with coproducts in both Translation ⋆ : λ_{v} → λ_{m}

1^{⋆} = 1
(X × Y)^{⋆} = X^{⋆} × Y^{⋆}
(X → Y)^{⋆} = X^{⋆} → T Y^{⋆}
(Θ ⊢ t : X)^{⋆} = Θ^{⋆} ⊢ t^{⋆} : T X^{⋆}
(Θ, x: X ⊢ x: X)^{⋆} = Θ^{⋆}, x: X^{⋆} ⊢ [x]: T X^{⋆}
(Θ ⊢ (): 1)^{⋆} = Θ^{⋆} ⊢ [()]: T 1
(Θ ⊢ (s, t): X × Y)^{⋆} = Θ^{⋆} ⊢ let x ← s^{⋆} in let y ← t^{⋆} in [(x, y)]: T (X^{⋆} × Y^{⋆})
(Θ ⊢ fst s: X)^{⋆} = Θ^{⋆} ⊢ let z ← s^{⋆} in [fst z]: T X^{⋆}
(Θ ⊢ snd s: Y)^{⋆} = Θ^{⋆} ⊢ let z ← s^{⋆} in [snd z]: T Y^{⋆}
(Θ ⊢ λx: X. s: X → Y)^{⋆} = Θ^{⋆} ⊢ [(λx: X^{⋆}. s^{⋆})]: T (X^{⋆} → T Y^{⋆})
(Θ ⊢ s t: Y)^{⋆} = Θ^{⋆} ⊢ let z ← s^{⋆} in let x ← t^{⋆} in z x: T Y^{⋆}

Translation ∗ : λ_{v} → λ_{l}

1^{∗} = I
(X × Y)^{∗} = X^{∗} ⊗ Y^{∗}
(X → Y)^{∗} = !(X^{∗} {− \atop ∘} Y^{∗})
(Θ ⊢ t : X)^{∗} = Θ^{∗} ⊢ t^{∗} : X^{∗}
(x⃗_{i}: X⃗_{i}, x: X ⊢ x: X)^{∗} = x⃗_{i}: X⃗_{i}^{∗}, x: X^{∗} ⊢ discard PX⃗_{i}(x⃗_{i}) in x: X^{∗}
(x⃗_{i}: X⃗_{i} ⊢ (): 1)^{∗} = x⃗_{i}: X⃗_{i}^{∗} ⊢ discard PX⃗_{i}(x⃗_{i}) in ∗: I
(x⃗_{i}: X⃗_{i} ⊢ (s, t): X × Y)^{∗} = x⃗_{i}: X⃗_{i}^{∗} ⊢ copy PX⃗_{i}(x⃗_{i}) as a⃗_{i}, b⃗_{i} in
s^{∗}[derelict a⃗_{i}/x⃗_{i}] ⊗ t^{∗}[derelict b⃗_{i}/x⃗_{i}]: X^{∗} ⊗ Y^{∗}
(x⃗_{i}: X⃗_{i} ⊢ fst s: X)^{∗} = x⃗_{i}: X⃗_{i}^{∗} ⊢ let a ⊗ b = s^{∗} in discard P_{Y} (b) in a: X^{∗}
(x⃗_{i}: X⃗_{i} ⊢ snd s: Y)^{∗} = x⃗_{i}: X⃗_{i}^{∗} ⊢ let a ⊗ b = s^{∗} in discard P_{X}(a) in b: Y^{∗}
(x⃗_{i}: X⃗_{i} ⊢ (λx: X. s): X → Y)^{∗} = x⃗_{i}: X⃗_{i}^{∗} ⊢ promote PX⃗_{i}(x⃗_{i}) for a⃗_{i} in λx: X^{∗}. s^{∗}[derelict a⃗_{i}/x⃗_{i}]: !(X^{∗} {− \atop ∘} Y^{∗})
(x⃗_{i}: X⃗_{i} ⊢ s t: Y)^{∗} = x⃗_{i}: X⃗_{i}^{∗} ⊢ copy PX⃗_{i}(x⃗_{i}) as a⃗_{i}, b⃗_{i} in
(derelict s^{∗}[derelict a⃗_{i}/x⃗_{i}]) (t^{∗}[derelict b⃗_{i}/x⃗_{i}]): Y^{∗}

Figure 4. Call-by-value translations

categories, with the motivating concrete example being that in which C is the category of predomains and continuous maps. In such a model F (X + Y) ≅ F X ⊕ F Y because F has a right adjoint. We add sums to our source calculi, and to λ_{l} and λ_{m}, using the usual syntax for injections and case analysis.

To extend the lifted call-by-name translations, we take (X +Y)^{†} = T X^{†} +T Y^{†} and (X +Y)^{‡} =!X^{‡}⊕!Y^{‡}. The isomorphism GX^{‡} ≅ GF X^{†} still holds with this definition, and the term translations are shown in Figure 8.

The call-by-value translations take (X +Y)^{⋆} = X^{⋆}+ Y^{⋆} and (X + Y)^{∗} = X^{∗} ⊕ Y^{∗}. The isomorphism X^{∗} ≅ F X^{⋆} still holds and the terms are shown in Figure 8. In this case we also have to define P_{X+Y}:

P_{X+Y} (a) = case a of inl b → promote P_{X}(b) for b′ in inl (derelict b′) | inr c → promote P_{Y} (c) for c′ in inr (derelict c′)

The extension of the direct translations is slightly more subtle. The Girard translation defines (X+Y)^{∘} = !X^{∘}⊕!Y^{∘}. Hence, to keep GX^{∘} ≅ X^{•}, we have to take (X + Y)^{•} = T (X^{•} + Y^{•}), so that the • translation is no longer a trivial inclusion. (Cf. the fact that the naive unlifted domain-theoretic semantics of a PCFlike language interprets sum types by the separated sum of domains.) The extended • translation also uses a macro D_{X}(·) such that x: T X^{•} ⊢ D_{X}(x): X^{•} and ∀y: X^{•}. D_{X}([y]) = y. The other equation which would make D_{X}(·) an algebra structure map does not seem to be necessary.

variables (intuitionistic)  x, y, z
variables (linear)  a, b, c
types (intuitionistic)  X, Y, Z ::= 1_{C} | A × B | A → B | GA
types (linear)  A, B, C ::= I | 1_{L} | A & B | A ⊗ B | A {− \atop ∘} B | F X
contexts (intuitionistic)  Θ  ::= x_{1} : X_{1}, …, x_{n} : X_{n}
contexts (linear)  Γ, Δ  ::= a_{1} : A_{1}, …, a_{n} : A_{n}

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

1_{L}-I \overline{Θ; Γ ⊢_{L} ()_{L}: 1_{L}}  1_{C}-I \overline{Θ ⊢_{C} ()_{C}: 1_{C}}

×-I \frac{Θ ⊢_{C} t : X  Θ ⊢_{C} u : Y}{Θ ⊢_{C} (t, u) : X × Y}  ×-E \frac{Θ ⊢_{C} s : X × Y}{Θ ⊢_{C} fst s : X}  \frac{Θ ⊢_{C} s : X × Y}{Θ ⊢_{C} snd s : Y}

&-I \frac{Θ; Γ ⊢_{L} f : A Θ; Γ ⊢_{L} g : B}{Θ; Γ ⊢_{L} (f, g) : A & B}  &-E \frac{Θ; Γ ⊢_{L} e : A & B}{Θ; Γ ⊢_{L} fst e : A}  \frac{Θ; Γ ⊢_{L} e : A & B}{Θ; Γ ⊢_{L} snd e : B}

I-I \overline{Θ; - ⊢_{L} ∗: I}  I-E \frac{Θ; Γ ⊢_{L} e: I  Θ; Δ ⊢_{L} f: A}{Θ; Γ, Δ ⊢_{L} let ∗ = e in f: A}

⊗-I \frac{Θ; Γ ⊢_{L} f : A Θ; Δ ⊢_{L} g : B}{Θ; Γ, Δ ⊢_{L} f ⊗ g : A ⊗ B} ⊗-E \frac{Θ; Γ ⊢_{L} e : A ⊗ B Θ; a : A, b : B, Δ ⊢_{L} h : C}{Θ; Γ, Δ ⊢_{L} let a ⊗ b = e in h : C}

→-I \frac{Θ, x : X ⊢_{C} u : Y}{Θ ⊢_{C} λx: X. u : X → Y}  →-E \frac{Θ ⊢_{C} s : X → Y  Θ ⊢_{C} t : X}{Θ ⊢_{C} s t : Y}

{− \atop ∘}-I \frac{Θ; Γ, a : A ⊢_{L} g : B}{Θ; Γ ⊢_{L} λa: A. g : A {− \atop ∘} B}  {− \atop ∘}-E \frac{Θ; Γ ⊢_{L} e : A {− \atop ∘} B  Θ; Δ ⊢_{L} f : A}{Θ; Γ, Δ ⊢_{L} e f : B}

G-I \frac{Θ; - ⊢_{L} f : A}{Θ ⊢_{C} Gf : GA}  G-E \frac{Θ ⊢_{C} s : GA}{Θ; - ⊢_{L} G^{−1}s : A}

F -I \frac{Θ ⊢_{C} t : X}{Θ; - ⊢_{L} F t : F X}  F -E \frac{Θ; Γ ⊢_{L} e : F X  Θ, x : X; Δ ⊢_{L} g : B}{Θ; Γ, Δ ⊢_{L} let F x = e in g : B}

Figure 5. Adjoint lambda calculus (λ_{a})

D_{1}(x) = ()
D_{X×Y} (x) = (D_{X}(let y ← x in [fst y]),

D_{Y} (let z ← x in [snd z]))

D_{X→Y} (x) = λy: X^{•}. D_{Y} (let f ← x in [f y])
D_{X+Y} (x) = let z ← x in z

The extended term translations are shown in Figure 8.

As our extension of the • translation to sums depends on D_{X}(·), if we were to add other base types B to λ then B^{•} should be a λ_{m} type equipped with an appropriate D_{B}(·). However (cf. our earlier remark about the ∗ translation), there seems no reason to demand that this be the free algebra structure on a type of the form T M_{B}.

Proposition 6.1 Each of Propositions 4.1, 4.2 and 4.3 remains true when the languages and translations are extended with coproducts as described above. □

7. Recursion

Our results also extend to languages with recursion, though there is some choice in exactly how recursion is treated. Brauner has already presented an extension of Proposition 4.1 in a linear model with parameterised fixpoints of all endomaps in the Kleisli category [8]. Bearing the case where C is predomains in mind, we instead use stronger version, due to Freyd, of Crole and Pitts’s notion of fixpoint object [9] so that we only require certain fixpoints in C.

Translation ♭ : λ_{m} → λ_{a} (extract).

1^{♭} = 1_{C}
(X × Y)^{♭} = X^{♭} × Y^{♭}
(X → Y)^{♭} = X^{♭} → Y^{♭}
(T X)^{♭} = GF X^{♭}
(Θ ⊢ u: Y)^{♭} = Θ^{♭} ⊢_{C} u^{♭}: Y^{♭}
(Θ ⊢ [t]: T X)^{♭} = Θ^{♭} ⊢_{C} GF t^{♭}: GF X^{♭}
(Θ ⊢ let x ← s in u: T Y)^{♭} = Θ^{♭} ⊢_{C} G(let F x = G^{−1}s^{♭} in G^{−1}u^{♭}): GF Y^{♭}

Translation ♯ : λ_{l} → λ_{a} (extract).

I^{♯} = I
(A ⊗ B)^{♯} = A^{♯} ⊗ B^{♯}
1^{♯} = 1_{L}
(A & B)^{♯} = A^{♯} & B^{♯}
(A {− \atop ∘} B)^{♯} = A^{♯} {− \atop ∘} B^{♯}
(!A)^{♯} = F GA^{♯}
(Γ ⊢ e: A)^{♯} = -; Γ^{♯} ⊢_{L} e^{♯}: A^{♯}
(Γ ⊢ promote e⃗_{i} for a⃗_{i} in f: !B)^{♯} = -; Γ^{♯} ⊢_{L} let F y⃗_{i} = e⃗_{i}^{♯} in F Gf^{♯}[F y⃗_{i}/a⃗_{i}] : F GB^{♯}
(Γ ⊢ derelict e: A)^{♯} = -; Γ^{♯} ⊢_{L} let F x = e^{♯} in G^{−1}x: A^{♯}
(Γ ⊢ discard e in f: B)^{♯} = -; Γ^{♯} ⊢_{L} let F x = e^{♯} in f^{♯}: B^{♯}
(Γ ⊢ copy e as a, b in f: B)^{♯} = -; Γ^{♯} ⊢_{L} let F x = e^{♯} in f^{♯}[F x/a, F x/b]: B^{♯}

Figure 6. Translation of monadic and linear calculi into adjoint calculus

Definition 7.1 A monad model has a Freyd fixpoint object (or ffpo) if it has an initial T -algebra σ: T Ω → Ω such that σ^{−1}: Ω → T Ω is a terminal coalgebra. (Here we intend algebra and coalgebra to be understood in the sense of algebra for a functor rather than algebra for a monad.)

Similarly, we say a linear model has a linear ffpo if there is an initial !-algebra σ̄: !Ω̄ → Ω̄ such that σ̄^{−1}: Ω̄ →!Ω̄ is a terminal coalgebra.

In a monad model with a ffpo, we can model an extension of λ_{m} which adds the syntax

\frac{Θ, x: T X ⊢ t: X}{Θ ⊢ mfix(x.t): X} by \frac{Θ × T X ⟶^{t} X}{Θ ⟶^{⟨1,⟨⟩;ω⟩;t̃} X}

where ω is the unique map such that ω; σ^{−1} = η_{1}; T ω and t̃ is the unique map such that

[figure: Θ × Ω; Θ × T Ω; X; Θ × T X; t̃; ⟨π_{1}, τ; T t̃⟩; 1 × σ; t]

commutes. Note that this requires that σ: T Ω → Ω be initial in a parameterised sense, but this is a consequence of the closed structure in C.

In a linear model with a linear ffpo, we can model an extension of λ_{l} which adds the syntax

\frac{Δ_{1} ⊢ e_{1}: !A_{1} ; ⋮ ; Δ_{n} ⊢ e_{n}: !A_{n}  a⃗_{i}: !A⃗_{i}, b: !B ⊢ f: B}{Δ_{1}, …, Δ_{n} ⊢ box e⃗_{i} for a⃗_{i} in lfix(b.f): B}

by

\frac{Δ_{i} ⟶^{e_{i}}!A_{i} (⨂_{i}!A_{i})⊗!B ⟶^{f} B}{⨂_{i} Δ_{i} ⟶^{⊗_{i}e_{i}} ⨂_{i}!A_{i} ⟶^{r;1⊗ω̄} (⨂_{i}!A_{i}) ⊗ Ω̄ ⟶^{f̂} B}

β rules:

\frac{Θ; Γ ⊢_{L} e: A  Θ; Γ ⊢_{L} f: B}{Θ; Γ ⊢_{L} fst (e, f) = e : A}  \frac{Θ ⊢_{C} s: X  Θ ⊢_{C} t: Y}{Θ ⊢_{C} fst (s, t) = s : X}

\frac{Θ; Γ ⊢_{L} e: A  Θ; Γ ⊢_{L} f: B}{Θ; Γ ⊢_{L} snd (e, f) = f : B}  \frac{Θ ⊢_{C} s: X  Θ ⊢_{C} t: Y}{Θ ⊢_{C} snd (s, t) = t : Y}

\frac{Θ; Γ ⊢_{L} e: A  Θ; Γ′ ⊢_{L} f: B  Θ; Δ, a: A, b: B ⊢_{L} g: C}{Θ; Γ, Γ′, Δ ⊢_{L} (let a ⊗ b = e ⊗ f in g) = g[e/a, f/b] : C}  \frac{Θ; Γ ⊢_{L} e: A}{Θ; Γ ⊢_{L} (let ∗ = ∗ in e) = e : A}

\frac{Θ; Γ, a: A ⊢_{L} e: B  Θ; Δ ⊢_{L} f: A}{Θ; Γ, Δ ⊢_{L} (λa: A. e) f = e[f/a] : B}  \frac{Θ, x: X ⊢_{C} s: Y  Θ ⊢_{C} t: X}{Θ ⊢_{C} (λx: X. s) t = s[t/x] : Y}

\frac{Θ ⊢_{C} s: X  Θ, x: X; Γ ⊢_{L} e: A}{Θ; Γ ⊢_{L} (let F (x) = F (s) in e) = e[s/x] : A}  \frac{Θ; - ⊢_{L} e: A}{Θ; - ⊢_{L} G^{−1}(G(e)) = e : A}

η rules:

\frac{Θ; Γ ⊢_{L} e: 1_{L}}{Θ; Γ ⊢_{L} e = ()_{L} : 1_{L}}  \frac{Θ ⊢_{C} s: 1_{C}}{Θ ⊢_{C} s = ()_{C} : 1_{C}}

\frac{Θ; Γ ⊢_{L} e: A & B}{Θ; Γ ⊢_{L} (fst e, snd e) = e : A & B}  \frac{Θ ⊢_{C} s: X × Y}{Θ ⊢_{C} (fst s, snd s) = s : X × Y}

\frac{Θ; Γ ⊢_{L} e: F X  Θ; Δ, a: F X ⊢_{L} f: B}{Θ; Γ, Δ ⊢_{L} (let F (x) = e in f[F (x)/a]) = f[e/a] : B}  \frac{Θ ⊢_{C} s: X → Y}{Θ ⊢_{C} (λx: X. s x) = s : X → Y}

\frac{Θ; Γ ⊢_{L} e: I  Θ; Δ, a: I ⊢_{L} f: B}{Θ; Γ, Δ ⊢_{L} (let ∗ = e in f[∗/a]) = f[e/a] : B}  \frac{Θ; Γ ⊢_{L} e: A {− \atop ∘} B}{Θ; Γ ⊢_{L} (λa: A. e a) = e : A {− \atop ∘} B}

\frac{Θ; Γ ⊢_{L} e: A ⊗ B  Θ; Δ, c: A ⊗ B ⊢_{L} f: C}{Θ; Γ, Δ ⊢_{L} (let a ⊗ b = e in f[a ⊗ b/c]) = f[e/c] : C}  \frac{Θ ⊢_{C} s: X}{Θ ⊢_{C} G(G^{−1}(s)) = s : X}

Figure 7. Equational axioms for λ_{a}

where ω̄ is the unique map such that ω̄; σ̄^{−1} = q; !ω̄ and f̂ is the unique map such that

[figure: (⨂_{i}!A_{i}) ⊗ Ω̄; (⨂_{i}!A_{i})⊗!Ω̄; (⨂_{i}!A_{i})⊗!((⨂_{i}!A_{i}) ⊗ Ω̄); (⨂_{i}!A_{i})⊗!B; B; 1 ⊗ σ̄; f̂; 1⊗!f̂; f]

commutes (where we have omitted the details of some context manipulation). Again, the existence of f̂ depends on suitably parameterised initiality, but this is a consequence of ordinary initiality in the presence of the closed structure in L.

Lemma 7.2 In any adjoint model (L, C, …), C has an ffpo if and only if L has a linear ffpo. □

So we now assume that we are working in an adjoint model with ffpos.

If we add recursion to λ_{⊥} by

\frac{Θ, x: X ⊢ t: X}{Θ ⊢ rec(x.t): X}

Direct translations

(Θ ⊢ inl t: X + Y)^{•} = Θ^{•} ⊢ [inl t^{•}]: T (X^{•} + Y^{•})
(Θ ⊢ case s of inl x → t | inr y → u: Z)^{•} = Θ^{•} ⊢ D_{Z}(let z ← s^{•} in [case z of inl x → t^{•} | inr y → u^{•}]): Z^{•}
(x⃗_{i}: X⃗_{i} ⊢ inl t: X + Y)^{∘} = inl (promote x⃗_{i} for a⃗_{i} in t^{∘}[a⃗_{i}/x⃗_{i}]): !X^{∘}⊕!Y^{∘}
(x⃗_{i}: X⃗_{i} ⊢ case s of inl x → t | inr y → u: Z)^{∘} = x⃗_{i}: !X⃗_{i}^{∘} ⊢ copy x⃗_{i} as a⃗_{i}, b⃗_{i} in case s^{∘}[a⃗_{i}/x⃗_{i}] of
inl x → t^{∘}[b⃗_{i}/x⃗_{i}] | inr y → u^{∘}[b⃗_{i}/x⃗_{i}]: Z^{∘}

Lifted translations

(Θ ⊢ inl t: X + Y)^{†} = T Θ^{†} ⊢ [inl t^{†}]: T (T X^{†} + T Y^{†})
(Θ ⊢ case s of inl x → t | inr y → u: Z)^{†} = T Θ^{†} ⊢ let w ← s^{†} in case w of inl x → t^{†} | inr y → u^{†}: T Z^{†}
(x⃗_{i}: X⃗_{i} ⊢ inl t: X + Y)^{‡} = x⃗_{i}: !X⃗_{i}^{‡} ⊢ inl (promote x⃗_{i} for a⃗_{i} in t^{‡}[a⃗_{i}/x⃗_{i}]): !X^{‡}⊕!Y^{‡}
(x⃗_{i}: X⃗_{i} ⊢ case s of inl x → t | inr y → u: Z)^{‡} = x⃗_{i}: !X⃗_{i}^{‡} ⊢ copy x⃗_{i} as a⃗_{i}, b⃗_{i} in case s^{‡}[a⃗_{i}/x⃗_{i}] of
inl x → t^{‡}[b⃗_{i}/x⃗_{i}] | inr y → u^{‡}[b⃗_{i}/x⃗_{i}]: Z^{‡}

Call-by-value translations

(Θ ⊢ inl t: X + Y)^{⋆} = Θ^{⋆} ⊢ let x ← t^{⋆} in [inl x]: T (X^{⋆} + Y^{⋆})
(Θ ⊢ case s of inl x → t | inr y → u: Z)^{⋆} = Θ^{⋆} ⊢ let w ← s^{⋆} in case w of inl x → t^{⋆} | inr y → u^{⋆}: T Z^{⋆}
(Θ ⊢ inl t: X + Y)^{∗} = Θ^{∗} ⊢ inl t^{∗}: X^{∗} ⊕ Y^{∗}
(x⃗_{i}: X⃗_{i} ⊢ case s of inl x → t | inr y → u: Z)^{∗} = x⃗_{i}: X⃗_{i}^{∗} ⊢ copy PX⃗_{i}(x⃗_{i}) as a⃗_{i}, b⃗_{i} in case s^{∗}[derelict a⃗_{i}/x⃗_{i}] of
inl x → t^{∗}[derelict b⃗_{i}/x⃗_{i}] | inr y → u^{∗}[derelict b⃗_{i}/x⃗_{i}]: Z^{∗}

Figure 8. Translations of coproducts

then we can extend the lifted translations by

• (Θ ⊢ rec(x.t): X)^{†} = T Θ^{†} ⊢ mfix(y.let x ← y in t^{†}): T X^{†}

• (x⃗_{i}: Θ, ⊢ rec(x.t): X)^{‡} = x⃗_{i}: !Θ^{‡} ⊢ box x⃗_{i} for a⃗_{i} in lfix(x.t^{‡}[a⃗_{i}/x⃗_{i}]): X^{‡}

In the call-by-value calculus λ_{v}, we add recursion just at function types:

\frac{Θ, f: X → Y, x: X ⊢ t: Y}{Θ ⊢ (rec f x = t): X → Y}

and we can then extend the call-by-value translations as follows:

•(Θ ⊢ (rec f x = t): X → Y)^{⋆} = Θ^{⋆} ⊢ [mfix(z.λx: X^{⋆}. let f ← z in t^{⋆})]: T (X^{⋆} → T Y^{⋆}) •(x⃗_{i}: X⃗_{i} ⊢ (rec f x = t): X → Y)^{∗} = x⃗_{i}: X⃗_{i}^{∗} ⊢ promote PX⃗_{i}(x⃗_{i}) for a⃗_{i} in box a⃗_{i} for b⃗_{i}

in lfix(f.λx: X^{∗}. t^{∗}[derelict b⃗_{i}/x⃗_{i}]): !(X^{∗} {− \atop ∘} Y^{∗})

The double variable rebinding caused by the fact that both promote and box… lfix build in substitution is unfortunate but could easily be avoided by incorporating promotion into the lfix rule.

Extending the correspondence between the direct translations to a language with recursion also involves using the D_{X}(·) macro which we introduced when considering coproducts. We add recursion to λ by

\frac{Θ, x: X ⊢ t: X}{Θ ⊢ rec(x.t): X}

and then extend the direct translations by

• (Θ ⊢ rec(x.t): X)^{•} =

Θ^{•} ⊢ mfix(y.t^{•}[D_{X}(y)/x]): X^{•}

• (x⃗_{i}: X⃗_{i} ⊢ rec(x.t): X)^{∘} = x⃗_{i}: !X⃗_{i}^{∘} ⊢ box x⃗_{i} for a⃗_{i} in lfix(x.t^{∘}[a⃗_{i}/x⃗_{i}]): X^{∘}

Proposition 7.3 Proposition 6.1 remains true when each of the languages and translations is extended with recursion as described above. □

The proof of Proposition 7.3 may be obtained by extending the adjoint calculus with terms and equations corresponding to the fixpoint objects in the model. By Lemma 7.2, it suffices to add such syntax to the nonlinear part of the calculus, as the linear versions then arise as derived rules. We omit the rather messy details, however.

8. Conclusions and Further Work

Are the linear and monadic calculi two sides of the same coin? More precisely, are they equivalent calculi, but viewed from different sides of the adjunction? The straightforward answer is certainly no, not least because adjoint models give rise to all linear models, but only to commutative monad models. (We do not yet know if it is possible to define a non-commutative linear calculus which corresponds to a wider class of monad models.) But to the extent that the two calculi can be used to give equivalent interpretations of each of our three source calculi, the answer seems to be yes.

Perhaps results formally similar to those presented here could be obtained for other intuitionistic modal logics, such as the inuitionistic S4 of [7]. It may be that the relationship between the translations is a consequence more of the □-like character of ! than of the restrictions on weakening and contraction in λ_{l}.

The significance of these results extends well beyond the treatment of partiality by lifting and many suggestive similarities remain. For example, both linear and monadic types have been used to add updateable state to functional languages in a controlled way [2, 15]. We hope that our work may serve as a starting point for a formal comparison of these approaches.

9. Acknowledgements

We should like to thank Gavin Bierman, Martin Hyland, Eugenio Moggi, Valeria de Paiva, Andy Pitts, Gordon Plotkin, Robert Seely and the attendees of the SCILL workshop (Syntactic Control of Interference and Linear Logic), held at Glasgow in August 1995, for fruitful discussions, advice and inspiration.

References

[1] S. Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Directions in Functional Programming, chapter 4, pages 65–116. Addison-Wesley, 1990.

[2] P. Achten and R. Plasmeijer. The ins and outs of Clean I/O. Journal of Functional Programming, 5(1):81–110, Jan. 1992.

[3] A. Barber. Dual intuitionistic linear logic. Draft paper, University of Edinburgh, Apr. 1995.

[4] P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Proceedings of Computer Science Logic 1994, Kazimierz, Poland, volume 933 of Lecture Notes in Computer Science. Springer-Verlag, 1995. Full version available as Technical Report 352, Computer Laboratory, University of Cambridge, October 1994.

[5] P. N. Benton, G. M. Bierman, and V. C. V. de Paiva. Computational types from a logical perspective I. Technical Report 365, Computer Laboratory, University of Cambridge, May 1995.

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

[7] G. M. Bierman and V. C. V. de Paiva. Intuitionistic necessity revisited. In Proceedings of Logic at Work Conference, Amsterdam, Dec. 1992.

[8] T. Brauner. The Girard translation extended with recursion. In Proceedings of Computer Science Logic 1994, Kazimierz, Poland, volume 933 of Lecture Notes in Computer Science. Springer-Verlag, 1995.

[9] R. L. Crole and A. M. Pitts. New foundations for fixpoint computations: FIX-hyperdoctines and the FIXlogic. Information and Computation, 98(2), June 1992.

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

[11] P. Lincoln and J. Mitchell. Operational aspects of linear lambda calculus. In Proceedings of the Seventh Symposium on Logic in Computer Science, Santa Cruz. IEEE Press, June 1992.

[12] I. Mackie. The Geometry of Implementation. PhD thesis, Imperial College, London, 1994.

[13] J. Maraist, M. Odersky, D. N. Turner, and P. Wadler. Call-by-name, call-by-value, call-by-need, and the linear lambda calculus. Technical report, Fakultät für Informatik, Universität Karlsruhe and Department of Computing Science, University of Glasgow, Mar. 1995.

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

[15] S. Peyton Jones and J. Launchbury. State in Haskell. Lisp and Symbolic Computation, 8(4):293–341, Dec. 1995.

[16] G. D. Plotkin. Call-by-name, call-by-value, and the lambda calculus. Theoretical Computer Science, 1:125–159, 1975.

[17] P. Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2:461–493, 1992. Special issue of selected papers from 6th Conference on Lisp and Functional Programming.

[18] P. Wadler. A syntax for linear logic. In Proceedings of the Ninth International Conference on the Mathematical Foundations of Programming Semantics, New Orleans, Louisiana, volume 802 of Lecture Notes in Computer Science. Springer Verlag, Apr. 1993.