Call-by-name, call-by-value, call-by-need, and the linear lambda calculus^{∗}

John Maraist Martin Odersky University of Karlsruhe^{†} David N. Turner Philip Wadler University of Glasgow^{‡}

10 November 1994

Abstract

Girard described two translations of intuitionistic logic into linear logic, one where A → B maps to (!A) {− \atop ∘} B, and another where it maps to !(A {− \atop ∘} B). We detail the action of these translations on terms, and show that the first corresponds to a call-by-name calculus, while the second corresponds to call-by-value. We further show that if the target of the translation is taken to be an affine calculus, where ! controls contraction but weakening is allowed everywhere, then the second translation corresponds to a call-by-need calculus, as recently defined by Ariola, Felleisen, Maraist, Odersky, and Wadler. Thus the different calling mechanisms can be explained in terms of logical translations, bringing them into the scope of the Curry-Howard isomorphism.

1 Introduction

Plotkin’s ‘Call-by-name, call-by-value, and the lambda calculus’ [Plo75] demonstrated how the two different calling mechanisms could be explained by two different translations into continuation passing style. At the time he wrote, the call-by-value translation was widely appreciated, but the call-by-name translation was less well known. The call-by-value translation had been reinvented several times [Rey93], while the call-by-name translation is credited by Plotkin to a private communication from Reynolds.

While we hesitate to compare our work to Plotkin’s, our goal here is similar. We demonstrate how the two different calling mechanisms can be explained by two different translations into linear logic. At the time we are writing, the call-by-name translation is widely appreciated, but the callby-value translation is less well known. Both translations can be found in the original paper of Girard [Gir87], the first based on mapping A → B into !A {− \atop ∘} B, and the second based on mapping it into !(A {− \atop ∘} B). The first translation is frequently studied, and known to correspond to call-by-name; the second translation is less frequently studied, and its correspondence to call-by-value is not completely obvious. As evidence of the latter we note that Girard once suggested [Gir92] that the second translation might be connected to Abramsky’s lazy lambda calculus [Abr92], although Abramsky’s calculus is call-by-name.

A number of different lambda calculi based on linear logic have been proposed, including work by Lafont [Laf88], Holmström [Hol88], Wadler [Wad90, Wad91, Wad93a, Wad93b], Abramsky [Abr93], Mackie [Mac91], Lincoln and Mitchell [LM92], Troelstra [Tro92], Benton, Bierman, dePaiva, and Hyland [BBdPH92], and della Rocca and Roversi [RR94]. Various embeddings of intuitionistic logic into linear logic have also been studied, including work by Girard [Gir87], Troelstra [Tro92], and Schellinx [Sch94]. The linear lambda calculus used in this paper is a minor refinement of one previously presented by Wadler [Wad93a, Wad93b], which is based on Girard’s successor to linear logic, the Logic of Unity [Gir93]. A similar calculus has been devised by Plotkin [Plo93].

∗Appears as Technical Report #5/95, Fakultät für Informatik, Universität Karlsruhe, and as Technical Report FP-94-12, Department of Computing Science, University of Glasgow.

†Institut für Programmstrukturen, Universität Karlsruhe, Postfach 6980, 76128 Karlsruhe, F. R. Germany. Email: maraist,odersky@ira.uka.de.

‡Department of Computing Science, University of Glasgow, Glasgow G12 8QQ, Scotland. E-mail:

dnt,wadler@dcs.glasgow.ac.uk.

Corresponding to Girard’s first translation we define a mapping ∗ from the call-by-name calculus to the linear calculus, and show that this mapping is sound, in that M ⟶^{name} → N implies M^{∗} ⟶^{lin} → N^{∗}, and complete, in that the converse also holds. Corresponding to Girard’s second translation we define a second mapping † from the call-by-value calculus to the linear calculus, and show that this mapping is also sound and complete, in that M ⟶^{val} N if and only if M^{†} ⟶^{lin} N^{†}. We believe these soundness and completeness results to be new; showing soundness is straightforward, while completeness is somewhat trickier to establish.

Our original motivation for studying these questions came from an interest not in call-by-name or in call-by-value, but instead in the call-by-need calculus, which was recently proposed by Ariola, Felleisen, Maraist, Odersky, and Wadler [AF94, MOW94, AFMOW95]. The call-by-name calculus is not entirely suitable for reasoning about functional programs in lazy languages, because the beta rule may copy the argument of a function any number of times. The call-by-need calculus uses a different set of reductions, large enough to guarantee observational equivalence with the call-by-name calculus. But like call-by-value, call-by-need guarantees that the argument to a function is not copied before it is reduced to a value.

The emphasis on avoiding copying suggests that the ‘resource conscious’ approach of linear logic may be relevant. In the linear lambda calculus (as in linear logic), the ‘!’ connective is used to control duplication (contraction) and discarding (weakening) of lambda terms (proofs). For call-by-need we wish to avoid duplication but not discarding, and so an appropriate target for our translation is an affine calculus, in which contraction is controlled by the ‘!’ connective but weakening is allowed everywhere. The use of ‘!’ to separately control contraction and weakening has been studied by Jacobs [Jac92].

We derive the call-by-need calculus from the call-by-value calculus in two steps. The first step adds ‘let’ terms, which enforce sharing, to the call-by-value calculus. The resulting call-by-let calculus is observationally equivalent to call-by-value; the † translation, easily extended, is still sound and complete. We then add one further law, which allows a value bound by a ‘let’ to be discarded without first being computed if the value is not needed for the result. The resulting callby-need calculus is observationally equivalent to call-by-name as opposed to call-by-value, and the † translation remains sound and complete if its target is taken to be an affine calculus as opposed to the linear calculus.

As a result, the call-by-value and call-by-need calculi are brought into the scope of the Curry-Howard isomorphism, as the † translation relates reductions in each to reductions of the linear calculus which have a clear logical explanation.

An additional contribution of this work is that we confirm our linear calculus to be confluent. Although many linear calculi have been described, relatively few possess claims of confluence, a notable exception being the work of della Rocca and Roversi [RR94].

The remainder of this paper is organised as follows. Section 2 introduces the linear lambda calculus. Sections 3–6 describe the call-by-name, call-by-value, call-by-let, and call-by-need calculi and their translations. For simplicity, we restrict our attention to function types only. Section 7 sketches how this work may be extended by adding products, by adding constants and primitive operations, or by removing types; and it remarks that adding sums or recursion is more problematic. Section 8 concludes.

2 Linear lambda calculus

We begin with a linear lambda calculus similar to one introduced previously by Wadler [Wad93a, Wad93b].

In many presentations of logic a key role is played by the structural rules: contraction provides

Syntactic domains

Types A, B, C ::= Z | !A | A {− \atop ∘} B
Terms L, M, N ::= x | !M | let !x = M in N | λx. M | M N

Typing judgements

Id \overline{x : A ⊢ x : A}  Dereliction \frac{Γ, x : A ⊢ M : B}{Γ, !x : !A ⊢ M : B}

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

!-I \frac{!Γ ⊢ M : A}{!Γ ⊢ !M : !A}  !-E \frac{Γ ⊢ M : !A  Δ, !x : !A ⊢ N : B}{Γ, Δ ⊢ let !x = M in N : B}

{− \atop ∘}-I \frac{Γ, x : A ⊢ M : B}{Γ ⊢ λx. M : A {− \atop ∘} B}  {− \atop ∘}-E \frac{Γ ⊢ M : A {− \atop ∘} B  Δ ⊢ N : A}{Γ, Δ ⊢ M N : B}

Reduction relation

(β{− \atop ∘})  (λx. M) N  → M[x := N]
(β!)  let !x = !M in N  → N[x := M]
(!{− \atop ∘})  (let !x = L in M) N  → let !x = L in (M N)
(!!)  let !y = (let !x = L in M) in N → let !x = L in (let !y = M in N)

Figure 1: The linear lambda calculus lin.

the only way to duplicate an assumption, while weakening provides the only way to discard one. In linear logic [Gir87], the presence of contraction or weakening is revealed in a formula by the presence of the ‘of course’ connective, written ‘!’. The Logic of Unity [Gir93] takes this one step further by introducing two sorts of assumption, one that cannot be contracted or weakened, which we will write x : A, and one which can, which we will write !x : !A.

Figure 1 presents the details of the linear lambda calculus lin. A type, corresponding to a formula of the logic, is either a base type, an ‘of course’ type, or a linear function; let Z range over base types, and A, B, C range over types. A term, corresponding to a proof in the logic, is either a variable, an ‘of course’ introducer, an ‘of course’ eliminator, a function abstraction, or a function application; let x, y, z range over variables, and L, M, N range over terms. We write M[x := N] for the result of substituting term N for every free occurrence of the variable x in term M.

