From Continuation Passing Style to Krivine’s Abstract Machine

Peter Selinger Department of Mathematics and Statistics University of Ottawa Ottawa, ON K1N 6N5, Canada

Abstract

We describe, for three different extensions of typed lambda calculus, how the rules for a version of Krivine’s abstract machine can be derived from those of continuation passing style (CPS) semantics. The three extensions are: Parigot’s λμcalculus, Pym and Ritter’s λμν-calculus, and an extension of the call-by-name lambda calculus with built-in types and primitive functions. We also show how Krivine’s abstract machine can be implemented on realistic hardware by compiling it into an idealized assembly language.

1 Introduction

Abstract machines play an important role in the implementation of programming languages. Examples include Warren’s 1983 abstract machine for Prolog, which is the basis for most modern Prolog implementations [12], and Cousineau’s 1990 categorical abstract machine for ML, on which the original Caml implementation was based (and from which it derives its name) [2]. The reason abstract machines are so useful is because, on the one hand, they are sufficiently “abstract” to relate easily to other kinds of mathematical semantics, such as equational semantics or continuation passing style (CPS) semantics. On the other hand, they are sufficiently “machine-like” to be easily implementable on real machines.

A particularly nice example of an abstract machine is Krivine’s machine for the call-by-name lambda calculus [6]. In this paper, we show how it is possible to “derive” the rules of Krivine’s abstract machine, in a semi-formal but systematic way, from a CPS semantics in the style of Hofmann and Streicher [5]. We do this for three extensions of the lambda calculus: the λμ-calculus, the λμν-calculus, and an extension of lambda calculus with built-in basic types and primitive functions. For each of these extensions, we also give an implementation of Krivine’s abstract machine, which takes the form of a compiler into an idealized assembly language.

It is interesting to note that Hofmann and Streicher’s CPS semantics can itself be derived, via a categorical completeness theorem, from a yet more abstract categorytheoretical semantics. This semantics is based on the interpretation of the λμν-calculus in a so-called control category, and it generalizes the familiar interpretation of the simply-typed lambda calculus in cartesian-closed categories [10]. Thus, one obtains the following sequence of constructions, leading systematically from the very abstract to the very concrete:

Categorical Semantics → CPS Semantics → Abstract Machine → Compiler

Krivine’s abstract machine therefore fits nicely into a multi-step process for designing implementations which are essentially “correct by contruction”, relative to a given high-level semantics. In this paper, we only consider the last two steps in this sequence; the first step, namely the relationship between the categorical semantics and the CPS semantics, is discussed elsewhere [10].

It should be stressed that, from a practical point of view, the implementation of the call-by-name lambda calculus derived in this paper is too inefficient to be of much use. Because our implementation follows the design of Krivine’s abstract machine very closely, it embodies a “naive” version of call-by-name evaluation, in which each subterm is possibly evaluated many times. More realistic implementations of call-by-name languages typically use a form of “lazy” evaluation to avoid this problem.

The development of CPS semantics, abstract machine, and a compiler, as presented in this paper, is a rational reconstruction and does not reflect the historical development of these concepts. As a matter of fact, Krivine’s formulation of his abstract machine predates the CPS semantics of Hofmann and Streicher, which in turns predates the categorical semantics in terms of control categories. Also, the connection between continuation semantics and abstract machines is well-known; for example, a treatment in the context of denotational semantics was given in [11]. We do not claim originality for any of the results presented in this article; rather, we hope to present them under a unique and unifying point of view.

2 The λμ-calculus

The λμ-calculus was originally introduced by Parigot as a proof-term calculus for classical logic [7]. Following Griffin’s earlier work, who showed that under the Curry-Howard isomorphism, classical logic corresponds to languages with control operators [4], the λμ-calculus can also be regarded as a prototypical call-by-name language with control primitives for handling continuations. In this respect, it is similar to programming languages with callcc or Felleisen’s C operator [3], except that the latter languages are call-by-value. The rewrite semantics of the λμ-calculus is not very intuitive, and Krivine’s abstract machine offers a more easily accessible way to understand its operational behavior. The control primitives are given a natural interpretation as certain manipulations of stack closures.

The λμ-calculus extends the simply-typed lambda calculus with a pair of control operators which can influence the sequential flow of control during the evaluation of a term. Normally, in call-by-name, a term M represents a computation which, upon demand, returns some result to its environment. For instance, if the term M appears in a context C[−], then the result which M computes will be returned to C[−].

Table 1: The typing rules for the λμ-calculus

(var)  \overline{Γ ⊢ x : A | Δ} if x:A ∈ Γ
(∗)  \overline{Γ ⊢ ∗ : ⊤ | Δ}
(pair)  \frac{Γ ⊢ M : A | Δ  Γ ⊢ N : B | Δ}{Γ ⊢ ⟨M, N⟩ : A ∧ B | Δ}
(π_{i})  \frac{Γ ⊢ M : A_{1} ∧ A_{2} | Δ}{Γ ⊢ π_{i}M : A_{i} | Δ}
(app) \frac{Γ ⊢ M : A → B | Δ  Γ ⊢ N : A | Δ}{Γ ⊢ MN : B | Δ}
(abs)  \frac{Γ, x:A ⊢ M : B | Δ}{Γ ⊢ λx^{A}.M : A → B | Δ}
(name)  \frac{Γ ⊢ M : A | Δ}{Γ ⊢ [α]M : ⊥ | Δ} if α:A ∈ Δ
(μ)  \frac{Γ ⊢ M : ⊥ | α:A, Δ}{Γ ⊢ μα^{A}.M : A | Δ}

In the λμ-calculus, terms are given the ability to ignore their immediate context and to return a result someplace else. Intuitively, this can be thought of as “sending” a result on a “channel”. We introduce a set of channel names α, β, etc., which are distinct from the usual lambda calculus variables x, y, z. The term [α]M causes the result of M to be sent on channel α. Dually, the term N = μα^{A}.P will start by evaluating P, but if in the process of doing so, anything is sent on the channel α, then this immediately becomes the result of N. Channel names are typed, and we say that a channel α has type A if values of type A can be sent along it. As we are in a sequential world, channels are refered to as continuations, and channel names α, β are refered to as control variables, or simply names.

This first interpretation of the λμ-calculus in terms of “channels” is only an intuitive approximation; a more accurate interpretation can be found in the description of the CPS translation or Krivine’s abstract machine below. Modulo some minor differences in typing, the term μα^{A}.M is a call-by-name analogue of callcc(λα^{¬A}.M) in the call-by-value world, where callcc is the call-with-current-continuation operator as it appears for instance in Scheme or Standard ML.

2.1 Syntax

We start from a simply-typed lambda calculus with finite products. Binary products are denoted A ∧ B, and the terminal type (or empty product) is denoted by ⊤.

To obtain the λμ-calculus, we first add a new type ⊥. The type ⊥ is thought of as the “empty type”, or the type of a term which never returns a result to its immediate context. Thus, the types of the λμ-calculus are given as follows, where σ ranges over a set of basic types:

A, B ::= σ ⊤ A ∧ B A → B ⊥

As usual, we sometimes write ¬A as an abbreviation for the type A → ⊥. The λμcalculus uses two sets of identifiers, variables and names, which are ranged over by x, y, … and α, β, …, respectively. Variables and names belong to two separate name spaces, which are usually assumed to be disjoint. Semantically, variables are bound to terms, whereas names are bound to continuations. The terms of the λμ-calculus are obtained from the terms of the simply-typed lambda calculus by adding two new term constructors, [α]M and μα^{A}.M. Thus, terms are given as follows:

