The Duality of Computation

Pierre-Louis Curien (CNRS and University Paris 7)^{∗} Hugo Herbelin (INRIA-Rocquencourt)^{†}

ABSTRACT

We present the \overline{λ}μμ̃-calculus, a syntax for λ-calculus + control operators exhibiting symmetries such as program/context and call-by-name/call-by-value. This calculus is derived from implicational Gentzen’s sequent calculus LK, a key classical logical system in proof theory. Under the Curry-Howard correspondence between proofs and programs, we can see LK, or more precisely a formulation called LK_{μμ̃}, as a syntax-directed system of simple types for \overline{λ}μμ̃-calculus. For \overline{λ}μμ̃-calculus, choosing a call-by-name or call-by-value discipline for reduction amounts to choosing one of the two possible symmetric orientations of a critical pair. Our analysis leads us to revisit the question of what is a natural syntax for call-by-value functional computation. We define a translation of λμ-calculus into \overline{λ}μμ̃-calculus and two dual translations back to λ-calculus, and we recover known CPS translations by composing these translations.

1. INTRODUCTION

Programming languages present implicit symmetries such as input/output, or program/context. Less obviously – as shown recently by Selinger in a categorical setting [22] –, the picture can be extended to evaluation mechanisms: there exists a symmetry between call-by-name and call-by-value.

On the logical side, the best fit for evidencing symmetries is sequent calculus (based on left and right introduction rules). But the correspondence between programs and proofs is traditionally explained through natural deduction (based on right introduction and right elimination rules), implication elimination (also called Modus Ponens) corresponding to procedure application. We believe that this tradition is in good part misleading. In this paper, we present a sequent

∗E-mail: Pierre-Louis.Curien@pps.jussieu.fr †E-mail: Hugo.Herbelin@inria.fr calculus style syntax that exhibits the above symmetries in a precise, (and – we believe – compelling) way.

A key step in this program was already accomplished in [12, 11], where it was shown that simply-typed λ-terms (or λμterms) in (call-by-name) normal form are in bijective correspondence with cut-free sequent calculus proofs in a suitable restriction of Gentzen’s LJ (or LK) [8]. Danos, Joinet, and Schellinx identified the same restriction of LK – and called it LKT – as part of a thorough investigation of linear logic encodings of classical proofs [5, 6]. Having gained through this correspondence the “naturalness” that was making the natural deduction usually preferred in practice, there was no reason any longer not to systematically study λ-calculus through sequent calculus rather than through the traditional Curry-Howard correspondence with natural deduction. Sequent calculus is far more well-behaved than natural deduction: it enjoys the subformula property, and destruction rules – cuts – are well characterized in contrast with the elimination rules of natural deduction which superimpose both a construction and a destruction operation: the application is a constructor in a term xM, but is destructive in a term (λx.M)N.

The leading goal at the root of the present work was to conceive a “sequent calculus” version of call-by-value λ-calculus and λμ-calculus. Our starting point was the observation that the call-by-value discipline manipulates input much in the same way as (the classical extension of) λ-calculus manipulates output. Computing MN in call-by-value can be viewed as filling the hole (hence an input) of the context M [ ] with the result of the evaluation of N. So the focus is on contexts waiting for values – a situation that sounds dual to that of (output) values being passed to continuations.

This leads us to a syntax with three different syntactic categories: contexts, terms, and commands^{1}. Commands are pairs consisting of a term and a context, they represent a closed system containing both the program and its environment. Correspondingly, we type these different categories with three kinds of sequents. The usual sequents Γ ⊢ Δ type commands, while the sequents typing terms (contexts)

1Danos has also recognized the relevance of these three categories in [4] where he extends the work of Ogata [17] on the relation between LKQ and call-by-value CPS-translations (LKQ is the other natural restriction of LK considered in [5, 6]). are of the form Γ ⊢ A | Δ (Γ | A ⊢ Δ). The symbol “|” serves to single out a distinguished conclusion/output (hypothesis/input), which stands for “where the computation will continue” (“where it happened before”).

In the rest of this introduction, we offer as a prologue a simple justification of the relevance of sequent calculus to the computational study of the λ-calculus. Call-by-name evaluation in the λ-calculus can be specified by the following inference rule:

\begin{matrix}M →^{∗} λx.P \\ MN → P [x ← N] \end{matrix} .

This recursive specification may be implemented with a stack as follows (M · S is the result of pushing M on top of S):

\begin{aligned}(MN , S) & → & (M , N · S) \\ (λx.P , N · S) & → & (P [x ← N] , S) \end{aligned}

This simple device is called Krivine abstract machine. It can be rephrased using contexts instead of stacks:

\begin{aligned}(MN , E) & → & (M , E[[ ]N]) \\ (λx.P , E[[ ]N]) & → & (P [x ← N] , E) \end{aligned}

(Recall that a context is a λ-term with a hole, denoted [ ], which can be filled with a term, or another context: e.g., E[[ ]N] is the context obtained by filling the hole of E with the context [ ]N.) Consider the evolution of the types of the holes in the contexts during the execution of the rules. If N has type A and if the hole of E has type B, then the hole of E[[ ]N] has type A → B. This corresponds to a left introduction of implication (note that holes in contexts correspond to inputs). Then the second rule of Krivine abstract machine reads as a cut between an implication which has been introduced on the right and an implication which has been introduced on the left. We are here in the world of sequent calculi, not of natural deduction.

In section 2, we recall the second author’s sequent calculus analysis of (call-by-name) λμ-calculus. In section 3, we discuss how to add call-by-value to the picture. This leads us in section 4 to \overline{λ}μμ̃-calculus and its typing system LK_{μμ̃}, a logical system for classical logic (limited to the implication connective) with the three kinds of sequents introduced above. In particular, we exhibit the symmetry between the call-by-name and call-by-value disciplines, by means of dual orientations of a single critical pair. In section 5, we analyze two subsyntaxes: the \overline{λ}μμ̃_{T} -calculus and the \overline{λ}μμ̃_{Q}- calculus, and the corresponding sequent calculi LKT_{μμ̃} and LKQ_{μμ̃}. These calculi correspond to LKT and LKQ; their relation with linear logic is explained in appendix B. Our translation of the λμ-calculus arrives in the intersection of these subsyntaxes, and the target reduction stays in \overline{λ}μμ̃_{T} - calculus (\overline{λ}μμ̃_{Q}-calculus) in the call-by-name (call-by-value) discipline.

Section 6 is a “reverse engineering” exercise. Guided by the goal of translating call-by-value normal forms into \overline{λ}μμ̃_{Q} normal forms, we revisit source call-by-value evaluation and syntax: we work on an extension of the λ-calculus with a let construct, and then on a restriction of this extension which in our opinion is the call-by-value counterpart of the λ-calculus.

In section 7, we complete the duality by adding the connective “-” (the difference). This allows us to exhibit fully the duality between terms and contexts. In section 8, we link our analysis to both the classical and the more recent works on continuation semantics. Finally, in section 9, we complete the description of cut-elimination in LK_{μμ̃}. We conclude in section 10.

2. CALL-BY-NAME λμ-CALCULUS IN SE-QUENT CALCULUS STYLE

In this section we present (a variant of) the \overline{λ}μ-calculus of [12]. This calculus is to sequent calculus what λμ-calculus is to natural deduction. (The syntax and the typing rules of simply-typed λμ-calculus are recalled in appendix A.) The syntax (as well as those of the subsequent sections) embodies the three syntactic categories discussed in the introduction:

Commands  c ::= ⟨v|E⟩
Contexts  E ::= α || v · E
Terms  v ::= x || μβ.c || λx.v

Its typing system is a sequent calculus based on judgements of the following form:

c : (Γ ⊢ Δ)  Γ | E : A ⊢ Δ  Γ ⊢ v : A | Δ

and typing rules are given below:

Γ | α : A ⊢ α : A, Δ

Γ, x : A ⊢ x : A | Δ