Contexts are sets containing the two forms of assumption, x : A and !x : !A, where each variable x is distinct. Let Γ and Δ range over contexts. If Γ and Δ are contexts with distinct variables, then Γ, Δ denotes their union. If Γ is a context of the form x_{1} : A_{1}, …, x_{n} : A_{n}, then !Γ is the context !x_{1} : !A_{1}, …, !x_{n} : !A_{n}.

A typing judgement Γ ⊢ M : A indicates that in context Γ term M has type A. There are five rules concerned with the ! connective: Dereliction, Contraction, and Weakening are structural rules, while !-I introduces and !-E eliminates the ! connective. An assumption of the form !x : !A can be introduced only by the !-E rule. The only thing that may be done with such an assumption is to duplicate it via Contraction, discard it via Weakening, or convert it to an assumption of the form x : A via Dereliction. Furthermore, in the !-I rule the context !Γ contains only assumptions of the form !x : !A. Analogous to the conclusion x : A ⊢ x : A of Id, the conclusion !x : !A ⊢ !x : !A may be derived by combining Id, Derelection, and !-I.

The reduction relation → is defined by the union of (the compatible closure of) the four given rules. We assume free and bound variables of a term are distinct in order to avoid capture; for instance, in rules (!{− \atop ∘}) and (!!), variable x cannot appear free in term N.

Some general notation: We write → → for the reflexive and transitive closure of →. We write = for the reflexive, symmetric, and transitive closure of →, and we write ≡ for syntactic identity.

When necessary, we may write the name of a calculus above a symbol to disambiguate, as in ⊢^{lin} or ⟶^{lin} →. We may also write the name of a rule below an arrow to indicate which rule is applied,

as in ⟶_{(β{− \atop ∘})}^{lin}.

Each of the reduction rules has a logical basis.

• Rule (β{− \atop ∘}) arises when a {− \atop ∘}-I rule meets a {− \atop ∘}-E rule, and the two rules annihilate.

• Rule (β!) arises when a !-I rule meets a !-E rule, and the two rules annihilate.

• Rule (!{− \atop ∘}) arises when a !-E rule meets a {− \atop ∘}-E rule, commuting one through the other.

• Rule (!!) arises when two !-E rules meet, commuting one through the other.

The action of reductions on proof trees is written out in full in Appendix A.

To evaluate a term of the form (let !x = M in N), it is sufficient to first reduce M to a term of the form !M′, and then substitute M′ for x in N. Thus we may view the term associated with !-E as forcing evaluation, and the term associated with !-I as suspending evaluation.

It is important to verify that the substitutions respect the restrictions on variables. In rule (β{− \atop ∘}), the variable x appears linearly in M, and so any free variable that appears linearly in N will still appear linearly in M[x := N]. Hence the substitution is well formed. In rule (β!) the variable x may appear any number of times in N, and so a free variable of M may be copied arbitrarily many times in N[x := M]. This is where distinguishing two sorts of assumptions is helpful: the constraint on the !-I rule guarantees that the term !M may only contain free variables that can appear any number of times. Hence this substitution is also well formed.

Some general terminology: A calculus satisfies the subject reduction property if whenever Γ ⊢ M : A and M → N then Γ ⊢ N : A. A calculus is confluent if whenever L → → M and L → → M′, there exists a term N such that M → → N and M′ → → N. All of the systems we study will possess both the subject reduction and confluence properties.

Proposition. lin satisfies subject reduction.

Proposition. lin is confluent.

Proof. The subject reduction result is inherent in what has been said above; full details appear in Appendix A. For confluence, the proof is similar to our proof of confluence for the call-by-need lambda calculus [MOW94], which uses Barendregt’s technique of marked and weighted redexes with a norm for weighted terms [Bar81]. We show (β{− \atop ∘}) and (β!, !{− \atop ∘}, !!) to be each individually Church-Rosser. In the former subsystem, the method is exactly that of Barendregt for (β). In the latter, we use the norm to show strong normalization, and a tedious but straightforward case analysis to show the weak Church-Rosser property; these two together imply a fully Church-Rosser system. Finally we show that multistep (β{− \atop ∘}) and (β!, !{− \atop ∘}, !!) reductions commute, and with subject reduction we have the result for the full system. □

We conclude this section with a few words about the relation of our linear lambda calculus to other formulations. For a fuller description of this relationship, see our previous work [Wad93a, Wad93b].

The formulation given here is based on the Logic of Unity [Gir93], but omitting the extra complication of polarities. In Girard’s presentation, the rule !-E does not appear, but it can be derived by combining his ! elimination rule (the fourth to last rule on the right in his Figure 2) with one of his structural rules (the last rule on the right in his Figure 1). We chose our formulation because it yields a simpler (β!) rule.

Our system follows the Logic of Unity, but differs from most other linear lambda calculi, in that we use two forms of assumption, which enables the subject reduction property to be established in a simple way. The other systems listed in the introduction either lack this property altogether, Syntactic domains

Types A, B, C ::= Z | A → B
Terms L, M, N ::= V | M N
Values  V, W ::= x | λx. M

Typing judgements

Id \overline{x : A ⊢ x : A}

Contraction \frac{Γ, y : A, z : A ⊢ M : B}{Γ, x : A ⊢ M[y := x, z := x] : B}  Weakening \frac{Γ ⊢ M : B}{Γ, x : A ⊢ M : B}

→-I \frac{Γ, x : A ⊢ M : B}{Γ ⊢ λx. M : A → B}  →-E \frac{Γ ⊢ M : A → B  Δ ⊢ N : A}{Γ, Δ ⊢ M N : B}

Reduction relation

(β→)  (λx. M) N → M[x := N]

Translation

\begin{aligned}Z^{∗} & ≡ & Z \\ (A → B)^{∗} & ≡ & (!A^{∗}) {− \atop ∘} B^{∗} \\ x^{∗} & ≡ & x \\ (λx. M)^{∗} & ≡ & λy. let !x = y in M^{∗} \\ (M N)^{∗} & ≡ & M^{∗} !N^{∗} \\ (x_{1} : A_{1}, …, x_{n} : A_{n})^{∗} & ≡ & !x_{1} : !A_{1}^{∗}, …, !x_{n} : !A_{n}^{∗} \end{aligned}

Figure 2: The call-by-name lambda calculus name.

or satisfy only a restricted version, or else possess full subject reduction but have a more complex syntax for ! introduction.

Also, most other systems treat Weakening and Contraction as logical rules with associated term forms. Our system treats Weakening and Contraction as structural rules, without the clutter of term forms. The result is more compact, and arguably more suitable as the basis of a programming language.

3 Call-by-name

Figure 2 reviews the call-by-name lambda calculus name and presents its translation into the linear lambda calculus. Types, terms, and values are standard: a type is a base type or function type, a term is a value or a function application, and a value is a variable or a function abstraction.

Contexts are sets of assumptions of the form x : A, where each variable x is distinct. A typing judgement Γ ⊢ M : A indicates that in context Γ term M has type A. The type rules are standard. We chose a formulation with Weakening and Contraction to stress the connection with the linear type system, the key difference being that now the use of Contraction and Weakening is unconstrained.

The call-by-name calculus has one reduction rule, (β→). This calculus of course satisfies the usual subject reduction and confluence results.

Proposition. name satisfies subject reduction.

Proposition. name is confluent.

Translation ∗ takes types, terms, and contexts A, M, Γ of the call-by-name lambda calculus name to types, terms, and contexts A^{∗}, M^{∗}, Γ^{∗} of the linear lambda calculus lin. In the translation of abstractions, y is a fresh variable, not appearing in M.

The idea behind this translation is that ! is added to the left of ⊢ and {− \atop ∘}, but not to the right. Every function argument is surrounded by !, which can be thought of as suspending evaluation, corresponding to the call-by-name discipline.

Proposition. Call-by-name translation. The translation ∗ from name to lin preserves substitution, types, and reductions.

(i) (M[x := N])^{∗} ≡ M^{∗}[x := N^{∗}].

(ii) Γ ⊢^{name} M : A if and only if Γ^{∗} ⊢^{lin} M^{∗} : A^{∗}.

(iii) M ⟶^{name} → N if and only if M^{∗} ⟶^{lin} → N^{∗}.

Proof. We prove (i) by an easy structural induction over terms of name, and prove (ii) by an easy structural induction over type derivations in name. To prove (iii) in the forward direction, we observe that reduction (β→) translates to