M, N ::= x ∗ ⟨M, N⟩ π_{1}M π_{2}M MN λx^{A}.M [α]M μα^{A}.M

A term of the form μα^{A}.M is called a μ-abstraction, and a term of the form [α]M is called a named term. In the terms λx^{A}.M and μα^{A}.M, the variable x, respectively the name α, is bound. As usual, terms are identified up to capture-free renaming of bound variables and names. We write FV(M) and FN(M) for the set of free variables and free names of M, respectively. For simplicity, we do not consider basic term constants at this point; we will show how to add them in Section 4.

The typing rules for λμ-terms are shown in Table 1. Here Γ ranges over variable contexts and Δ ranges over name contexts, which are (finite) assignments of types to variables and names, respectively. A typing judgment is an expression of the form Γ ⊢ M : A | Δ. It asserts that the term M is well-typed of type A, assuming that its free variables and names have the types declared in Γ, respectively Δ. Note that the turnstile “⊢”, the colon “:”, and the vertical bar “|” are all part of the syntax of typing judgments; thus, a typing judgment is a 4-tuple consisting of a variable context, a term, a type, and a name context. Valid typing judgments are those which can be derived from the rules in Table 1.

Note the typing rules for (name) and (μ). The term [α]M has type ⊥, reflecting the fact that such a term never returns anything to its immediate environment. Similarly, in the term μα^{A}.M, we assume that the subterm M has type ⊥, as we have no use for its value. These typing conventions differ slightly from Parigot’s original formulation of the λμ-calculus, where the type ⊥ only occured implicitly, and only at the top level.

One notable difference between the λμ-calculus and its call-by-value cousins is that we use a separate name space for continuations, rather than identifying them with variables of type ¬A (or A cont, as this type is known in ML). While this distinction would make no difference in call-by-value, it turns out to be an important optimization in call-by-name.

Another difference is that in ML, the term which is analogous to [α]M would be given an arbitrary type B, and in μα^{A}.M, the subterm M would have type A. However, this difference is unimportant, as we can replace the first term by μβ^{B}.[α]M, for a dummy name β, and the second one by μα^{A}.[α]M, in cases where the alternate typing is required.

The fact that we write the name context Δ on the right-hand side of a typing judgment is motivated by logic: under the formulas-as-types correspondence, a typing judg-

Table 2: Axioms of the call-by-name λμ-calculus

Axioms for the lambda calculus with products:

(β_{→}) (λx^{A}.M)N  = M[N/x] : B
(η_{→}) λx^{A}.Mx = M : A → B if x ∉ FV(M)
(β_{∧}) π_{i}⟨M_{1}, M_{2}⟩  = M_{i} : A_{i}
(η_{∧}) ⟨π_{1}M, π_{2}M⟩  = M : A ∧ B
(η_{⊤}) ∗  = M : ⊤

Axioms for λμ:

(ζ_{→}) (μα^{A→B}.M)N = μβ^{B}.M[[β]^{(−)}N/[α]^{(−)}] : B if β ∉ FN(M, N)
(ζ_{∧}) π_{i}(μα^{A_{1}×A_{2}}.M) = μβ^{A_{i}}.M[[β]π_{i}^{(−)}/[α]^{(−)}] : A_{i} if β ∉ FN(M)
(β_{μ}) [α′]μα^{A}.M  = M[α′/α] : ⊥
(η_{μ}) μα^{A}.[α]M = M : A if α ∉ FN(M)
(β_{⊥}) [ξ^{⊥}]M  = M : ⊥

ment x_{1}:A_{1}, …, x_{n}:A_{n} ⊢ M : B | α_{1}:B_{1}, …, α_{m}:B_{m} corresponds to a logical implication A_{1} ∧…∧A_{n} ⇒ B ∨B_{1} ∨…∨B_{m}. Operationally, we think of M as a function in n arguments, with m + 1 alternative ways of returning a result.

2.2 Equational theory

The equational theory of the λμ-calculus is an extension of that of the call-by-name lambda calculus. The axioms are shown in Table 2. These axioms use three kinds of substitution. We write M[N/x] for the usual substitution of a term N for a variable x in M. We write M[α′/α] for the substitution of a name α′ for another name α in M. Finally, we consider the so-called mixed substitution: If M is a term, C^{(−)} is a context, and α is a name, then the mixed substitution M[C^{(−)}/[α]^{(−)}] is the result of recursively replacing any subterm of the form [α]^{(−)} by C^{(−)} in M. For all three kinds of substitution, appropriate care must be taken to avoid the capture of free variables. Also note that technically, each equation M = N is understood to be stated within a particular typing context, and equations are only between well-typed terms. However, we usually omit the typing context from the notation. For more details, see e.g. [10].

It is possible to give an operational semantics of the λμ-calculus in terms of a reduction relation based on a directed version of the axioms of Table 2. However, this notion of reduction is neither intuitive nor particularly enlightening. We prefer to discuss the operational semantics of the λμ-calculus in terms of a CPS translation (in Section 2.3) and via an abstract machine (in Section 2.4).

Table 3: The CPS translation of the call-by-name λμ-calculus

\underline{x}  = λk^{K_{A}}.x̃k  where x : A
\underline{∗}  = λk^{K_{⊤}}.□_{R}k
\underline{⟨M, N⟩} = λk^{K_{A∧B}}.[\underline{M}, \underline{N}]k where M : A, N : B
\underline{π_{1}M}  = λk^{K_{A}}.\underline{M}(inl k) where M : A ∧ B
\underline{π_{2}M}  = λk^{K_{B}}.\underline{M}(inr k) where M : A ∧ B
\underline{MN}  = λk^{K_{B}}.\underline{M}⟨\underline{N}, k⟩ where M : A → B, N : A
\underline{λx^{A}.M} = λ⟨x̃, k⟩^{K_{A→B}}.\underline{M}k where M : B
\underline{[α]M} = λk^{K_{⊥}}.\underline{M}α̃ where M : A
\underline{μα^{A}.M} = λα̃^{K_{A}}.\underline{M}∗  where M : ⊥

2.3 CPS semantics

We give a continuation passing style (CPS) semantics of the λμ-calculus in the style of Hofmann and Streicher [5]. The target language of this CPS translation is a lambda calculus λ^{R×+} with finite sums, products, and a distinguished type R, called the type of responses. Function types in the target calculus are restricted to the case A → R. Thus, every application MN in the target calculus is of type R, as is the body of any lambda abstraction.

To keep the notation brief, we use various forms of syntactic sugar for the sums and products of the target calculus. We use patterned lambda abstraction λ⟨x, y⟩^{A×B}.M as an abbreviation for λz^{A×B}.M[π_{1}z/x, π_{2}z/y]. We also use the co-pairing notation [M, N] as an abbreviation for the term

λk^{A+B}.case k of inl k_{1} → Mk_{1} | inr k_{2} → Nk_{2}.

Notice that [M, N] is the term that corresponds to ⟨M, N⟩ under the canonical isomorphism (A + B) → R ≅ (A → R) × (B → R). The initial type 0 is equipped with a type cast operator: If M has type 0, then □_{A}M has type A.

