An Implementation of the Call-By-Name λμν-Calculus

Peter Selinger^{∗} Department of Mathematics University of Michigan Ann Arbor, MI 48109-1109

Abstract

We describe an experimental, low-level implementation of the λμν-calculus. The implementation is based on a Krivine-style abstract machine, which is in turns derived from a simple CPS semantics.

Parigot’s λμ-calculus was originally invented as a proof-term calculus for classical logic [2]. One can also regard it as a prototypical call-by-name programming language with control primitives. However, its operational significance is not very well understood, particularly because it does not have a very satisfactory rewrite semantics. The λμν-calculus was proposed by Pym and Ritter as an extension of the λμ-calculus with disjunction types [4], again motivated by proof theory.

Here, we hope to clarify the operational meaning of these calculi by giving a Krivine-style abstract machine semantics and an implementation. The meaning of the control operators and of the disjunction types can be explained in the machine model in terms of certain operations on stacks. Our abstract machine semantics is derived from a CPS semantics in the style of Hofmann and Streicher [1]. In [6], we have shown that this CPS semantics is in turns closely related, via a completeness theorem, to the category-theoretical models of the disjunctive λμν-calculus.

We also describe a low-level implementation of the abstract machine. It translates λμν-terms directly into a subset of the C language. The implementation, which is written in ML, is available from [5].

1 Syntax

1.1 The syntax of the λμ-calculus

The λμ-calculus is an extension of the simply-typed lambda calculus with certain control operators. In addition to the usual constructs of the simply-typed lambda calculus, there are two new term constructors: the term μα.M statically binds the current continuation to the name α before evaluating M. The term [α]M applies the continuation α to the term M. Thus, as a first approximation, one can think of μα.M as callcc(λα.M) in Standard ML of New Jersey or Scheme, and of [α]M as throw α M. However, there are some differences. First, the λμ-calculus is call-by-name, whereas ML and Scheme are call-by-value. The second difference lies in the typing: the λμ-calculus knows an “empty type” ⊥, which is the type of an expression such as [α]M which never returns. In ML, such an expression has an arbitrary type. Dually, in μα.M, we require M to be of type ⊥. The third difference is that the λμ-calculus has two separate name spaces: variables x, y, … bind terms, whereas names α, β, … bind continuations. This distinction, while operationally insignificant, is sometimes technically convenient — for instance, it simplifies the statement of duality in [6]. By convention, we say that an A-accepting continuation α has type A, and not type A cont as in ML.

Formally, the λμ-calculus is defined as follows. Types, ranged over by A, B, …, are built from a set B of basic types by the grammar:

A ::= B 1 A ∧ B A → B ⊥

Let V and N be two given, disjoint, infinite sets of variables x, y, … and names α, β, …, respectively. Sometimes the former are called object variables and the latter control variables. Let K be a set of typed constants c^{A}, d^{B}, . . ..

∗This research was done while the author was visiting BRICS, Basic Research in Computer Science, Centre of the Danish National Research Foundation.

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

(var)  \overline{Γ, x:A ⊢ x : A | Δ}
(const)  \overline{Γ ⊢ c^{A} : A | Δ}
(∗)  \overline{Γ ⊢ ∗ : 1 | Δ}
(pair) \frac{Γ ⊢ M : A | Δ  Γ ⊢ N : B | Δ}{Γ ⊢ ⟨M, N⟩ : A ∧ B | Δ}
(π_{1})  \frac{Γ ⊢ M : A ∧ B | Δ}{Γ ⊢ π_{1}M : A | Δ}
(π_{2})  \frac{Γ ⊢ M : A ∧ B | Δ}{Γ ⊢ π_{2}M : B | Δ}

(app) \frac{Γ ⊢ M : A → B | Δ  Γ ⊢ N : A | Δ}{Γ ⊢ MN : B | Δ}
(abs)  \frac{Γ, x:A ⊢ M : B | Δ}{Γ ⊢ λx^{A}.M : A → B | Δ}
(pass)  \frac{Γ ⊢ M : A | α:A, Δ}{Γ ⊢ [α]M : ⊥ | α:A, Δ}
(μ)  \frac{Γ ⊢ M : ⊥ | α:A, Δ}{Γ ⊢ μα^{A}.M : A | Δ}
(weaken) \frac{Γ ⊢ M : A | Δ  Γ ⊆ Γ′  Δ ⊆ Δ′}{Γ′ ⊢ M : A | Δ′}