(λy. let !x = y in M^{∗}) !N^{∗} ⟶_{(β{− \atop ∘})}^{lin} let !x =!N^{∗} in M^{∗} ⟶_{(β!)}^{lin} M^{∗}[x := N^{∗}] .

For the backward direction, we consider the grammar

S, T ::= x | λy. let !x = y in S | S !T | let !x =!S in T ,

which defines the set of lin terms reachable from translations of terms in name: M^{∗} ⟶^{lin} → S. We then define an erasure ∘ that takes this set back into name:

x^{∘} ≡ x
(λy. let !x = y in S)^{∘} ≡ λx. S^{∘}
(S !T)^{∘} ≡ S^{∘} T^{∘}
(let !x =!S in T)^{∘} ≡ T^{∘}[x := S^{∘}] .

It is straighforward to show:

(a) The mapping ∘ is a right-inverse of ∗: M^{∗∘} ≡ M, for all M in name.

(b) The mapping ∘ sends lin-reduction sequences to name-reduction sequences: if S ⟶^{lin} T then S^{∘} ⟶^{name} → T^{∘}.

Now, M^{∗} ⟶^{lin} → N^{∗} implies by (b) that M^{∗∘} ⟶^{name} → N^{∗∘}, which implies by (a) that M ⟶^{name} → N. □

It is not hard to show that if L^{∗} ⟶^{lin} → M, then there exists a name term N such that M ⟶^{lin} → N^{∗}, and hence we also have that M =^{name} N if and only if M^{∗} =^{lin} N^{∗}.

4 Call-by-value

Figure 3 reviews the call-by-value lambda calculus val and presents its translation into the linear lambda calculus. Types, terms, and values are as in the call-by-name calculus.

There is one reduction rule, a restriction of the (β→) rule of call-by-name to the case when the function argument is a value. Again, the usual subject reduction and confluence results apply.

Proposition. val satisfies subject reduction.

Proposition. val is confluent.

Translation † takes types, terms, and contexts A, M, Γ of val to types, terms, and contexts A^{†}, M^{†}, Γ^{†} of lin. There is also an auxiliary mapping ‡ from types and values A, V of val to Syntactic domains As for name.

Typing judgements As for name.

Reduction relation

(β→_{v})  (λx. M) V → M[x := V]

Translation

A^{†} ≡ !A^{‡}
Z^{‡} ≡ Z
(A → B)^{‡} ≡ (A^{†} {− \atop ∘} B^{†})
V^{†} ≡ !V^{‡}
(M N)^{†} ≡ (let !z = M^{†} in z) N^{†}
x^{‡} ≡ x
(λx. M)^{‡} ≡ λy. let !x = y in M^{†}
(x_{1} : A_{1}, …, x_{n} : A_{n})^{†} ≡ !x_{1} : A_{1}^{†}, …, !x_{n} : A_{n}^{†}

Figure 3: The call-by-value lambda calculus val.

types and terms A^{‡}, V^{‡} of lin; this mapping omits the outermost ‘!’. As before, in the translation of applications and abstractions y and z are fresh variables not appearing in M.

The idea behind this translation is that ! is added on both the left and right of ⊢ and {− \atop ∘}. Function arguments are no longer surrounded by !, so the argument will be reduced until a ! is encountered before evaluation of the function body proceeds. Under this translation, the only terms beginning with ! are those of the form V^{†} ≡!V^{‡}, so function arguments are forced to reduce to values.

Proposition. Call-by-value translation. The translation † from val to lin preserves substitution of values, preserves types, and preserves reductions.

(i) (M[x := V])^{†} ≡ M^{†}[x := V^{‡}].

(ii) Γ ⊢^{val} M : A if and only if Γ^{†} ⊢^{lin} M^{†} : A^{†}, and Γ ⊢^{val} V : A if and only if Γ^{†} ⊢^{lin} V^{‡} : A^{‡}.

(iii) M ⟶^{val} → N if and only if M^{†} ⟶^{lin} → N^{†}.

Proof. Prove (i) and (ii) similarly to name. To prove (iii) in the forward direction, observe that (β→_{v}) translates to

(let !z =!(λy. let !x = y in M^{†}) in z) !V^{‡} ⟶_{(β!)}^{lin} (λy. let !x = y in M^{†}) !V^{‡}
⟶_{(β{− \atop ∘})}^{lin} let !x =!V^{‡} in M^{†}
⟶_{(β!)}^{lin} M^{†}[x := V^{‡}] .

The backward implication follows from two results stated in the next section: that the implication holds in an enriched call-by-value calculus let, and that reduction in let conservatively extends reduction in val. □

It is easily shown that M =^{val} N implies M^{†} =^{lin} N^{†}, but the converse is not true. For instance, the val terms ((λx. M)L) N and (λx. M N) L are not equal in val, but their translations are equal in lin.

Syntactic domains As for val, plus the following:

Terms L, M, N ::= ⋯ | let x = M in N

Typing judgements As for val, plus the following:

Let \frac{Γ ⊢ M : A  Δ, x : A ⊢ N : B}{Γ, Δ ⊢ let x = M in N : B}

Reduction relation

(I)  (λx. M) N  → let x = N in M
(V)  let x = V in M  → M[x := V]
(C)  (let x = L in M) N  → let x = L in (M N)
(A)  let y = (let x = L in M) in N → let x = L in (let y = M in N)

Translation As for val, plus the following:

(let x = M in N)^{†} ≡ let !x = M^{†} in N^{†}

Figure 4: The call-by-let calculus let.

5 Call-by-let

It is common to define (let x = M in N) ≡ (λx. N) M. Say we add ‘let’ as a new term form to the call-by-value lambda calculus. Since

(let x = M in N)^{†}  ≡  ((λx. N) M)^{†}
≡  (let !z =!(λy. let !x = y in N^{†}) in z) M^{†}
⟶_{(β!)}^{lin} (λy. let !x = y in N^{†}) M^{†}
⟶_{(β{− \atop ∘})}^{lin} let !x = M^{†} in N^{†} ,

it is reasonable to define the first term to be equal to the last. We refer to this new calculus as the call-by-let calculus let. One might ask what set of reductions is required in order to guarantee that M ⟶^{let} → N if and only if M^{†} ⟶^{lin} → N^{†}. The answer is that a somewhat larger set of reductions is now required.

Figure 4 defines the call-by-let lambda calculus let and presents its translation into the linear lambda calculus. The terms are the same as previously, plus a ‘let’ contruct, and the values remain unchanged. The types and type rules are also the same, with the addition of the obvious rule for ‘let’.

Reduction for let is defined by (the compatible closure of) the four rules (I), (V), (C), (A), which stand for ‘Introduce’, ‘Value’, ‘Commute’, and ‘Associate’. As before, subject reduction and confluence both hold.

Proposition. let satisfies subject reduction.

Proposition. let is confluent.

Proof. Subject reduction can be verified straightforwardly. Confluence is easily shown by modifying the our previous results for call-by-need [MOW94]. □

The translation † is extended by adding a clause for ‘let’.

Proposition. Call-by-let translation. The translation † from let to lin preserves substitution of values, preserves types, and preserves reductions.

(i) (M[x := V])^{†} ≡ M^{†}[x := V^{‡}].

(ii) Γ ⊢^{let} M : A if and only if Γ^{†} ⊢^{lin} M^{†} : A^{†}, and Γ ⊢^{let} V : A if and only if Γ^{†} ⊢^{lin} V^{‡} : A^{‡}.

(iii) M ⟶^{let} → N if and only if M^{†} ⟶^{lin} → N^{†}.

Proof. The proof of (i) and (ii) is similar to that for val. To prove (iii) in the forward direction, consider each possible reduction in let. Reduction by rule (I) translates to

(let z =!(λy. let !x = y in M^{†}) in z) N^{†} ⟶_{(β!)}^{lin} (λy. let !x = y in M^{†}) N^{†}
⟶_{(β{− \atop ∘})}^{lin} let !x = N^{†} in M^{†} .

Reduction by rule (V) translates to

let !x =!V^{‡} in M^{†} ⟶_{(β!)}^{lin} M^{†}[x := V^{‡}] .

Reduction by rule (C) translates to

(let !z = (let !x = L^{†} in M^{†}) in z) N^{†} ⟶_{(!!)}^{lin} (let !x = L^{†} in (let !z = M^{†} in z)) N^{†}
⟶_{(!{− \atop ∘})}^{lin} let !x = L^{†} in ((let !z = M^{†} in z) N^{†}) .

And reduction by rule (A) translates to (!!) in lin.