Definition (Call-by-name CPS translation). We assume that the target calculus has a chosen type σ̃ for each basic constant σ of the λμ-calculus. For each type A of the λμ-calculus, we define a pair of types K_{A} and C_{A} of the target calculus, which are respectively called the type of continuations and of computations of type A:

K_{σ}  = σ̃,  if σ is a basic type,
K_{⊤}  = 0,
K_{A∧B} = K_{A} + K_{B},
K_{A→B} = C_{A} × K_{B},
K_{⊥}  = 1,
C_{A}  = K_{A} → R.

For each variable x and each name α of the λμ-calculus, we assume a distinct chosen variable x̃, respectively α̃, of the target calculus. The call-by-name CPS translation \underline{M} of a typed term M is defined in Table 3. It respects the typing in the following sense:

\frac{x_{1}:B_{1}, …, x_{n}:B_{n} ⊢ M : A | α_{1}:A_{1}, …, α_{m}:A_{m}}{x̃_{1}:C_{B_{1}}, …, x̃_{n}:C_{B_{n}}, α̃_{1}:K_{A_{1}}, …, α̃_{m}:K_{A_{m}} ⊢ \underline{M} : C_{A}} .

This CPS translation, for the fragment without product types, is due to Hofmann and Streicher [5]. It differs from Plotkin’s original call-by-name translation [8] by introducing one less double negation at function types, thus taking advantage of the products of the target language.

The CPS translation respects the equational theory in the sense that M = N holds in the equational theory of the λμ-calculus if and only if \underline{M} = \underline{N} holds in the equational theory of the target calculus.

Remark. The above CPS translation for the λμ-calculus can be derived abstractly, via a categorical representation theorem, from a category-theoretic interpretation of the λμcalculus. This interpretation takes place in a class of so-called “control categories”, and it generalizes the well-known interpretation of the simply-typed lambda calculus in cartesian-closed categories. For details, see [10].

2.4 From the CPS semantics to Krivine’s abstract machine

In this section, we describe a rational reconstruction of Krivine’s abstract machine directly from the CPS semantics, adopted to the λμ-calculus. Note that an abstract machine interpretation was already sketched in the very last paragraph of Parigot’s original paper on the λμ-calculus [7].

We start by observing that each continuation type K_{A} is equipped with a set of canonical term constructors, shown in the following table. Here, k ranges over continuations and M over computations.

Type:  Constructors:
K_{⊤} = 0  −
K_{A∧B} = K_{A} + K_{B}  inl k, inr k
K_{A→B} = C_{A} × K_{B}  ⟨M, k⟩
K_{⊥} = 1  ∗

There is also a top-level continuation κ, which is the first continuation passed (presumably by the operating system) to the entire program.

Next, we change the notation for continuations. A pair ⟨M, k⟩ will be written in infix notation M::k. Instead of inl k and inr k, we will write tag_{1}::k and tag_{2}::k, respectively. We write nil for ∗, and also for κ, the top-level continuation. To summarize, we arrive at the following syntax for continuations:

k ::= tag_{1}::k tag_{2}::k M::k nil.

As this notation suggests, we will think of a continuation as an ordered list, which will be used as a stack. The elements of this stack are the tags tag_{1} and tag_{2}, as well as computations M. The symbol nil represents the empty stack.

Table 4: The transitions of the abstract machine

CPS  Abstract Machine
\underline{x}k  → x̃k  \{x, σ, k\}  → \{M, τ, k\}, where σ(x) = M^{τ}.
\underline{⟨M, N⟩}(inl k) → \underline{M}k  \{⟨M, N⟩, σ, tag_{1}::k\} → \{M, σ, k\}
\underline{⟨M, N⟩}(inr k) → \underline{N}k  \{⟨M, N⟩, σ, tag_{2}::k\} → \{N, σ, k\}
\underline{π_{1}M}k  → \underline{M}(inl k)  \{π_{1}M, σ, k\}  → \{M, σ, tag_{1}::k\}
\underline{π_{2}M}k  → \underline{M}(inr k)  \{π_{2}M, σ, k\}  → \{M, σ, tag_{2}::k\}
\underline{MN}k  → \underline{M}⟨\underline{N}, k⟩  \{MN, σ, k\}  → \{M, σ, N^{σ}::k\}
\underline{λx^{A}.M}⟨N, k⟩ → \underline{M}[N/x̃]k  \{λx.M, σ, N^{τ}::k\} → \{M, σ(x ↦ N^{τ}), k\}
\underline{[α]M}k  → \underline{M}α̃  \{[α]M, σ, k\}  → \{M, σ, k′\}, where σ(α) = k′.
\underline{μα.M}k  → \underline{M}[k/α̃]∗  \{μα.M, σ, k\}  → \{M, σ(α ↦ k), nil\}

After having changed the notation for continuations, we will now also change the notation for computations, i.e., for translated terms. In order to avoid having to do substitutions, we introduce the notion of a closure. A closure is a pair M^{σ} of a term M and an environment σ. An environment for M is a map from the free variables of M to closures, and from the free names of M to continuation, i.e., stacks. An environment σ is also sometimes called an activation record.

The states of Krivine’s abstract machine are triples {M, σ, k}, consisting of a term, an environment, and a stack. Informally, a state \{M, σ, k\} represents the term \underline{M′}k of type R of the target language of the CPS transform, where M′ is the term represented by the closure M^{σ}. The transition rules of the abstract machine can be read off directly from the corresponding transitions of the CPS semantics. Both sets of transitions are shown in Table 4.

Note how the continuation-manipulating operations of the λμ-calculus, namely the terms μα^{A}.M and [α]M, correspond to manipulations of entire stacks, rather than individual stack elements. In particular, the μα construction requires saving an image of the entire current stack into a variable α. In actual implementations, such an operation can be implemented in several different ways. One possibility, which we will follow in Section 5, is to make an actual copy of the current stack somewhere on the heap, and to store a pointer to it in the variable α. Such a stack copy is called a stack closure. This implementation is conceptually simple, but potentially expensive if the stack tends to be large. Another possibility is to implement stacks as linked lists, and to use sharing instead of copying to implement the μ-operation. This reduces the cost of each μ-operation, but it can lead to an increased load for the garbage collector. See [1] for a thorough discussion of the tradeoffs of the various implementations.

The initial state for a closed program M is {M, ∅, nil}. In other words, a program starts executing in the empty environment, and with an empty stack. It is easy to see from Table 4 that the transition relation of the abstract machine is deterministic, i.e., each state has at most one successor state. On the other hand, there are clearly some states from which no transition is possible. Several such states are designated as special halting states, and we write:

{∗, σ, nil}  → halt “unit”
{⟨M, N⟩, σ, nil} → halt “pair”
{λx.M, σ, nil} → halt “function”

In these cases, we say that the machine halts and outputs a result, which is one of the strings “unit”, “pair”, or “function”. This indicates that the λμ-expression has been reduced to a unit term, to a pair, or to a lambda abstraction (neither of which will be evaluated further).

A state which neither allows a valid transition nor is a designated halting state is called an error state. An example of an error state is {⟨M, N⟩, σ, P^{τ}::k}. This state represents a run-time typing error, because if the current term is a pair ⟨M, N⟩, then the abstract machine expects either tag_{1} or tag_{2} on top of the stack, to indicate which of two possible branches is to be taken. It does not make sense, in this situation, to find P^{τ} on top of the stack. We imagine that the abstract machine will abort execution when it encounters an error state; a real machine might engage in undefined behavior or even crash.