The pair (B, K) is called a signature of the λμ-calculus, and sometimes denoted by Σ. Raw terms M, N, … are given by the grammar:

M ::= x c^{A} ∗ ⟨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 passification term. In the terms λx^{A}.M and μα^{A}.M, the variable x, respectively the name α, is bound. As usual, we identify raw terms up to renaming of bound variables and names.

The typing of the λμ-calculus is defined as follows. An object context Γ = x_{1}:B_{1}, x_{2}:B_{2}, …, x_{n}:B_{n} is a finite, possibly empty sequence of pairs of an object variable and a type, such that x_{i} ≠ x_{j} for all i ≠ j. We write Γ ⊆ Γ′ if Γ is contained in Γ′ as a set. A control context Δ = α_{1}:A_{1}, α_{2}:A_{2}, …, α_{m}:A_{m} is defined analogously. A typing judgment is an expression of the form Γ ⊢ M : A | Δ. The context Γ declares the types of the free variables, and Δ declares the types of the free names of M. If there are n variables in Γ and m names in Δ, then one can think of M as a function in n arguments which has m + 1 possible result channels. Valid typing judgments are derived by the rules in Table 1.

The reason that we write the control context on the right comes from logic: A sequent

x_{1}:B_{1}, …, x_{n}:B_{n} ⊢ M : A | α_{1}:A_{1}, …, α_{m}:A_{m}

corresponds to a proof of the formula

B_{1} ∧ … ∧ B_{n} ⇒ A ∨ A_{1} ∨ … ∨ A_{m}.

1.2 Adding classical disjunction: The λμν-calculus

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

\begin{aligned}A & ::= & … A ∨ B \\ M & ::= & … ⟨α⟩M να^{A}.M \end{aligned}

with typing rules:

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

For technical reasons, these typing rules are the mirror images of those of Pym and Ritter [4]. Like μ-abstraction and passification, 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. One way to use these constructs is to circumvent a problem that comes from static scoping: a function can never catch a term that one of its arguments throws. Consider the following term of the λμ-calculus:

(λx^{B}.M(x))(N([α]P))

Here, the α of the argument does not lie within the scope of any μ-abstractions that appear in M. Thus, M cannot “catch” (provide a continuation for) the term P that is thrown on α. For this reason, the control operators of the λμ-calculus, like callcc, are not suitable to model exception handling. On the other hand, in the λμν-calculus, one can abstract from α as follows:

(λx^{A∨B}.M(⟨α⟩x))(να′^{A}.N([α′]P))

Now it is possible for M to “catch”, on the name α, the term P that is thrown by its argument x on the name α′. This usage of the disjunction type A ∨ B is reminiscent of the way in which throws-clauses provide type-safe exception handling in Java. The operational meaning of the disjunction type will be stated more precisely in the CPS semantics and the abstract machine semantics below.

Pym and Ritter remark that in the call-by-name case, the disjunction type A ∨ B is not the same as the disjoint sum type A + B which is customarily defined via inl/inr/case constructs. To distinguish them, we sometimes refer to A ∨ B as “classical” disjunction.

We close the section on syntax by remarking that the alternative, symmetric syntax for disjunction from [6] is in fact interdefinable with the syntax given here:

\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}

2 The CPS interpretation of the call-by-name λμν-calculus

We adopt the CPS semantics of [6] to the λμν-calculus. The target of the CPS translation is a lambda calculus λ^{R×+} with sum, products, and a distinguished type R of responses. In the target of the translation, function types are restricted to the case A → R, and consequently, lambda abstractions λx.M occur only when M has type R.

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, which is customarily defined as an abbreviation for λz^{A×B}.M[π_{1}z/x, π_{2}z/y]. We also use the co-pairing notation [M, N] as a shorthand for the expression (λk^{A+B}.case k of inl k_{1}: Mk_{1} or 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). We also use lambda abstraction patterns for co-pairing; thus λ[x, y]^{A+B→R}.M is a shorthand for λz^{A+B→R}.M[λa^{A}.z(inl a)/x, λb^{B}.z(inr b)/y]. The initial type 0 comes 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 basic type Ã for each basic type A ∈ B of λμ. For each type A of the λμ-calculus, we define a pair of types K_{A} and C_{A} of the target calculus, called, respectively, the type of continuations and of computations of type A:

K_{A}  = Ã,  if A is a basic type,
K_{1}  = 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.

For each variable x and each name α of the λμ-calculus, we assume a distinct variable x̃, respectively α̃, of the target calculus. The call-by-name CPS translation \underline{M} of a typed term M is given in Table 2. 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}} .  (1)

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

\underline{x}  = λk^{K_{A}}.x̃k  where x : A
\underline{∗}  = λk^{K_{1}}.□_{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 : ⊥
\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

This CPS translation, for the fragment without conjunction and disjunction, was discovered by Hofmann and Streicher [1]. It differs from Plotkin’s original call-by-name translation [3] by introducing one less double negation at function types, thus taking advantage of the richer target language. For details, see [6].

3 From CPS to an abstract machine

In this section, we describe how to pass from the CPS semantics to an abstract machine semantics. Recall that each continuation type comes with a set of canonical continuation constructors, shown in the following table:

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

Here, k ranges over continuations and M over terms. Moreover, we can have basic continuations at basic types. Here, we consider only one such basic continuation called stop of type K_{A}, where A is the type of the entire program. For the machine semantics, it is not necessary that A is a basic type.

Next, we forget the types and change the notation for continuations. We use the infix notation x::k for pairing ⟨x, k⟩. We also write inl::k and inr::k for left and right injection. Moreover, we will write stop as nil and ∗ as ∗::nil. Thus, the syntactic class of continuations now looks like this:

k ::= inl::k inr::k M::k ∗::nil k′::k nil.

As the notation suggests, a continuation is really a stack, whose elements are tags of the form inl, inr, and ∗, terms, and continuations.

In order to avoid substitutions in our abstract machine, we introduce term closures. A term closure is a pair M^{σ}, where M is a term and σ = ⟨σ_{0}, σ_{1}⟩ is a pair of maps such that σ_{0} assigns term closures to the free variables of M, and such that σ_{1} assigns continuations to the free names of M. σ is also called an environment or an activation record.

The states of the abstract machine are triples {M, σ, k} of a term, an environment, and a stack. Informally, if a closure M^{σ} represents the term M′, then the state \{M, σ, k\} represents the term \underline{M′}k of type R of the target language of the CPS transform. The transition rules for our abstract machine can be read directly off the corresponding transitions of the CPS. Both are shown in Table 3. The initial state for a closed program M is {M, ∅, nil}.

Notice that there is no transition from {∗, σ, k}. This is because in a well-typed program, such a state can never occur unless k = nil, in which case the machine stops with result ∗. More generally, one can show that a well-typed program does not stop until it reaches a state with an empty stack.

Table 3: The transitions of the abstract machine

CPS  Abstract Machine
\underline{x}k  → x̃k  \{x, σ, k\}  → \{M, τ, k\}, where σ_{0}(x) = M^{τ}.
\underline{⟨M, N⟩}(inl k) → \underline{M}k  \{⟨M, N⟩, σ, inl::k\} → \{M, σ, k\}
\underline{⟨M, N⟩}(inr k) → \underline{N}k  \{⟨M, N⟩, σ, inr::k\} → \{N, σ, k\}
\underline{π_{1}M}k  → \underline{M}(inl k)  \{π_{1}M, σ, k\}  → \{M, σ, inl::k\}
\underline{π_{2}M}k  → \underline{M}(inr k)  \{π_{2}M, σ, k\}  → \{M, σ, inr::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}∗  → \underline{M}α̃  \{[α]M, σ, ∗::nil\}  → \{M, σ, k\}, where σ_{1}(α) = k.
\underline{μα.M}k  → \underline{M}[k/α̃]∗  \{μα.M, σ, k\}  → \{M, σ(α ↦ k), ∗::nil\}
\underline{⟨α⟩M}k  → \underline{M}⟨α̃, k⟩  \{⟨α⟩M, σ, k\}  → \{M, σ, k′::k\}, where σ_{1}(α) = k′.
\underline{να.M}⟨k′, k⟩ → \underline{M}[k′/α̃]k  \{να.M, σ, k′::k\} → \{M, σ(α ↦ k′), k\}

To sketch a proof of the correctness of the machine, we reintroduce types. Typed term closures and typed continuations are defined by mutual recursion. A typed term 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 closures, respectively stacks, of the appropriate types. Stacks are typed as follows:

\frac{k : A}{inl_{A,B}::k : A ∧ B}  \frac{k : B}{inr_{A,B}::k : A ∧ B}  \frac{k : B}{\{Γ ⊢ M : A | Δ, σ\}::k : A → B}

\overline{∗::nil : ⊥}  \frac{k′ : A  k : B}{k′::k : A ∨ B}  \frac{(A the top-level type)}{nil : A}

It is now straightforward to check the following:

1. The initial state {M, ∅, nil} is typable, if M is a well-typed program.

2. The transitions of the abstract machine preserve types.

3. Every typable state of the abstract machine, for which the current stack is not nil, has a unique successor state.

4. The transitions of the abstract machine, starting from state {M, ∅, k}, correspond precisely to the top-most reduction sequence of the term \underline{M}k, where one never reduces under a λ.

4 Adding basic types and constants

We now show how to add some meaningful basic types and constants to the language. This complicates the semantics somewhat and leads away from the “pure” call-by-name discipline, because functions that operate on basic types must, by necessity, evaluate their arguments before operating on them. Nevertheless, there is a systematic way of adding basic constants and functions to the CPS semantics and to the abstract machine in the framework of the previous two sections.

4.1 CPS semantics with basic constants

Basic types, such as integers or booleans, differ from other types, because they come with a natural notion of value. In the semantics that we are about to give, we assume that basic functions, such as addition or logical “and”, evaluate all their arguments before they operate on them. Thus we do not accommodate “lazy” basic functions, such as lazy multiplication, which does not evaluate the second argument if the first argument is zero.

We consider the λμν-calculus over a given algebraic signature, i.e., over a set of basic types A, B, … and a set of basic constants c : A and basic functions f : B_{1} → … → B_{n} → A. For the CPS semantics, we consider the same target calculus as before. Moreover, we assume that each basic type A of the λμν-calculus is interpreted by a given type V_{A} of the target calculus, together with interpretations c̃: V_{A}, respectively f̃: V_{B_{1}} → … → V_{B_{n}} → V_{A}, of the basic constants and functions. The type V_{A} is called the type of values of type A. We refine our CPS semantics by letting Ã = V_{A} → R. Continuation and computation types are defined as before:

K_{A}  = V_{A} → R,  if A is a basic type,
K_{1}  = 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 the value types V_{A} are only defined at basic types. To the interpretation of terms from Table 2, we add the following interpretation of basic constants c : A and basic functions f : B_{1} → … → B_{n} → A:

\begin{aligned}\underline{c} & = & λk.kc̃, \\ \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})))). \end{aligned}