\begin{matrix}Γ ⊢ v : A | Δ Γ | E : B ⊢ Δ \\ Γ | (v · E) : A → B ⊢ Δ \end{matrix}

\begin{matrix}c : (Γ ⊢ β : B , Δ) \\ Γ ⊢ μβ.c : B | Δ \end{matrix}

\begin{matrix}Γ, x : A ⊢ v : B | Δ \\ Γ ⊢ λx.v : A → B | Δ \end{matrix}

\begin{matrix}Γ ⊢ v : A | Δ Γ | E : A ⊢ Δ \\ ⟨v|E⟩ : (Γ ⊢ Δ) \end{matrix}

The notations ⟨v|E⟩ can be read as some context E[ ] filled with v; when E = α, it becomes just another notation for the naming construction [α]v in λμ-calculus.

Terms can be reduced by the following reductions rules:

\begin{aligned}(→) & ⟨λx.v_{1}|(v_{2} · E)⟩ & → & ⟨v_{1}[x ← v_{2}]|E⟩ \\ (μ) & ⟨μβ.c|E⟩ & → & c[β ← E] \end{aligned}

Normal forms are those terms where either v = x or (E = α and v ≠ μβ.c) in subexpressions of the form ⟨v|E⟩.

Remark 2.1. Our treatment of \overline{λ}μ-calculus does not any longer follow totally the “cut=redex” paradigm of sequent calculus as in [12]. Another treatment could have been to add the two (contraction) rules

\begin{matrix}Γ, x : A | E : A ⊢ Δ \\ ⟨x|E⟩ : (Γ, x : A ⊢ Δ) \end{matrix}

\begin{matrix}Γ ⊢ V : B | β : B , Δ (V = x or V = λx.v) \\ ⟨V |α⟩ : (Γ ⊢ β : B , Δ) \end{matrix}

and restrict the cut rule to the other combinations of v, E. Then we have the “cut=redex” paradigm of sequent calculus, but another annoying phenomenon shows up: there are two derivations of ⟨x|α⟩. This can in turn be solved by removing the introduction rule for x but then ⟨v|E⟩ does not any longer include the ⟨x|E⟩ construction which must be added explicitly in the grammar. No perfect world.

Until section 9, we ignore the explicit process of substitution, i.e., as in natural deduction, we consider that the replacement is actually carried out completely in a single step. This makes it easier to convey our main observations and results.

We note that any normal \overline{λ}μ-term v has the following form:

\begin{matrix}v ::= x || μβ.c || λx.v \\ c ::= ⟨λx.v|α⟩ || ⟨x|v_{1} · . . . v_{n} · α⟩ \end{matrix}

We now define two translations ^{N} and ^{n} of λμ-calculus into the \overline{λ}μ-calculus. The translation ^{N} preserves normal forms, while the translation ^{n} is compositional, i.e., preserves the structure of (applicative) terms.

The translation ^{N} involves a parameterization by a context (a trick that goes back to Plotkin’s so-called colon translation [19]):

x^{N} = x
(λx.M)^{N} = λx.M^{N}
(μβ.c)^{N} = μβ.c^{N}
([α]M)^{N} = M_{α}^{N}
(MN)_{E}^{N} = M_{N^{N} ·E}^{N}
V_{E}^{N} = ⟨V^{N} |E⟩ where V = x || λx.M || μα.M

Proposition 2.2. The translation ^{N} maps normal terms to normal terms.

Proof. A λμ-normal form is either a variable x, or an abstraction λx.M (μβ.c) where M (c)is normal, or an expression [α]M where M is normal and not a μ abstraction, or an expression xM_{1} … M_{n}. The latter two cases correspond to the two situations in which a “cut” ⟨v|E⟩ is not a redex.

Notice that the term μβ.[α](… (xM_{1}) … M_{k}) and its translation μβ.⟨x|(M_{1}^{N} · (… (M_{k}^{N} · α) …))⟩ are essentially the same terms, up to a rearrangement. In the translation ^{N}, applicative terms are turned the other way round: a variable applied to a first argument, then to a second, and so on, becomes (an encoding of) a variable applied to a list of arguments.

With simple adjustments (consisting in restricting inessentially the syntax of the λμ-calculus and in atomizing the (μ)- rule), the statement of proposition 2.2 can be improved: it is essentially an isomorphism, i.e., a bijection that preserves reduction step by step both ways. Consider the following restriction of the syntax of the λμ-calculus that disallows applications in contexts of the form λx.[ ] and M[ ] (this is no real restriction since any application MN can be replaced by an expansion μα.[α](MN), cf. appendix A):

v ::= x || λx.v || μβ.c
c ::= [α]a
a ::= v || av

As for reduction, we decompose the (μ) rule of \overline{λ}μ-calculus in smaller steps according to the form of the context:

\begin{aligned}(μ_{app}) & ⟨μβ.c|v · E⟩ & → & ⟨μβ.(c[β ← v · β])|E⟩ \\ (μ_{var}) & ⟨μβ.c|α⟩ & → & c[β ← α] \end{aligned}

With these adjustments, proposition 2.2 can be restated as:

The translation ^{N} is an isomorphism: it is bijective, maps normal forms to normal forms, and preserves reductions step by step.

The translation ^{n} which we define now is compositional but does not preserve normal forms. This sort of translation is quite well known, since it amounts to translate natural deduction into sequent calculus.

x^{n} = x
(λx.M)^{n} = λx.M^{n}
(μβ.c)^{n} = μβ.c^{n}
([α]M)^{n} = ⟨M^{n}|α⟩
(MN)^{n} = μα.⟨M^{n}|N^{n} · α⟩

The translation ^{n} maps a normal form to its image by the previous translation modulo the use of the rule (μ) only (“administrative redexes”). Thanks to the insertion of μ at each application node, the translation simulates the reduction rule of λμ-calculus without need to refine the (μ) rule.

Proposition 2.3. The translation ^{n} is a homomorphism from λμ-terms to \overline{λ}μ-terms, i.e., it preserves (call-by-name) reduction. Moreover, for any λμ-term M, M^{n} reduces by repeated applications of the rule (μ) to M^{N}.

Proof. Preservation of reduction is trivial. Note that the preservation is even step to step: if v_{1} → v_{2}, then v_{1}^{n} → v_{2}^{n}. The second part of the statement is an easy consequence of the following:

\begin{matrix}(μβ.[α](xM_{1} … M_{k})^{n} →^{⋆} \\ μβ.⟨x|(M_{1}^{n} · (… (M_{k}^{n} · α) …))⟩ (k (μ) steps) \end{matrix}

Remark 2.4. Without logical or computational loss, one may force the body of a λ-abstraction to have the form μα.c (expanding λx.v as λx.μα.⟨v|α⟩ when necessary). This observation leads to a variant of the \overline{λ}μ-calculus where the λabstraction is replaced by a double abstraction λ(x, α).c, with the following typing rule:

\begin{matrix}c : (Γ, x : A ⊢ β : B, Δ) \\ Γ ⊢ λ(x, α).c : A → B | Δ \end{matrix}

.

3. CALL-BY-VALUE: INTRODUCING μ̃

Traditionally, one explains how to encode call-by-name in call-by-value by introducing explicit operators that freeze the evaluation of arguments. The same idea can be applied to encode call-by-value on top of call-by-name, now freezing the function until its argument is evaluated. The familiar construct let x = N in P can be understood in this way. Suppose that we want to compute an application MN in a call-by-value discipline. A first step may consist in writing (let x = N in Mx), with the intention that N should be evaluated before being passed to Mx, or equivalently that the application of M should be delayed until the argument N is evaluated. The expression can also be written as E[N], where E = (let x = [ ] in Mx). In order to encode such contexts, we introduce a new binding operator μ̃, which will turn out to be dual to μ. We encode (let x = [ ] in P), evaluated in a context E_{0}, as μ̃x.⟨P |E_{0}⟩. The μ̃-abstraction allows us to turn (or freeze) the expression P into a context waiting for the value of its hole. If P = Mx, we get μ̃x.⟨μα′.⟨M|x · α′⟩|E_{0}⟩, which reduces by (μ) to μ̃x.⟨M|x · E_{0}⟩.

What is the typing rule for μ̃? First, if c is a command, then μ̃x.c is a context (which is dual to μβ.c). The typing rule is as follows:

\begin{matrix}c : (Γ, x : B ⊢ Δ) \\ Γ | μ̃x.c : B ⊢ Δ \end{matrix}

One adds the following cut-elimination rule:

(μ̃)  ⟨v|μ̃x.c⟩ → c[x ← v]

which forms a critical pair with the (μ)-rule, in any command of the form ⟨μβ.c_{1}|μ̃x.c_{2}⟩. We impose that the (μ)- rule has priority in such a redex, yielding c_{1}[β ← μ̃x.c_{2}]. The (compositional) interpretation of the λμ-calculus is now redefined as follows:

x^{v} = x

(MN)^{v} = μα.⟨N^{v}|μ̃x.⟨M^{v}|x · α⟩⟩
(λx.M)^{v} = λx.M^{v}
([α]M)^{v} = ⟨M^{v}|α⟩
(μβ.c)^{v} = μβ.c^{v}

We next show how the call-by-value reduction is simulated through this translation:

((λx.M)N)^{v} =  μα.⟨N^{v}|μ̃x.⟨λx.M^{v}|x · α⟩⟩
→_{(→)} μα.⟨N^{v}|μ̃x.⟨M^{v}|α⟩⟩
→_{(μ̃)} μα.⟨M^{v}[x ← N^{v}]|α⟩
(N = x or λy.P)

The last unfreezing step is conditioned by the form of N^{v}: if N is a value in the sense of [19], i.e., is an abstraction or a variable, then the (μ̃)-reduction can be applied. Otherwise, N^{v} begins with a μ, which prevents an immediate application of (μ̃) and forces the evaluation of N^{v}.

A final remark before we can start to capitalize our analysis of call-by-name and call-by-value is that the translation we just defined for call-by-value works as well as it stands for call-by-name, provided one changes the priorities in the reduction system. If one now applies μ̃ as early as possible, then M^{v} reduces by repeated use of the μ̃ rule to M^{n}. We define the call-by-name (call-by-value) discipline as the application of the three rewrite rules (→), (μ), and (μ̃) giving priority to (μ̃) (to (μ)). Then, in call-by-name, M^{n} is just an optimized version of the translation M^{v}. We shall therefore use the neutral symbol ^{†}, instead of ^{v}, and proposition 2.3 can now be rephrased as follows:

The translation ^{†} is a homomorphism for call-by-name reduction. Moreover, for any λμ-term M, M^{†} reduces by repeated applications of the rules (μ̃) and (μ) to M^{N}.

This suggests to consider a call-by-value counterpart ^{V} to translation ^{N} and to proposition 2.2. But this raises the question of what should actually be considered as call-by-value normal forms in the λ-calculus. We defer this analysis until section 6.

4. THE SYSTEM LK_{μμ̃}

Collecting together the ingredients of the last two sections, we arrive at the \overline{λ}μμ̃-calculus whose syntax is

c ::= ⟨v|e⟩
v ::= x || μβ.c || λx.v
e ::= α || μ̃x.c || v · e

and evaluation rules are:

\begin{aligned}(→) & ⟨λx.v_{1}|v_{2} · e⟩ & → & ⟨v_{2}|μ̃x.⟨v_{1}|e⟩⟩ \\ (μ) & ⟨μβ.c|e⟩ & → & c[β ← e] \\ (μ̃) & ⟨v|μ̃x.c⟩ & → & c[x ← v] \end{aligned}

Observe we have not supposed yet any commitments for call-by-name or call-by-value reduction. This depends on the order of the last two rules:

Call-by-value consists in giving priority to the (μ)-redexes (which serve to encode the terms, say, of the form MN), while call-by-name gives priority to the (μ̃)-redexes.

The two disciplines are hereafter referred to as CBN reduction and CBV reduction, respectively.

At the typing level, we obtain LK_{μμ̃} whose typing judgements are:

\begin{matrix}c : (Γ ⊢ Δ) \\ Γ ⊢ v : A | Δ \\ Γ | e : A ⊢ Δ \end{matrix}

and whose typing rules are:

\begin{matrix}Γ ⊢ v : A | Δ Γ | e : A ⊢ Δ \\ ⟨v|e⟩ : (Γ ⊢ Δ) \end{matrix}

Γ | α : A ⊢ α : A, Δ

Γ, x : A ⊢ x : A | Δ

\begin{matrix}c : (Γ ⊢ β : B, Δ) \\ Γ ⊢ μβ.c : B | Δ \end{matrix}

\begin{matrix}c : (Γ, x : A ⊢ Δ) \\ Γ | μ̃x.c : A ⊢ Δ \end{matrix}

\begin{matrix}Γ ⊢ v : A | Δ Γ | e : B ⊢ Δ \\ Γ | v · e : A → B ⊢ Δ \end{matrix}

\begin{matrix}Γ, x : A ⊢ v : B | Δ \\ Γ ⊢ λx.v : A → B | Δ \end{matrix}

A λμ-term is translated into a \overline{λ}μμ̃-term as follows:

x^{†} = x (MN)^{†} = μα.⟨N^{†}|μ̃x.⟨M^{†}|x · α⟩⟩ (λx.M)^{†} = λx.M^{†} ([α]M)^{†} = ⟨M^{†}|α⟩ (μβ.c)^{†} = μβ.c^{†}

and a judgement Γ ⊢ M : A | Δ of the λμ-calculus is trans-

lated into a LK_{μμ̃} judgement Γ ⊢^{LK_{μμ̃}} M^{†} : A | Δ.

It can be proved that the translation is a homomorphism from call-by-value λμ-calculus [16] to the \overline{λ}μμ̃-calculus in call-by-value discipline.

Remark 4.1. The above formulation of the rule (→) is different from that of section 2, but is closely related to it: the former (→) is just the application of the new (→) immediately followed by (μ̃), which is always possible in CBN reduction, and is possible in CBV reduction when v_{2} is a variable or an abstraction, as required by the call-by-value discipline of the λ-calculus. (See also the decomposition of call-by-value β reduction in two steps, using an explicit let, in section 6.) The new formulation of the rule presents some redundancy with the translation ^{†}: the old version of (→) works as well as the new one as far as the reduction of some M^{†} is concerned, and the simpler translation ^{n} would also work even in call-by-value provided one takes the new version of (→). See also remark 8.4.

But in the larger context of the full LK_{μμ̃}, the new rule is the only one to make sense in CBV, while the translation † has been designed in such a way that its image (unlike that of ^{n}) lies in the intersection of two natural subsystems of LK_{μμ̃}, which we introduce next.

5. TWO WELL-BEHAVED SUBSYNTAXES

In this section, we define subcalculi of \overline{λ}μμ̃-calculus that we call \overline{λ}μμ̃_{T} -calculus and \overline{λ}μμ̃_{Q}-calculus because their typing systems correspond to the systems LKT and LKQ of [5, 6].

Their definition is guided by the requirement of stability under call-by-name and call-by-value evaluation, respectively (propositions 5.1 and 5.3).

Syntax of \overline{λ}μμ̃_{T}  Judgements of LKT_{μμ̃}

\begin{matrix}c ::= ⟨v|e⟩ \\ v ::= x || μβ.c || λx.v \\ E ::= α || v · E \\ e ::= μ̃x.c || E \end{matrix}  c : (Γ ⊢ Δ) ; Γ ⊢ v : A | Δ ; Γ ; E : A ⊢ Δ ; Γ | e : A ⊢ Δ

The contexts E are called applicative contexts. The typing rules are the same as those of LK_{μμ̃} for ⟨v|e⟩, μβ.c, μ̃x.c, x, and λx.v. The other rules are as follows:

Γ ; α : A ⊢ α : A, Δ

\begin{matrix}Γ ⊢ v : A | Δ Γ ; E : B ⊢ Δ \\ Γ ; (v · E) : A → B ⊢ Δ \end{matrix}

\begin{matrix}Γ ; E : A ⊢ Δ \\ Γ | E : A ⊢ Δ \end{matrix}

In the judgement Γ ; E : A ⊢ Δ, the sign “;” not only delineates a distinguished hypothesis, but also puts linearity constraints on this hypothesis: it is a stoup, in the terminology of Girard [9]. Note that implicit contractions are present in the left implication rule. On the other hand, the μ̃ mechanism is the only way to switch from a distinguished hypothesis to another hypothesis. The syntactic restrictions on LKT_{μμ̃} say that this can be done only at the price of turning the “;” into a “|”. Putting these observations together, we see that the rules of LKT_{μμ̃} guarantee that a formula in the stoup is never subject to a contraction rule. For the same reasons, it cannot be subject to a weakening rule (weakening outside the stoup is implicit in the typing rule for α).

Proposition 5.1. For any λμ-term M, M^{†} and any of its CBN reducts in \overline{λ}μμ̃-calculus lies in \overline{λ}μμ̃_{T} -calculus.

Remark 5.2. The typing system considered in section 2 lives within LKT_{μμ̃}. Therefore, we shall call it LKT_{μ}. In retrospect, in that section, we should have written Γ ; E : A ⊢ Δ as judgement instead of Γ | E : A ⊢ Δ. Notice also that with ^{n} or ^{N} instead of ^{†}, one has a sharpening: the reducts of the translation lie all in the \overline{λ}μ-calculus, in either case.

We now turn to the call-by-value restriction.

Syntax of \overline{λ}μμ̃_{Q}  Judgements of LKQ_{μμ̃}

\begin{matrix}c ::= ⟨v|e⟩ \\ V ::= x || λx.v \\ v ::= μβ.c || V \\ e ::= α || μ̃x.c || V · e \end{matrix}  c : (Γ ⊢ Δ) ; Γ ⊢ V : A; Δ ; Γ ⊢ v : A | Δ ; Γ | e : A ⊢ Δ

The terms V are called values. The typing rules are the same as in LK_{μμ̃} for ⟨v|e⟩, μβ.c, μ̃x.c, α, and λx.v. The other rules are as follows:

Γ, x : A ⊢ x : A; Δ

\begin{matrix}Γ ⊢ V : A; Δ Γ | e : B ⊢ Δ \\ Γ | (V · e) : A → B ⊢ Δ \end{matrix}

\begin{matrix}Γ, x : A ⊢ v : B | Δ \\ Γ ⊢ λx.v : A → B; Δ \end{matrix}

\begin{matrix}Γ ⊢ V : A; Δ \\ Γ ⊢ V : A | Δ \end{matrix}

Proposition 5.3. For any λμ-term M, M^{†} and any of its CBV reducts in \overline{λ}μμ̃-calculus lies in \overline{λ}μμ̃_{Q}-calculus.

Hence, for any λμ-term M, M^{†} stands in the intersection of \overline{λ}μμ̃_{T} -calculus and \overline{λ}μμ̃_{Q}-calculus (it uses only V ’s and E’s, in our notation), and its reducts stay in the relevant subsyntax once an evaluation discipline has been fixed.

The systems \overline{λ}μμ̃_{T} -calculus and \overline{λ}μμ̃_{Q}-calculus are also wellbehaved without reference to the λμ-calculus. It is easy to check that \overline{λ}μμ̃_{T} -calculus (\overline{λ}μμ̃_{Q}-calculus) is stable under CBN (CBV) reduction and that normal commands lies in \overline{λ}μ-calculus (\overline{λ}μ̃-calculus, defined in next section).

6. WHAT IS CBV λ-CALCULUS?

In section 2, we arrived at a perfect correspondence between call-by-name λμ-normal forms and (call-by-name) \overline{λ}μnormal forms. We wish to reach the same goal for call-by-value normal forms. Moreover, for the purposes of duality, we wish to eliminate the need of the μ-operation to encode call-by-value computation, since we did not need the μ̃ operator to encode call-by-name computation. Recall Plotkin’s definition of call-by-value reduction:

(β_{V}) (λx.M)V → M[x ← V]

(V variable or abstraction) .

A typical (β_{V}) normal form is thus (λx.M)(yN), whose translation

μα.⟨μβ.⟨N^{†}|μ̃z.⟨y|z · β⟩⟩|μ̃t.⟨λx.M^{†}|t · α⟩⟩

contains a (→) redex. A simple way out is to extend the syntax of the λ-calculus with a let construct:

M ::= x || λx.M || MN || let x = N in M

and to replace (β_{V}) by the following reduction rules:

(let) (λx.M)N → (let x = N in M)
(let_{β}) (let x = V in M) → M[x ← V]

(V variable or abstraction)

Then we extend the translation in the following way:

(let x = N in M)^{†} = μα.⟨N^{†}|μ̃x.⟨M^{†}|α⟩⟩ .

But consider now a term of the form (λxx′.M)(yN)V, which is normal for β_{V}, and whose (let) + (let_{β}) normal form is (let x = yN in λx′.M)V. We have:

((let x = yN in λx′.M)V)^{†}

= μα.⟨V^{†}|μ̃z.⟨μα′.⟨(yN)^{†}|μ̃x.⟨λx′.M^{†}|α′⟩⟩|z · α⟩⟩ ↓_{(μ̃)} μα.⟨μα′.⟨(yN)^{†}|μ̃x.⟨λx′.M^{†}|α′⟩⟩|V^{†} · α⟩ ↓_{(μ)} μα.⟨(yN)^{†}|μ̃x.⟨λx′.M^{†}|V^{†} · α⟩⟩ ↓_{(→)} μα.⟨(yN)^{†}|μ̃x.⟨M^{†}[x′ ← V^{†}]|α⟩⟩ = (let x = yN in M[x′ ← V])^{†}

Hence the translation is able to reduce the “hidden” redex (λx′.M)V. To avoid this mismatch, we introduce a further rule in the source language:

(let_{app}) (let x = a in M)N → (let x = a in (MN))

(x not free in N) .

This rule allows us to reduce (λxx′.M)(yN)V as follows:

(λxx′.M)(yN)V → (let x = yN in λx′.M)V
→ let x = yN in (λx′.M)V
→ let x = yN in M[x′ ← V] .

Consider now a term of the form (λx.M)((λy.V)(zN)) (y not free in M), which is normal for β_{V}, and whose (let) + (let_{β}) normal form is let x = (let y = zN in V) in M. We have:

(let x = (let y = zN in V) in M)^{†}

= μα.⟨μα′.⟨(zN)^{†}|μ̃y.⟨V^{†}|α′⟩⟩|μ̃x.⟨M^{†}|α⟩⟩ ↓_{(μ)} μα.⟨(zN)^{†}|μ̃y.⟨V^{†}|μ̃x.⟨M^{†}|α⟩⟩⟩ ↓_{(μ̃)} μα.⟨(zN)^{†}|μ̃y.⟨M^{†}[x ← V^{†}]|α⟩⟩ = (let y = zN in M[x ← V])^{†}

Here again the translation manages to reduce the “hidden” redex (let x = V in M). This leads us to introduce another rule:

(let_{let}) let x = (let y = N in M) in P

→ let y = N in (let x = M in P) (y not free in P)

It is easily checked that the (let) + (let_{β}) + (let_{app}) + (let_{let}) normal forms are as follows:

M ::= x || λx.M || let x = xMM_{1} … M_{n} in M || xMM_{1} … M_{n} It is possible at this stage to write a translation ^{V} from this set of normal forms to \overline{λ}μμ̃-terms in call-by-value normal form. But we would have to use μ in the translation, typically in a term like x(yM), for which one has to write

(x(yM))_{α}^{V} = ⟨x|μβ.⟨y|M^{V} · β⟩ · α⟩ .

In order to avoid placing applicative subterms in the contexts, and hence in order to achieve our second goal of “getting rid of μ”, we introduce a last rule:

(let_{exp}) Ma → (let x = a in Mx)

(a application or let expression)

The (let) + (let_{β}) + (let_{app}) + (let_{let}) + (let_{exp}) normal forms are as follows:

\begin{matrix}V ::= x || λx.M \\ M ::= V || let x = yV V_{1} … V_{n} in M || xV V_{1} … V_{n} \end{matrix}

We are now ready for our call-by-value normal form to normal form translation, which is defined below. Note the use of the double abstraction (cf. remark 2.4 – the point is that we need μ only under a λ):

x^{V} = x (λx.M)^{V} = λ(x, α).M_{α}^{V}

V_{α}^{V} = ⟨V^{V}|α⟩ (xV V_{1} … V_{n})_{α}^{V} = ⟨x|V^{V} · V_{1}^{V} · . . . · V_{n}^{V} · α⟩ (let x = yV V_{1} … V_{n} in M)_{α}^{V}

= ⟨y|V^{V} · V_{1}^{V} · . . . · V_{n}^{V} · μ̃x.M_{α}^{V}⟩

In this translation, there is no μ. This suggests to consider a calculus symmetric to the \overline{λ}μ-calculus of section 2, which we therefore call the \overline{λ}μ̃-calculus. At the typing level, we call the system LKQμ̃, to stress that it is a subsystem of LKQ_{μμ̃} (just as LKT_{μ} is a subsystem of LKT_{μμ̃}, cf. remark 5.2).

Syntax of \overline{λ}μ (LKT_{μ})  Syntax of \overline{λ}μ̃ (LKQμ̃)

\begin{matrix}c ::= ⟨v|E⟩ \\ v ::= x || λ(x, α).c || μβ.c \\ E ::= α || v · E \end{matrix}  \begin{matrix}c ::= ⟨V |e⟩ \\ V ::= x || λ(x, α).c \\ e ::= α || μ̃x.c || V · e \end{matrix}

The rewrite rules for LKQμ̃ are (μ̃) and the following new incarnation of the rule (→):

⟨λ(x, α).c|V · e⟩ → c[x ← V, α ← e]

Reading this back in λ-calculus style, we arrive at the following syntax, which we call λμ̃-calculus:

\begin{matrix}c ::= [α](V V_{1} … V_{n}) || let x = V V_{1} … V_{n} in c \\ V ::= x || λ(x, α).c \end{matrix}

where usual λx.V can be seen as a shortcut for λ(x, α).[α]V (α not free in V). We endow the λμ̃-calculus with the following reduction rules:

(β_{V}^{1} ) let y = (λ(x, α).c_{1})V_{1} … V_{n} in c_{2}

→ c_{1}[x ← V_{1}][ [α]a ← let y = aV_{2} … V_{n} in c_{2}]

(β_{V}^{2} ) [β]((λ(x, α).c)V_{1} … V_{n})

→ c[x ← V_{1}][ [α]a ← [β](aV_{2} … V_{n})]

(let_{β}) let x = V in c → c[x ← V]

where c_{1}[ [α]a ← c_{2}] is the term obtained by replacing every occurrence of [α](V V_{1} … V_{n}) in c_{1} by c_{2} where a is replaced by (V V_{1} … V_{n}). Remark that (β_{V}) derives directly from (β_{V}^{2} )(seeing λx.V as a shortcut for λ(x, α).[α]V). The translation ^{V} is straightforwardly adapted to λμ̃-terms, and defines in fact a bijection between the two syntaxes:

x^{V} = x

(λ(x, α).c)^{V} = λ(x, α).c^{V}

([α](V V_{1} … V_{n}))^{V} = ⟨V^{V}|V_{1}^{V} · . . . · V_{n}^{V} · α⟩

(let x = V V_{1} … V_{n} in c)^{V} = ⟨V^{V}|V_{1}^{V} · . . . · V_{n}^{V} · μ̃x.c^{V}⟩

We can now state the CBV counterpart of proposition 2.2.

Proposition 6.1. The translation ^{V} is an isomorphism from λμ̃-terms to \overline{λ}μ̃-terms.

Remark 6.2. In [20], Sabry and Felleisen characterized the theory induced on λ-calculus by the call-by-value CPS translation as the theory induced by the following two equations in addition to (β_{V}):

(β_{lift}) E[(λx.M)Q] = (λx.E[M])Q
(E ::= [ ] || EN || (λx.P)E)
(β_{flat}) xV_{1}V_{2} = (let y = xV_{1} in yV_{2})

Our rules (let_{app}) and (let_{let}) correspond exactly to (β_{lift}) (cases EN and (λx.P)E, respectively). Note that the other (let) rules are transparent from the point of view of the λcalculus (without let). The rule (β_{flat}), interpreted from right to left, corresponds to the following η-like equation^{2}:

μ̃x.⟨x|E⟩ = E (x not free in e)

Hence Sabry and Felleisen’s analysis of call-by-value λ-calcu-lus agrees with ours.

Remark 6.3. If we restrict to “η-long” \overline{λ}μ̃-terms (obtained by repeatedly applying expansions E → μ̃x.⟨x|E⟩), then we arrive at a syntax isomorphic to (a classical extension of) one of the calculi (based on Moggi’s computational λ-calculus) considered by Sabry and Wadler in [21], called λ_{c⋆⋆}:

c ::= [α]V || [α](V V_{1}) || let x = V in c || let x = V V_{1} in c V ::= x || λ(x, α).c

(See also [13].) Note that in the restricted syntax, there are no nested applications, or, equivalently, no expressions of the form V_{1} ·(V_{2} ·(⋯ (V_{n} ·E) ⋯)) with n ≥ 2. For example, V_{1} · (V_{2} · E) expands to V_{1} · μ̃x.⟨x|V_{2} · E⟩.

7. COMPLETION OF THE DUALITY

In order to dualize terms and contexts, we introduce a connective dual to implication: the difference connective, denoted “-”. The syntax of \overline{λ}μμ̃-calculus is extended as follows

2This equation is dual to the equation μα.[α]M = M (α not free in M) in λμ-calculus (cf. appendix A).

(we still call the extension \overline{λ}μμ̃-calculus):

c ::= ⟨v|e⟩
v ::= x || μβ.c || λx.v || e · v
e ::= α || μ̃x.c || v · e || βλ.e

We add the following computation rule:

(−)  ⟨(e_{2} · v)|βλ.e_{1}⟩ → ⟨v|e_{1}[β ← e_{2}]⟩

and the following typing rules to LK_{μμ̃}:

\begin{matrix}Γ | e : B ⊢ β : A, Δ \\ Γ | βλ.e : B − A ⊢ Δ \end{matrix}

\begin{matrix}Γ | e : A ⊢ Δ Γ ⊢ v : B | Δ \\ Γ ⊢ (e · v) : B − A | Δ \end{matrix}

We define a duality of \overline{λ}μμ̃-calculus into itself which works as follows at the type level:

X^{∘} = X
(A → B)^{∘} = B^{∘} − A^{∘}
(B − A)^{∘} = A^{∘} → B^{∘}

The translations c^{∘}, v^{∘}, and e^{∘} of commands, terms, and contexts are defined by recursively applying the following table of duality:

\begin{matrix}x & α & μβ & μ̃x & e · v & v · e & λx & βλ \\ α & x & μ̃x & μβ & v · e & e · v & βλ & λx \end{matrix}

Proposition 7.1. In LK_{μμ̃}, we have:

\begin{matrix}c : (Γ ⊢ Δ) \\ Γ ⊢ v : A | Δ \\ Γ | e : A ⊢ Δ \end{matrix} \} ⇔ \{ \begin{matrix}c^{∘} : (Δ^{∘} ⊢ Γ^{∘}) \\ Δ^{∘} | v^{∘} : A^{∘} ⊢ Γ^{∘} \\ Δ^{∘} ⊢ e^{∘} : A^{∘} | Γ^{∘} \end{matrix}

One can extend the definition of \overline{λ}μμ̃_{T} -calculus and \overline{λ}μμ̃_{Q}- calculus in such a way that the above proposition restricts and refines to a duality between \overline{λ}μμ̃_{T} -calculus and \overline{λ}μμ̃_{Q}- calculus. We just give the extended syntax of \overline{λ}μμ̃_{T} -calculus and \overline{λ}μμ̃_{Q}-calculus and leave the rest to the reader:

\overline{λ}μμ̃_{T} -calculus  \overline{λ}μμ̃_{Q}-calculus

\begin{matrix}c ::= ⟨v|e⟩ \\ v ::= x || μβ.c || λx.v || E · v \\ E ::= α || v · E || βλ.e \\ e ::= μ̃x.c || E \end{matrix}  \begin{matrix}c ::= ⟨v|e⟩ \\ V ::= x || λx.c || e · V \\ v ::= μβ.c || V \\ e ::= α || μ̃x.c || V · e || βλ.e \end{matrix}

8. CPS TRANSLATIONS

In this section, R stands for a fixed (arbitrary) type constant. We define a translation of LK_{μμ̃} types into intuitionistic types (i.e., the types of the simply-typed λ-calculus, written using the mathematical notation where B^{A} means the space of functions from A to B) as follows:

X^{◁} = X
(A → B)^{◁} = R^{A^{◁}×R^{B^{◁}}} = R^{(A−B)^{◁}}
(B − A)^{◁} = B^{◁} × R^{A^{◁}}

Note that if we read R as “false”, then the image of the translation of A → B (resp. B − A) reads as classically equivalent to A → B (resp. B − A). We next define a translation of \overline{λ}μμ̃-terms to λ-terms as follows:

⟨v|e⟩^{◁} = v^{◁}e^{◁}
α^{◁} = α
x^{◁} = λk.kx
(μβ.c)^{◁} = λβ.c^{◁}
(μ̃x.c)^{◁} = λx.c^{◁}
(λx.v)^{◁} = λk.k(λ(x, β).v^{◁}β)
(v · e)^{◁} = λk.v^{◁}(λx.k(x, e^{◁}))
(βλ.e)^{◁} = λ(y, β).e^{◁}y
(e · v)^{◁} = λk.v^{◁}(λy.k(y, e^{◁}))

Proposition 8.1.

\begin{matrix}c : (Γ ⊢^{LK_{μμ̃}} Δ) \\ Γ ⊢^{LK_{μμ̃}} v : A | Δ \\ Γ | e : A ⊢^{LK_{μμ̃}} Δ \end{matrix} \} ⟹ \{ \begin{matrix}Γ^{◁}, R^{Δ^{◁}} ⊢^{λ} c^{◁} : R \\ Γ^{◁}, R^{Δ^{◁}} ⊢^{λ} v^{◁} : R^{R^{A^{◁}}} \\ Γ^{◁}, R^{Δ^{◁}} ⊢^{λ} e^{◁} : R^{A^{◁}} \end{matrix}

Moreover, the translation validates the CBV discipline.

Remark 8.2. When restricted to LKQ_{μμ̃}, proposition 8.1 can be sharpened in such a way that the following additional implication holds:

Γ ⊢ V : A; Δ ⟹ Γ^{◁}, R^{Δ^{◁}} ⊢^{λ} V^{◁} : A^{◁}

provided one translates x as x, λx.V as λ(x, β).V^{◁}β and V as λk.kV^{◁} when considered as a v.

Note that the disymmetry of the λ-calculus forces the callby-value orientation of the (μ) − (μ̃) critical pair:

\begin{aligned}⟨μβ.c_{1}|μ̃x.c_{2}⟩^{◁} & = & (λβ.c_{1}^{◁})(λx.c_{2}^{◁}) \\ & → & c_{1}^{◁}[β ← λx.c_{2}^{◁}] . \end{aligned}

But the translation also takes care of the call-by-name discipline, via duality. We set ^{▷} = ^{◁} ∘ ^{∘}. Then we have:

X^{▷} = X
(A → B)^{▷} = B^{▷} × R^{A^{▷}}
(B − A)^{▷} = R^{(B→A)^{▷}} = R^{A^{▷}×R^{B^{▷}}}

Note that this time A^{▷} reads as classically equivalent to ¬A[X ← ¬X]. Note also that ^{▷} can alternatively be taken as primitive and ^{◁} defined as ^{◁} = ^{▷} ∘ ^{∘}.

Proposition 8.3.

\begin{matrix}c : (Γ ⊢^{LK_{μμ̃}} Δ) \\ Γ ⊢^{LK_{μμ̃}} v : A | Δ \\ Γ | e : A ⊢^{LK_{μμ̃}} Δ \end{matrix} \} ⟹ \{ \begin{matrix}R^{Γ^{▷}}, Δ^{▷} ⊢^{λ} c^{▷} : R \\ R^{Γ^{▷}}, Δ^{▷} ⊢^{λ} v^{▷} : R^{A^{▷}} \\ R^{Γ^{▷}}, Δ^{▷} ⊢^{λ} e^{▷} : R^{R^{A^{▷}}} \end{matrix}

Moreover, the translation validates the CBN discipline.

Combining ^{▷} and ^{◁} with the translation ^{n} from λμ-terms, we obtain two CPS-translations to λ-terms:

(CBN) Γ ⊢^{λμ} M : A | Δ ⇒ Δ^{▷}, R^{Γ^{▷}} ⊢^{λ} M^{n ▷} : R^{A^{▷}}
(CBV) Γ ⊢^{λμ} M : A | Δ ⇒ Γ^{◁}, R^{Δ^{◁}} ⊢^{λ} M^{n ◁} : R^{R^{A^{◁}}}

The two translations are known in the literature: ^{n ▷} is the (call-by-name) Lafont-Hofmann-Streicher translation [14] , and ^{n ◁} is (the extension to call-by-value λμ-calculus of) Plotkin’s call-by-value translation [19]. The following dictionary is useful to recognize this:

CBN  CBV

\begin{matrix}K_{A} = A^{∘◁} \\ C_{A} = R^{K_{A}} \end{matrix}  \begin{matrix}V_{A} = A^{◁} \\ K_{A} = R^{V_{A}} \\ C_{A} = R^{K_{A}} \end{matrix}

C_{Γ}, K_{Δ} ⊢^{λ} M^{n▷} : C_{A}  V_{Γ}, K_{Δ} ⊢^{λ} M^{n◁} : C_{A}

\begin{matrix}K_{A→B} \\ = (B^{∘} − A^{∘})^{◁} \\ = K_{B} × C_{A} \end{matrix}  \begin{matrix}V_{A→B} \\ = R^{V_{A}×R^{V_{B}}} \\ ≅ V_{A} → C_{B} \end{matrix}

Here, the letters V, K, and C stand for values, continuations, and computations, respectively. Lafont-Hofmann-Streicher semantics maps computations to computations and interprets a continuation of type A → B as a pair of a computation of type A and a continuation of type B (think of the stack N · S of section 1). Plotkin’s call-by-value semantics maps values to computations, and interprets a value of type A → B as a function from values to computations. repeatedly

Remark 8.4. If we combine ^{▷} and ^{◁} with the translation † rather than with the translation ^{n}, the picture is as follows: in CBN, M^{†▷} reduces to M^{n▷}, while, in CBV, M^{†◁} provides a right-to-left variant of Plotkin’s translation. For M = M_{1}M_{2}, we get respectively:

\begin{matrix}λk.M_{1}^{n◁}(λm.M_{2}^{n◁}(λn.m(n, k))) \\ λk.M_{2}^{†◁}(λn.M_{2}^{†◁}(λm.m(n, k))) . \end{matrix}

9. HEAD REDUCTION IN AN ABSTRACT MACHINE

In this section, we specify two kinds of (weak) head reduction machine.

The first machine is quite standard and based on environments. Instead of commands ⟨v|e⟩, we manipulate expressions having the form ⟨v{ρ_{1}}|e{ρ_{2}}⟩, where ρ_{1} and ρ_{2} are (explicit) environments, i.e., lists of bindings of the form (x = v{ρ}) or (α = e{ρ}). Given ρ_{1} and x, we write ρ_{1}(x) = v{ρ_{2}} if (x = v{ρ_{2}}) is the first binding of x appearing in ρ_{1}. The notation ⟨v|e⟩{ρ} is a shorthand for ⟨v{ρ}|e{ρ}⟩. To evaluate a command c, we start the machine with c{}.

⟨(λx.v_{1}){ρ_{1}}|(v_{2} · e){ρ_{2}}⟩
→ ⟨v_{1}{(x = v_{2}{ρ_{2}}) · ρ_{1}}|e{ρ_{2}}⟩
⟨(μβ.c){ρ_{1}}|e{ρ_{2}}⟩
→ c{(β = e{ρ_{2}}) · ρ_{1}}
⟨v{ρ_{1}}|(μ̃x.c){ρ_{2}}⟩
→ c{(x = v{ρ_{1}}) · ρ_{2}}
⟨x{ρ_{1}}|e{ρ_{2}}⟩
→ ⟨ρ_{1}(x)|e{ρ_{2}}⟩ (ρ_{1}(x) is defined)
⟨v{ρ_{1}}|α{ρ_{2}}⟩
→ ⟨v{ρ_{1}}|ρ_{2}(α)⟩ (ρ_{2}(α) is defined)

Remark that bindings of terms (contexts) have the restricted form (x = V {ρ}) ((α = E{ρ})) when reducing CBV (CBN).

The second machine exploits the idea of encoding environments by means of indexes in a stack as in the Pointer Abstract Machine from Danos-Regnier [7] (a restriction of it was studied in a previous work of the authors [3]).

The stack is a sequence of bindings that bind either a term or a context. Each binding denotes both a closure and an environment of which it is the more recent binding. Each binding comes with two indexes counted from the bottom of the stack. The first index points in the stack to where the environment of the term (or context) which turns it into a closure begins. The second index points to where the environment of which the binding is the more recent closure goes on. The concrete syntax for bindings is:

(x =^{n} v{p}) or (α =^{n} e{p}) (n, p natural numbers) .

A state of the machine is ⟨v{p}|e{q}⟩s. If s is a stack, we denote its length by |s|, and s|_{n} is the stack popped |s| − n times (thus, |s|_{n}| = n). To evaluate ⟨v|e⟩, we start from ⟨v{0}|e{0}⟩. The rules of the machine are as follows:

⟨(λx.v_{1}){p}|(v_{2} · e){q}⟩{s}

→ ⟨v_{1}{|s|}|e{q}⟩{(x =^{p} v_{2}{q}) · s}

⟨(μβ.⟨v|e′⟩){p}|e{q}⟩{s}

→ ⟨v{|s|}|e′{|s|}⟩{(β =^{p} e{q}) · s}

⟨v{p}|(μ̃x.⟨v′|e⟩){q}⟩{s}

→ ⟨v′{|s|}|e{|s|}⟩{(x =^{q} v{p}) · s}

⟨x{p}|e{q}⟩{s} → ⟨(s|_{p})(x)|e{q}⟩ ((s|_{p})(x) is defined)

⟨v{p}|α{q}⟩{s} → ⟨v{p}|(s|_{q})(α)⟩ ((s|_{q})(α) is defined)

⟨v{p}|e{q}⟩{s} → ⟨v{p}|e{q}⟩{s − min(|s| − p, |s| − q)} where

((x =^{n} v{p}) · s)(x) = v{p}

((y =^{n} v{p}) · s)(x) = (s|_{n})(x) x ≠ y

((α =^{n} e{q}) · s)(x) = (s|_{n})(x)

and similarly for s(α).

Remark 9.1. The last rule acts as a garbage collecting rule: it removes the part of the stack which is used neither by the term (the code) nor by its context. For instance, in a functional language with flat atomic types (even with fixpoints, e.g. PCF), the application of the last rule guarantees that a program of atomic type ends with an empty stack.

10. RELATED AND FUTURE WORKS

This section contains miscellaneous remarks organized along hopefully helpful keywords.

• Symmetry. Altogether, we have defined six calculi: the full \overline{λ}μμ̃ syntax in CBN and CBV discipline (section 4), the subsyntaxes \overline{λ}μμ̃_{T} -calculus / LKT_{μμ̃} and \overline{λ}μμ̃_{Q}-calculus / LKQ_{μμ̃} (section 5), and as further restrictions the \overline{λ}μcalculus (section 2) and the \overline{λ}μ̃-calculus (section 6). At all these levels, the duality of call-by-name and call-by-value is governed by the symmetry of the μ-terms and the μ̃-terms. The situation is summarized in the following table. In the table, ↩ shows a source-to-target direction (cf. proposition 5.3), while ↔ indicates stronger one-to-one correspondences (cf. proposition 2.2 and 6.1). It would be interesting to complete this picture by adding more strong correspondences ↔. One could in particular show that CBV λμ-calculus (for which let arrives naturally) relates to CBV \overline{λ}μμ̃-calculus. One could also consider call-by-name λ-calculus plus let, which has CBN \overline{λ}μμ̃-calculus as a target. In such a calculus, one could delay some substitutions, as in let x = yM_{1} in M_{2} (or μα.⟨y|v_{1} · μ̃x.⟨v_{2}|α⟩⟩), i.e. we could force some sharing of subcomputations.

Logic Syntax Evaluation  Language

LK_{μμ̃}  \overline{λ}μμ̃ \{ \begin{matrix}ND \\ CBN \\ CBV \end{matrix}
LKT_{μμ̃}  \overline{λ}μμ̃_{T}  CBN
LKQ_{μμ̃}  \overline{λ}μμ̃_{Q}  CBV  ↩ CBV λμ
LKT_{μ}  \overline{λ}μ  CBN  ↔ CBN λμ
LKQμ̃  \overline{λ}μ̃  CBV  ↔  λμ̃

• Non-determinism. In [1] and [23], the non-determinism of classical logic is encapsulated in critical pairs similar to the (μ)−(μ̃) pair. But no explicit connection with call-by-name / call-by-value appears in those works.

• Semantics. It is fairly clear that our syntax LK_{μμ̃} with the CBN (CBV) machine can be interpreted in Selinger’s control (co-control) categories: the categorical construction interpreting → (−) is an exponent (a co-exponent), and − (→) is a weak co-exponent (a weak exponent). It should be interesting and useful to work out the details of this interpretation.

• Dynamics. Laurent has investigated (CBN) proof-nets for an extended polarized linear logic that closely corresponds to λμ-calculus [15]. These proof-nets enjoy a simple correctness criterion. This suggests that a proof-net representation of LK_{μμ̃} is possible.

• Games. We intend to develop a game interpretation of our calculi. A game-theoretic analysis of call-by-value has been given by Honda and Yoshida [13]. One could hope to sharpen the analysis so as to obtain a game-theoretic reading of the duality of computation.

• Expressivity. We have used the difference connective in a purely formal way. It would be interesting to study this connective for its own sake and to get insights into its computational meaning. Crolard has initiated this kind of investigation [2]. One way of seeing the difference connective is that it allows us to view contexts as values: v·e is both a context whose hole has a function type A → B (as explained in the introduction) and a pair of values of type B −A (viewed as a product type). Under the latter interpretation, a cut of the form ⟨λ(x, α).c|e⟩ appears as a destructive let: “evaluate e to a pair, and bind the two components of the pair to x and α, respectively”.

11. REFERENCES

[1] F. Barbanera and S. Berardi, A symmetric λ-calculus for “classical” program extraction, Information and Computation 125, 103-117 (1996).

[2] Tristan Crolard, Typage des coroutines en logique soustractive, Proc. Journées Francophones des Langages Applicatifs, Collection Didactique, INRIA (http://pauillac.inria.fr/jfla99/index.html) (1999).

[3] P.-L. Curien, H. Herbelin, Computing with Abstract Böhm Trees, in the Proceedings of the 3rd Fuji International Symposium on Functional and Logic Programming, Eds M. Sato & Y. Toyama, World Scientific, 20-39 (1998).

[4] V. Danos, Sequent Calculus and Continuation Passing Style Compilation. To appear in the Proceedings of the 11th Congress of Logic, Methodology and Philosophy of Science, held in Cracow, Kluwer (1999).

[5] V. Danos, J.-B. Joinet, H. Schellinx, LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication, in Advances in Linear Logic, 211-224, Cambridge University Press (1995).

[6] V. Danos, J.-B. Joinet, H. Schellinx, A New Deconstructive Logic: Linear Logic, in The Journal of Symbolic Logic 62(3), 755-807 (1997).

[7] V. Danos, L. Regnier, Machina ex deo, ou encore quelque chose à dire sur la machine de Krivine, unpublished (1990).

[8] G. Gentzen, Investigations into logical deduction (1935), e.g. in Gentzen collected works, Ed M. E. Szabo, North Holland, 68ff (1969).

[9] J.-Y. Girard, On the unity of logic, Annals of Pure and Applied Logic 59, 201-217 (1993).

[10] Ph. de Groote, On the relation between the λμ-calculus and the syntactic theory of control, Lecture Notes in Computer Science 822 (1994).

[11] H. Herbelin, A lambda-calculus structure isomorphic to sequent calculus structure, Proc. of Computer Science Logic (CSL 94), Lecture Notes in Computer Science 933, 61-75 (1994). Doctorat, Université Paris 7 (1995).

[12] H. Herbelin, Séquents qu’on calcule, Thèse de Doctorat, Université Paris 7 (1995).

[13] K. Honda and N.Yoshida, Game-theoretic analysis of call-by-value computation, Proc. ICALP 97, Lecture Notes in Computer Science 1256, Springer (1997).

[14] M. Hofmann, T. Streicher, Continuation models are universal for λμ-calculus, Proc. Logic in Computer Science (1997).

[15] O. Laurent, Polarized proof-nets and λμ-calculus, draft (1999).

[16] C. H. L. Ong, C. A. Stewart, A Curry-Howard Foundation for functional computation with control, Proceedings of ACM SIGPLAN-SIGACT Symposium on Principle of Programming Languages, Paris, ACM Press, January (1997).

[17] I. Ogata, Constructive Classical Logic as CPS-calculus, to appear in IJFCS (International Journal of Foundations of Functional Programming).

[18] M. Parigot, λμ-calculus: An algorithmic interpretation of classical natural deduction, Proc. of the International Conference on Logic Programming and Automated Reasoning, St. Petersburg, Lecture Notes in Computer Science 624 (1992).

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

[20] A. Sabry, M. Felleisen, Reasoning about programs in continuation-passing style, Lisp and Symbolic Computation 6(3/4), 287-358 (1993).

[21] A. Sabry, P. Wadler, A reflection on call-by-value, TOPLAS 19(6) (1997).

[22] P. Selinger, Control categories and duality: on the categorical semantics of the λμ-calculus, draft (1999).

[23] C. Urban, G. Bierman, Strong normalization of cut-elimination in classical logic, Proc. Typed Lambda Calculus and Applications, Lecture Notes in Computer Science (1999).

APPENDIX

A. THE λμ-CALCULUS

The λμ-calculus [18] is an extension of the λ-calculus that deals with multiple conclusions and therefore allows us to account for classical reasoning. Under the Curry-Howard isomorphism, it can be seen as a λ-calculus with control operators, and is indeed equivalent to, say, Felleisen’s λCcalculus [10]. For the sake of consistency with our framework, we consider two syntactic categories: the terms and the commands, and, accordingly, two kinds of typing judgements:

Syntax:

\begin{matrix}M ::= x || MN || λx.M || μβ.c \\ c ::= [α]M \end{matrix}

Typing judgements:

Γ ⊢ M : A | Δ  c : (Γ ⊢ Δ)

Typing rules:

Γ, x : A ⊢ x : A | Δ

\begin{matrix}Γ ⊢ M : A → B | Δ Γ ⊢ N : A | Δ \\ Γ ⊢ MN : B | Δ \end{matrix}

\begin{matrix}Γ, x : A ⊢ M : B | Δ \\ Γ ⊢ λx.M : A → B | Δ \end{matrix}

\begin{matrix}c : (Γ ⊢ β : B, Δ) \\ Γ ⊢ μβ.c : B | Δ \end{matrix}

\begin{matrix}Γ ⊢ M : A | α : A, Δ \\ [α]M : (Γ ⊢ α : A, Δ) \end{matrix}

Reduction rules (in call-by-name):

\begin{aligned}(λx.M)N & → & M[x ← N] \\ (μβ.c)N & → & μα.c[β ← (α, N)] \\ [α](μβ.c) & → & c[β ← α] \end{aligned}

where substitution is the usual (capture-avoiding) substitution in the first rule and the third rule, while in the second rule one replaces every subterm of c of the form [β]M by [α](MN). There is an additional rule, similar to the η-reduction, which we do not include as a reduction rule (rather, we treat it implicitly as an expansion rule):

μα.[α]M = M  (α not free in M)

B. LINEAR DECORATION OF LKT_{μμ̃} AND

LKQ_{μμ̃}

In this section, we complete the work of section 5 by providing translations of LKT_{μμ̃} and LKQ_{μμ̃} into linear logic. Arrow types are translated as in [5].

The translation of LKT_{μμ̃} into linear logic is defined as follows on formulas:

X^{T} = X (A → B)^{T} = !?A^{T} →?B^{T} .

Such a translation which consists only in inserting modalities at some places without any other modification is called a linear decoration.

Proposition B.1.

\begin{matrix}Γ ⊢^{LKT_{μμ̃}} Δ \\ Γ ⊢^{LKT_{μμ̃}} A | Δ \\ Γ ; A ⊢^{LKT_{μμ̃}} Δ \\ Γ | A ⊢^{LKT_{μμ̃}} Δ \end{matrix} \} ⟹ \{ \begin{matrix}!?Γ^{T} ⊢^{LL}?Δ^{T} \\ !?Γ^{T} ⊢^{LL}?A^{T} ,?Δ^{T} \\ !?Γ^{T} , A^{T} ⊢^{LL}?Δ^{T} \\ !?Γ^{T} ,!?A^{T} ⊢^{LL}?Δ^{T} \end{matrix}

The linear decoration for LKQ_{μμ̃} is defined as follows:

X^{Q} = X (A → B)^{Q} = !A^{Q} →?!B^{Q} .

Proposition B.2.

\begin{matrix}Γ ⊢^{LKQ_{μμ̃}} Δ \\ Γ ⊢^{LKQ_{μμ̃}} A; Δ \\ Γ ⊢^{LKQ_{μμ̃}} A | Δ \\ Γ | A ⊢^{LKQ_{μμ̃}} Δ \end{matrix} \} ⟹ \{ \begin{matrix}!Γ^{Q} ⊢^{LL}?!Δ^{Q} \\ !Γ^{Q} ⊢^{LL} A^{Q},?!Δ^{Q} \\ !Γ^{Q} ⊢^{LL}?!A^{Q},?!Δ^{Q} \\ !Γ^{Q},!A^{Q} ⊢^{LL}?!Δ^{Q} \end{matrix}