Note that, as we can see from Table 4, the transitions of the abstract machine, starting from an initial state {M, ∅, nil}, correspond precisely to the top-most reduction sequence of the term \underline{M}κ (modulo some administrative reductions).

2.5 Type soundness

A crucial property of the abstract machine is that a well-typed program does not reach an error state.

Proposition 2.1 (Type soundness). If M is a well-typed, closed term of the λμcalculus, then there is no sequence of transitions leading from state {M, ∅, nil} to an error state.

As a matter of fact, the simply-typed λμ-calculus without explicit recursion is strongly normalizing, and thus a halting state is always reached in a finite number of steps. However, once recursion is added, it is possible to obtain a non-terminating sequence of reductions.

Type soundness is best proved by giving a typed version of the abstract machine. Typed closures and typed stacks are defined by mutual recursion. A typed closure is a pair {Γ ⊢ M : A | Δ, σ}, where Γ ⊢ M : A | Δ is a valid typing judgment and σ is an environment that maps the variables and names from Γ and Δ to typed closures, respectively typed stacks, of the appropriate types. Stacks are typed as follows:

\frac{k : A}{tag_{1}^{A,B}::k : A ∧ B}  \frac{k : B}{tag_{2}^{A,B}::k : A ∧ B}
k : B {Γ ⊢ M : A | Δ, σ}::k : A → B
nil^{⊥} : ⊥

nil^{A_{top}} : A_{top}

Here, A_{top} is the top-level type of the entire program. Note that not only term closures, but also the tags tag_{1} and tag_{2} and the empty stack nil carry type annotations. Finally, a typed abstract machine state is {Γ ⊢ M : A | Δ, σ, k}, where {Γ ⊢ M : A | Δ, σ} is a typed closure and k is a typed stack of type A. Note that the type of k matches that of M. It is now straightforward to check the following:

1. The initial state {M, ∅, nil} is typable, if M is a well-typed closed λμ-term.

2. The transitions of the abstract machine preserve well-typedness.

3. Every well-typed abstract machine state is either a halting state, or else it has a unique successor state. In particular, a well-typed state cannot be an error state.

3 Adding classical disjunction

The λμν-calculus is an extension of the λμ-calculus with a type A ∨ B of classical disjunctions, first introduced by Pym and Ritter [9]. In call-by-name languages, the type of classical disjunctions is distinct from the more familiar intuitionistic “sum” type A + B, which is usually defined via left and right injections and case distinctions. In fact, the two disjunctions (intuitionistic and classical) are related by the type isomorphism A + B ≅ (¬¬A) ∨ (¬¬B). This implies that classical disjunctions can be regarded as more primitive than sum types. As we will see, classical disjunctions can be naturally interpreted in Krivine’s abstract machine as the ability to push and pop entire stack closures to and from the current stack.

3.1 The λμν-calculus

Pym and Ritter [9] propose the following straightforward way of adding a disjunction type to the λμ-calculus:

Types: A, B ::= … A ∨ B
Terms: M, N ::= … ⟨α⟩M να^{A}.M

with typing rules:

(ang) \frac{Γ ⊢ M : A ∨ B | Δ}{Γ ⊢ ⟨α⟩M : B | Δ} if α:A ∈ Δ, (ν) \frac{Γ ⊢ M : B | α:A, Δ}{Γ ⊢ να^{A}.M : A ∨ B | Δ} .

Like μ-abstractions and named terms, these two additional term constructors manipulate continuations. One can think of a term M of type A ∨ B as a term of type B which has access to an unnamed continuation of type A. The term ⟨α⟩M gives this unnamed continuation the name α. Dually, the term να^{A}.M abstracts a continuation of name α in M. The resulting calculus is known as the λμν-calculus. Its equational theory is obtained from that of the λμ-calculus by adding the following three axioms:

(ζ_{∨}) [β]⟨α⟩μγ^{A∨B}.M = M[[β]⟨α⟩^{(−)}/[γ]^{(−)}] : ⊥
(β_{∨}) ⟨α′⟩να^{A}.M  = M[α′/α] : ⊥
(η_{∨}) να^{A}.⟨α⟩M  = M : A ∨ B  if α ∉ FN(M)

We also need to extend the definition of a mixed substitution M[C^{(−)}/[α]^{(−)}] to replace any subterm of the form ⟨α⟩^{(−)} by μβ^{B}.C(μα^{A}.[β]⟨α⟩^{(−)}), where β is a fresh name.

3.2 Classical and intuitionistic disjunction

In the lambda calculus, one usually defines a “disjoint sum type” A + B via the “inl”, “inr”, and “case” constructs. Pym and Ritter remark that in the call-by-name case, the disjunction type A ∨ B, as defined in the previous section, does not coincide with the disjoint sum type A + B. To distinguish them, we sometimes refer to A ∨ B as “classical” disjunction and to A + B as “intuitionistic” disjunction.

An interesting fact is that intuitionistic disjunction can be defined in terms of classical disjunction. Namely, we can define

A + B  := ¬¬A ∨ ¬¬B
inl M  := να.μβ.[α]λk.kM
inr M  := να.μβ.[β]λk.kM
case M of inl x → N | inr y → P := μγ.(μα.(⟨α⟩M)(λy.[γ]P))(λx.[γ]N)

Here, ¬A is an abbreviation for the function type A → ⊥. With these definitions, the usual equational call-by-name laws for “inl”, “inr”, and “case” are derivable from those of the λμν-calculus. On the other hand, the classical disjunction A∨B is not definable in terms of the intuitionistic disjunction type. Thus, classical disjunction should be throught of as a very primitive operation, a low-level building block from which more high-level constructs can be built.

To further illustrate the difference between the two disjunctions, we remark that classical disjunction satisfies certain type isomorphisms such as associativity (A∨B)∨ C ≅ A ∨ (B ∨ C) and domination A ∨ ⊤ ≅ ⊤. The corresponding isomorphisms do not hold for intuitionistic disjunction. For a more in-depth discussion of type isomorphisms, see e.g. [10].

3.3 Alternative syntax

A different, more symmetric syntax for the classical disjunction type was used in [10]. Readers who are familiar with [10] may appreciate knowing that the two notations are interdefinable as follows:

\begin{aligned}να^{A}.M & = & μ(α^{A}, β^{B}).[β]M \\ ⟨α⟩M & = & μβ^{B}.[α, β]M \end{aligned}  and  \begin{aligned}μ(α^{A}, β^{B}).M & = & να^{A}.μβ^{B}.M \\ [α, β]M & = & [β]⟨α⟩M. \end{aligned}

3.4 CPS semantics and abstract machine interpretation

The CPS translation of Section 2.3 easily extends to classical disjunction: We define

K_{A∨B} = K_{A} × K_{B},
\underline{⟨α⟩M} = λk^{K_{B}}.\underline{M}⟨α̃, k⟩ where M : A ∨ B,
\underline{να^{A}.M} = λ⟨α̃, k⟩^{K_{A∨B}}.\underline{M}k where M : B.

To derive an abstract machine model from this CPS semantics, observe that the disjunction introduces a new kind of continuation of the form ⟨k′, k⟩. In the context of abstract machines, we write this continuation as k′::k, and we interpret it as a stack whose topmost element is (a pointer to) a stack closure. The corresponding abstract machine transitions are derived directly from the CPS semantics:

CPS  Abstract Machine
\underline{⟨α⟩M}k  → \underline{M}⟨α̃, k⟩  \{⟨α⟩M, σ, k\} → \{M, σ, k′::k\}, where σ(α) = k′.
\underline{να.M}⟨k′, k⟩ → \underline{M}[k′/α̃]k  \{να.M, σ, k′::k\} → \{M, σ(α ↦ k′), k\}

Thus, we see that the connectives of classical disjunction correspond to the ability to push and pop stack closures to/from the current stack. We also introduce a new halting state, which applies in case a ν-abstraction encounters an empty stack:

{να.M, σ, nil} → halt “disjunction”.

An alternative way to think of the classical disjunction type is as a kind of function type, where the argument is a continuation variable instead of a term. Thus, a term of type A ∨ B can be thought of as a kind of function which accepts a continuation variable of type A and turns into a term of type B. Note the perfect analogy between the following pairs of reduction rules of Krivine’s abstract machine:

{MN, σ, k}  → {M, σ, N^{σ}::k},  where M : A → B,
{⟨α⟩M, σ, k}  → {M, σ, k′::k},  where M : A ∨ B, and
{λx.M, σ, N^{τ}::k} → {M, σ(x ↦ N^{τ}), k}, where λx.M : A → B,
{να.M, σ, k′::k} → {M, σ(α ↦ k′), k}, where να.M : A ∨ B.

This helps explain why, in call-by-name, there is a type isomorphism between A → (B ∨ C) and B ∨ (A → C). A term of either type can be regarded as expecting an argument of type A and a continuation of type B; the only difference is the order in which these two items are expected.

4 Adding basic types and operations

We now consider how the addition of built-in datatypes, such as integers or booleans, affects the CPS semantics and Krivine’s abstract machine. Basic types complicate the semantics somewhat, because they lead away from a “pure” call-by-name discipline. This is because primitive operations on basic types, for instance addition or multiplication, must necessarily evaluate their arguments before operating on them. Thus, even in a call-by-name language, basic operations are necessarily call-by-value.

It is therefore necessary to extend Krivine’s machine with a call-by-value evaluation mechanism at basic types. It is interesting that the rules for the abstract machine can again be derived systematically from the corresponding CPS semantics.

4.1 CPS semantics

In call-by-name languages, built-in basic types, such as integers or booleans, differ from other types, because they are equipped with a natural notion of value. These values are never stored in variables, but they are computed just before a built-in operation is applied. For simplicity, we assume for the moment that all built-in functions, such as addition or logical “and”, are strict, i.e., they evaluate all their arguments before they operate on them. Thus we do not at first consider “lazy” basic operations such as lazy multiplication, which evaluates its second argument only if the first argument is non-zero. We will get back to the question of lazy functions in Section 4.3.

We consider the λμν-calculus over a given algebraic signature, i.e., over a set of basic types σ, τ, … and a set of typed constant symbols c : σ and of typed function symbols f : τ_{1} → … → τ_{n} → σ. As usual, n is called the arity of the function symbol f. For the CPS semantics, we consider the same target calculus as before. Moreover, we assume that each basic type σ of the λμν-calculus is interpreted by a chosen type V_{σ} of the target calculus, together with chosen interpretations c̃ : V_{σ}, respectively f̃ : V_{τ_{1}} → … → V_{τ_{n}} → V_{σ}, of the primitive constants and functions. The type V_{σ} is called the type of values of type σ. We refine the CPS semantics from Sections 2.3 and 3.4 by letting K_{σ} = V_{σ} → R, when σ is a basic type. Thus, continuation and computation types are defined as before:

K_{σ}  = V_{σ} → R,  if σ is a basic type,
K_{⊤}  = 0,
K_{A∧B} = K_{A} + K_{B},
K_{A→B} = C_{A} × K_{B},
K_{⊥}  = 1,
K_{A∨B} = K_{A} × K_{B},
C_{A}  = K_{A} → R.

Notice that a value type V_{A} is only defined when A is a basic type, and not when A is an arbitrary type. We extend the CPS translation of Table 3 with the following interpretation of primitive constants c : σ and functions f : τ_{1} → … → τ_{n} → σ:

\underline{c} = λk.kc̃,  (1)
\underline{f} = λ⟨x_{1}, …, x_{n}, k⟩.x_{1}(λv_{1}.x_{2}(λv_{2}…. x_{n}(λv_{n}.k(f̃v_{1} … v_{n})))). (2)

Here k : K_{σ}, x_{i} : C_{τ_{i}}, and v_{i} : V_{τ_{i}}. Notice that the interpretation of a constant symbol c is actually a special case of the interpretation of an n-ary function symbol f, namely the case when n = 0. The reader should check that this CPS translation does indeed have the required behavior. In particular, the term fN_{1} … N_{n} is evaluated by first evaluating all arguments from left to right, and then applying f̃ to the result.

4.2 Abstract machine interpretation

We extend the abstract machine interpretation to accommodate basic types and functions. As usual, we start by examining the kinds of continuations introduced by the new language feature. The CPS translation of primitive functions, shown in equation (2), introduces a new kind of continuation which is a function. We need to fit this into the “continuations as stacks” paradigm of Section 2.4. Fortunately, a careful examination of the CPS semantics reveals that, all the continuation functions which occur during the β-reduction of the CPS translation of a term are of one particular form:

λv_{j}.N_{j+1}(λv_{j+1}…. N_{n}(λv_{n}.k(f̃c_{1} … c_{j−1}v_{j}v_{j+1} … v_{n}))),  (3)

where 1 ≤ j ≤ n. In the abstract machine, each term N_{i} is represented by a closure N_{i}^{σ_{i}}, and we will represent a continuation of the form (3) by the formal expression

[f c_{1} … c_{j−1} • N_{j+1}^{σ_{j+1}} … N_{n}^{σ_{n}}]::k.

The expression [f c_{1} … c_{j−1} • N_{j+1}^{σ_{j+1}} … N_{n}^{σ_{n}}] is called a frame, and it is typically implemented as a fixed-size array of data on top of the current stack (i.e., whose size depends only on the symbol f). This is analogous to the notion of a stack frame in imperative programming languages, i.e., a data structure on the stack, containing variables belonging to a particular scope or procedure. The symbol “•” is a special place holder which corresponds to a memory location which previously contained the closure N_{j}^{σ_{j}}, and where the value c_{j} is going to be stored next.

Before giving the transition rules of the extended abstract machine, we need to introduce one more new feature, and that is the notion of a value state. Recall that a state \{M, σ, k\} of Krivine’s abstract machine corresponds to a term of the form \underline{M}k under CPS. Because of the presence of values in the CPS semantics, there is now a new kind of state which is of the form kc, where k is a continuation of a basic type A, and c is a value of type A, i.e., an element of V_{A}. We call a state of the form kc a value state, and we denote it in the abstract machine as a pair {c, k}^{v}. Note that, unlike an ordinary state of the form {M, σ, k}, a value state {c, k}^{v} does not require an environment.

The CPS semantics of primitive constants and functions, as embodied in equations (1) and (2), has the following transitions, where j < n and d = f̃c_{1} … c_{n−1}c:

\begin{aligned}\underline{c}k & → & kc̃ \\ \underline{f}⟨N_{1}, ..., N_{n}, k⟩ & → & N_{1}(λv_{1}....N_{n}(λv_{n}.k(f̃v_{1}...v_{n}))) \\ (λv_{j}.N_{j+1}(...(λv_{n}.k(f̃c_{1}...c_{j−1}v_{j}...v_{n}))))c & → & N_{j+1}(...(λv_{n}.k(f̃c_{1}...c_{j−1}cv_{j+1}...v_{n}))) \\ (λv_{n}.k(f̃c_{1}...c_{n−1}v_{n}))c & → & kd, \end{aligned}

These can now be immediately translated to transition rules of the abstract machine:

\begin{aligned}\{c, σ, k\} & → & \{c, k\}^{v} \\ \{f, σ, N_{1}^{σ_{1}}::...::N_{n}^{σ_{n}}::k\} & → & \{N_{1}, σ_{1}, [f • N_{2}^{σ_{2}}...N_{n}^{σ_{n}}]::k\} \\ \{c, [f c_{1}...c_{j−1} • N_{j+1}^{σ_{j+1}}...N_{n}^{σ_{n}}]::k\}^{v} & → & \{N_{j+1}, σ_{j+1}, [f c_{1}...c_{j−1}c • N_{j+2}^{σ_{j+2}}...N_{n}^{σ_{n}}]::k\} \\ \{c, [f c_{1}...c_{n−1} •]::k\}^{v} & → & \{d, k\}^{v}. \end{aligned}

In these rules, it is again assumed that f is an n-ary function symbol, that j < n, and that d = f̃c_{1} … c_{n−1}c. We also introcuce two new halting states: a value state with empty stack is a halting state with result c, and an n-ary built-in function f will halt with value “function” if the stack contains fewer than the required n arguments.

{c, nil}^{v} → halt c,
{f, σ, k} → halt “function”, if size(k) < n.

4.3 “Impure” functions

So far, we have only considered primitive functions of the form f : τ_{1} → … → τ_{n} → σ, where all of τ_{1}, …, τ_{n} and σ are basic types. Sometimes, it is useful to allow primitive functions with arbitrary result type, i.e., of the form f : τ_{1} → … → τ_{n} → A, where A is any type. We refer to these more general basic functions as “impure”.

One example of an impure basic function is the if-then-else function if_{B} : bool → (B → B → B) which maps true to λxy.x and false to λxy.y. Here, bool is a builtin type of booleans, and B is any type. Another example is the “lazy multiplication” function lazymult : int → (int → int), where int is the type of integers. By definition, the function lazymultmaps 0 to the constant function λx.0, and any other integer n to λx.mult n x, where mult is the usual strict multipliction operation. We can regard both ifand lazymultas impure, strict basic functions in one argument.

Another useful example of an impure function is the side-effecting print function. In call-by-name, one can model sequential composition N; M by application NM, where N is a term that performs some effects and then returns λx.x. As an application of this idea, we can consider a family of basic functions print_{B} : int → (B → B). The intended meaning is that (print n); M prints the integer n and then behaves like M.

4.4 Semantics of impure functions

The CPS semantics of impure basic functions is straightforward. For each impure basic function symbol f : τ_{1} → … → τ_{n} → A, we need a chosen term f̃: V_{τ_{1}} → … → V_{τ_{n}} → C_{A} of the target language of the CPS translation. The term f is then translated as follows:

\underline{f} = λ⟨x_{1}, …, x_{n}, k⟩.x_{1}(λv_{1}.x_{2}(λv_{2}…. x_{n}(λv_{n}.(f̃v_{1} … v_{n})k))). (4)

Here, k : K_{A}, x_{i} : C_{τ_{i}}, and v_{i} : V_{τ_{i}}. Note that the only difference between equations (2) and (4) is the order of the terms f̃v_{1} … v_{n} and k. For impure functions, the term f̃v_{1} … v_{n} is of type C_{A}, whereas for pure functions, it is of type V_{A}. It follows that the interpretation of an impure function does not coincide with that of a pure function, even in the case where A happens to be a basic type: the interpretation of a pure function always produces a value, whereas the interpretation of an impure function potentially produces an arbitrary computation.

In concrete cases, we rely on the target language of the CPS transform to supply us with “native” implementations of the required functionality. To interpret the basic function if : bool → (B → B → B), we assume that V_{bool} is the type of booleans of the target language, and we define the function ĩf : V_{bool} → C_{B→B→B} such that ĩftrue = \underline{λxy.x} and ĩffalse = \underline{λxy.y}. The interpretation of lazymultis similar.

The easiest way to interpret the side-effecting print function (although there are better ways) is to assume that the target language of the CPS transform also allows side effects. In this case, we need a primitive function p̃rint : V_{int} → C_{B→B} of the target language, such that p̃rint n has the behavior of printing n and then returning \underline{λx.x}.

For the abstract machine interpretation, we will overload the frame notation by writing [f c_{1} … c_{j−1} • N_{j+1}^{σ_{j+1}} … N_{n}^{σ_{n}}]::k for the expression

λv_{j}.N_{j+1}(λv_{j+1}…. N_{n}(λv_{n}.(f̃c_{1} … c_{j−1}v_{j}v_{j+1} … v_{n})k)),

in the case where f is an impure basic function. Note that this is not quite the same as equation (3). From the CPS semantics of the impure basic functions if and print, we have

(λv.(ĩfv)k)true  → \underline{λxy.x}k
(λv.(ĩfv)k)false → \underline{λxy.y}k
(λv.(p̃rint v)k)c ⟶^{outputc} \underline{λx.x}k.

Here the label “outputc” denotes a side effect taking place as part of the reduction. This immediately gives rise to the corresponding abstract machine rules:

{true, [if•]::k}  → {λx.λy.x, ∅, k}
{false, [if•]::k} → {λx.λy.y, ∅, k}
{c, [print •]::k} ⟶^{outputc} {λx.x, ∅, k}

5 Implementing the abstract machine

In this section, we give an implementation of Krivine’s abstract machine, and its various extensions, in an idealized, low-level assembly language. This illustrates that, despite its name, the abstract machine is not as “abstract” as one might think; it can be implemented, with relatively little effort, on a standard von Neumann style “concrete” machine. Note that the implementation takes the form of a compiler, and not of an interpreter; thus, the final program does not run by updating a data structure, but by executing actual code.

As already pointed out in the introduction, the implementation given here is not efficient enough to be useful in practice. Its main flaw is that it uses a naive call-by-name evaluation strategy, in which each subterm is possibly evaluated many times. This is the same evaluation strategy which is embodied in Krivine’s abstract machine, and since our goal is to follow the abstract machine model as faithfully as possible, we resist the temptation to optimize. It can be argued that any substantial improvement to the implementation is best carried out at the abstract machine level, or even at the level of CPS translations, rather than at the compiler level.

We also take the liberty to ignore certain practical aspects of implementations, such as garbage collection and efficient register allocation. In our “ideal” implementation, we simply assume that there are infinitely many registers and an infinite amount of memory available.

5.1 Target assembly language

The target language of our compiler is an idealized assembly language whose instruction set shown in Table 5. It differs from actual assembly languages in several respects. First, we assume that there are infinitely many registers. Second, we assume that there are built-in instructions for certain high-level operations such as memory allocation (alloc ) and the manipulation of stack closures (save , restore ); these would not normally be available as separate instructions, but would be implemented as macros or system calls.