Here k : K_{A}, x_{i} : C_{B_{i}}, and v_{i} : V_{B_{i}}. Notice that the interpretation of c is actually a special case of that of f for n = 0. The reader can convince herself that this CPS semantics behaves indeed as required: The term fN_{1} … N_{n} is evaluated by first evaluating all arguments from left to right, and then applying f̃ to the result.

So far, we have accounted only for “pure” basic functions that return basic values. It is also possible to add basic functions to the language whose result type is not a basic type. For instance, if B is the type of booleans, we may consider a family of basic functions if_{A} : B → (A → A → A) which maps true to λxy.x and false to λxy.y. Thus, iftrueMN reduces to M, and iffalseMN reduces to N. We regard ifas a unary basic function with return type A → A → A. For the CPS semantics, we assume that the target language has a type V_{B} of booleans, and we define ĩf : V_{B} → C_{A→A→A} by ĩftrue = \underline{λxy.x} and ĩffalse = \underline{λxy.y}. Then

\underline{if} = λ⟨x, k⟩.x(λb.ĩfbk)

Another useful example of a basic function that returns a term is the 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. Now consider a basic function print_{N,A} : N → (A → A). The intended meaning is that (print n); M prints the integer n and then behaves like M. For the CPS semantics, we need a function p̃r : V_{N} → R → R of the target language to model the side effect of printing. We then have

\underline{print} = λ⟨x, k⟩.x(λn.p̃r n(\underline{λx.x}k)).

4.2 Abstract machine semantics with basic constants

We extend the abstract machine semantics to accommodate basic types. In the CPS semantics, we have introduced a new kind of continuations that are functions. We need to fit these new continuations into our “continuations as stacks” paradigm. Fortunately, the CPS semantics only introduces very special kinds of continuation functions, namely ones of the 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}))),

where 1 ≤ j ≤ n. These can be represented as a particularly simple kind of closure, which we call a frame: we denote the above continuation by

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

