# A reflection on call-by-value.

One way to model a sound and complete translation from a source calculus into a target calculus is with an adjoint or a Galois connection. In the special case of a reflection, one also has that the target calculus is isomorphic to a subset of the source. We show that three widely studied translations form reflections. We use as our source language Moggi's computational lambda calculus, which is an extension of Plotkin's call-by-value calculus. We show that Plotkin's CPS translation, Moggi's monad translation, and Girard's translation to linear logic can all be regarded as reflections from this source language, and we put forward the computational lambda calculus as a model of call-by-value computation that improves on the traditional call-by-value calculus. Our work strengthens Plotkin's and Moggi's original results and improves on recent work based on equational correspondence, which uses equations rather than reductions.Categories and Subject Descriptors: D.1.1 [Programming Techniques]: Applicative Functional) Programming; D.3.4 [Programming Languages]: Processors -- compilers; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic

General Terms: Languages, Theory

Additional Key Words and Phrases: Category theory, compiling, continuations, Galois connections

1. INTRODUCTION

Compiler correctness is a central concern of computing. It is often expressed in the form of a diagram.

[DIAGRAM OMITTED]

Here the upper arrow indicates reduction in the source calculus S; the lower arrow indicates reduction in the target calculus T; the downward arrow indicates the compiling map *; and the upward arrow indicates the decompiling map #.

The diagram states that compiling, evaluating in the target, and decompiling is equivalent to evaluating in the source. There are two forms this equivalence may take.