The proof of the backward direction is similar to the corresponding proof for call-by-name. One shows that the set of lin terms reachable from translations of terms in let is produced by the grammar:

Term image  S, T ::= !U | P S | let !x = S in T
Value image  U ::= x | λy.let !x = y in S
Prefix  P ::= U | let !x = S in P .

An erasure # that takes this set back into let is given by:

x^{#} ≡ x
(λy.let !x = y in S)^{#} ≡ λx.S^{#}
(!U)^{#} ≡ U^{#}
(P S)^{#} ≡ P^{#} S^{#}
(let !x = S in D[x])^{#} ≡ (D[M′])^{#}
(let !x = S in T)^{#} ≡ let x = S^{#} in T^{#} T ≢ D[x]
(let !x = S in P)^{#} ≡ let x = S^{#} in P^{#} P ≢ D[x]

where D ranges over contexts in the language

D ::= [ ] | D M | let !y = D in M .

It is straightforward to show that # is a right inverse of †. Furthermore, an analysis of linreductions shows that # sends lin-reduction sequences to let-reduction sequences. The result then follows as in the call-by-name case. □

What is the relationship between val and let? Clearly, every β→_{v}-reduction in val can be simulated in let by a pair of (I) and (V) reductions. That is, let-reduction extends val-reduction. Furthermore, one can show that the extension is conservative:

Proposition. For all M, N ^{∈} val, M ⟶^{val} → N if and only if M ⟶^{let} → N.

Proof. Again, the direction M ⟶^{val} → N ⟹ M ⟶^{let} → N is trivial.

The reverse direction relies on the intuitive idea that if a let-reduction sequence results in a val-term, all let-structures manipulated by (A) and (C) contractions must be (V)-contracted away. As a contrast, note that the following does not hold:

[figure: M; N; M′; N′; (I); (I); (β →_{v}); (I, V, C, A)] .

The details of the proof are in Appendix B. □

Syntactic domains As for lin.

Typing judgements As for lin, but changing Weakening as follows:

Weakening \frac{Γ ⊢ M : B}{Γ, x : A ⊢ M : B}

Reduction relation As for lin, plus the following:

(!Weakening)  let !x = M in N → N,  if x is not free in N

Figure 5: The affine lambda calculus aff.

Syntactic domains As for let.

Typing judgements As for let.

Reduction relation As for let, plus the following:

(G)  let x = M in N → N,  if x is not free in N

Translation As for let, except into aff rather than lin.

Figure 6: The call-by-need lambda calculus need.

6 Call-by-need

In the call-by-name translation, every function argument was surrounded by !, and so could be freely duplicated or discarded. In the call-by-value and call-by-let translations, only values are surrounded by !, and so non-values cannot be duplicated, but also cannot be discarded. The call-by-need calculus differs from these in that any term may be discarded if it is not needed, but a term should not be duplicated unless and until it has been reduced to a value. Thus, we wish to shift to a calculus where discarding (Weakening) is always allowed, but duplication (Contraction) remains under the strict control of the ‘!’ connective.

Figure 5 presents the details of the resulting affine lambda calculus aff. The types, terms, and contexts are the same as for the linear lambda calculus lin. The type rules are also identical to those for lin, with the exception that the rule Weakening of lin, which allows weakening only on assumptions of the form !x : !A, is replaced by a rule which allows weakening on assumptions of the form x : A. This is strictly stronger than the previous rule, as the previous rule can be derived by combining this Weakening with Dereliction.

Reduction is defined by (the compatible closure of) the rules (β{− \atop ∘}), (β!), (!{− \atop ∘}), (!!) together with a new rule (!Weakening). Again, this rule has a logical basis.

• Rule (!Weakening) arises when a !-E rule meets a Weakening rule, commuting one through the other.

As required, the effect of rule (!Weakening) is to allow the term M in let !x = M in N to be discarded if it is not needed, without first reducing M to the form !M′.

Again, the logical origin of the rules ensures the subject reduction property. Furthermore, confluence still holds.

Proposition. aff satisfies subject reduction.

Proposition. aff is confluent.

Proof. These are easily demonstrated by modifying the equivalent proofs for lin. □

Figure 6 defines the call-by-need calculus need, which can be derived as a slight modification of the call-by-let calculus let. The only change is the addition of a new reduction rule (G), which can be thought of as the surface manifestation of the underlying reduction (!Weakening). The name (G) stands for ‘Garbage collection’.

Proposition. need satisfies subject reduction.

Proposition. need is confluent.

Proof. Subject reduction is easy, requiring just one more case than let. We have previously published a proof of confluence for call-by-need [MOW94]. □

By design, if † is now viewed as taking the call-by-need calculus need into the affine calculus aff, then the transformation result still holds.

Proposition. Call-by-let translation. The translation † from need to aff preserves substitution of values, preserves types, and preserves reductions.

(i) (M[x := V])^{†} ≡ M^{†}[x := V^{‡}].

(ii) Γ ⊢^{need} M : A if and only if Γ^{†} ⊢^{aff} M^{†} : A^{†}, and Γ ⊢^{need} V : A if and only if Γ^{†} ⊢^{aff} V^{‡} : A^{‡}.

(iii) M ⟶^{need} → N if and only if M^{†} ⟶^{aff} → N^{†}.

Proof. The proof is as before, noting that the reduction (G) in need translates to (!Weakening) in aff. □

We conclude this section with some results on the observational behavior of the calculi we have studied. Some general terminology: Assume two calculi, say X and Y, extended with constants and primitives as outlined in Section 7.3. Assume that calculus X is bigger than calculus Y, that is, that every term of X is also a term of Y, but not necessarily conversely. Also assume that both systems have the same constants and primitives, and the same delta rules defining the value of these. We say that calculus X is observationally equivalent to calculus Y if for every term M in calculus Y, and for every constant c, we have M ⟶^{X} → c if and only if M ⟶^{Y} → c. The previous section’s result on conservative extension of let over val one have the following corollary.

Proposition. let is observationally equivalent to val.

Now, the addition of the single law (G) changes the situation significantly.

Proposition. need is observationally equivalent to name.

Proof. We showed in previous work [MOW94], that if M is a term and V is a value (both in name) such that M ⟶^{name} V, then there exist terms M_{1}, … M_{k} and a value V′ such that

M ⟶^{need} let x_{1} = M_{1} in ⋯ let x_{k} = M_{k} in V′.

The proof can be modified to show the same result with V ≡ V′. By taking V ≡ c and repeatedly applying (G), we get that M ⟶^{name} → c implies M ⟶^{need} → c. The reverse implication is easy. □

7 Extensions

We sketch here how our results extend to products, and to constants and primitives. We explain why extension to sums or to recursion are more difficult. We also note that the results extend easily to an untyped language.

7.1 Products

The extensions for products and for constants and primitives are straightforward, and are shown in Figures 7, 8, and 9. We discuss products in this section, and constants and primitives in the next.

The linear calculus may be extended with the additive product ‘&’ of linear logic, as shown in Figure 7. The call-by-name translation of ordinary products × into additive product & is

Types A, B, C ::= ⋯ | A & B
Terms L, M, N ::= ⋯ | (M, N) | fst M | snd M | c | p M_{1} ⋯ M_{k}

Typing judgements

&-I \frac{Γ ⊢ M : A  Γ ⊢ N : B}{Γ ⊢ (M, N) : A & B}  &-E_{1} \frac{Γ ⊢ M : A & B}{Γ ⊢ fst M : A}  &-E_{2} \frac{Γ ⊢ M : A & B}{Γ ⊢ snd M : B}

Const \overline{⊢ c : type_{lin}(c)}  Prim \frac{Γ_{1} ⊢ M_{1} : type_{lin}(p, 1) ⋯ Γ_{k} ⊢ M_{k} : type_{lin}(p, k)}{Γ_{1}, …, Γ_{k} ⊢ p M_{1} ⋯ M_{k} : type_{lin}(p, 0)}

Reduction relation

(β&_{1})  fst (M, N)  → M
(β&_{2})  snd (M, N)  → N
(!&_{1})  fst (let !x = L in M) → let !x = L in (fst M)
(!&_{2})  snd (let !x = L in M) → let !x = L in (snd M)
(δ)  p c_{1} ⋯ c_{k}  → apply_{lin}(p, c_{1}, …, c_{k})

Figure 7: Extending the linear lambda calculus (lin).

entirely straightforward, and follows the work of Girard, as shown in Figure 8. The call-by-value translation is also fairly straightforward, as shown in Figre 9. The call-by-value translation involves two points of note.

First, we maintain the uniform principle that values correspond to introducers while other term forms correpsond to eliminators. In call-by-value, the components of a pair are restricted to values. Hence, the only pair former is (V, W), where the two components are themselves values. The more general construct (M, N) may be added to the call-by-value language by defining it as an abbreviation for (λx. λy. (x, y)) M N. Restricting pairing to values makes the reduction rules and the translation easier to define, and corresponds to a restriction on pairs that arises naturally in call-by-need calculi [Lau93, AFMOW95].

Second, the call-by-value translation also uses the additive product ‘&’ of linear logic. In contrast, Girard’s version of this translation [Gir87] defines

(A × B)^{†} ≡ A^{†} ⊗ B^{†} ,

uses the multiplicative (or tensor) product ‘⊗’ of linear logic. These two products are related by the isomorphism !(A & B) ≃ (!A) ⊗ (!B). Thus our translation is isomorphic to Girard’s, since

A^{†} ⊗ B^{†} ≡ (!A^{‡}) ⊗ (!B^{‡}) ≃ !(A^{‡} & B^{‡}) ≡ !(A × B)^{‡} ≡ (A × B)^{†} .

All results carry through for the extended calculi.

7.2 Sums

Extending the call-by-name translation to sums is straightforward. At the type level, following Girard, the translation is defined by:

(A + B)^{∗} ≡ (!A^{∗}) ⊕ (!B^{∗}) .

Here ⊕ is the additive (or direct) sum of linear logic; the term translation follows immediately.

Extending the call-by-value translation to sums is more problematic. At the type level, again following Girard, we would expect a definition satisfying the isomorphism

(A + B)^{†} ≃ A^{†} ⊕ B^{†} .

Types A, B, C ::= ⋯ | A × B
Terms L, M, N ::= ⋯ | fst M | snd M | p M_{1} ⋯ M_{K}
Values  V, W ::= ⋯ | (M, N) | c

Typing judgements

×-I \frac{Γ ⊢ M : A  Γ ⊢ N : B}{Γ ⊢ (M, N) : A × B}  ×-E_{1} \frac{Γ ⊢ M : A × B}{Γ ⊢ fst M : A}  ×-E_{2} \frac{Γ ⊢ M : A × B}{Γ ⊢ snd M : B}

Const

⊢ c : type_{name}(c)

Prim

Γ_{1} ⊢ M_{1} : type_{name}(p, 1) ⋯ Γ_{k} ⊢ M_{k} : type_{name}(p, k) Γ_{1}, …, Γ_{k} ⊢ p M_{1} ⋯ M_{k} : type_{name}(p, 0)

Reduction relation

(β×_{1})  fst (M, N) → M
(β×_{2})  snd (M, N) → N
(δ)  p c_{1} ⋯ c_{k} → apply_{name}(p, c_{1}, …, c_{k})

Translation

(A × B)^{∗} = A^{∗} & B^{∗}
(M, N)^{∗} = (M^{∗}, N^{∗})
(fst M)^{∗} = fst M^{∗}
(snd M)^{∗} = snd M^{∗}
c^{∗} = c
(p(M_{1}, …, M_{k}))^{∗} = p(M_{1}^{∗}, …, M_{k}^{∗})
type_{lin}(c) = (type_{name}(c))^{∗}
type_{lin}(p, i) = (type_{name}(p, i))^{∗}
apply_{lin}(p c_{1} ⋯ c_{k}) = (apply_{name}(p, c_{1}, …, c_{k}))^{∗}

Figure 8: Extending the call-by-name lambda calculus (name).

As with products it is desirable to re-express the left hand side in the form !(A+B)^{‡}. Unfortunately, it is not clear how to choose a C such that (!A) ⊕ (!B) ≃ !C, and as a result the treatment of sums is less clear.

7.3 Constants and primitives

All of the lambda calculi discussed may be straightforwardly extended by the addition of constants c and primitive applications p M_{1} ⋯ M_{k} of arity k, as shown in Figures 7–9. We specify a total function ‘type’ giving the type of each constant and the types of the arguments and results of each primitive, and a partial function ‘apply’ giving a closed term for each defined application of a primitive to constants. Plotkin [Plo75] explains why it is convenient for ‘apply’ to yield closed terms rather than constants. For the translation to be valid, the interpretation of primitives in the linear calculus must be related to the interpretations in both the call-by-name and call-by-value calculi, as shown in the figures. Again, all results carry through for the extended calculi.

This extension to constants and primitives is particularly useful because it supports the simple version of the operational equivalence theorems given in Section 6. A desire to avoid constants led to a somewhat more complex operational equivalence theorem in our previous work [AFMOW95].

Types A, B, C ::= ⋯ | A × B
Terms L, M, N ::= ⋯ | fst M | snd M | p M_{1} ⋯ M_{k}
Values  V, W ::= ⋯ | (V, W) | c

Typing judgements

×-I_{v} \frac{Γ ⊢ V : A  Γ ⊢ W : B}{Γ ⊢ (V, W) : A × B}  ×-E_{1} \frac{Γ ⊢ M : A × B}{Γ ⊢ fst M : A}  ×-E_{2} \frac{Γ ⊢ M : A × B}{Γ ⊢ snd M : B}

Const \overline{⊢ c : type_{val}(c)}  Prim \frac{Γ_{1} ⊢ M_{1} : type_{val}(p, 1) ⋯ Γ_{k} ⊢ M_{k} : type_{val}(p, k)}{Γ_{1}, …, Γ_{k} ⊢ p M_{1} ⋯ M_{k} : type_{val}(p, 0)}

Reduction relation

(β×_{1}_{v})  fst (V, W) → V
(β×_{2}_{v})  snd (V, W) → W
(δ)  p c_{1} ⋯ c_{k} → apply_{val}(p, c_{1}, …, c_{k})

Translation

(A × B)^{‡} = A^{‡} & B^{‡}
(fst M)^{†} = let !z = M^{†} in fst z
(snd M)^{∗} = let !z = M^{†} in snd z
(p M_{1} ⋯ M_{k})^{†} = let !x_{1} = M_{1}^{†} in ⋯ let !x_{k} = M_{k}^{†} in p x_{1} ⋯ x_{k}
(V, W)^{‡} = (V^{‡}, W^{‡})
c^{‡} = c
type_{lin}(c) = (type_{name}(c))^{†}
type_{lin}(p, i) = (type_{name}(p, i))^{†}
apply_{lin}(p, c_{1}, …, c_{k}) = (apply_{name}(p, c_{1}, …, c_{k}))^{†}

Figure 9: Extending the call-by-value lambda calculus (val).

7.4 Recursion

Adding recursion to the translation is more difficult. There are two problems.

First, it is not clear what typing to use for a recursion operator in the linear calculus. The call-by-name translation suggests that corresponding to the typing

Rec \frac{Γ, x : A ⊢ M : A}{Γ ⊢ μx. M : A}

in name, we should take

Rec \frac{!Γ, !x : !A ⊢ M : A}{!Γ ⊢ μx. M : A}

in lin. But the call-by-value translation suggests that corresponding to the typing

Rec \frac{Γ, x : A ⊢ V : A}{Γ ⊢ μx. V : A}

in val, we should take

Rec \frac{!Γ, !x : !A ⊢ M : !A}{!Γ ⊢ μx. M : !A}

in lin. It is not clear how to reconcile these two choices.

Second, adding recursion to call-by-need poses additional difficulties, as noted in our previous work [AFMOW95]. In order to maintain the sharing typical of call-by-need implementations of recursion, it appears necessary to shift from single, nonrecursive bindings (let x = M in N) to multiple, recursive bindings (let x_{1} = M_{1}, … x_{k} = M_{k} in N). This doesn’t appear to pose any fundamental difficulties for translation, but the expected increase in the size of the calculus is awkward.

7.5 Untyped languages

The confluence and translation results do not depend on types, and so carry through directly for untyped version of these calculi. The only trickiness is that we have used the type rules of the linear lambda calculus to enforce the constraint that variables bound by linear assumptions appear linearly, and that all free variables of a term !M are bound by ! assumptions. It is easy to enforce the same constraints without recourse to types, for instance by using well-formedness judgements. (These can be derived from our typing judgements by simply erasing all the types!)

8 Conclusions

We have shown that call-by-name, call-by-value, call-by-let, and call-by-need can be explained by translations into linear and affine lambda calculi. These transformations begin to provide a logical explanation of call-by-value and call-by-need in the style of the Curry-Howard isomorphism. While we have illuminated substantial issues in the relationship of the various calculi in terms of their translations into the linear calculus, many interesting questions remain. We conclude this summary by mentioning three such issues.

8.1 Standard reductions

Our previous work on call-by-need has actually used a slightly different version of the (V) rule,

(V)  let x = M in C[x] → C[V],

where C is an arbitrary context. If the (β!) rule of the linear and affine calculi is changed in a similar way, then the translation is still preserved.

All three systems of reduction, name, val, and need possess notions of ‘standard’ reduction: normal order for call-by-need, applicative order for call-by-value, and a more complex order for call-by-need which is described in our previous work. In each case, the value of the standard reductions is that they correspond closely to the operational semantics of the language in question. One reason for adopting the variant (V) rule above is that it enables this close correspondence in the case of call-by-need.

We conjecture that there is also a standard reduction order for the linear and affine calculi lin and aff. We have not considered the question of whether the translations preserve standard reductions, or bear some other interesting relation to them.

8.2 Eta rules

It is common to include an (η →) rule in the call-by-name calculus, and an (η →_{v}) rule in the call-by-value calculus.

(η →)  λx. (M x) → M,  if x not free in M
(η →_{v})  λx. (V x) → V,  if x not free in V

Similarly, one might add (η{− \atop ∘}) and (η!) rules to the linear lambda calculus.

(η{− \atop ∘})  λx. (M x)  → M,  if x not free in M
(η!)  let !x = M in !x → M

Types  A, B, C ::= Z | A → B
Terms  L, M, N ::= V | E
Values V ::= x | λx. M
Non-values E  ::= M N | let x = M in N

Typing judgements As for let.

Reduction relation

(β_{v})  (λx. M) V  → M[x := V]
(η_{v})  λx. (V x)  → V,  if x not free in V
(let_{v})  let x = V in M  → M[x := V]
(id)  let x = M in x  → M
(comp)  let y = (let x = L in M) in N → let x = L in (let y = M in N)
(let.1)  E M  → let z = E in z M
(let.2)  V E  → let x = E in V x

Figure 10: Moggi’s computational lambda calculus comp.

The second of these is similar to the right unit law in Moggi’s computation lambda calculus [Mog88, Mog89]. Just as a (β) rule simplifies a logical introduction followed by the corresponding logical elimination, so each of these (η) rules simplifies a logical elimination followed by the corresponding logical introduction.

One would expect that the translation ∗ from name to lin should preserve the (η) rule, that the translation † from val to lin should preserve the (η_{v}) rule, and that the translation † from need to aff should preserve the (η) rule. None of these are the case, which suggests that perhaps more reduction rules should be added to lin and aff. Various rules seem possible, but so far we have not found rules with the same logical resonance as those considered in this paper.

8.3 Equality and Moggi’s computational lambda calculus

In addition to reduction, one usually also considers a theory of equality. Given a confluent notion of reduction → →, one defines = as its reflexive, symmetric, and transitive closure. It follows from the Church-Rosser theorem that M = N if and only if there exists a term L such that M → → L and N → → L.

For the translation ∗ from name to lin, it is relatively easy to show that not only do we have that M ⟶^{name} → N if and only if M^{∗} ⟶^{lin} → N^{∗}, but we also have M =^{name} N if and only if M^{∗} =^{lin} N^{∗}.

For the translation † from let to lin, the fact that M ⟶^{let} → N if and only if M^{†} ⟶^{lin} → N^{†} guarantees that M =^{let} N implies M^{†} =^{lin} N^{†}. However, the reverse implication does not hold, since we may have M^{†} ⟶^{lin} → L and N^{†} ⟶^{lin} → L without having L be of the form K^{†} for some K in let. For instance, it is easy to see that (let x = M in x N)^{†} =^{lin} (M N)^{†}, but not (let x = M in x N) =^{let} (M N).

It is reasonable to ask if more laws could be added to let to yield a theory (LET’) for which

M =^{let′} N if and only if M^{∗} =^{lin} N^{∗}. A candidate for such a theory is Moggi’s computational lambda calculus comp [Mog88, Mog89], as shown in Figure 10. (The version shown here is based on the untyped reduction calculus, which appears in the technical report [Mog88] but not the LICS paper [Mog89].) The grammar of this theory is the same as for let, except that both values and non-values are distinguished. This system satisfies subject reduction, and Moggi shows that it is confluent. The system is designed so that, apart from rule (β_{v}), it is strongly normalising, even without types.

It is not hard to show that the equalities of let are properly contained in the equalities of comp; that is, M =^{let} N implies M =^{comp} N, but not conversely. Furthermore, the reductions of let and the reductions of comp are incomparable; that is, M ⟶^{let} → N does not imply M ⟶^{comp} → N, nor is the converse true. It is interesting open question whether there is an extension of let that has the same equalities as comp. It is a further interesting question to know if there is an extension of lin such that the encoding of the extended let into the extended lin via † is sound and complete.

This question brings us full circle. Plotkin showed that the continuation passing style (CPS) translation from val into itself is sound but not complete [Plo75]. Moggi designed comp to be sound and complete for the monad translation (which generalises CPS) [Mog88], and Sabry and Felleisen verified that the CPS translation from comp into val is both sound and complete [SF93], thus answering the question implicitly raised by Plotkin.

It can be seen that the questions raised here about complete extensions of let are in a similar vein. It is not clear if the translations into linear lambda calculus described here will have the same value as the translations into continuation passing style described by Plotkin. But if our answers are not as good, we can at least claim to be asking the right sort of questions!

References

[Abr92] S. Abramsky, The lazy lambda calculus. In D. Turner, editor, Research topics in functional programming, Addison-Wesley, 1992.

[Abr93] S. Abramsky, Computational interpretations of linear logic. Theoretical Computer Science 111:3–57, 1993.

[AF94] Z. Ariola and M. Felleisen, The call-by-need lambda calculus. Technical Report CIS-TR-94-23, Department of Computer Science, University of Oregon, October 1994.

[AFMOW95] Z. Ariola, M. Felleisen, J. Maraist, M. Odersky, and P. Wadler. A call-by-need lambda calculus. Symposium on Principles of Programming Languages, ACM Press, San Francisco, California, January 1995.

[Bar81] H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Computer Science. North-Holland Publishing Company, 1981.

[BH90] H. P. Barendregt and K. Hemerik. Types in Lambda Calculus and Programming Languages, Proc. ESOP ’90, European Symposium on Programming, p. 1–35. Springer-Verlag, Lecture Notes in Computer Science 432, 1990.

[BBdPH92] N. Benton, G. Bierman, V. de Paiva, and M. Hyland, Type assignment for intuitionistic linear logic. Draft paper, August 1992.

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

[Gir92] J.-Y. Girard, Message to ‘linear’ electronic mailing list, September 1992.

[Gir93] J.-Y. Girard, On the unity of logic. Annals of Pure and Applied Logic, 59:201–217, 1993.

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

[Jac92] B. Jacobs, Semantics of weakening and contraction. Manuscript, Cambridge University, May 1992. Available from bjacobs@cwi.nl.

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

[Lau93] J. Launchbury, A natural semantics for lazy evaluation, Symposium on Principles of Programming Languages, ACM Press, Charleston, South Carolina, January 1993.

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

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

[Mog88] E. Moggi, Computational lambda-calculus and monads. Technical Report ECS-LFCS-88-66, Laboratory for the Foundations of Computer Science, University of Edinburgh, October 1988.

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

[MOW94] J. Maraist, M. Odersky, and P. Wadler. The call-by-need lambda calculus (Unabridged). Technical Report 28/94, Fakultät für Informatik, Universität Karlsruhe, October 1994. Also appears as a technical report of the Department of Computing Science, University of Glasgow.

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

[Plo93] G. D. Plotkin, private communication. (During the 1993 MFPS, even!)

[Rey93] J. C. Reynolds, The discoveries of continuations. Lisp and Symbolic Computation, 6(3/4):233–248, November 1993.

[RR94] S. R. della Rocca and L. Roversi, Lambda calculus and intuitionistic linear logic. Manuscript, July 1994. (Available from L. Roversi, University of Pisa,

rover@di.unipi.it.)

[Sch94] H. Schellinx, The noble art of linear decorating. Ph.D. dissertation, Institute for Logic, Language, and Computation, University of Amsterdam, 1994.

[SF93] A. Sabry and M. Felleisen, Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 6(3/4):289–360, November 1993.

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

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

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

[Wad93a] P. Wadler, A syntax for linear logic. Ninth International Conference on the Mathematical Foundations of Programming Semantics, New Orleans, Louisiana, April 1993. Springer Verlag, LNCS 802.

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

A Subject reduction for linear calculus

This appendix details the proof of the subject reduction theorem for the linear calclus lin.

Rule (β{− \atop ∘}) arises when a {− \atop ∘}-I rule meets a {− \atop ∘}-E rule.

x : A ⊢ x : A ; \begin{matrix}· \\ · \\ · \end{matrix} ; Γ, x : A ⋯ ⊢ M : B ; \overline{{− \atop ∘}-I} ; Γ ⊢ λx. M : A {− \atop ∘} B  \begin{matrix}· \\ · \\ · \end{matrix} ; Δ ⊢ N : A
\overline{→-E}
Γ, Δ ⊢ (λx. M) N : B
⇓

\begin{matrix}· \\ · \\ · \end{matrix} ; Δ ⊢ N : A

\begin{matrix}· \\ · \\ · \end{matrix}

Γ, Δ ⊢ M[x := N] : B

Rule (β!) arises when a !-I rule meets a !-E rule.

\begin{matrix}· \\ · \\ · \end{matrix} ; !Γ ⊢ M : A ; \overline{!-I} ; !Γ ⊢ !M : !A  \overline{Id} ; x_{1} : A ⊢ x_{1} : A ⋯ \overline{Id} ; x_{k} : A ⊢ x_{k} : A ; \begin{matrix}· \\ · \\ · \end{matrix} ; Δ, x_{1} : A, … x_{k} : A ⊢ N_{1...k} : B ; = ; Δ, !x : !A ⊢ N : B
\overline{!-E}
!Γ, Δ ⊢ let !x = !M in u : B

⇓

\begin{matrix}· \\ · \\ · \end{matrix} ; !Γ_{1} ⊢ M_{1} : A ⋯ \begin{matrix}· \\ · \\ · \end{matrix} ; !Γ_{k} ⊢ M_{k} : A

\begin{matrix}· \\ · \\ · \end{matrix}

!Γ_{1}, …, !Γ_{n}, Δ ⊢ N_{1...k}[x_{1} := M_{1}, …, x_{k} := M_{k}] : B = !Γ, Δ ⊢ N[x := M] : B

This rule requires some additional explanation. The double bars stand for a number of applications of Contraction, Weakening, and Dereliction. Subscripts have been introduced to handle the renaming required by contraction. Assume Δ, !x : !A ⊢ N : B, where there are k occurrences of x in N. Let N_{1...k} be the same term where these occurrences are replaced respectively by the distinct fresh variables x_{1}, …, x_{k}, so that N = N_{1...k}[x_{1} := x, … x_{k} := x]. Assume !Γ ⊢ M : A. For each i in the range 1 … k, let σ_{i} be a substitution taking the variables in Γ into fresh distinct variables, and take M_{i} = M[σ_{i}] and Γ_{i} = Γ[σ_{i}].

Rule (!!) arises when two !-E rules meet, commuting one through the other.

\begin{matrix}· \\ · \\ · \end{matrix} ; Γ ⊢ L : !A  \begin{matrix}· \\ · \\ · \end{matrix} ; Δ, !x : !A ⊢ M : !B
\overline{!-E}
Γ, Δ ⊢ let !x = L in M : !B

\begin{matrix}· \\ · \\ · \end{matrix} Θ, !y : !B ⊢ N : C

\overline{!-E}

Γ, Δ, Θ ⊢ let !y = (let !x = L in M) in N : C

⇓

\begin{matrix}· \\ · \\ · \end{matrix} Γ ⊢ L : !A \begin{matrix}· \\ · \\ · \end{matrix} ; Δ, !x : !A ⊢ M : !B \begin{matrix}· \\ · \\ · \end{matrix} ; Θ, !y : !B ⊢ N : C

\overline{!-E}
Δ, Θ, !x : !A ⊢ let !y = M in N : C
\overline{!-E}
Γ, Δ, Θ ⊢ let x = L in (let y = M in N) : C

Rule (!{− \atop ∘}) arises when a !-E rule meets a {− \atop ∘}-E rule, commuting one through the other.

\begin{matrix}· \\ · \\ · \end{matrix} ; Γ ⊢ L : !A  \begin{matrix}· \\ · \\ · \end{matrix} ; Δ, !x : !A ⊢ M : B {− \atop ∘} C
\overline{!-E}

Γ, Δ ⊢ let !x = L in M : B {− \atop ∘} C

\begin{matrix}· \\ · \\ · \end{matrix} Θ ⊢ N : B

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

Γ, Δ, Θ ⊢ (let !x = L in M) N : C

⇓
\begin{matrix}· \\ · \\ · \end{matrix} ; Γ ⊢ L : !A  \begin{matrix}· \\ · \\ · \end{matrix} ; Δ, !x : !A ⊢ M : B {− \atop ∘} C  \begin{matrix}· \\ · \\ · \end{matrix} ; Θ, ⊢ N : B ; \overline{{− \atop ∘}-E} ; Δ, Θ, !x : !A ⊢ M N : C
\overline{!-E}
Γ, Δ, Θ ⊢ let x = L in (M N) : C

The (!W) rule of affine lambda calculus arises when commuting (!-E) through Weakening.

\begin{matrix}· \\ · \\ · \end{matrix} Γ ⊢ M : !A \begin{matrix}· \\ · \\ · \end{matrix} ; Δ ⊢ N : B

\overline{Weakening}

Δ, !x : !A ⊢ N : B

\overline{!-E}

Γ, Δ ⊢ let !x = M in N : B
⇓

\begin{matrix}· \\ · \\ · \end{matrix} ; Δ ⊢ N : B

= Weakening

Γ, Δ ⊢ N : B

B let as a conservative extension of val

Definition. We take the operator .^{−LET} to map let-terms to val-terms by reverting letexpressions to applications of abstractions, viz.,

(let x = M in N)^{−LET} = (λx. (M^{−LET})) (N^{−LET})  (M N)^{−LET} = (M^{−LET}) (N^{−LET})
x^{−LET} = x  (λx. M)^{−LET} = λx. (M^{−LET}) .

Proposition. Let M ⟶_{R}^{let} N, for some rule R. Then M[x := V] ⟶_{R}^{let} N[x := V].

Proof. Trivial, since replacing one value by another will not prevent any contractions, but note that the result does not hold for substitution of arbitrary terms. □

Proposition. Let M ≡ let x = M_{0} in M_{1}.

1. If M ⟶_{(I,V)}^{let} → N ^{∈} val, then there exists some value V_{0} such that

M_{0} ⟶_{(I,V)}^{let} → V_{0} , and
M_{1}[x := V_{0}] ⟶_{(I,V)}^{let} → N .

2. If M ⟶_{(I,V)}^{let} → V, then there exists some value V_{0} such that

M_{0} ⟶_{(I,V)}^{let} → V_{0} , and
M_{1}[x := V_{0}] ⟶_{(I,V)}^{let} → V .

Proof. Part 1 holds because the let-binding must be removed for N to be a val-term. Taking σ to be the name of the reduction

σ : M ⟶_{(I,V)}^{let} → N ,

we must clearly have σ = σ_{1} + σ_{2} + σ_{3},

σ_{1} : M ≡ let x = M_{0} in M_{1} ⟶_{(I,V)}^{let} → let x = V_{0} in M′_{1}
σ_{2} :  let x = V_{0} in M′_{1} ⟶_{(I,V)}^{let} → M′_{1}[x := V_{0}]
σ_{3} :  M′_{1}[x := V_{0}] ⟶_{(I,V)}^{let} → N .

where σ_{1} is the interleaving of two independant reductions

σ_{1a} : M_{0} ⟶_{(I,V)}^{let} → V_{0} , and
σ_{1b} : M_{1} ⟶_{(I,V)}^{let} → M′_{1} .

By the preceeding proposition, σ_{1b} gives us

M_{1}[x := V_{0}] ⟶_{(I,V)}^{let} → M′_{1}[x := V_{0}] ,

and the result follows. Part 2 is similar; again the top-level let-construct must be contracted away to produce the given result. □

Proposition. Let ⟨M, M′⟩ ^{∈} (A, C), M′ ⟶_{(I,V)}^{let} → N ^{∈} val. Then

M ⟶_{(I,V)}^{let} → N .

Proof. For ⟨M, M′⟩ ^{∈} (A) we have

M ≡ let x = (let y = M_{0} in M_{1}) in M_{2}
M′ ≡ let y = M_{0} in (let x = M_{1} in M_{2}) .

We know that M_{0} ⟶^{let} → V_{0}, M_{1}[y := V_{0}] ⟶^{let} → V_{1} and M_{2}[y := V_{1}] ⟶^{let} → N from the preceeding proposition, and the result follows.

For ⟨M, M′⟩ ^{∈} (C) we have

M ≡ (let x = M_{0} in M_{1}) M_{2}
M′ ≡ let x = M_{0} in (M_{1} M_{2}) .

As before, we have M_{0} ⟶^{let} → V_{0} and

(M_{1} M_{2})[x := V_{0}] ⟶_{(I,V)}^{let} → N ,

and since X ^{∉} fv(M_{2}),

(M_{1} M_{2})[x := V_{0}] ≡ (M_{1}[x := V_{0}]) M_{2}

we have the the result as follows,

M ≡ (let x = M_{0} in M_{1}) M_{2}
⟶_{(I,V)}^{let} → (let x = V_{0} in M_{1}) M_{2}
⟶_{(V)}^{let} (M_{1}[x := V_{0}]) M_{2}
⟶_{(I,V)}^{let} → N .

□

Proposition. Let M ⟶^{let} M′ ⟶_{(I,V)}^{let} → N ^{∈} val. Then M ⟶_{(I,V)}^{let} → N.

Proof. Unfortunately the preceeding result does not generalize very easily. The problem arises from internal (A)-redexes like

(λx. f (λx. x) (f (λx. x x))) (λg. let y = let z = g g in z z in y y) ,

where the (A)-redex must be both duplicated and given substitutions before it reduces to produce two (V)-redexes.

The solution is to use an extended reduction system over marked let-bindings. The markings are reminiscent of Barendregt’s marked (β →)-redexes [Bar81], except that where Barendregt marks terms which already are redexes, we mark bindings which must — since N ^{∈} val — becomes (V)-redexes.

We rely on a series of three basic lemmas for the result, both of which rely rely on keeping track of the marked bindings.

1. Lemma. For M ^{∈} let (unmarked!) and subterms and contexts such that

M ≡ C_{1}[(λx. M_{0}) N_{0}] ⟶_{(I′)}^{let} C_{1}[let x = N_{0} in M_{0}]
⟶_{(V)}^{let} C_{2}[M_{1}[x := V_{1}]] ≡ N ,

we also have

M ⟶_{(I)}^{let} → C′_{2}[let x = V′_{1} in M′_{1}] ⟶_{(V)}^{let} C′_{2}[M′_{1}[x := V′_{1}]] ⟶_{(I′)}^{let} → N ,

where we have at least one of the two identities M_{1} ≡ M′_{1} and V_{1} ≡ V′_{1}, and if not both then the (I′)-redex is within either M_{1} or V_{1}.

Proof. Trivial, by induction on the contexts. □

This lemma means that we may postpone (I)-contractions until just before the (V) contraction which removes the new binding, introducing never-removed bindings only last. We may end with more (I)-contractions than before, but the number of (V)-contractions will remain constant.

2. The first lemma lets us extend the usual standardization properties for call-by-value to (I, V)- reduction. We do not need to spell out the strategy; rather, we need only its existance for the following property.

Lemma. There is a standard strategy ⟶_{s} for selecting (I, V)-redexes with the property that for all M ^{∈} let (which (I, V)-reduces to an abstraction) we have V_{0} ^{∈} let such that

M ⟶_{(I,V)}^{let} → V ⟹ M ⟶_{s} V_{0} ⟶_{(I,V)}^{let} → V .

Proof. We write M ⟶_{(I^{?}V)}^{let} N iff either

(a) M ⟶_{(V)}^{let} N or

(b) M ⟶_{(I)}^{let} M′ ⟶_{(V)}^{let} N, where the (I)-contractum and (V)-contractum are the same.

Then by the first lemma, we have that any let reduction sequence can be written as ⟶_{(I^{?}V)}^{let}

contractions followed by ⟶_{(I)}^{let} contractions, and the lemma follows from the correponding

result for val sequences by identifying ⟶_{(I^{?}V)}^{let} steps with β_{v} → steps in terms equivalent

modulo (I)-reduction. □

3. Here we introduce terms including marked let bindings, let′.

Lemma. If we have N ^{∈} let (unmarked!) and C, C_{i}, M′_{i}, V′_{i}, M′′_{i} ^{∈} let′ such that

C[let′ y = M′_{0} in let′ x = V_{0} in M′′_{0}]
⟶_{(V)}^{let} C[let′ y = M′_{0} in M′′_{0}[x := V_{0}]]
⟶_{(I,V)}^{let} → C_{1}[let′ y = V′_{1} in M′′_{1}] ⟶_{(V′)}^{let} C_{1}[M′′_{1}[y := V′_{1}]]
⟶_{(I,V)}^{let} → C_{2}[let′ y = V′_{2} in M′′_{2}] ⟶_{(V′)}^{let} C_{2}[M′′_{2}[y := V′_{2}]]
⋮
⟶_{(I,V)}^{let} → C_{n}[let′ y = V′_{n} in M′′_{n}] ⟶_{(V′)}^{let} C_{n}[M′′_{n}[y := V′_{n}]]

then we have V′_{0}, C′_{i,j} all in let′ such that

C[let’ y = M_{0} in let’ x = V_{0} in M′′_{0}]

⟶_{(I,V)}^{let} C[let’ y = V′_{0} in let’ x = V_{0} in M′′_{0}]
⟶_{(V)}^{let} C[let’ x = V_{0}[y := V′_{0}] in M′′_{0}[y := V′_{0}]]
⟶_{(V)}^{let} C[(M′′_{0}[y := V′_{0}])[x := (V_{0}[y := V′_{0}])]]
≡ C′_{1,1}[V′_{0}] ⟶_{(I,V)}^{let} C′_{1,1}[V′_{1}] ≡ C′_{1,2}[V′_{0}] ⟶_{(I,V)}^{let} C′_{1,2}[V′_{1}]
≡ ⋯ ≡ C′_{1,i_{1}}[V′_{0}] ⟶_{(I,V)}^{let} C′_{1,i_{1}}[V′_{1}]
≡ C′_{2,1}[V′_{0}] ⟶_{(I,V)}^{let} C′_{2,1}[V′_{1}] ≡ C′_{2,2}[V′_{0}] ⟶_{(I,V)}^{let} C′_{2,2}[V′_{1}]
≡ ⋯ ≡ C′_{2,i_{1}}[V′_{0}] ⟶_{(I,V)}^{let} C′_{2,i_{1}}[V′_{1}]
⋮
≡ C′_{n,1}[V′_{0}] ⟶_{(I,V)}^{let} C′_{n,1}[V′_{1}] ≡ C′_{n,2}[V′_{0}] ⟶_{(I,V)}^{let} C′_{n,2}[V′_{1}]
≡ ⋯ ≡ C′_{n,i_{1}}[V′_{0}] ⟶_{(I,V)}^{let} C′_{n,i_{1}}[V′_{1}] ≡ N .

Proof. Follows immediately from the preceeding result. □

Then to prove the proposition, we observe that elementary analysis of term structures will resolve all cases except that described by the last lemma, so the result follows immediately. □

Proposition. Let M ⟶^{let} → N ^{∈} val. Then

M ⟶_{(I,V)}^{let} → N .  (1)

Proof. Follows immediately from the above result by induction on the length of the length of reduction sequence. □ Proposition. Let M, M_{0} ^{∈} let and M′_{0}, N ^{∈} val such that

[figure: M_{0}; M′_{0}; N ^{∈} val; let; (I, V); −LET; val] .

1. If M ⟶_{(V)}^{let} → M_{0}, then M^{−LET} ⟶^{val} → M′_{0}:

[figure: M; ∃M′; M_{0}; M′_{0}; N ^{∈} val; let; (V); let; (I, V); −LET; val; ^{. . . . . . .}; let; . . . . . . . .; val] .

2. If M ⟶_{(I)}^{let} → M_{0}, then M^{−LET} ≡ M′_{0}:

[figure: M; M_{0}; M′_{0}; N ^{∈} val; let; (I); let; (I, V); −LET; val; ^{. . . . . . . . . .}; let] .

Proof. Part 1 is by a simple structural induction on M; part 2 is trivial. □ Proposition. For M ^{∈} let, if M ⟶_{(I,V)}^{let} → N ^{∈} val then M^{−LET} ⟶^{val} → N. Proof. Follows from the previous result by induction on the length of the reduction sequence. Proposition. For M, N ^{∈} val, if M ⟶^{let} → N then M ⟶^{val} → N. Proof. Follows from the preceeding proposition and Equation 1, since for M ^{∈} val we have M^{−LET} ≡ M:

M ⟶^{let} → N ^{∈} val ⟹ M ⟶_{(I,V)}^{let} → N ^{∈} val
⟹ M^{−LET} ⟶^{val} → N
⟹ M ⟶^{val} → N .