Of course, we will also replace the terms N_{j+1}, …, N_{n} by closures.

Recall that a state \{M, σ, k\} of our abstract machine corresponds to a term of the form \underline{M}k under CPS. Because we have introduced values to the CPS semantics, we now add a new kind of state {c, k}, called a value state, to the abstract machine. Such a state needs no environment, and it corresponds to a term of the form kc̃ under CPS.

The CPS semantics of the “pure” basic functions has the following transitions:

\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_{j+1}…. N_{n}(λv_{n}.k(f̃c_{1} … c_{j−1}v_{j}v_{j+1} … v_{n}))))c

→ N_{j+1}(λv_{j+1}…. N_{n}(λv_{n}.k(f̃c_{1} … c_{j−1}cv_{j+1} … v_{n}))),  where j < n
(λv_{n}.k(f̃c_{1} … c_{n−1}v_{n}))c → kd,  where d = f̃c_{1} … c_{n−1}c.

These translate directly to transitions of the abstract machine:

\begin{aligned}\{c, σ, k\} & → & \{c, k\} \\ \{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\} & → & \{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\} & → & \{d, k\}, \end{aligned}

where d = f̃c_{1} … c_{n−1}c and j < n. The rules for the non-pure basic functions ifand print are

{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

We give a low-level implementation of the abstract machine. The target language of the implementation is a certain fragment of the C language. This fragment does not use any of the built-in block structure of C, nor function calls (except for a few auxiliary functions which could be implemented by macros), nor the native machine stack. Control is strictly via goto and if-then-else statements. Thus, the output of the compiler is very close to machine language, except that we ignore issues of register allocation and spilling.

Terms M are represented by program points. The compiled code uses a stack to represent the k-component of a state {M, σ, k}, and a heap to hold term closures and stack closures. A term closure M^{σ} is a heap-allocated record of |σ| + 1 words, the first of which holds a pointer to M, and the remaining ones hold pointers to the values of σ. A stack closure is a heap-allocated data structure representing an immutable snapshot of a stack. A stack of size n is represented by a record of n + 1 words, the first of which holds the number n, and the remaining ones hold the actual stack data.

On the stack, the tokens ∗, inl, and inr are represented by the numbers 0, 1, and 2, respectively. Term closures and stack closures are represented by pointers to the heap. 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 elements tag_{f}, n, j, c_{1}, …, c_{j−1}, p_{j+1}, … p_{n} on the stack. Here, tag_{f} is an integer tag representing the function f, which could be a pointer to code in some implementations. n is the arity of f, j is the position of the • in the frame, c_{1}, …, c_{j−1} are representations of the respective values, and p_{j+1}, …, p_{n} are pointers to the closures N_{j+1}^{σ_{j+1}}, …, N_{n}^{σ_{n}}.

Within the compiler, terms are represented by judgments Γ ⊢ M | Δ. Here Γ and Δ are functions that assign an l-value to each free variable, respectively name, that may occur in M. An l-value is represented as an expression, such as clos[15] or reg5, which will at runtime yield a pointer to a heap-object. Thus, if x is a variable in the domain of Γ, then Γ(x) points to the heap-object that corresponds to x, and similarly for Δ(α). Γ and Δ are implemented as lists of key-value pairs. If a closure for Γ ⊢ M | Δ is build, then the order of the variables and names in Γ and Δ determines the order of the data in the activation record.

The translation of a judgment [[Γ ⊢ M | Δ]]_{v} is a piece of C-code that ends with a goto- or return-statement. It depends on an integer v, which is the number of the next unused “register”, i.e., global variable. The compiler keeps track globally of the largest index v_{max} that was used by any subterm, and provides the variables reg_{0}, …, reg_{v_{max}} . Thus, we assume that there is a potentially infinite supply of registers; of course, in real machine language, there would be a limited number of registers, and one would have to use spilling to allocate additional values in memory.

Table 4: The compilation of terms

[[Γ ⊢ ∗ | Δ]]_{v}  = return "()";

[[Γ ⊢ x | Δ]]_{v} = clos = Γ(x);

goto jump;
[[Γ ⊢ ⟨M, N⟩ | Δ]]_{v} = if (stackempty()) return "pair";
if (pop()==1) {

[[Γ ⊢ M | Δ]]_{v}

}

[[Γ ⊢ N | Δ]]_{v}

[[Γ ⊢ π_{1}M | Δ]]_{v}  = \begin{matrix}push(1); \\ [[Γ ⊢ M | Δ]]_{v} \end{matrix}

[[Γ ⊢ π_{2}M | Δ]]_{v}  = \begin{matrix}push(2); \\ [[Γ ⊢ M | Δ]]_{v} \end{matrix}

[[Γ ⊢ MN | Δ]]_{v} = /* build closure for N */

tmp=alloc(n + m + 1);

tmp[0] = switch_{N};

tmp[1] = Γ(x_{1});

…

tmp[n] = Γ(x_{n});
tmp[n+1] = Δ(α_{1});

…

tmp[n+m] = Δ(α_{m});
push(tmp);

[[Γ ⊢ M | Δ]]_{v}

label_{N}:

[[{x_{i} ↦ clos[i]}_{i} ⊢ N | {α_{j} ↦ clos[n + j]}_{j}]]_{0}

(where FV(N) = x_{1}, …, x_{n} and FN(N) = α_{1}, …, α_{m})

[[Γ ⊢ λx.M | Δ]]_{v} = if (stackempty()) return "fn";

reg_{v} = pop();

[[x:reg_{v}, Γ ⊢ M | Δ]]_{v+1}

[[Γ ⊢ [α]M | Δ]]_{v} = if (stackempty()) return "pass";
loadstack(Δ(α));

[[Γ ⊢ M | Δ]]_{v}

[[Γ ⊢ μα.M | Δ]]_{v} =

reg_{v} = savestack();

push(0);

[[Γ ⊢ M | α:reg_{v}, Δ]]_{v+1}

[[Γ ⊢ ⟨α⟩M | Δ]]_{v} = \begin{matrix}push(Δ(α)); \\ [[Γ ⊢ M | Δ]]_{v} \end{matrix}

[[Γ ⊢ να.M | Δ]]_{v} = if (stackempty()) return "nu";

reg_{v} = pop();

[[Γ ⊢ M | α:reg_{v}, Δ]]_{v+1}

Table 5: The compilation of basic constants and functions

[[Γ ⊢ c | Δ]]_{v} = value = c;

                                     goto intvalue;

[[Γ ⊢ true | Δ]]_{v} = value = 1;

                                     goto boolvalue;

[[Γ ⊢ false | Δ]]_{v} = value = 0;

                                     goto boolvalue;
                  [[Γ ⊢ f | Δ]]_{v}  = if (stackheight()< n) return "fn";

/* build frame for f */

                                     clos = pop();
                                     push(1);
                                     push(n);

                                     push(tag_{f});

                                     goto jump;

The translation of terms is defined in Tables 4 and 5, and the translation of a closed program is shown in Table 6. We have slightly simplified the translation here by omitting type casts between integers and pointers, as well as those parts of the code that are responsible for producing verbose output.

The global variable clos is used to hold a pointer to the current closure during a jump to a “regular” state (not a value-state). At the destination of the jump, execution will resume relative to this closure. In this implementation, jumps proceed in two steps: all jumps first go to a global “dispatch” section, labeled “jump” in Table 6, which reads clos[0] and jumps to the appropriate piece of code. Thus, we distinguish between a switch, which is an internal representation of a program point, and a label, which is a pointer to the actual code. This trick is necessary because in C, labels are not first-class objects. However, in an actual machine-language implementation, one could represent switches directly as pointers to code.

The implementation knows two basic types: integers and booleans. There are two special program points boolvalue and intvalue, also shown in Table 6, which correspond to value states of the abstract machine. At these program points, the global variable value is assumed to hold the current value. The translation of constants is shown in Table 5, where c is an integer constant, and f is an n-ary function constant.

In addition, each basic function has a handler which pops the appropriate values from the stack and performs the required calculation. The handlers for a generic unary function f and a binary function g on integers are shown in Table 7, as well as the handlers for if and print. The implementation also provides a function printbool which acts like print, except that it prints a boolean.

5.1 The runtime system

The compiled code relies on a small runtime system, which provides some auxiliary functions for handling the stack and the heap, as well as code for runtime errors, conversions, and reading command-line arguments. In a real implementation, these functions would be expanded to in-line code.

• void push(void *) and void *pop(void): push, respectively pop, data to and from the stack.

• int stackempty(): tests whether the stack is empty.

• int stackheight(): returns the current size of the stack.

• void *getstack(int n): gets the nth element from the stack, where n = 0 is the topmost element.

• void modifystack(int n,void *x): sets the nth element of the stack to x.

Table 6: The compilation of a closed program

[[M]] = #include "runtime.c"
char *compiled() {
void **clos, **tmp;
int value, arity, j, ftag;

void *reg_{0};

…

void *reg_{v_{max}} ;

[[∅ ⊢ M | ∅]]_{0}

jump: switch(clos[0]) {

case switch_{N_{0}}: goto label_{N_{0}};

…

case switch_{N_{k}}: goto label_{N_{k}};

default: runtimeerr("unknown label");
}
boolvalue:
if (stackempty()) return value ? "true" : "false";
goto applyfunction;
intvalue:
if (stackempty()) return int2str(value);
applyfunction:
arity = getstack(1);
j = getstack(2);
if (j<arity) {
  clos = getstack(2+j);
  modifystack(2+j,value);
  modifystack(2,j+1);
  goto jump;
  }
ftag = pop();
pop();
pop();
switch (ftag) {

… /* handlers for basic functions */ …

default:
  runtimeerr("unknown function tag");
}
}

Table 7: Handlers for some basic functions

case tag_{f}:

value = f(value);
goto intvalue;

case tag_{g}:
reg_{0} = pop();

value = g(reg_{0}, value);
goto intvalue;

case tag_{if}:

if (value) {

[[∅ ⊢ λx.λy.x | ∅]]_{0}

}

[[∅ ⊢ λx.λy.y | ∅]]_{0}

case tag_{print}:

output(int2str(value));

[[∅ ⊢ λx.x | ∅]]_{0}

• void *savestack(void): creates a new stack closure from the current stack, resets the stack, and returns a pointer to the new closure.

• void loadstack(void *addr): restores the stack from the stack closure found at addr.

• void *alloc(int n): allocates n consecutive words on the heap and returns a pointer to them.

• void runtimeerr(char *): issues a runtime error and aborts execution.

• char *int2str(int n): converts an integer to a string.

• void output(char *s): writes the string s to standard output.

• main(): reads the command-line arguments and calls the compiled function.

In addition, there are a few routines that handle verbose output.

5.2 Running the compiler

The compiler is written in ML. It takes λμν-terms to C code. No parsing or type-checking is performed in this experimental implementation, but the correctness of the implementation depends on the typability of the source term. λμν-terms are represented as elements of the abstract datatype term:

type var = string;
type fnconst = string;
datatype term = Var of var | Unit | Pair of term*term | Proj1 of term
| Proj2 of term | App of term*term | Lam of var*term
| Pass of var*term | Mu of var*term | Ang of var*term
| Nu of var*term | Intconst of int | True | False
| Fnconst of fnconst;

Here, a variable x is represented as Var "x". Application MN is App(M,N), lambda abstraction λx.M is Lam("x",M), and similar for μ- and ν-abstraction. Passification [α]M is Pass("a",M), and ⟨α⟩M is Ang("a",M). Integer and boolean constants are represented as Intconst n, True, and False, and basic functions as Fnconst "+". The available basic functions are

            +, -, *, /, succ, ~, and, or, not, iszero, <, >, =, >=, =<, if, print, printbool

One can add additional basic functions by editing the definition of fnconstdef in the ML code.

The compiler is available in three dialects of ML: SML/NJ 0.93, Caml Light, and Objective Caml. The current version can be found at [5]. To load the compiler, type

                   use "compiler.sml";  from SML,
                   include "compiler.ml";; from Caml Light, or
                   #use "compiler.oml";;  from Objective Caml.

Then type compile term "myfile.c";; to generate a C-program from a term source. The output is written to the file myfile.c. This can be compiled with any C-compiler, for instance by typing gcc myfile.c -o myfile. Make sure that the file runtime.c is in the same directory, because it is included. Finally, execute the code via

myfile [-v].

The -v option causes the program to write detailed information about the evaluation to standard output. In this mode, a representation of each state of the underlying abstract machine is printed, as well as information on each new term or stack closure that is created.

References

[1] 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.

[2] 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.

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

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

[5] P. Selinger. An implementation of the call-by-name λμν-calculus. Available from http://www.math.lsa.umich.edu/ ˜ selinger/lammunu/, 1998.

[6] P. Selinger. Control categories and duality: on the categorical semantics of the lambda-mu calculus. Math. Struct. in Computer Science, 2000. To appear.