The only data type of the assembly language is a word, which can be interpreted as an integer, a boolean (with 0 = false, 1 = true), or as a pointer. We assume that

Instruction Meaning
move w, v Store the value v in location w
add w, v  Add v to w
push v  Push the value v onto the stack
pop w  Pop a value from the stack and store it in w
cmp v_{1}, v_{2} Compare the two values, and remember the result
bne v  If previous cmp resulted in not equal, jump to location v
bge v  If previous cmp resulted in greater than or equal jump to location v
jump v  Jump to address v
call v  Call subroutine at address v
alloc w, v Allocate v words of memory and store a pointer to them in w
save w  Make a stack closure from the current stack, and store a pointer to it in w
restore v Replace the current stack by a copy of the stack closure pointed to by v
exit v  Exit with result v

Table 5: Instruction set of the idealized assembly language

there are infinitely many registers R_{1}, R_{2}, …, as well as four distinguished registers SP, SS, C, and V, each of which can hold a word.

We assume that there are infinitely many addressable memory cells, each of which holds a word. A memory reference takes the form [R, n], where R is a register and n is a literal integer. The expression [R, n] refers to the contents of the memory cell at address R+n. An ℓ-value (assignable value) is either a register or a memory reference. A value is either an ℓ-value or a literal integer. Literal integers are often written as #n in assembly language instructions.

The memory is divided into two separate regions: the stack and the heap. The stack is manipulated in the usual way via the push and pop instructions, and also via the two special registers SP and SS, which represent the stack pointer and the stack size, respectively. We assume that the stack grows downward (towards lower memory addresses), and that the stack pointer SP points to the memory cell just below the stack, so that [SP, 1] refers to the topmost element on the stack. Setting the register SS to 0 has the effect of emptying the stack.

The instruction set of the assembly language is shown in Table 5. Here, the letter w ranges over ℓ-values and the letter v ranges over values. The meaning of most instructions should be clear. Note that there is only one move instruction, which can be used, among other things, to copy a value from memory to a register or vice versa. The push and pop instructions implicitly update the registers SP and SS. Some high-level operations are included for convenience: alloc is used to allocate memory from the heap. save and restore are used to manipulate stack closures and will be explained in more detail later, and the exit instruction ends the computation and returns a result which is a word; it is up to the environment to interpret this word correctly as an integer, a boolean, or a pointer to a literal string, depending on the type of the program being run.

When writing assembly language code, each instruction can be preceded by an optional label, which provides a symbolic reference to the address of the instruction. We use a semicolon “;” to introduce a comment.

5.2 Data representation

We need to specify how the various kinds of data of Krivine’s abstract machine are represented in memory. Specifically, we need to fix a representation for term closures, stack closures, and for items on the stack. Terms themselves are represented as code, and will be discussed in Section 5.3.

Term closures and stack closures are allocated on the heap. A term closure N^{σ} is represented as n + 1 consecutive words a_{0}, …, a_{n} in memory. Here a_{0} is a pointer to the code for the term N, and a_{1}, …, a_{n} are pointers to representations of the closures σ(x_{1}), …, σ(x_{n}), where x_{1}, …, x_{n} are the free variables and names of N.

A stack closure is represented by a record of n + 1 words, of which the first one holds the number n, and the remaining ones hold the actual stack data. For convenience, we provide a save w instruction, which makes a heap-allocated closure from the current stack and returns a pointer to it in w. We also provide a restore v instruction, which erases the current stack and replaces it by a copy of the stack closure pointed to by v.

The stack of the abstract machine is of course implemented as the native stack of the assembly language. Most individual items on the stack are represented as single words, except for frames, which are represented as records of several words. The tags tag_{1} and tag_{2} are represented as the integers 1 and 2, respectively. Term closures and stack closures are represented as pointers to the respective objects on the heap. The representation of nil is, of course, the empty stack. A frame [f c_{1} … c_{j−1} • N_{j+1}^{σ_{j+1}} … N_{n}^{σ_{n}}] is represented as a sequence of n + 1 words f_{j}, c_{1}, …, c_{j−1}, b, p_{j+1}, …, p_{n}. Here, f_{j} is a special tag which uniquely determines f and j (actually, we will implement f_{j} as a pointer to code). c_{1}, …, c_{j−1} are literal values, b is an undefined word (occupying the position of the “•” in the frame), and p_{j+1}, …, p_{n} are pointers to representations of the closures N_{j+1}^{σ_{j+1}}, …, N_{n}^{σ_{n}}.

5.3 Compilation of terms

Terms are not represented as data structures, but rather as code to be executed. Since a term needs to be able to access the values of its free variables, it is executed in the context of a particular closure, the current closure of the term. By convention, we assume that there is a special register C which always contains a pointer to the current closure. Thus, the calling convention for invoking a specific closure is to store a pointer to it in the register C, then jump to the address [C, 0].

When the abstract machine is in a value state, the current value needs to be stored somewhere; by convention, we store it in the special register V. (As a matter of fact, the registers C and V are never used simultaneously, so it would be possible to use just one register for both purposes. However, doing so would add no conceptual clarity). The representation of stack frames was arranged in such a way that, when the machine reaches a value state, the topmost item on the stack is a tag f_{j}. We interpret this as an Lambda calculus

[[x]]_{s} =

move C, s(x) jump [C, 0]

[[λx.M]]_{s} =

cmp SS, #0 bne l

exit  “function”

l : pop R [[M]]_{s(x↦R)}

(where l is a fresh label and R is a fresh register.)

[[MN]]_{s} =

; build closure for N alloc R, #(n + 1) move [R, 0], #l move [R, 1], s(x_{1}) … move [R, n], s(x_{n}) push R [[M]]_{s}

l : [[N]]_{(x_{1}↦[C,1],...,x_{n}↦[C,n])}

(where l is a fresh label, R is a fresh register, and FV(N) ∪ FN(N) = {x_{1}, …, x_{n}}.)

[[⟨M, N⟩]]_{s} =

cmp SS, #0 bne l_{1}

exit  “pair”

l_{1} : pop R cmp R, #1 bne l_{2} [[M]]_{s}

l_{2} : [[N]]_{s}

(where l_{1}, l_{2} are fresh labels, and R is a fresh register.)

[[π_{i}M]]_{s} =

push #i

[[M]]_{s}

[[∗]]_{s} =
exit  “unit”

\underline{λμ-Calculus}
[[μα.M]]_{s} =

; build a stack closure save R ; clear the stack move SP, #0 [[M]]_{s(α↦R)}

(where R is a fresh register.)

[[[α]M]]_{s} =

restore s(α)
[[M]]_{s}

Classical disjunction (λμν-calculus)

[[να.M]]_{s} =

cmp SS, #0
bne l
exit  “disjunction”

l : pop R

[[M]]_{s(α↦R)}

(where l is a fresh label and R is a fresh register.)

[[⟨α⟩M]]_{s} =

push s(α)
[[M]]_{s}

Table 6: The compilation of terms Basic constants

[[n]]_{s} =

move V, #n cmp SS, #0 bne l exit V

l : pop R jump R

(where l is a fresh label and R is a fresh register.)

[[true]]_{s} = [[1]]_{s}

[[false]]_{s} = [[0]]_{s}

“Pure” basic functions

[[f]]_{s} =

; check for sufficient arguments cmp SS, #n bge f_{0}