-- Soundness. Every reduction in the source is valid in the target: If [M.sup.*] ?? S [N.sup.#] then [M.sup.*] ?? T N. -- Completeness. Every reduction in the target is valid in the source: If [M.sup.*] ?? T N then M ?? S [N.sup.#].

If both properties are present, one has what theorists call an adjoint or a Galois connection.

Sometimes one has a further pleasant property, that compiling is a left inverse to decompiling, [N.sup.#*] [equivalent] N for every target term N, where [equivalent] is syntactic identity (up to renaming). This special form of an adjoint is called a reflection. Whenever a reflection exists, the target is isomorphic to a subset of the source, which we call the kernel.

We show that three widely studied translations may be regarded as reflections. Our source calculus is the computational calculus, [Lambda.sub.c], of Moggi [1988], which extends the call-by-value lambda calculus, [Lambda.sub.v], of Plotkin [1975]. Our first translation is the continuation passing style (CPS) translation, also of Plotkin [1975]. Our second translation is into the monadic metalanguage, [Lambda.sub.ml], also of Moggi [1988]. The CPS translation arises as a special case of the monad translation, and factors through it. Our third translation is into a calculus based on the linear logic of Girard [1987]. Our linear calculus is closely related to formulations devised independently by Wadler [1993b] and Barber [1995].

We do not merely shoehorn the classic CPS and monad translations into a new framework, we actually improve on them, taking results previously proved for equalities and extending them to reductions. Further, we show for the first time that Moggi's computational lambda calculus [Lambda.sub.c], actually has computational content, and therefore might serve as an improvement over Plotkin's call-by-value lambda calculus [Lambda.sub.v].

Plotkin [1975] showed, among other things, that the call-by-value CPS translation was sound but not complete, in that it preserves but does not reflect equalities. Plotkin devised the call-by-value lambda calculus [Lambda.sub.v], to model some operational properties of programming languages, notably procedure calls. It was a calculus with a reduction theory, from which one can derive an equational theory. As usual, we take equality to be the symmetric, transitive, and reflexive closure of reduction; it follows from the Church-Rosser theorem that two terms are equal if and only if they reduce to a common term. Plotkin's CPS translation (here written *) takes the call-by-value calculus [Lambda.sub.v], (the source) into the traditional call-by-name lambda calculus [Lambda.sub.n] (the target). Plotkin proved the translation is sound, in that if M = N in the source then [M.sup.*] = [N.sup.*] in the target, and showed it is not complete, in that the converse does not hold. He proved soundness by showing that the translation preserves reductions, so if M ?? N in the source then [M.sup.*] ?? [N.sup.*] in the target.

A baker's dozen of years later, Moggi [1988] showed, among other things, that the call-by-value monad translation is both sound and complete, in that it preserves and reflects equalities. Moggi devised the monadic metalanguage [Lambda.sub.ml] to model some denotational properties of programming languages, notably computational effects and their interaction with procedure calls; the theory included CPS as a special case. The original [Lambda.sub.ml] had an equational theory only. Moggi's monad translation (here written *) takes the computational lambda calculus [Lambda.sub.c] (the source) into the metalanguage [Lambda.sub.ml] (the target). The translation is both sound and complete, in that M = N in the source if and only if [M.sup.*] = [N.sup.*] in the target. This is hardly a surprise, as [Lambda.sub.c] was designed precisely so this result would hold.

Later still, Sabry and Felleisen [1993] strengthened Plotkin's result using Moggi's. Their variant of the CPS translation (here written *) takes the computational lambda calculus [Lambda.sub.c] (the source) into the traditional call-by-name lambda calculus [Lambda.sub.n] (the target). They showed that M = N in the source if and only if [M.sup.*] = [N.sup.*] in the target. Further, they introduced an inverse CPS translation (here written #) such that M = N in the target if and only if [M.sub.#] = [N.sub.*] in the source, and M = [M.sup.*#] in the source, and [N.sup.#*] = N in the target. Taken together, these conditions amount to an equational correspondence. This result showed that monads in general and continuations in particular satisfy exactly the same equations.

Hatcliff and Danvy [1994] strengthened Moggi's result by showing that the monad translation is also an equational correspondence. This extension of Moggi's unsurprising result is equally unsurprising.

What is surprising is how little attention was paid to reductions. The original technical report [Moggi 1988] specified theories of reduction and of equality for [Lambda.sub.c]; however, only the equality theory of [Lambda.sub.c] appears in the conference paper [Moggi 1989], and [Lambda.sub.c] rates barely a line in the journal version [Moggi 1991]. None of these contains a reduction theory for [Lambda.sub.ml], though this was considered by Hatcliff and Danvy [1994]. However, ours is the first work we know of to relate the reductions of [Lambda.sub.c] and [Lambda.sub.ml].

Our results supersede all of the preceding results, replacing equalities with reductions. The existence of an adjoint is equivalent to stating that M ?? N in the source implies [M.sup.*] ?? [N.sup.*] in the target, and M ?? N in the target implies [M.sup.#] ?? [N.sup.*] in the source, and M ?? [M.sup.*#] in the source, and [N.sup.#*] ?? N in the target. These trivially imply the existence of an equational correspondence. Further, since we have a reflection, the mere equality [N.sup.#*] = N of the equational correspondence is here replaced by syntactic identity [N.sup.#*] [equivalent] N.

Although Moggi introduced a confluent reduction theory for [Lambda.sub.c], it appears to be treated purely as a technical trick to aid equational reasoning. There is no evidence that Moggi considered it as a model of computation via reduction (and he later confirmed this in a personal communication). Further, [Lambda.sub.c] has two rules, (let.1) and (let.2) that look more like expansions then reductions. The order Moggi picked for them was dictated purely by a technicality: the need for confluence. Nonetheless, the results here show that [Lambda.sub.c] relates closely to several models of computation, including ordinary lambda calculus via CPS and the monadic metalanguage. More precisely, there exists an isomorphism between the kernel of [Lambda.sub.c] and suitably "shrunk" versions of each of the target calculi. It turns out that the dubious rules (let.1) and (let.2) have a natural interpretation as administrative reductions (that is, they can be viewed as occurring at compile time rather than run time), which makes them far more intuitive: they correspond to the naming of subterms, which is considered one of the beneficial properties of CPS.

The process of "shrinking" the target languages T deserves some clarification. In general the goal is to find a sublanguage [T.sub.*] of T whose set of terms is a subset of the set of T-terms and whose reductions are consistent with the T-reductions. The restricted set of [T.sub.*]-terms is straightforward to specify: it should contain those terms (1) that are reachable from the source language via the translation to the target language and (2) that are closed under the [T.sub.*]-reductions. The set of [T.sub.*]-reductions is more problematic to specify. Ideally the restricted set of reductions would be the same as the set of T-reductions, only restricted to the smaller syntax. And indeed such a case arises when restricting [Lambda.sub.ml] to [Lambda.sub.ml*]. The other two cases are less than ideal. For the shrinking of [Lambda.sub.n] to [Lambda.sub.cps], some of the reductions of [Lambda.sub.cps] correspond to a sequence of two [Lambda.sub.n]-reductions. For the shrinking of [Lambda.sub.lin] to [Lambda.sub.lin*], one of the [Lambda.sub.lin]. reductions corresponds to an equality of [Lambda.sub.lin]. One way to fix this bad fit between [Lambda.sub.lin] and [Lambda.sub.lin*]. might be to develop a new linear calculus with a more suitable computational model.

While the step from equalities to reductions seems natural in retrospect, we doubt we would have taken it without the guiding light of category theory. In particular, we were motivated by noting the close resemblance between the notion of equational correspondence in Sabry and Felleisen [1993] and the properties of an adjunction.

Related Work. Like the wheel, CPS is such an excellent idea that it was reinvented many times [Reynolds 1993). Two formalizations are due to Fischer [1972] and Plotkin [1975]. It was proposed as a basis for compiler construction by Steele [1978] and subsequently exploited by Kranz et al. [1986], Appel [1992], and others.

One might hope that the variant CPS translation of Fischer [1972] is also a reflection. An earlier version of this article [Sabry and Wadler 1996] claimed this was the case, but gave no proof. We should have been more cautious. Here we show that it is impossible for the Fischer CPS translation to be a reflection.

In applications of CPS to compiling, one first translates the source into the target via CPS and then optimizes the target. One claim of Sabry and Felleisen [1993] was that one could perform the same optimizations directly in the source, and this was further elaborated by Flanagan et al. [1993]. However, the claim was not properly justified: it was only shown that the same equations hold in the source and target. Here we show for the first time that the same reductions hold in source and target, which more properly corresponds to optimization.

Lawall and Danvy [1993] make much of relating forward and inverse translations via two Galois connections and an isomorphism. Their Galois connections are induced from the translations and are not defined a priori. Furthermore, their order is based on the syntactic structure of terms as opposed to their semantic properties under reduction, and it is not preserved by their isomorphism. Hence their three maps do not compose to give a single Galois connection between source and target, whereas here we show such a connection.

Administrative reductions play a central role in many CPS translations, from Plotkin's work onward. Sabry and Felleisen [1993] show a correspondence between what they dub the A-reductions in the source and administrative reductions in the target similar correspondences are studied by Flanagan et al. [1993] and Hatcliff and Danvy [1994]. Here we show that administrative reductions correspond precisely to the reductions M [right arrow] [M.sup.*#] implied by the existence of the adjunction, and we show that the A-normal form corresponds to the kernel of the reflection, the isomorphic image of the target in the source.

The adjunction is a central abstraction of category theory [Mac Lane 1971] and has the Galois connection as a degenerate case [Davey and Priestley 1990]. Adjoints and Galois connections have long been the tool of choice for relating semantic models, but are less often used to relate operational models. A notable exception is the work of Melton et al. [1985], who discuss a notion of compiler correctness strikingly similar to ours. However, their Galois connections happen to be insertions (the map * from source to target is injective), while ours are reflections (the map # from target to source is injective).

Moggi [1988] presents [Lambda.sub.c] as an untyped calculus of reductions and presents [Lambda.sub.ml] as a typed calculus of equalities. Here we uniformly use untyped calculi of reductions. So far as we can see, everything works equally well for typed calculi of reductions, such as those considered by Hatcliff and Danvy [1994], since we conjecture that our translations preserve types.

This article is a revised and extended version of a conference paper with the same title [Sabry and Wadler 1996). The material on the linear calculus and on the Fischer CPS translation is new.

Outline. The remainder of this article is structured as follows. Section 2 summarizes our results. Section 3 introduces Galois connections and reflections. Section 4 reviews the traditional translation of [Lambda.sub.v] into [Lambda.sub.ml] and reviews why it fails to be a reflection. Section 5 shows that there is a reflection between [Lambda.sub.c] and a variant [Lambda.sub.ml*] of [Lambda.sub.ml]. Section 6 factors this reflection through an intermediate calculus [Lambda.sub.c*] corresponding to the isomorphic image of [Lambda.sub.ml*] in [Lambda.sub.c]. Section 7 extends the results to a translation into linear logic, and Section 8 deals with translations into CPS. Section 9 observes that the variant CPS translation due to Fischer cannot be a reflection. Section 10 describes related work. Section 11 concludes.

2. SUMMARY

If you like to see a summary in advance, read this section now; if you like to see a summary on completion, save it until the end. Depending on your preference, you may thereby read this section once, twice, or never.

Figure 1 illustrates a road-map of the terrain we cover. First, we consider the traditional monad translation from into [Lambda.sub.v] into [Lambda.sub.ml]. This translation is not a reflection; but expanding [Lambda.sub.v] into [Lambda.sub.c], shrinking [Lambda.sub.ml] into [Lambda.sub.ml*], and fine-tuning the translation finally yields a reflection in [Lambda.sub.c] of [Lambda.sub.ml*]. The existence of a reflection guarantees that there is a kernel [Lambda.sub.c*] of [Lambda.sub.c] that is isomorphic to [Lambda.ml*]. Calculus [Lambda.sub.c] has seven reduction rules, and [Lambda.sub.c*] arises by normalizing with respect to two of these rules: (let.1) and (let.2).

[FIGURE 1 ILLUSTRATION OMITTED]

Second, we consider the translation from [Lambda.sub.v] to a linear calculus [Lambda.sub.lin]. The translation has essentially the same properties as the previous monad translation. As before, making the translation into a reflection requires expanding [Lambda.sub.v] into [Lambda.sub.c] and shrinking [Lambda.sub.lin] to [Lambda.sub.lin*]; the reflection also guarantees that [Lambda.sub.lin*] is isomorphic to the kernel computational calculus [Lambda.sub.c*].

Finally we consider the traditional CPS translation from [Lambda.sub.v] into [Lambda.sub.n]. Again, this translation is not a reflection; but expanding [Lambda.sub.v] into [Lambda.sub.n] shrinking [Lambda.sub.n] into [Lambda.sub.cps], and fine-tuning the translation yields a reflection in [Lambda.sub.c] of [Lambda.sub.cps]. Again, the existence of a reflection guarantees that there is a kernel [Lambda.sub.c**] of [Lambda.sub.c] that is isomorphic to [Lambda.sub.cps]. Calculus [Lambda.sub.c**] arises by normalizing [Lambda.sub.c*] with regard to one further reduction rule (assoc). Furthermore, the CPS translation factors through both the monad translation and the linear translation; so there is also a kernel [Lambda.sub.ml**] of [Lambda.sub.ml*] and a kernel [Lambda.sub.lin**] of [Lambda.sub.lin*] that is also isomorphic to [Lambda.sub.cps].

3. GALOIS CONNECTIONS AND REFLECTIONS

Let us review the standard results about Galois connections and reflections [Davey and Priestley 1990; Mac Lane 1971; Melton et al. 1985]. The standard results need to be adapted slightly, as reduction is a preorder (it is reflexive and transitive) but not a partial order (it is not antisymmetric).

We write [right arrow] for a single-step of reduction; ?? for the reflexive and transitive closure of reduction; = for the reflexive, transitive, and symmetric closure of reduction [equivalent] and for syntactic identity up to renaming.

Assume a source calculus S with reduction relation ?? S and a target calculus T with reduction relation ?? T. Reductions are directed in such a way that they correspond to evaluation steps or optimizations. Let the maps * : S [right arrow] T and # : T [right arrow] S correspond to compiling and decompiling, respectively. Finally, let [M.sub.S], [N.sub.S] range over terms of S, and let [M.sub.T], [N.sub.T] range over terms of T.

Definition 3.1. Maps * and # form a Galois connection from S to T whenever

[M.sub.S] ?? S [N.sub.T.sup.#] if and only if [M.sub.S.sup.*] T [N.sub.T].

There is an alternative characterization of a Galois connection.

Proposition 3.2. Maps * and # form a Galois connection from S to T if and only if the following four conditions hold.

(1) [M.sub.S] ?? S [M.sub.S.sup.*#],

(2) [N.sub.T.sup.#*] T [N.sup.T],

(3) [M.sub.S ?? S [N.sub.S] implies [M.sub.s.sup.* ?? T [N.sub.S.sup.*],

(4) [M.sub.T] ?? T [N.sub.T] implies [N.sub.T.sup.#] ?? S [N.sub.T.sup.#].

If the same four conditions hold with ?? S and ?? T replaced by = S and = T, then one has an equational correspondence, as defined by Sabry and Felleisen [1993]. Hence, every Galois connection implies an equational correspondence, though not conversely.

If the compiling map * is left inverse to the decompiling map #, then one has a reflection.

Definition 3.3. Maps * and # form a reflection in S of T if they form a Galois connection and [N.sub.T] [equivalent] [N.sub.T#*].

For a reflection, # is necessarily injective. Galois connections and reflections compose.

Proposition 3.4. Let *1 and #1 form a Galois connection and (reflection) from S to T, and [*.sub.2] and [#.sub.2] form a Galois connection (reflection) from T to U. Then [*.sub.1] [*.sub.2] and [#.sub.2][#.sub.1] form a Galois connection (reflection) from S to U.

Every reflection factors into an inclusion and an order isomorphism. Write [S.sup.*#] for the subset of S containing just those terms of the form [M.sup.*#], and write Id : [S.sup.*#] S for the trivial inclusion function. A reflection * and # in S of T is an inclusion if # is the identity (and hence S [contains or equal to] T) and is an order isomorphism if * and # are inverses (and hence S [congruent] T).

Proposition 3.5. Let * and # form a reflection in S of T.

(1) Translations *# and Id form an inclusion in S of [S.sup.*#]. (2) Translations * and # form an order isomorphism between [S.sup.*#] and T.

The composition of the inclusion and the isomorphism is the original reflection.

The proposition is illustrated in Figure 2, which shows calculi S and T and the images [S.sup.*], [T.sup.#], [S.sup.*#], and [T.sup.#*] of these calculi under maps * and #. The kernel [S.sup.*#] of S is isomorphic to T.

[FIGURE 2 ILLUSTRATION OMITTED]

The summary illustrated in Figure 1 demonstrates repeated use of this proposition. Each reflection is factored into an inclusion (shown vertically) and an order isomorphism (shown horizontally).

For a Galois connection, one normally has two additional results, that [M.sup.*] [equivalent] [M.sup.*#*] and [P.sup.#] [equivalent] [P.sup.#*#]. These proofs depend on antisymmetry and hence do not apply here. (As a counterexample to antisymmetry, we have YI [right arrow] I (YI) [right arrow] YI, but YI ?? I(YI); I is the identity, and Y is the fixpoint combinator. Note that antisymmetry can only fail for terms with no normal form.) In any event, both equivalences do follow from the stronger property of being a reflection.

4. MONADS: THE PROBLEM

Let us review the traditional translation from the call-by-value calculus into the monad calculus, and see why it fails to be a reflection.

Plotkin's call-by-value calculus [Lambda.sub.Nu] is summarized in Figure 3. We let x, y, z range over variables, L, M, N range over terms, and V, W range over values. A term is either a value or an application, and a value is either a variable or an abstraction. The call-by-value nature of the calculus is expressed by limiting the argument to a value in ([Beta].[Nu]) and by limiting the function to a value in ([Eta].[Nu]).

[FIGURE 3 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

An important aspect of each calculus with which we deal is that it is confluent. Confluence ensures that optimizations (reductions) can be combined in any order.

Proposition 4.1. The reductions of [Lambda.sub.[Nu] are confluent.

Moggi's monadic metalanguage [Lambda.sub.ml] is summarized in Figure 4. This calculus distinguishes values from computations. Functions may accept and return either values or computations and are defined by the call-by-name rules ([Beta]) and ([Eta]). Two terms relate values to computations: the term [M] denotes the computation that does nothing save return the value M; and the term let x ?? L in N denotes the computation that composes computation L and N by first performing L, binding its result to x, and then performing N. The interaction of these terms is described by the three rules ([[Beta]].let), ([Eta].let), and (assoc). The rule (assoc) is only valid if the obvious scoping restrictions are satisfied (y is not bound in L, and x is not bound in N). We omit such restrictions in the remainder of the article.

[FIGURE 4 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Proposition 4.2. The reductions of [Lambda.sub.ml] are confluent.

A translation * from [Lambda.sub.Nu] to [Lambda.sub.ml] is described in Figure 5. In the case of applications, the translation introduces two variables x and y that occur free in neither L nor M. Translation * on terms uses an auxiliary translation [dagger] on values. The two translations are related by a substitution lemma, N*[x := [V.sup.[dagger]] [equivalent] (N[x:= V])*, which is easily checked by induction over the structure of terms.

[FIGURE 5 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The translation * is sound in that M ?? N implies M* ?? N*. This is easily checked by looking at the translation of ([Beta].v),

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

and similarly for ([Eta].[Nu]).

However, the translation is not complete even in the weak sense required by equational correspondence: M* =ml N* does not imply M =v N. For example, it is easy to check that

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

while if L is not a value then the equivalence does not hold in the call-by-value calculus.

Proposition 4.3. The translation *: [Lambda.sub.Nu] [right arrow] [Lambda.sub.ml is sound, but does not generate an equational correspondence.

5. MONADS: THE SOLUTION

To refine the translation *: [Lambda.sub.Nu] [right arrow] [Lambda.sub.ml] into a reflection requires three steps: first, grow [Lambda.sub.Nu] into [Lambda.sub.c]; second, shrink [Lambda.sub.ml] into [Lambda.sub.ml*] third, fine-tune the translation *.

Step one grows [Lambda.sub.Nu] into [Lambda.sub.c], which is summarized in Figure 6. The new calculus corresponds to Moggi's untyped computational [Lambda]-calculus as it appeared in his original Edinburgh LFCS Technical Report [Moggi 1988, Def 6.2]. It was carefully designed to model directly the effect of translation into [Lambda.sub.ml]. This is achieved by adding to A, a term let x ?? M in N which mimics the term let x ?? M in N of [Lambda.sub.ml]; by adding to [Lambda.sub.c] reductions corresponding to each reduction of [Lambda.sub.ml]; and by adding to [Lambda.sub.c] two more reductions, (let.1) and (let.2), which mimic the effect of the translation from [Lambda.sub.Nu] into [Lambda.sub.ml].

[FIGURES 6 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Let P, Q range over nonvalues. Rules (let. 1) and (let.2) are restricted to act on nonvalues, since values yield a reduction in the opposite direction via ([Beta].let).

You may wonder: is the new form (let x = M in N) necessary, or could it be represented by ([Lambda]x. N)M instead? The latter is possible, but then the rules ([Beta].let), ([Eta].let), (assoc), (let.1), and (let.2) all become more difficult to read. Further, we prefer for historical reasons to stick to Moggi's formulation.

You may also wonder: do the rules (let.1) and (let.2) point in the right direction? They do: the direction explicitly captures the evaluation order of the subexpressions of an application. To evaluate an application, we evaluate the function position to a value (let.1), and then evaluate the argument to a value (let.2). Furthermore, reversing the rules would yield a nonconfluent system. For example, reversing (let.1), we have P = (let y = (let x = L in M) in yN) reduces to ((let x = L in M)N). We also have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

which shows that confluence fails. The system as given is confluent, as was shown by Moggi [1988].

Proposition 5.1. The reductions of [Lambda.sub.c] are confluent.

Step two shrinks [Lambda.sub.ml] into [Lambda.sub.ml*], which is summarized in Figure 7. The grammar of [Lambda.sub.ml] is the smallest one that contains all terms in the image of the translation * : [Lambda.sub.Nu] [right arrow] [Lambda.sub.ml] of the previous section and which is closed under the reductions of [Lambda.sub.ml]. The new grammar differs from the old in two key ways: applications MN in [Lambda.sub.ml] are restricted to the form VW in [Lambda.sub.ml*], and computations [M] in [Lambda.sub.ml] are restricted to the form [VI in [Lambda.sub.ml*].

[FIGURE 7 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The reduction rules are restricted accordingly. Since all applications have the form VW, rules ([Beta]) and ([Eta]) and rules ([Beta].v) and ([Eta].v) have the same effect on the calculus. This provides an analogue of Plotkin's indifference property, which states that call-by-value and call-by-name evaluation yield the same result for terms in CPS.

Proposition 5.2. The grammar of [Lambda.sub.ml*] is closed under the reductions of [Lambda.sub.ml]. That is, if M [right arrow] N in [Lambda.sub.ml] and M is in [Lambda.sub.ml*], then N is also in [Lambda.sub.ml*], and M [right arrow] N in [Lambda.sub.ml*].

The proof is an easy case analysis. It follows as a corollary from Proposition 4.2 that the reductions of [Lambda.sub.ml*] are confluent.

Step three adapts the translation * : [Lambda.sub.Nu] [right arrow] [Lambda.sub.ml] to the new calculi. The straight-forward choice is to leave the translation as is, adding a line for let.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Here [dagger] is as in Figure 5. The meaning of the overbars will be explained shortly.

Alas, this translation is not even sound in our stronger sense: it preserves the equalities of [Lambda.sub.c] but not reductions. The key problem is with rule (let.2), which requires ([Beta].let) reductions in both directions.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The solution is to consider the ([Beta].let) reductions as part of the translation. The two overlined occurrences of let introduced in the translation of applications are regarded as administrative occurrences. A second stage is added to the translation, where all administrative ([Beta].let) redexes (that is, ones where the relevant let is overlined) are reduced.

This somewhat awkward description as a two-stage translation with administrative redexes may be replaced by the equivalent translation given in the first half of Figure 8. This was derived by a simple case analysis on applications, with according simplification. The obvious homomorphism, shown in the second half of the figure, serves as the inverse translation. It is now straightforward to verify that these constitute a reflection.

[FIGURE 8 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Proposition 5.3. Translations * and # (see Figure 8) form a reflection in [Lambda]c of [Lambda.sub.ml*].

Proof. To prove that the translations form a reflection, we must establish the following (see Proposition 3.2 and Definition 3.3):

(1) For M [element of] [Lambda.sub.c], M [right arrow] M*#, (2) For M [element of] [Lambda.sub.ml*], M#* [equivalent] M, (3) For M, N [element of] [Lambda.sub.c], M [right arrow] N implies M* [right arrow] N*, (4) For M, N [element of] [Lambda.sub.ml*], M [right arrow] N implies M# [right arrow] N#.

Parts (1) and (2) are verified by induction over the structure of terms, and parts (3) and (4) are verified by induction over the length of reduction sequences. We show the proof of case (3) in detail. The main part of the proof is to show that every reduction between terms in [Lambda.sub.c] corresponds to a sequence of reductions between the translated terms. We proceed by cases:

Case [Beta].v. We have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where the last step follows by Substitution Lemma 5.4.

Case [Eta].v. We have

([Lambda]x.Vx)* [equivalent] [[Lambda]x.V[dagger]x] [right arrow] [V[dagger]]

[equivalent] V*.

Case [Beta].let. We have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where the last step follows by Substitution Lemma 5.4.

Case [Eta].let. We have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Case assoc. We have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Case let.1. We have

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Case let.2. We have (VQ)* [equivalent] let y ?? Q* in (Vy)* [equivalent] (let y = Q in Vy)*.

The proofs of cases (3) and (4) above rely on the following substitution lemma.

Lemma 5.4. Let M, V be terms of the appropriate sort in [Lambda.sub.c] and N, W be terms of the appropriate sort in [Lambda.sub.ml*]; then we have

M*[x := V[dagger]] [equivalent] (M[x := V])*

N#[x := W[dagger]] [equivalent] (N[x := W])*.

6. MONADS: THE FACTORIZATION

Proposition 3.5 guarantees that there must be an isomorphic image of [Lambda.sub.ml*] within [Lambda.sub.c]. It consists of exactly those terms of the form M*#. We name this calculus [Lambda.sub.c*], and it is summarized in Figure 9. The grammar is identical to [Lambda.sub.c], except general applications MN are replaced by value applications VW, much as in the move from [Lambda.sub.ml] to [Lambda.sub.ml*].

[FIGURE 9 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The terms of [Lambda.sub.c*] can be characterized as the terms of [Lambda.sub.c] in (let.1) and (let.2) normal form. Once a term has been normalized with respect to these two rules, they are never required again -- that is, none of the other rules will introduce a (let.1) or (let.2) redex.

As guaranteed by Proposition 3.5, the reflection * : [Lambda.sub.c] [right arrow] [Lambda.sub.ml*] factors into an inclusion *1 : [Lambda.sub.c] [right arrow] [Lambda.sub.c*] and an order isomorphism *2 : [Lambda.sub.c*] [right arrow] [Lambda.sub.ml*], given in Figures 10 and 11. The proposition even shows how to compute these: *1 is *#; #1 is the identity; *2 is a restriction of *; and #2 is #. What is a pleasant bonus, not guaranteed by the proposition, is that *1 has a simple interpretation: it reduces a term of [Lambda.sub.c] to (let.1) and (let.2) normal form, hence yielding a term of [Lambda.sub.c*].

[FIGURES 10 & 11 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

7. LINEAR CALCULUS

Figure 12 summarizes a linear lambda calculus similar to the ones studied by Wadler [1993a; 1993b] and Maraist et al. [1995]. The calculus contains two sorts of variables: a, b, c range over linear variables which are used exactly once in a term, while x, y, z range over classical variables which may appear any number of times. These conventions are the ones used by Benton [1995] and Benton and Wadler [1996]. Introduction and elimination of linear implication - [Omicron] corresponds, respectively, to abstraction over linear variables [Lambda]a. N and application LM. Introduction and elimination of the modality ! corresponds to the term forms !M and let !x = L in N.

[FIGURE 12 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

There are two important side conditions on the grammar: each linear variable is used exactly once, and no linear variable appears free in a term of the form M. Informally, evaluation of the term let !x = L in N proceeds by first evaluating L to a term of the form !M and then substituting M for x in N. Thus we may view the term !M as suspending evaluation and the term let !x = L in N as forcing the corresponding evaluation. The requirement that no linear variable appears free in !M ensures that the substitution of M for x does not violate the requirement that each linear variable is used exactly once.

All the rules of the calculus correspond to simplification of proofs in linear logic. The rules ([Beta]-[Omicron]) and ([Beta].!) simplify a logical introduction followed by the corresponding logical elimination. The rules ([Eta].-[Omicron]) and ([Eta].!) simplify a logical elimination followed by the corresponding logical introduction. Note that there is no need for a side condition in ([Eta].-[Omicron]), since linear variables can only occur once in a term. The rules (!-[Omicron]), (-[Omicron]!), and (!!) correspond to commuting conversions. All of the rules, except for (-[Omicron]!), were discussed by Maraist et al. [1995]. We explain the significance of the additional (-[Omicron]!) rule in Section 7.2 after studying the translation from [Lambda.sub.v] to [Lambda.sub.lin].

7.1 Reflection of Linear Calculus in Call-by-Value

Our starting point is the translation from [Lambda.sub.v] to [Lambda.sub.lin] of Maraist et al. [1995], which is described in Figure 13. This translation maps ([Beta].v) reductions to reductions in the linear calculus:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

However, this naive linear translation fails to be a reflection for much the same reasons that the naive monad translation failed, as described in Section 4. As in [Lambda.sub.ml] we can prove in [Lambda.sub.lin] that

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

which is not provable in the call-by-value calculus if L is not a value. Analogous to Section 5, the solution to this problem is to extend the source calculus from [Lambda.sub.v] to [Lambda.sub.c], to restrict the target calculus from [Lambda.sub.lin] to [Lambda.sub.lin*], and to fine-tune the corresponding translation. Instead of constructing these calculi and translations from scratch, we exploit the existing isomorphism between [Lambda.sub.c*] and [Lambda.sub.ml*] to guide the design of [Lambda.sub.lin*]. The idea is to adapt the optimized translation from [Lambda.sub.c*] to [Lambda.sub.ml*] to a translation from [Lambda.sub.c*] to the linear calculus. The target of this translation would be the kernel linear calculus [Lambda.sub.lin*].

[FIGURE 15 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The isomorphism is spelled out by the maps *2 and #2 between [Lambda.c*] and [Lambda.sub.lin*], shown in Figure 15. Note the similarity between these two maps and the corresponding maps between [Lambda.sub.c*] and [Lambda.sub.ml*] in Figure 11. The terms and reduction rules of the restricted linear calculus in Figure 14 are derived from the terms and reduction rules of [Lambda.sub.c*] using the map *2 of Figure 15.

Proposition 7.1.1. The terms and reductions of the calculi [Lambda.sub.c*] and [Lambda.sub.lin*] are isomorphic. In other words, for all M, N [Epsilon] [Lambda.sub.c*] and P, Q [Epsilon] [Lambda.sub.lin*], we have

-- [M.sup.*#] [equivalent] M and [P.sup.#*] [equivalent] P,

-- If M [right arrow] N then [M.sup.*] [right arrow] [N.sup.*], and

-- If P [right arrow] Q then [P.sup.#] [right arrow] [Q.sup.#].

The existence of the isomorphism immediately implies several properties of [Lambda.sub.lin*].

Proposition 7.1.2. The calculus [Lambda.sub.lin*] is confluent and closed under reduction.

For this approach to make sense, it remains to verify that the calculus [Lambda.sub.lin*] is really a restriction of [Lambda.sub.lin] in the sense that all reductions rules in [Lambda.sub.lin*] must be provable in [Lambda.sub.lin]. For most of the rules, this is straightforward to verify. The only nonobvious rule is the [Lambda.sub.lin*] version of ([Eta]. -o), which can be proved in [Lambda.sub.lin] as follows:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Note that the proof uses equalities rather than reductions, indicating the bad fit between [Lambda.sub.lin] and [Lambda.sub.lin*].

Putting together the inclusion in [Lambda.sub.c] of [Lambda.sub.c*] of Figure 10 and the isomorphism between [Lambda.sub.c*] and [Lambda.sub.lin*] of Figure 15, we can immediately construct a reflection in [Lambda.sub.c] of [Lambda.sub.lin*].

Proposition 7.1.3. Translations * and # (see Figure 16) form a reflection in [Lambda.sub.c] of [Lambda.sub.lin*].

[FIGURE 16 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

7.2 Eta-Rules for Linear Logic

Maraist et al. [1995] were concerned with a similar problem: finding translations between call-by-value calculi and linear calculi that are both sound and complete. They adopt a similar solution: expanding the source calculus from VAL to LET. One significant difference is that their source calculus does not contain an ([Eta].v) rule, and their target calculus does not contain ([Eta]. -o), ([Eta].!], and (-o!).

Furthermore, when Maraist et al. [1995] attempted to add the ([Eta].v) rule to the call-by-value calculus, and the ([Eta].-o) and ([Eta].!) rules to the linear lambda calculus, they noted that the translation from the call-by-value calculus to the linear calculus does not preserve ([Eta].v). They suggested that perhaps more reductions rules should be added to the linear calculus if such reductions could be justified logically. We have indeed followed their suggestion to solve the problem by adding the rule (-o!), which is the symmetric commuting conversion from (!-o). (The symmetry is not complete, since we are evaluating the subexpressions of an application from left-to-right.) With the addition of the (-o!) rule, the translation from the call-by-value calculus to the linear calculus preserves the ([Eta].v) rule as we have shown.

8. CONTINUATIONS

The development for continuations is paralleled by the development for monads and the linear calculus. Just as [Lambda.sub.v] maps into [Lambda.sub.ml] via the traditional call-by-value monad translation, so does [Lambda.sub.v] map into [Lambda.sub.n] via the traditional call-by-value CPS translation:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

A remarkable property of this translation is that one may always choose k to be exactly the same name, without fear of name clash. Again, this translation is sound but not complete.

To refine the translation * : [Lambda.sub.v] [right arrow] [Lambda.sub.n] into a reflection also requires three steps: first, grow the source [Lambda.sub.v] into [Lambda.sub.c]; second, shrink the target [Lambda.sub.n] into [Lambda.sub.cps]; third, finetune the translation *. Step one was already accomplished as part of the monad development. Like for the linear calculus, steps two and three are best considered in reverse order, as the calculus of step two should be the image of the modified translation of step three.

To refine the translation * : [Lambda.sub.v] [right arrow] [Lambda.sub.n], it is suitably extended for let and has some reductions labeled as administrative.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The translation now takes place in three stages. Stage one applies the translation proper. Stage two reduces any administrative ([Beta]) redexes -- that is, ones where the relevant [Lambda] is overlined. Stage three strips the leading [Lambda] k, which always appears and so is redundant.

This three-stage translation may be replaced by the equivalent translation given in the first half of Figure 18. The old translation relates to the new as follows: [M.sup.*old] [equivalent] [Lambda]k. [M.sup.*new], where k is the distinguished continuation variable. The auxiliary translation M: K closely resembles a translation introduced by Plotkin [1975] to capture the effect of administrative reductions.

[FIGURE 18 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Step two shrinks the target [Lambda.sub.n] into [Lambda.sub.cps], which is summarized in Figure 17. The grammar is the smallest one that is in the image of the refined translation *. An additional class of nonterminals, K, is added to the grammar, ranging over continuations. This class contains the distinguished free variable k and contains those lambda expressions which may be substituted for k.

[FIGURE 17 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Examination reveals that each of the rules ([Beta]) and ([Eta]) arises in exactly two situations, yielding four rules in the target [Lambda.sub.cps] corresponding to four of the seven rules in the source [Lambda.sub.c]. It is easily verified that the grammar is indeed closed under reduction. Every application has a value as an argument, so call-by-value and call-by-name reductions have the same effect on the language, which explains Plotkin's indifference property.

Proposition 8. 1. The grammar of [Lambda.sub.cps] is closed under the reductions of [Lambda.sub.cps].

The inverse translation # of Figure 18 is now easily derived. It has three parts, one for each component of the target grammar. A term M in [Lambda.sub.cps] maps to a term M# in [Lambda.sub.c]; a value V in [Lambda.sub.cps] maps to a value [V.sup.??] in [Lambda.sub.c]; and a continuation K in [Lambda.sub.cps] maps to an evaluation context [K.sup.??] in [Lambda.sub.c]. An evaluation context C is a term with a hole [], and if C is an evaluation context then C[M] denotes the result of replacing the hole in C by the term M. The filling operation is straightforward, since the holes of our evaluation contexts are never in the scope of a bound variable.

We can now verify that the maps of Figure 18 constitute a reflection.

Proposition 8.2. Translations * and # form a reflection in [Lambda.sub.c] of [Lambda.sub.cps].

Proof. We prove each of the four parts of Proposition 3.2 separately. The proof of part (1)

M [right arrow] M*#

requires a stronger inductive hypothesis,

[K.sup.??][M] [right arrow] (M : K)#,

but is otherwise straightforward. As usual the proofs rely on the relevant substitution lemmas. []

Lemma 8.3. Let M, V be terms of the appropriate sorts in [Lambda.sub.c], and let K be in [Lambda.sub.cps]; then (M : K)[x := V[dagger]] [equivalent] (M[x := V]) : K.

Lemma 8.4. Let M, V, K be terms of the appropriate sort in [Lambda.sub.cps]; then

[K.sup.??][M#[x := [V.sup.??]] [right arrow] (M[x := V][k := K])#.

This completes the parallel development of the reflection; there is also a parallel development of the factorization. Proposition 3.5 guarantees that there must be an isomorphic image of [Lambda.sub.cps] within [Lambda.sub.c]. We name this calculus [Lambda.sub.c**], and it is summarized in Figure 19. Just as the grammar of [Lambda.sub.cps] has three components: terms, values, and continuations -- so the grammar of [Lambda.sub.c**] has three components: terms, values, and contexts. Observe that, despite the introduction of contexts, each term still possesses a unique decomposition in terms of the syntax. (For instance, the term xy corresponds to K[VW], where K is []; V is x; and W is y.)

The terms of [Lambda.sub.c**] can be characterized as the terms of [Lambda.sub.c] in (let.1), (let.2), and (assoc) normal form. As in the previous development, once a term has been normalized, no further reductions ever introduce a (let.1) or (let.2) redex. Alas, the same cannot be said of (assoc). The reduction ([Beta].[Upsilon]) may indeed introduce a further (assoc) redex, as shown by the counterexample

let x = (([Lambda]y.let z = ab in c) d) in e

[right arrow] let x = (let z = ab in c) in e.

To gain insight into the problem, consider the corresponding CPS reduction:

(([Lambda]y.[Lambda]. (a b ([Lambda]z. kc))) d ([Lambda]x. ke))

[right arrow] (a b ([Lambda]z. ([Lambda]x. ke)c))

The image of this in [Lambda.sub.c**] is

let x = (([Lambda]y. let z = ab in c) d) in e

[right arrow] let z = ab in let x = c in e

where the right-hand side is in (assoc)-normal form. The CPS language achieves this normalization using the metaoperation of substitution which traverses the CPS term to locate k and replace it by the continuation thus effectively "pushing" the continuation deep inside the term.

In order to properly match the behavior of CPS, we therefore add a corresponding metaoperation to [Lambda.sub.c**], M : K shown in Figure 19. Using the new metaoperation we can extend the problematic source reduction ([Beta].[Upsilon]) with a built-in (assoc)-normalization action that mirrors the action of ([Beta]) on CPS terms. (An alternative to adding metanotation for substitution may be to move to calculi that use explicit substitution, but we have not explored this possibility.)

[FIGURE 19 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

There is one pitfall to avoid: since reductions apply to any subterm, one may be tempted to apply rule ([Beta].[Upsilon]) to the subterm (([Lambda]y. let z = ab in c) d) in the counterexample by taking K to be [] rather than let x = [] in e. To step around this pitfall, we use a nonstandard convention that pattern-matching a term against the left-hand side of ([Beta].[Upsilon]) should select the maximal K.

Again, as guaranteed by Proposition 3.5, the reflection * : [Lambda.sub.c] [right arrow] [Lambda.sub.cps] factors into an inclusion *1 : [Lambda.sub.c] [right arrow] [Lambda.sub.c**] and an order isomorphism *2 [Lambda.sub.c**] [right arrow] [Lambda.sub.cps], given in Figures 20 and 21. Again, these can be computed directly from the proposition, and again there is a bonus: *1 has a simple interpretation as reducing a term of [Lambda.sub.c] to its (let.1), (let.2), and (assoc) normal form.

[FIGURE 20 & 21 MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

In addition, the CPS translation factors through the monad translation. One may translate [Lambda.sub.ml] into [Lambda.sub.cps] as follows:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Regarding this as a two-stage translation with administrative reductions yields a reflection. As before, the reflection factors through a calculus [Lambda.sub.ml**], corresponding to the subset of [Lambda.sub.ml*] consisting of terms in (assoc) normal form. The three calculi [Lambda.sub.c**], [Lambda.sub.ml] and [Lambda.sub.cps] are isomorphic.

In a similar way, the isomorphism between [Lambda.sub.c**] and [Lambda.sub.lin] of Figure 15 can be adapted to an isomorphism between [Lambda.sub.c**] and a kernel of the linear calculus [Lambda.sub.lin**] in (!!) normal form. Figure 1 diagrams the situation.

9. THE FISCHER TRANSLATION

The CPS translation of Fischer [1972] differs from the CPS translation of Plotkin [1975] in that it swaps the order of function argument and continuation, allowing additional administrative reductions to be performed. Here is the Fischer translation, for comparison with the Plotkin translation in Section 8.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

For example, the term ([Lambda]x. x)y yields ([Lambda]x.[Lambda]k.kx)yk under the Plotkin translation, and it yields ([Lambda]x.kx)y under the Fischer translation, where in each case one reduces all administrative ([Beta]) redexes and strips the leading [Lambda]k.

An earlier version of this article claimed that the Fischer CPS translation could be made a reflection, but gave no proof. Here we withdraw that claim. We show that the Fischer translation cannot be a reflection, nor can it be a Galois connection with the source calculus [Lambda.sub.c]. However, it may be a Galois connection with a different source calculus.

The Fischer translation cannot be a reflection. Thanks to administrative reduction, no term in the image of the Fischer translation will contain a [Lambda]k redex; but in order to be closed under reduction, the target language must contain such redexes. For example, take M [equivalent] ([Lambda]f. fx)([Lambda]y.y), so that M* [equivalent] ([Lambda]f. fkx)([Lambda]k.[Lambda]y.ky). Then M* [right arrow] P, where P [equivalent] ([Lambda]k.[Lambda]y.ky)kx. But there is no source term with Fischer translation P, so we cannot have P#* [equivalent] P. Note that this argument is independent of the reductions in the source language.

Further, the Fischer translation cannot be a Galois connection when the source calculus is [Lambda.sub.c]. For example, take M [equivalent] f(([Lambda]x.x)y) and N [equivalent] ([Lambda]x. fx)y. Both terms have the same Fischer translation, namely M* [equivalent] N* [equivalent] P [equivalent] ([Lambda]x. fkx)y. Since we have a Galois connection, we require that M ?? M*# [equivalent] P* and N ?? N*# [equivalent] #P in [Lambda.sub.c], and so fy is the only possible choice for P#. For a Galois connection we also require that P#* ?? P but this fails, since P#* [equivalent] fky ?? ([Lambda]x. fkx)y [equivalent] P.

We saw in Section 4 that a naive translation with no administrative reductions fails to be a reflection. Here we see that the Fischer translation has too many administrative reductions to be a reflection. Just as Goldilock's porridge must be neither too hot nor too cold, administrative reductions must be neither too many nor too few.

Nonetheless, it may be possible to find a Galois connection based on the Fischer translation with a different choice of source calculus. We leave this as an open question.

10. RELATED WORK

Plotkin [1975], among other contributions, formalizes the call-by-value CPS translation and shows that it preserves but does not reflect equalities: if M = N in [Lambda.sub.v] then M* = N* in [Lambda.sub.n], but not conversely. Here and throughout, we write * for the variant of the CPS translation under consideration, and hope this will lead to no confusion.

Sabry and Felleisen [1993] strengthen Plotkin's result by making the implication above reversible. They extend the call-by-value lambda calculus [Lambda.sub.v] with a set of reductions X such that M = N in [Lambda.sub.v]X if and only if M* = N* in [Lambda.sub.v]. As they note, [Lambda.sub.v]X and [Lambda.sub.c] prove the same equalities; but they do not prove the same reductions.

Sabry and Felleisen [1993] introduce the notion of equational correspondence described in Section 3, and they prove that their translation constitutes such a correspondence. In fact, they prove something stronger, making their translation almost, but not quite, a Galois connection: their translation satisfies all four conditions of Proposition 3.2, except that condition (2), P#* ?? P, is replaced by the weaker P#* = P. (Compare this to the stronger P#* [equivalent] P required of a reflection.)

They also single out a subset A of X and observe that these A-reductions correspond directly to the administrative reductions on CPS terms. Their terms in A-normal form roughly correspond to our kernel calculus [Lambda.sub.c**], of terms in (let.1), (let.2), and (assoc) normal form.

However, Sabry and Felleisen use Fischer's CPS translation, which we have seen cannot be a reflection. It remains an open question whether there is a variant of Sabry and Felleisen's work which yields a Galois connection.

Flanagan et al. [1993] apply the results of Sabry and Felleisen [1993]. They suggest that CPS translation may not be so beneficial after all: it may be better to work directly in the source calculus. They show that terms in A-normal form behave similarly to CPS terms, demonstrating this via a sequence of abstract machines. They also briefly sketch possible applications of the full set of reductions X. But they fail to observe our central point: that for optimization purposes one wants a result showing correspondence of reductions rather than correspondence of equations.

Lawall and Danvy [1993] give a factoring of CPS similar to the one described here and refer to Galois connections. They relate four languages: a source language, a kernel source language, a kernel target language, and a target language. The first two relate via a Galois connection; the middle two are isomorphic; and the last two again relate via a Galois connection. The first two parts of their factorization are similar to our inclusion in [Lambda.sub.c] of [Lambda.sub.c**], and our order isomorphism from [Lambda.sub.c**] to [Lambda.sub.cps]. Their third step schedules evaluation, determining for each application whether the function or argument evaluates first. Here we use a language where the function always evaluates before the argument, so we need no counterpart of their third step.

The Galois connections of Lawall and Danvy are based on an artificial ordering induced directly from the translations. One might argue that they are misusing the notion of Galois connection and are instead dealing with the somewhat weaker notion of a pair of translations * and # satisfying [M.sup.*#* equivalent.sub.T M.sup.*] and [P.sup.#*# equivalent.sub.s P.sup.#]. As they note, their artificial ordering is unsatisfactory, because their middle isomorphism between the source kernel and target kernel does not respect this ordering: it is not an order isomorphism, and hence not a Galois connection. Thus, their factorization cannot be viewed as a composition of Galois connections. In contrast, we use a natural ordering relation, and our Galois connections do compose. Whereas their isomorphism violates the ordering of their Galois connection, our isomorphism arises as a consequence of our Galois connection, as shown by Proposition 3.5.

Hatcliff and Danvy [1994] consider translations analogous to our translations from [Lambda.sub.v] to [Lambda.sub.ml], and from [Lambda.sub.ml] to [Lambda.sub.cps]. They also look at translations from other source languages into [Lambda.sub.ml], an issue we ignore. They show the translation from [Lambda.sub.v] to [Lambda.sub.ml] is sound; we give the stronger result that the translation from [Lambda.sub.c] to [Lambda.sub.ml] is a reflection. They also show that the translation from [Lambda.sub.ml] to [Lambda.sub.cps] is an equational correspondence; again we give the stronger result that it is a reflection.

Maraist et al. [1995] consider translations into a linear lambda calculus. That paper extends the call-by-value calculus VAL to the calculus LET; this article extends the call-by-value calculus [Lambda.sub.v] to the calculus [Lambda.sub.c]. The earlier paper stressed the analogy of the linear translation with the CPS translation; as can be seen from the work here, an analogy of the linear translation with the monad translation is even more apposite.

11. CONCLUSION

This section describes a number of possible extensions of our results and draws a conclusion about [Lambda.sub.c] as a model of call-by-value.

Standard Reduction. Most lambda calculi possess a notion of standard reduction, characterized by two properties. First, at most one standard reduction applies to a term. Second, if any sequence of reductions reduces a term to an answer, then the sequence of standard reductions will also do so. Hence standard reductions capture the behavior of an evaluator. Plotkin [1975] specified standard reductions for [Lambda.sub.v], and his results for CPS demonstrate not only that reductions are preserved, but also that standard reductions are preserved. (He expresses this in a different but equivalent form by saying that evaluation is preserved.) Hatcliff and Danvy [1994] give similar results for translation from Moggi's [Lambda.sub.ml] into CPS. It appears straightforward (1) to extend the work here by specifying a suitable notion of standard reduction for each of the calculi involved and (2) to show that the given translations are still reflections if one replaces reductions by standard reductions.

Call-by-Value and Call-by-Need. Maraist et al. [1995] study a call-by-let calculus that is closely related to [Lambda.sub.c] and that translates into linear logic. By extending the call-by-let calculus with just one law,

let x = M in N [arrow right] N, if x [not element of] fv (N),

the authors derive a call-by-need calculus [Ariola et al. 1995] that translates into affine logic. We conjecture that when augmented with the above law, [Lambda.sub.c] also yields a model of call-by-need.

A Reflection on Call-by-Value. Plotkin's original paper on [Lambda.sub.v] laid out two key properties of this calculus: first, it is adequate to describe evaluation, and second, it is inadequate to prove some equalities that we might reasonably expect to hold between terms. The first was demonstrated by a correspondence between [Lambda.sub.v] and the SECD machine of Landin [1964]. The second was demonstrated by observing that there are terms that are not provably equal in [Lambda.sub.v], but whose translations into CPS are provably equal.

Moggi defined [Lambda.sub.c] as an extension of [Lambda.sub.v] that is sound and complete for all monad models and hence proves a reasonably large set of equalities. He picked a confluent calculus to ease symbolic manipulation, but made no claims that [Lambda.sub.c] was itself a reasonable model of computation. Sabry and Felleisen showed that [Lambda.sup.c] proves two terms equal exactly when their CPS translations are equal. This reinforces the claim that [Lambda.sub.c] yields a good theory of equality, but because they dealt only with equational correspondence, again says nothing about [Lambda.sub.c] as a model of computation. Our results here relate [Lambda.sub.c] reductions to reductions in [Lambda.sub.ml] and [Lambda.sub.cps], both widely accepted as models of computation. We hereby put forward [Lambda.sub.c] as a model of call-by-value computation that improves on [Lambda.sub.v].

REFERENCES

Appel, A. W. 1992. Compiling with Continuations. Cambridge University Press, Cambridge, Mass.

Ariola. Z. M., Felleisen, M., Maraist, J., Odersky, M., and Wadler, P. 1995. A call-by-need lambda calculus. In the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, 233-246.

Barber, A. 1995. Dual intuitionistic linear logic. Draft, Dept. of Computer Science, Univ. of Edinburgh, Edinburgh, U.K.

Benton, N. and Wadler, P. 1996. Linear logic, monads, and the lambda calculus. In the Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif.

Benton, P. N. 1995. A mixed linear and non-linear logic: Proofs, terms, and models. In Proceedings of Computer Science Logic (Kazimierz, Poland, 1994). Lecture Notes in Computer Science, vol. 933. Springer-Verlag, Berlin. Full version available as Tech. Rep. 352, Computer Laboratory, Univ. of Cambridge, October 1994.

Davey, B. A. and Priestley, H. A. 1990. Introduction to Lattices and Order. Cambridge University Press, Cambridge, Mass.

Fischer, M. 1972. Lambda calculus schemata. In Conference on Proving Assertions about Programs. SIGPLAN Not. 7, 1, 104-109. Revised version in Lisp and Symbolic Computation 6, 3/4 (1993), 259-287.

Flanagan,, C., Sabry, A., Duba, B., and Felleisen, M. 1993. The essence of compiling with continuations. In the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, New York, 237-247.

Girard, J.-Y. 1987. Linear logic. Theoret. Comput. Sci. 50, 1-102.

Hatcliff, J. and Danvy, O. 1994. A generic account of continuation-passing styles. In the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language. ACM Press, New York, 458-471.

Kranz, D., Kelsey, R., Rees, J., Hudak, P., Philbin, J., and Adams, N. 1986. Orbit: An optimizing compiler for Scheme. In the ACM SIGPLAN Symposium on Compiler Construction. SIGPLAN Not. 21, 7, 219-233.

Landin, P. 1964. The mechanical evaluation of expressions. Comput. J. 6, 4, 308-320.

Lawall, J. and Danvy, O. 1993, Separating stages in the continuation-passing transform. In the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, 124-136.

Mac Lane, S. 1971. Categories for the Working Mathematician. Springer-Verlag, Berlin.

Maraist, J., Odersky, M., Turner, D. N., and Wadler, P. 1995. Call-by-name, call-by-value, call-by-need and the linear lambda calculus. In the International Conference on the Mathematical Foundations of Programming Semantics.

Melton, A., Schmidt, D. A,, and Strecker, G. 1985. Galois connections and computer science applications. In Category Theory and Computer Programming. Lecture Notes in Computer Science, vol. 240. Springer-Verlag, Berlin, 299-312.

Moggi, E, 1988. Computational lambda-calculus and monads. Tech. Rep. ECS-LFCS-88-86, Univ. of Edinburgh, Edinburgh, U.K.

Moggi, E. 1989. Computational lambda-calculus and monads. In the Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 14-23.

Moggi, E. 1991. Notions of computation and monads. Inf. Comput. 93, 55-92.

Plotkin, G. 1975. Call-by-name, call-by-value, and the [Lambda]-calculus. Theoret. Comput. Sci. 1, 125-159.

Reynolds, J. C. 1993. The discoveries of continuations. Lisp Symbol. Comput. 6, 3/4, 233-247.

Sabry, A. and Felleisen, M. 1993. Reasoning about program in continuation-passing style. Lisp Symbol. Comput. 6, 3/4, 289-360.

Sabry, A. and Wadler, P. 1996. A reflection on call-by-value. In SIGPLAN International Conference on Functional Programming. ACM Press, New York, 13-24.

Steele, G. L. 1978. Rabbit: A compiler for Scheme. MIT AI Memo 474, Massachusetts Institute of Technology, Cambridge, Mass.

Wadler, P. 1993a. A syntax for linear logic. In the International Conference on the Mathematical Foundations of Programming Semantics. Lecture Notes in Computer Science, vol. 802. Springer-Verlag, Berlin.

Wadler, P. 1993b. A taste of linear logic (Invited talk). In Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 711. Springer-Verlag, Berlin.

Printer friendly Cite/link Email Feedback | |

Author: | Sabry, Amr; Wadler, Philip |
---|---|

Publication: | ACM Transactions on Programming Languages & Systems |

Date: | Nov 1, 1997 |

Words: | 10488 |

Previous Article: | Combinatory formulations of concurrent languages. |

Next Article: | Commutativity analysis: a new analysis technique for parallelizing compilers. |

Topics: |