exit  “function”

f_{0} : move C, [SP, 1] push #f_{1} jump [C, 0]

(repeat following code for j = 1 … n − 1) f_{j} : move [SP, j], V

move C, [SP, j + 1] push #f_{j+1} jump [C, 0]

f_{n} : move [SP, n], V ; n values are now on top of stack

call  native_{f}

pop V cmp SS, #0 bne l exit V

f_{n+1} : pop R jump R

(where n ≥ 1 is the arity of f, f_{0},…,f_{n+1} are fresh labels, and R is a fresh register.)

Some “impure” basic functions

[[if]]_{s} =

cmp SS, #1
bge  if_{0}
exit  “function”

if_{0} : pop C

push #if_{1}
jump [C, 0]

if_{1} : cmp V, #0

bne  if_{2}
[[λxy.y]]_{∅}

if_{2} : [[λxy.x]]_{∅}

(where if_{0},…,if_{n+1} are fresh labels.)

[[print]]_{s} =

cmp SS, #1

bge  print_{0}
exit  “function”

print_{0} : pop C push #print_{1} jump [C, 0]

print_{1} : push V

call  native_{print}

[[λx.x]]_{∅} (where print_{0}, print_{1} are fresh labels.)

Table 7: The compilation of terms, continued address to jump to. Thus, the convention in a value state is to put the value into the register V, then pop the topmost address from the stack and jump to it. If a value state encounters an empty stack, then the program halts and the current value is the result of the computation.

A compiled term must know where to find the values of its free variables, either as offsets within the current closure, or in registers or elsewhere in memory. Therefore, the translation of a term M is defined relative to a symbol table s, which is a function from the free variables of M to symbolic values. For example, the symbol table might specify that the value of the free variables x, y, and z can be found in [C, 1], [C, 2], and in the register R_{4}, respectively. Note that a symbol table s is a compile-time concept and maps variables to symbolic values, unlike an environment σ, which is a run-time concept and maps variables to actual values. We write s(x ↦ v) for the symbol table obtained from s by adding a mapping of the variable x to the symbolic value v.

We use the notation [[M]]_{s} to denote the assembly code for the term M under the symbol table s. The rules of translation are derived directly from the corresponding rules of the abstract machine, and they are shown in Tables 6 and 7. Note that the translation proceeds by recursion on the structure of terms. Also note that the translation [[M]]_{s} of a term is always a piece of assembly code which ultimately ends in a jump or exit instruction.

5.4 The translation of individual terms

The code for a variable x simply invokes the closure that x points to. According to our calling convention for closures, this is done by loading a pointer to the closure into the register C, then jumping to the address [C, 0].

The code for a lambda abstraction λx.M simply pops a value from the stack and binds it to the variable x; thereafter, it behaves like M. Three additional lines of code are needed to test whether the stack is empty, in which case the program halts.

The code for an application MN builds a term closure for N; this is done by allocating n + 1 words of memory, and storing in them the address of the code for N, as well as the values of the free variables x_{1}, …, x_{n} of N. A pointer to the term closure is then pushed onto the stack before M is executed. Note that the code for the term N is given separately, and is generated relative to a new symbol table where the variables x_{1}, …, x_{n} are mapped to the respective offsets into the “current” closure (i.e., the closure which will be current when N is invoked).

The translations of pairs, projections, and unit are straightforward and follow directly from the corresponding rules of the abstract machine. The code for a pair pops a tag from the stack, whereas the code for a projection pushes a tag onto the stack.

The code for a μ-abstraction μα.M saves the current stack into a new stack closure, and then executes M in the context of an empty stack, and with the name α bound to the stack closure just created.

The code for [α]M replaces the current stack by the stack closure pointed to by α. The code for a ν-abstraction pops a pointer to a stack closure from the stack and

binds it to the variable α. Note that this code is almost identical to that of a λabstraction, except that, in case of an empty stack, the result of the program is “disjunction” instead of “function”.

The code for ⟨α⟩M pushes a pointer to a stack closure onto the stack.

The code for basic integer and boolean constants, which is shown in Table 7, reflects our convention for value states. Namely, the convention specifies to put the value into the special register V, then jump to the address on top of the stack, if any. If the stack is empty, V is returned as the result of the program.

The code for a “pure” basic function is interesting. We first check whether there are enough closures on the stack to form a frame. Note that the data representation of a frame was chosen in such a way that the rule

{f, σ, N_{1}^{σ_{1}}:: …::N_{n}^{σ_{n}}::k} → {N_{1}, σ_{1}, [f • N_{2}^{σ_{2}} … N_{n}^{σ_{n}}]::k}

does not require any rearrangment of the n closures; the first frame is simply built by pushing the address f_{1} onto the stack. The first closure N_{1}^{σ_{1}}, a pointer to which is stored in the stack frame, is then invoked. Eventually, this closure reaches a value state, and following the convention for value states, it will jump to the address on top of the stack, in this case f_{1}, with V being the value just computed. This value is stored in the current frame, and then the remaining closures N_{2}^{σ_{2}}, …, N_{n}^{σ_{n}} are evaluated in the same way, until the top n items on the stack contain the actual arguments to the function f. At this point, we call a subroutine which contains some native implementation of the function f. The convention is that this native implementation expects its n arguments on top of the stack, and returns its result on top of the stack as well. After the subroutine call returns, we simply pop the result value off the stack and follow the protocol for value states.

Finally, Table 7 shows the implementation of two “impure” basic functions, the “if” and “print” functions which were already discussed in Section 4.3. Both these functions use a simplified form of the mechanism for pure basic functions (specialized for unary functions) to evaluate the closure on top of the stack and to obtain a value V. The “if” function then simply executes λxy.x or λxy.y, depending whether V = true or V = false. The “print” function calls a subroutine to print the value V, then executes λx.x.

References

[1] W. D. Clinger, A. H. Hartheimer, and E. M. Ost. Implementation strategies for first-class continuations. Higher-Order and Symbolic Computation, 12:7–45, 1999.

[2] G. Cousineau. The categorical abstract machine. In G. Huet, editor, Logical Foundations of Functional Programming, pages 25–45. Addison-Wesley, 1990.

[3] M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103:235–271, 1992.

[4] T. G. Griffin. A formulae-as-types notion of control. In POPL ’90: Proceedings of the 17th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1990.

[5] M. Hofmann and T. Streicher. Continuation models are universal for λμ-calculus. In Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 387–397, 1997.

[6] J.-L. Krivine. Un interpreteur du lambda-calcul. Draft, available from ftp://ftp.logique.jussieu.fr/pub/distrib/krivine/interprt.pdf.

[7] M. Parigot. λμ-calculus: An algorithmic interpretation of classical natural deduction. In Proceedings of the International Conference on Logic Programming and Automated Reasoning, St. Petersburg, Springer LNCS 624, pages 190–201, 1992.

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

[9] D. Pym and E. Ritter. On the semantics of classical disjunction. Preprint, 1998.

[10] P. Selinger. Control categories and duality: on the categorical semantics of the lambda-mu calculus. Math. Struct. in Computer Science, 11(2), 2001.

[11] T. Streicher and B. Reus. Classical logic, continuation semantics and abstract machines. Journal of Functional Programming, 8(6):543–572, Nov. 1998.

[12] D. H. D. Warren. An abstract prolog instruction set. Technical Note 309, SRI International, 1983.