Logical Methods in Computer Science
Vol. 6 (3:1) 2010, pp. 1–37
www.lmcs-online.org

Submitted
Published

Oct. 12, 2009
Jul. 11, 2010

LAZY EVALUATION AND DELIMITED CONTROL
RONALD GARCIA a , ANDREW LUMSDAINE b , AND AMR SABRY c
a

b,c

Carnegie Mellon University
e-mail address: rxg@cs.cmu.edu
Indiana University
e-mail address: {lums,sabry}@cs.indiana.edu

Abstract. The call-by-need lambda calculus provides an equational framework for reasoning syntactically about lazy evaluation. This paper examines its operational characteristics.
By a series of reasoning steps, we systematically unpack the standard-order reduction relation of the calculus and discover a novel abstract machine definition which, like
the calculus, goes “under lambdas.” We prove that machine evaluation is equivalent to
standard-order evaluation.
Unlike traditional abstract machines, delimited control plays a significant role in the
machine’s behavior. In particular, the machine replaces the manipulation of a heap using
store-based effects with disciplined management of the evaluation stack using control-based
effects. In short, state is replaced with control.
To further articulate this observation, we present a simulation of call-by-need in a callby-value language using delimited control operations.

1. Introduction
From early on, the connections between lazy evaluation (Friedman and Wise, 1976;
Henderson and Morris, 1976) and control operations seemed strong. One of these seminal
papers on lazy evaluation (Henderson and Morris, 1976) advocates laziness for its coroutinelike behavior. Specifically, it motivates lazy evaluation with a solution to the same fringe
problem: how to determine if two trees share the same fringe without first flattening each
tree and then comparing the resulting lists. A successful solution to the problem traverses
just enough of the two trees to tell that they do not match. The same fringe problem
is also addressed in Sussman and Steele’s original exposition of the Scheme programming
1998 ACM Subject Classification: D.3.1.
Key words and phrases: call-by-need, reduction semantics, abstract machines, delimited continuations,
lambda calculus.
a
This work was supported by the National Science Foundation under Grant #0937060 to the Computing
Research Association for the CIFellows Project.
b,c
This work was supported by NSF awards CSR/EHS 0720857 and CCF 0702717.

l

LOGICAL METHODS
IN COMPUTER SCIENCE

c
DOI:10.2168/LMCS-6 (3:1) 2010

CC

R. Garcia, A. Lumsdaine, and A. Sabry
Creative Commons

2

R. GARCIA, A. LUMSDAINE, AND A. SABRY

language (Sussman and Steele Jr., 1975). One of their solutions uses a continuation passingstyle representation of coroutines. More recently, Biernacki et al. (2005) explores a number
of continuation-based solutions to same fringe variants.
Same fringe is not the only programming problem that can be solved using either lazy
evaluation or continuations. For instance, lazy streams and continuations are also used to
implement and reason about backtracking (Wand and Vaillancourt, 2004; Kiselyov et al.,
2005). Strong parallels in the literature have long suggested that lazy evaluation elegantly
embodies a stylized use of coroutines. Indeed, we formalize this connection.
Call-by-need evaluation combines the equational reasoning capabilities of call-by-name
with a more efficient implementation technology that systematically shares the results of
some computations. However, call-by-need’s evaluation strategy makes it difficult to reason
about the operational behavior and space usage of programs. In particular, call-by-need
evaluation obscures the control flow of evaluation. To facilitate reasoning, semantic models (Launchbury, 1993; Sestoft, 1997; Friedman et al., 2007; Nakata and Hasegawa, 2009),
simulations (Okasaki et al., 1994), and tracing tools (Gibbons and Wansbrough, 1996) for
call-by-need evaluation have been developed. Many of these artifacts use an explicit store
or store-based side-effects (Wang, 1990) to represent values that are shared between parts
of a program. Stores, being amorphous structures, make it difficult to establish program
properties or analyze program execution. This representation of program execution loses
information about the control structure of evaluation.
The call-by-need lambda calculus was introduced by Ariola et al. (1995) as an alternative to store-based formalizations of lazy evaluation. It is an equational framework for
reasoning about call-by-need programs and languages. Following Plotkin (1975), these authors present a calculus and prove a standardization theorem that links the calculus to a
complete and deterministic (i.e. standard order) reduction strategy. The calculus can be
used to formally justify transformations, particularly compiler optimizations, because any
terms it proves equal are also contextually equivalent under call-by-need evaluation.
Call-by-need calculi were investigated by two groups (Maraist et al., 1998; Ariola and Felleisen,
1997). The resulting two calculi are quite similar but their subtle differences yield trade-offs
that are discussed in the respective papers. Nonetheless, both papers connect their calculi
to similar standard-order reduction relations.
One notable feature of Ariola and Felleisen’s calculus (and both standard-order reduction relations) is the use of evaluation contexts within the notions of reduction. It has been
observed that evaluation contexts correspond to continuations in some presentations of language semantics (Felleisen and Friedman, 1986; Biernacka and Danvy, 2007). However, in
these systems evaluation contexts are used to model variable references and demand-driven
evaluation, not first-class continuations.
This paper exposes how Ariola et al.’s call-by-need evaluation relates to continuations.
By systematically unpacking the standard-order reduction relation of the calculus, we discover a novel abstract machine that models call-by-need style laziness and sharing without
using a store. Instead, the machine manipulates its evaluation context in a manner that
corresponds to a stylized use of delimited control operations. The machine’s behavior reveals a connection between control operations and laziness that was present but hidden in
the reduction semantics.
To directly interpret this connection in the terminology of delimited control, we construct a simulation of call-by-need terms in the call-by-value language of Dybvig et al.

LAZY EVALUATION AND DELIMITED CONTROL

3

(2007), which provides a general framework for delimited continuations with first-class generative prompts.
Our concrete specifications of the relationship between call-by-need and delimited control firmly establish how lazy evaluation relates to continuations and other control-oriented
language constructs and effects. Implementations of both the machine and the simulation
are available at the following url:
http://osl.iu.edu/~garcia/call-by-need.tgz.
2. The Call-by-need Lambda Calculus
The remainder of this paper examines Ariola and Felleisen’s formalization of call-byneed (Ariola and Felleisen, 1997). The terms of the calculus are standard:
t ::= x | λx.t | t t
The call-by-need calculus, in direct correspondence with the call-by-value and call-by-name
lambda calculi, distinguishes lambda abstractions as values:
v ::= λx.t
Call-by-need is characterized by two fundamental properties: a computation is only performed when its value is needed, and the result of any computation is remembered and
shared so that it only needs to be computed once. This calculus distinguishes two additional subsets of the term language to help represent these properties.
To capture the notion of necessary computations, the calculus distinguishes the set of
lambda abstractions that immediately need the value of their argument. To define this set,
the calculus appeals to a notion of evaluation contexts, a set of terms that each have a
single hole () in them:
E ::=  | E t | (λx.E[x]) E | (λx.E) t
Given the evaluation contexts, the set of lambda abstractions in question is defined syntactically as (λx.E[x]), the set of lambda abstractions whose bodies can be decomposed into
an evaluation context and a free instance of the abstracted variable.
The intuition for this definition is as follows. Evaluation contexts are essentially terms
with a single hole in them. When used in the style of Felleisen and Hieb (1992), evaluation
contexts indicate those locations in a program that are subject to evaluation. As such, a
lambda abstractions of the form (λx.E[x]) will immediately refer to the value of its argument
when its body is evaluated. Here, E[x] is not a language construct, but rather metalinguistic
notation for a side condition on the term in the body of the lambda abstraction.
The syntactic structure of call-by-need evaluation contexts give some hint to the nature
of computation captured by this calculus. First, the context production E t indicates that
evaluation can focus on the operator position of an application regardless of the structure
of the operand. This property is also true of call-by-name and call-by-value and reflected
in their respective evaluation contexts. Second, the (λx.E[x]) E production indicates the
operand of an application expression can be evaluated only if the operator is a lambda
abstraction that immediately needs its argument. This restriction does not hold for call-byvalue1, where any lambda abstraction in operator position justifies evaluating the operand.
1assuming left-to-right evaluation of application expressions

4

R. GARCIA, A. LUMSDAINE, AND A. SABRY

This restriction on evaluation corresponds with our intuitive understanding of call-by-need.
Third, the (λx.E) t production indicates that evaluation can proceed under a lambda abstraction when it is in operator position. Though not immediately obvious, this trait is
used by the calculus to capture the process of sharing computations among subterms.
To capture the notion of shared computations, the call-by-need calculus distinguishes
lambda abstractions with explicit bindings for some variables, calling them answers:
a ::= v | (λx.a) t
Answers are a syntactic representation of (partial) closures. An answer takes the form of a
lambda term nested inside some applications. The surrounding applications simulate environment bindings for free variables in the nested lambda term. This representation makes
it possible for the calculus to explicitly account for variable binding and to syntactically
model how call-by-need evaluation shares lazily computed values.
The calculus has three notions of reduction:
(λx.E[x]) v
→need (λx.E[v]) v
(λx.a) t1 t2
→need (λx.a t2 ) t1
(λx1 .E[x1 ]) ((λx2 .a) t1 ) →need (λx2 .(λx1 .E[x1 ]) a) t1
The first reduction rule substitutes a value for a single variable instance in an abstraction.
The rule retains the binding and abstraction so as to share its computation with other
variable references as needed. The second and third reduction rules commute an application
with an answer binding to expose opportunities for reduction without duplicating not-yetneeded computations. These two rules help to ensure that computations will be shared
among references to a common variable.
As popularized by Barendregt (1981), each reduction assumes a hygiene convention.
When combined with the evaluation contexts, the notions of reduction yield a deterministic
standard order reduction relation (7−→sr ) and its reflexive-transitive closure ( 7−→
→sr ).
Definition 2.1. t1 7−→sr t2 if and only if t1 ≡ E[tr ], t2 ≡ E[tc ] and tr →need tc .
Terms of the calculus satisfy unique decomposition, meaning that any program (i.e.
closed term) that is not an answer can be decomposed exactly one way into a context E
and redex tr . This property ensures that 7−→sr is deterministic. Standard order reduction
is an effective specification of call-by-need evaluation: if t is a program (i.e. closed term),
then t call-by-need evaluates to an answer if and only if t 7−→
→sr a for some answer a.
3. From Reduction Semantics to Machine Semantics
Some reduction semantics have been shown to correspond directly to abstract machine
semantics, thereby establishing the equivalence of a reducer and a tail-recursive abstract
machine implementation (Felleisen and Friedman, 1986; Felleisen et al., 2009). In particular, Danvy and Nielsen (2004) introduces a method and outlines criteria for mechanically
transforming reduction semantics into abstract machine semantics. However, proceeding
directly from the reduction semantics for call-by-need to a tail-recursive abstract machine
semantics poses some challenges that do not arise with other reduction semantics like callby-name and call-by-value.
A straightforward call-by-need reducer implementation naı̈vely decomposes a term into
a context and a redex. Any application could be one of three different redexes, each of

LAZY EVALUATION AND DELIMITED CONTROL

5

which is nontrivial to detect, so whenever the decompose function detects an application, it
sequentially applies several recursive predicates to the term in hopes of detecting a redex.
If the term is a redex, it returns; if not, it recursively decomposes the operator position.
Call-by-need redexes require more computational effort to recognize than either callby-name or call-by-value. For instance, given a term t, only a fixed number of terminal
operations are required to detect whether t is a call-by-name redex: one to check if the
term is an application, one to access the operator position, and one to check if the operator
is an abstraction.
Contrast this with the call-by-need redex (λx.E[x])((λy.a)t). Given a call-by-need term
tx , testing whether it matches this redex form requires an unknown number of operations:
check if tx is an application; check if its operator position is a lambda abstraction; check, in
an unknown number of steps, if the operator’s body can be decomposed into E[x], where x
is both free in E and bound by the operator; and finally check, in an unknown number of
steps, if the operand has the inductive structure of an answer.
To make matters worse, some terms can be decomposed into the form E[x] in more
than one way. For instance, consider the term (λx.(λy.y) x). It can be decomposed as both
(λx.E1 [y]) and (λx.E2 [x]) where E1 ≡ (λy.) x and E2 ≡ (λy.y) . As such, a recursive
procedure for decomposing a term cannot stop at the first variable it finds: it must be able
to backtrack in a way that guarantees it will find the right decomposition E[x]—and in turn
the right redex—if there is one.
Recall that one of the evaluation contexts has the form (λx.E)t. This means that redex
evaluation can occur “under binders” (Moggi and Sabry, 2004; Kameyama et al., 2008). All
three call-by-need notions of reduction shuffle lambda abstractions about in unusual ways.
Furthermore, while reducing a recursive routine, a call-by-need evaluator may end up performing reductions under multiple copies of the same lambda abstraction. Call-by-name and
call-by-value evaluators can address hygiene concerns by using environments and closures,
but a call-by-need evaluator must prevent its evaluation context from incorrectly capturing free variable references. Any evaluator that goes under lambdas must pay particular
attention to hygiene (Xi, 1997).
Since this work was originally published, Danvy et al. (2010) have adapted and extended the method of Danvy and Nielsen (2004) to produce a related abstract machine for
call-by-need.
3.1. Towards an Abstract Machine. To find call-by-need redexes tail-recursively, we apply an insight from the CK abstract machine (Felleisen and Friedman, 1986; Felleisen et al.,
2009). The CK machine implements an evaluation strategy for call-by-value based on a reduction semantics using the (inside-out) evaluation contexts , E[ t] and E[(λx.t) ]. To
find a redex, the machine iteratively examines the outermost constructor of a term and uses
the evaluation context to remember what has been discovered. Since call-by-value satisfies
unique decomposition, this approach will find the standard redex if there is one.
To illustrate this in action, we walk through an example. Consider the program
(λx.x) λy.y. Evaluation begins with configuration h[ ], (λx.x) λy.yi. Underlining indicates
subterms that the machine knows nothing about; at the beginning of evaluation, it knows
nothing about the entire term. On the first step of the reduction, the machine detects that
the term is an application (λx.x) λy.y. To examine the term further, the machine must
move its focus to either the operator or operand of this application. Since the machine is tail
recursive, it must also push an evaluation context to store the as-yet uncovered structure

6

R. GARCIA, A. LUMSDAINE, AND A. SABRY

of the term. The only context it can reliably push at this point is [ λy.y]: it cannot push
[(λx.x) ] because it has not yet discovered that the operator position is a value. So the
machine pushes the [ λy.y] context, which serves as a reminder that it is focused on the
operator of an application.
On the second step of the reduction, the machine detects that the operator is an abstraction λx.x, and observes that the innermost context is [ λy.y]. In response, the machine
pops the context, focuses on λy.y, and pushes the context [(λx.x) ], since the operator is
now known to be a value. This context serves as a reminder that evaluation is currently
focused on the operand of an application that can be reduced once that operand becomes
a value.
On the third step, the machine detects the abstraction (λy.y), and remembers that the
innermost context is [(λx.x) ]. At this point, the machine has deduced enough information
to recognize the redex (λx.x) λy.y. This example illustrates how the CK machine uses a
depth-first left-to-right search strategy to detect call-by-value redexes.
Now consider the same term under call-by-need using a similar strategy. As with callby-value, the top-level application can be detected, the operand can be pushed onto the
evaluation context, and the operator can be exposed as the abstraction λx.x. At this
point behavior must diverge from call-by-value because the body of the abstraction is still
unknown and call-by-need does not have [(λx.t) ] contexts for arbitrary t. However, callby-need does have contexts of the form [(λx.) λy.y]. Therefore, it is possible to proceed
under the first lambda abstraction, push the context, and focus on x.
The term is exposed as a variable x, which combines with the context [(λx.) λy.y]
to form the term (λx.E[x]) λy.y (where E ≡ ). At this point, enough information has
been uncovered to push the context [(λx.[x]) ] and focus on λy.y. The abstraction λy.y
is recognized, and with that a call-by-need redex (λx.[x]) λy.y has been found. Success
with this example suggests a promising strategy for implementing call-by-need reduction
tail-recursively.
3.2. An Initial Abstract Machine. In this section, we elaborate the above search strategy into a simple but inefficient tail-recursive abstract machine. We present it without proof
and then by a series of correct transformations we derive an efficient machine that we prove
correct.
This abstract machine uses the same terms, values, and answers as the calculus. However, it introduces two alternate notions. First, the machine uses a more versatile representation of evaluation contexts. As observed in Danvy and Nielsen (2004), evaluation
contexts can be mathematically specified in more than one way. For optimal flexibility, we
define evaluation contexts as lists of frames, where the empty list [ ] and single-frame lists
[f ] are our simple units, and the operator ◦ stands for list concatenation.
f ::=  t | (κx.E)  | (λx.) t
E ::= [ ] | [f ] ◦ E | E ◦ [f ]
where E ◦ [ ] = [ ] ◦ E = E
and E1 ◦ (E2 ◦ E3 ) = (E1 ◦ E2 ) ◦ E3
When two contexts are composed, the second context is plugged into the hole of the first
context: for example [ t2 ] ◦ [ t1 ] = [( t1 ) t2 ].

LAZY EVALUATION AND DELIMITED CONTROL

7

We call the frame [(λx.) t] a binder frame. It represents a variable binding in the
context. It can be read as [let x = t in ], but we use the former notation to emphasize that
call-by-need evaluation proceeds under lambdas. This observation motivates our analysis
of hygiene in Section 4.5.
We call the frame [(κx.E) ] a cont frame, in reference to continuations. The construction (κx.E) is called a cont and replaces the metalinguistic term notation (λx.E[x]) from
the calculus. We use a different notation for conts than lambda terms to indicate that in
the machine conts are distinct from terms (they are of type Cont rather than type Term
in an implementation). Conts indicate nontrivial structural knowledge that the machine
retains as it searches for a redex. This distinction matters when we establish continuation
semantics for machine states. As we shall see, a cont frame represents a suspended variable
reference.
Finally we call the frame [ t] an operand frame, and it represents a term waiting for
an abstraction.
The abstract machine also introduces a notion of redexes:
r ::= a t | (κx.E) a
Redexes are distinguished from terms in the machine, meaning that in an implementation,
the type Redex is distinct from the type Term. This distinction suggests that conts (κx.E)
are neither terms nor first-class entities in the call-by-need language: they only appear in
evaluation contexts and in redexes. As we discuss below, the machine distinguishes one
more kind of redex than the calculus.
The transition rules for the machine are staged into four distinct groups: refocus,
rebuild, need, and reduce. Each machine configuration can be related to a term in the
language of the calculus. The refocus rules examine the current term and push as many
operand frames [ t] as possible. A refocus configuration hE, tif represents the term E[t].
hE, tif

(Refocus)

hE, xif
hE, λx.tif
hE, t1 t2 if

7→ hE, [ ], xin
7
→
hE, λx.tib
7→ hE ◦ [ t2 ], t1 if

Upon reaching a variable, refocus transitions to the need rules; upon reaching a lambda
abstraction, it transitions to the rebuild rules.
The rebuild rules search up into the context surrounding an answer for the next applicable redex. A rebuild configuration hE, aib represents the term E[a].
hE, aib

(Rebuild)

h[ ], aib
hE ◦ [ t1 ], aib
hE ◦ [(λx.) t1 ], aib
hE1 ◦ [(κx.E2 ) ], aib

7
→
7→
7→
7→

a
hE, a t1 id
hE, (λx.a) t1 ib
hE1 , (κx.E2 ) aid

These rules examine the current context and proceed to build a maximal answer-shaped
term, progressively wrapping binder frames around the current answer. If the entire context
is consumed then evaluation has completed and the entire program is an answer. Upon

8

R. GARCIA, A. LUMSDAINE, AND A. SABRY

reaching an operand or cont frame, a redex has been found, and rebuild transitions to the
reduce rules. These rules resemble the refocusaux rules of Danvy and Nielsen (2004).
The need rules also examine the context, but they search for the binder frame that
corresponds to the variable under focus. A need configuration hE1 , E2 , xin represents the
term E1 [E2 [x]].
hE, E, xin

(Need)

hE1 ◦ [(λx.) t], E2 , xin 7→ hE1 ◦ [(κx.E2 ) ], tif
hE1 ◦ [f ], E2 , xin 7→ hE1 , [f ] ◦ E2 , xin
where, [f ] 6≡ [(λx.) t]
Since input programs are closed, the associated binder must be somewhere in the context. Upon finding the right binder frame, a cont frame [(κx.E) ] is pushed onto the
context and evaluation proceeds to refocus on the operand from the associated binder
frame.
The reduce rules simulate the notions of reduction from the calculus. A reduce configuration hE, rid represents the term E[r] where a cont κx.E represents the term λx.E[x].
hE, rid

(Reduce)

hE1 , (κx.E2 ) vid
hE1 , (κx1 .E2 ) ((λx2 .a) t)id
hE, (λx.a) t1 t2 id
hE, (λx.t1 ) t2 id

7
→
7→
7→
7→

hE1 , (λx.E2 [v]) vif
hE1 , (λx2 .(λx1 .E2 [x1 ]) a) tif
hE, (λx.a t2 ) t1 if
hE ◦ [(λx.) t2 ], t1 if

Each of the first two reduce rules transforms a cont into a lambda abstraction by
plugging its context with a term and abstracting its variable. As such, each reduce rule
transforms a redex into a pure term of the calculus and transitions to a refocus configuration,
which searches for the next redex.
The reduce rules also handle terms of the form (λx.t1 ) t2 , even though such terms are
not call-by-need redexes. Including this rule gives the set of redexes greater uniformity: all
terms of the form a t are redexes, just like the terms of the form (κx.E) a. This symmetry
is not exhibited in the call-by-need calculus. However, Ariola and Felleisen (1997) defines
and uses an auxiliary let calculus that adds the reduction
(λx.t1 ) t2 →need let x = t2 in t1
to the calculus and defines the other reductions in terms of the let expressions. The fourth
reduce rule corresponds to this reduction rule. However, our presentation shows that an
auxiliary let term, though compatible with this model, is not needed to specify call-by-need:
the syntax of pure calculus terms suffices. Furthermore, treating this rule as a reduction
here anticipates a change we make to the machine (Section 4.5) that adds explicit variable
renaming to that rule. Finally, the reduce rules are improved in the next section so that all
reduce rules change their representative terms nontrivially.
Machine evaluation of a program t begins with the refocus configuration h[ ], tif and
terminates if it arrives at an answer a. Its behavior in between can be summarized as follows:
search downwards until a value or variable reference is reached. If a variable reference is
reached, store a cont in the context to remember the variable reference and proceed to

LAZY EVALUATION AND DELIMITED CONTROL

9

evaluate its binding. If an abstraction is reached, accumulate an answer up to the innermost
redex, or the top of the evaluation context if none is found. In short, the machine performs
a depth-first, left-to-right traversal in search of a call-by-need redex. Along the way it
uses the evaluation context to store and retrieve information about program structure,
particularly the location of variable bindings (using binder frames) and variable references
(using cont frames). The refocus, rebuild, and need rules leave the term representation of
their configurations unchanged (e.g. if hE1 , t1 if 7→ hE2 , t2 if then E1 [t1 ] ≡ E2 [t2 ]), and the
reduce rules embody the notions of reduction from the calculus.
Our strategy for producing this machine builds on the strategy of Danvy and Nielsen
(2004), which mechanizes the direct transformation of reduction semantics into abstract machine semantics. That report introduces and verifies a general method for using reduction
semantics that meet certain criteria to construct a function that “refocuses” an arbitrary
term-context pair to a redex-context pair. The resulting function can then be used to induce
an abstract machine semantics. Unfortunately that refocus function construction does not
apply to the call-by-need lambda calculus because the calculus does not meet the required
criteria. In particular, the construction requires that a maximally-decomposed closed term
(i.e. program) will focus on a value or a redex. However, call-by-need evaluation contexts
can decompose down to variable references, which are neither redexes nor values under
call-by-need. There are however other ways to produce an abstract machine from a reduction semantics which may apply to the call-by-need calculus studied here. For instance,
Danvy et al. (2010) devise a variant of the let-based call-by-need reduction semantics, implement it, and use a program-transformation based approach to produce a refocus function
and abstract machine implementation.
The following partial trace demonstrates how the initial abstract machine discovers the
first redex for our running example (λx.x) λy.y:
h[ ], (λx.x) λy.yif

7→

[ λy.y], λx.x

7→

[ ], (λx.x) λy.y

d

7→

[(λx.) λy.y], x

7→

[(κx.[ ]) ], λy.y

7→

[(κx.[ ]) ], λy.y

f

7→

[ λy.y], λx.x

f

7→

[(λx.) λy.y], [ ], x

b

7→

[ ], (κx.[ ]) λy.y

f

b
n

d

4. Refining the Machine
In this section we study the behavior of the abstract machine and make some improvements based on our observations. These changes lead us from the initial machine above to
our final machine specification.
4.1. Grabbing and Pushing Conts. The need rules linearly search the nearest context
for a binder frame that matches the variable under question. This process can be specified
as one step:
hE1 ◦ [(λx.) t] ◦ E2 , xin 7→ hE1 ◦ [(κx.E2 ) ], tif
where [(λx.) t] ∈
/ E2
This evaluation step accumulates a segment of the current evaluation context and stores it.
In general, abstract machines that model control operators represent control capture in a
similar manner. In this particular case, only part of the evaluation context is captured, and
the amount of context captured depends on the dynamic location in the context of a certain

10

R. GARCIA, A. LUMSDAINE, AND A. SABRY

frame. As such, the need rules seem to perform some kind of delimited control capture. This
analogy becomes stronger upon further analysis of the first reduce rule from Section 3.2.
The machine uses its structural knowledge of κx.E to construct the abstraction λx.E[v].
However, the resulting machine configuration no longer retains any of the structure that
had previously been discovered. Recall our example execution trace from Section 3.2. The
machine reduces the redex found at the end of that trace as follows:
[ ], (κx.[ ]) λy.y

d

7→ h[ ], (λx.λy.y) λy.yif

By returning to refocus following the reduction, the machine loses all structural knowledge
of the term. To continue execution, it must examine the structure of the contractum from
scratch. Fortunately, the evaluator can be safely improved so that it retains knowledge of
the contractum’s structure:
Proposition 4.1.
hE1 , (λx.E2 [v]) vif 7−→
→ hE1 ◦ [(λx.) v] ◦ E2 , vib
Proof. Corollary of hE1 , E2 [v]if 7−→
→ hE1 ◦ E2 , vib , which is proven by induction on E2 .
This proposition justifies replacing the first reduce rule with one that pushes the evaluation context embedded in the cont and proceeds to rebuild an answer:
hE1 , (κx.E2 ) vid 7→ hE1 ◦ [(λx.) v] ◦ E2 , vib
This short-circuit rule extends the current evaluation context with a binder frame and the
context E2 that was inside the cont. The rule is suggestive of delimited control because
machine models of control operators generally represent the reinstatement of delimited
continuations by extending the current context with a piece of captured evaluation context.
Of more immediate interest, though, is how reduction of our example now proceeds:
[ ], (κx.[ ]) λy.y

d

7→ [(λx.) (λy.y)], λy.y

b

All knowledge of the contractum’s structure is retained, though much of it is now stored in
the evaluation context.
4.2. Shifting Binder Frames. The second and third reduce rules from Section 3.2 also
discard structural information. Specifically, they both transition to the forgetful refocus
rule. However their information can be preserved.
Proposition 4.2.
hE, (λx.a t2 ) t1 if 7−→
→ hE ◦ [(λx.) t1 ], a t2 id .
Proof. Corollary of hE1 , aif 7−→
→ hE1 , aib , which is proven by induction on a.
Proposition 4.3. If E2 does not capture x1 (Section 4.5), then
hE1 , (λx2 .(λx1 .E2 [x1 ]) a) tif 7−→
→ hE1 ◦ [(λx2 .) t], (κx1 .E2 ) aid .
Proof. Corollary of hE1 , aif 7−→
→ hE1 , aib and
hE1 , (λx1 .E2 [x1 ]) tif 7−→
→ hE1 ◦ [(κx1 .E2 ) ], tif , which is proven by case analysis and induction on E2 .

LAZY EVALUATION AND DELIMITED CONTROL

11

These propositions justify short-circuiting the respective evaluation rules. The new
rules improve the behavior of the abstract machine.
hE1 , (κx1 .E2 ) ((λx2 .a) t)id 7→ hE1 ◦ [(λx2 .) t], (κx1 .E2 ) aid
hE, (λx.a) t1 t2 id 7→ hE ◦ [(λx.) t1 ], a t2 id
By fast-forwarding to reduce, the rules retain the discovered term structure and thereby
avoid retracing the same terms again.
4.3. Answer = Binders × Value. The transition rules repeatedly create binder frames
out of terms and reabsorb those frames into answers. In this section we simplify this
protocol. We distinguish answers from terms by providing them a separate representation:
a ::= TE, vU, where E = [(λxi .) ti ]
An answer is now represented as a tuple containing the nested lambda abstraction and
the sequence of binder frames that are wrapped around it in the old presentation (we use
overlines to indicate sequences). This presentation bears strong similarity to calculi with
explicit substitutions (Abadi et al., 1991) in that each binder frame [(λx.) t] corresponds
to a substitution [t/x]. An answer can be seen as a lambda term nested inside a sequence
of explicit substitutions, v[ti /xi ].
The rebuild rules could be reformulated as a three place configuration, hE, E, vib , but
instead we immediately apply the same improvement that we applied to the need rules in
Section 4.1. For instance, the new transition rule for rebuilding to a cont frame is:
hE1 ◦ [(κx.E2 ) ] ◦ E3 , vib 7→ hE1 , (κx.E2 ) TE3 , vUid
where E3 = [(λxi .) ti ]
Returning to our running example, reduction from its most recent state (at the end of
Section 4.1) transitions to a final answer, signaling the end of execution:
[(λx.) λy.y], λy.y

b

7→ T[(λx.) λy.y], λy.yU

4.4. Aggregate Reduction. Now that answers explicitly carry their binders in aggregate,
the reduce rules can be substantially consolidated. Currently, the second and third reduce
rules iteratively remove the top binder frame from an answer and push it onto the evaluation
context. This process repeats until the answer is just a lambda abstraction. At that point,
the second and third reduce rules defer to the first and fourth reduce rules respectively.
This corresponds exactly with standard-order reduction (cf. Definition 2.1):
Proposition 4.4.
E[((λxn . . . . ((λx1 .((λx0 .v) t0 )) t1 ) . . . ) tn ) t] 7−→
→sr
E[((λxn . . . . ((λx1 .((λx0 .v t) t0 )) t1 ) . . . ) tn )].
E[(λx.E[x]) ((λxn . . . . ((λx1 .((λx0 .v) t0 )) t1 ) . . . ) tn )] 7−→
→sr
E[((λxn . . . . ((λx1 .((λx0 .(λx.E[x]) v) t0 )) t1 ) . . . ) tn )].
Proof. By induction on the structure of the answer term, using the unique decomposition
lemma of Ariola and Felleisen (1997).

12

R. GARCIA, A. LUMSDAINE, AND A. SABRY

Using the new answer representation, each pair of associated reduce rules can be merged
into one omnibus rule that moves all the binder frames at once and simultaneously performs
a reduction using the underlying value.
hE1 , (κx.E2 ) TE3 , vUid 7→ hE1 ◦ E3 ◦ [(λx.) v] ◦ E2 , vib
hE1 , TE2 , (λx.t1 )U t2 id 7→ hE1 ◦ E2 ◦ [(λx.) t2 ], t1 if
As a result of these transformations, both conts and answers contain evaluation contexts. Furthermore, conts and answers are not terms of the calculus, and the machine never
reverts a cont or answer to a term. The rules that create them, rebuild for answers and
need for conts, capture part of the evaluation context, and the rules that consume them,
the reduce rules, reinstate the captured contexts.
4.5. Variable Hygiene. Presentations of calculi often invoke a hygiene convention and
from then on pay little attention to bound or free variables. In this manner, calculi do
not commit to any of the numerous ways that hygiene can be enforced. Many abstract
machines, however, use environments or explicit sources of fresh names to guarantee hygiene
and thereby provide a closer correspondence to concrete implementations. In this section,
we augment the call-by-need machine with simple measures to enforce hygiene.
Our primary hygiene concerns are that evaluation occurs under binders and binders
are shifted about in unusual ways. In order to ensure that binding structure is preserved
throughout evaluation, we need to be able to reason locally, within each machine configuration, about bound variables. To make this possible, we make one last change to the
machine. We add a list of names to each machine configuration.
X ::= xi
Most of the machine rules simply pass the list of names along to the next transition. One
of the reduce rules manipulates the list of names.
hX | E1 , TE2 , λx.t1 U t2 id 7−→nam

X, x′ E1 ◦ E2 ◦ [(λx′ .) t2 ], t1 [x′ /x]

f

x′ ∈
/ X (D.2)

When this rule goes under a lambda, it adds the name of its bound variable to the list X
of variables. The notation X, x expresses adding a new name x to X. If the bound variable
x on the left hand side of the rule is already a member of X, then the variable is renamed
as part of the transition. As such, X can be considered a set.
Now each machine configuration has one of five forms:
hX | E, ?i ::= hX | TE, vUi | hX | E, rid | hX | E, tif
| hX | E, vib | hX | E, xin
We use the notation hX | E, ?i below to uniformly discuss all configuration types, where
X refers to the list of names, E refers to the context, and ? refers to the term or redex.
For a final configuration hX | TE, vUi, ? refers to the answer’s underlying value v, and E
corresponds to the answer’s binder frames E. We use the metavariable C to range over
configurations when the internal structure does not matter.

LAZY EVALUATION AND DELIMITED CONTROL

13

The call-by-need abstract machine uses the set X of names to keep track of active
variables: any variable x whose binding instance has been pushed into a binder frame
[(λx.) t]:
AV ([ ])
= ∅
AV ([(λx.) t] ◦ E)
= { x } ∪ AV (E)
AV ([ t] ◦ E)
= AV (E)
AV ([(κx.E1 ) ] ◦ E) = AV (E1 ) ∪ { x } ∪ AV (E)
Cont-bound variables are counted among the active variables because machine evaluation
must have gone under a binding to construct the cont frame.
The renaming condition on the (D.2) reduce rule ensures that active variables are
mutually distinguishable. This guarantees that the machine’s need rule can never capture
the wrong evaluation context and thus execute the wrong bound expression.
Renaming is not obviously sufficient to ensure bound variable hygiene because of how
the machine manipulates evaluation contexts. For instance, even though the need rule is
guaranteed to only match a variable with the right binder frame, we have no guarantee
that the right binder frame could never be trapped inside a cont frame and hidden from
view while a need transition searches for it. Were this to happen, the machine would get
stuck. Furthermore, the reduction rules flip and shift evaluation contexts that might contain
binder frames. If a binder frame were to end up below another context frame that contains
references to its bound variable, then those references would no longer be bound in the
context; the need rule would exhaust the evaluation context if it attempted to resolve any
of these references.
To verify that machine evaluation is well-formed, we establish well-formedness conditions that suffice to ensure safe evaluation and we show that they hold for evaluation of
all programs. The well-formedness conditions rely on straightforward notions of captured
context variables (CV ) and free context variables (F V ):
CV ([ ])
CV (E ◦ [(λx.) t])
CV (E ◦ [ t])
CV (E ◦ [(κx.E1 ) ])

=
=
=
=

∅
{ x } ∪ CV (E)
CV (E)
CV (E)

F V ([ ])
F V ([(λx.) t] ◦ E)
F V ([ t] ◦ E)
F V ([(κx.E1 ) ] ◦ E)

=
=
=
=

∅
F V (t) ∪ (F V (E) − { x })
F V (E) ∪ F V (t)
F V (E) ∪ (F V (E1 ) − { x })

As expected, these two notions are related.
Lemma 4.5.
(1) F V (E1 ) ⊆ F V (E1 ◦ E2 ).
(2) CV (E1 ◦ E2 ) = CV (E1 ) ∪ CV (E2 ).
(3) F V (E1 ◦ E2 ) = F V (E1 ) ∪ (F V (E2 )\CV (E1 )).
Proof. By induction on the length of E1 , E2 , and E1 respectively.

14

R. GARCIA, A. LUMSDAINE, AND A. SABRY

To establish that binder frames remain properly positioned, we define a notion of wellformed evaluation contexts:
Definition 4.6. A Machine context/name pair is well formed, notation X | E wf, iff:
(1) F V (E) = ∅;
(2) AV (E) = { x | x occurs in X }
(3) Each active variable of E is distinct: if E1 ◦ E2 ∈ E then AV (E1 ) ∩ AV (E2 ) = ∅, and
if [(κx.E1 ) ] ∈ E then x ∈
/ AV (E1 ).
These well-formedness criteria ensure that a context has no unbound variable references,
that active variables cannot interfere with each other, and that X is simply a particular
ordering of the E’s active variables. The captured variables of E are also distinct since
every captured variable is an active variable.
Furthermore, machine configurations also have a notion of well-formedness:
X | E wf F V (?) ⊆ CV (E)
hX | E, ?ic wf

c 6≡ d

X | (E1 ◦ [(κx.E2 ) ] ◦ E3 ) wf F V (v) ⊆ CV (E1 ◦ [(κx.E2 ) ] ◦ E3 )
hX | E1 , (κx.E2 ) TE3 , vUid wf
X | (E1 ◦ [ t] ◦ E2 ) wf F V (v) ⊆ CV (E1 ◦ [ t] ◦ E2 )
hX | E1 , TE2 , vU t2 id wf
These well-formedness conditions ensure that the evaluation contexts E are well-formed,
that the list of names X matches the active variables of E, and that the free variables
of the term under focus are captured by the context. To account for redexes, the wellformedness conditions for each reduce configuration reflect the well-formedness conditions
for the corresponding rebuild configuration. As shown below, well-formed reduce configurations hX | E, rid wf ensure that reduce rules can be safely performed without implicit
renaming.
Well-formedness of the reduce configurations ensures that the reduce transitions require
no implicit bound-variable renaming to preserve hygiene. Well-formedness of the need
configuration guarantees that it cannot be “stuck”: since x ∈ CV (E), a well-formed need
configuration always has a binder frame [(λx.) t] that matches the variable under focus,
so the configuration can transition.
Well-formedness of configurations combined with rule D.2’s name management ensures
that machine evaluation respects variable binding structure.
Theorem 4.7. If t is a closed term of the calculus, then h∅ | [ ], tif wf.
Proof. ∅ | [ ] wf and F V (t) ⊆ CV ([ ]) = ∅.
Theorem 4.8. Let C1 and C2 be configurations. If C1 wf and C1 7−→nam C2 then C2 wf.
Proof. By cases on 7−→nam . The cases are immediate except when C1 7−→nam C2 by a
reduce rule. The proofs for both kinds of reduce configurations are similar, so we present
only one of the cases:
Case (C1 = hX | E1 , (κx.E2 ) TE3 , vUid ).
By definition, C1 7−→nam C2 = hX | E, vib , where E = E1 ◦ E3 ◦ [(λx.) v] ◦ E2 . Since the

LAZY EVALUATION AND DELIMITED CONTROL

15

transition rule introduces no new active variables, X should remain the same. Furthermore,
all the active variables remain distinct, though x is now introduced by the binder frame
[(λx.) v] rather than the cont frame [(κx.E2 ) ]. It remains to show that F V (v) ⊆ CV (E)
and that F V (E) = ∅.
First, since C1 wf, it follows by inversion that X | (E1 ◦ [(κx.E2 ) ] ◦ E3 ) wf and
F V (v) ⊆ CV (E1 ◦ [(κx.E2 ) ] ◦ E3 ) = CV (E1 ◦ E3 ) ⊆ CV (E).
By Lemma 4.5, F V (E1 ) = F V (E1 ◦ [(κx.E2 ) ]) = F V (E1 ◦ [(κx.E2 ) ] ◦ E3 ) = ∅.
Since CV ([(κx.E2 ) ]) = ∅, it follows from Lemma 4.5 that F V (E3 ) ⊆ CV (E1 ) and
from the definition of F V that F V (E2 ) ⊆ CV (E1 ) ∪ { x }. From these it follows that
F V (E) = ∅.

In short, well-formedness of the reduce configurations ensures that the reduce rules
can be safely performed without any implicit renaming. Since the machine preserves wellformedness, this property persists throughout evaluation. The rest of this paper only considers well-formed configurations.
4.6. An Abstract Machine for Call-by-need. Putting together our observations from
the previous section, we now present the specification of the abstract machine. Figure 1
presents its 7−→nam transitions rules. We have derived a heap-less abstract machine for
call-by-need evaluation. It replaces the traditional manipulation of a heap using store-based
effects with disciplined management of the evaluation stack using control-based effects. In
short, state is replaced with control.
Machine evaluation of a program t begins with h∅ | [ ], tif and terminates at hX | TE, vUi.
5. Correctness of the Machine
The previous section proves that the machine manipulates terms in a manner that
preserves variable binding. In this section, we prove that those manipulations correspond
to standard-order call-by-need evaluation.
To proceed, we first establish correspondences between abstract machine configurations and call-by-need terms. As we have alluded to previously, abstract machine contexts
correspond directly to calculus contexts:
C[[[ ]]]
C[[[ t] ◦ E]]
C[[[(κx.E1 ) ] ◦ E2 ]]
C[[[(λx.) t] ◦ E]]

=
=
=
=


C[[E]] t
(λx.C[[E1 ]][x]) C[[E2 ]]
(λx.C[[E]]) t

Redexes also map to call-by-need terms:
C[[TE, vU t]]
= (C[[E]][v]) t
C[[(κx.E1 ) TE2 , vU]] = (λx.C[[E1 ]][x]) (C[[E2 ]][v])
Given that terms map identically to terms, configuration mapping is defined uniformly:
C[[hX | E, ?i]] = C[[E]][ C[[?]] ]

16

R. GARCIA, A. LUMSDAINE, AND A. SABRY

hX | E, rid

(Reduce)

(D.1) hX | E1 , (κx.E2 ) TE3 , vUid
(D.2)
hX | E1 , TE2 , λx.t1 U t2 id
hX | E, tif
(F.1)
(F.2)
(F.3)

hX | E1 ◦ E3 ◦ [(λx.) v] ◦ E2 , vib
hX, x′ | E1 ◦ E2 ◦ [(λx′ .) t2 ], t1 [x′ /x]if

x′ ∈
/X

(Refocus)

hX | E, xif
hX | E, λx.tif
hX | E, t1 t2 if

hX | E, vib

7−→nam
7−→nam

7−→nam
7−→nam
7−→nam

hX | E, xin
hX | E, λx.tib
hX | E ◦ [ t2 ], t1 if

(Rebuild)

(B.1)
hX | Eb , vib
(B.2)
hX | E1 ◦ [ t] ◦ Eb , vib
(B.3) hX | E1 ◦ [(κx.E2 ) ] ◦ Eb , vib

7 →nam
−
7−→nam
7−→nam

hX | TEb , vUi
hX | E1 , TEb , vU tid
hX | E1 , (κx.E2 ) TEb , vUid

where Eb = [(λxi .) ti ]
hX | E, xin

(Need)

(N.1) hX | E1 ◦ [(λx.) t] ◦ E2 , xin
where [(λx.) t] ∈
/ E2

7−→nam

hX | E1 ◦ [(κx.E2 ) ], tif

Figure 1: Call-by-need Machine
Since the calculus is defined over alpha equivalence classes, we reason up to alpha equivalence
when relating terms to machine configurations.
We now state our fundamental correctness theorems. First we guarantee soundness,
the property that every step of the abstract machine respects standard-order reduction.
Theorem 5.1. If t1 = C[[C1 ]] and C1 7−→nam C2 , then t1 7−→
→sr t2 , for some t2 = C[[C2 ]].
Proof. By cases on 7−→nam . Only rules D.1 and D.2 are not immediate. The other rules
preserve equality under C[[C]].
Corollary 1 (Soundness).
If t = C[[C]] and C 7−→
→nam hX | TE, vUi, then t 7−→
→sr a, for some a = C[[hX | TE, vUi]].
Proof. By induction on the length of the 7−→
→nam sequence.
We also prove completeness, namely that abstract machine reduction subsumes standard order reduction.
Theorem 5.2 (Completeness).
If t = C[[C]] and t 7−→
→sr a, then C 7−→
→nam hX | TE, vUi, with a = C[[hX | TE, vUi]].
Proof. This proof proceeds by induction on the length of 7−→
→sr sequences. It utilizes
Proposition 4.4 to accelerate the 7−→sr rules in accordance with 7−→nam . It also relies on a
number of lemmas to establish that 7−→nam will find the unique redex of a term from any
decomposition of a term into a context E and a subterm t.

LAZY EVALUATION AND DELIMITED CONTROL

17

Theorem 5.3 (Correctness). If t = C[[C]], then
t 7−→
→sr a

if and only if

C 7−→
→nam hX | TE, vUi

with a = C[[hX | TE, vUi]].
5.1. Discussion. This abstract machine has nice inductive properties. The refocus rules
always dispatch on the outermost term constructor. The rebuild and need rules dispatch
on a prefix of the context, though each has different criteria for bounding the prefix.
The abstract machine’s evaluation steps should not be seen as merely a desperate search
for a redex. Rather, the machine exposes the fine-grain structure of call-by-need evaluation,
just as the CK machine and the Krivine machine (Krivine, 2007) model evaluation for callby-value and call-by-name respectively. Answers are the partial results of computations, and
the rebuild rules represent the process of reconstructing and returning a result to a reduction
site. Furthermore, the need rules can be viewed as a novel form of variable-lookup combined
with lazy evaluation. The evaluation context captures the rest of computation, but not in
order: variable references cause evaluation to skip around in a manner that is difficult to
predict.
The way that variables behave in these semantics reveals a connection to coroutines.
The reduction rule D.2 binds a variable to a delayed computation; referencing that variable
suspends the current computation and jumps to its associated delayed computation. Upon
completion of that computation, any newly delayed computations (i.e. binder frames) are
added to the evaluation context and the original computation is resumed.
The standard-order reduction relation of the call-by-need lambda calculus defines an
evaluator concisely but abstractly. Surely unique decomposition, standardization, and hygiene ensure the existence of a deterministic evaluator, but these properties do not spell out
the details or implications. Based on a reasoned inspection of standard-order reduction, we
expose its computational behavior and capture it in a novel abstract machine that has no
store. The improvements to the initial machine produce a variant that effectively assimilates computational information, explicitly accounts for variable hygiene and thereby reveals
coarse-grained operational structure implicit in call-by-need standard-order evaluation.
5.2. Extensions. The machine presented above describes evaluation only for the pure
lambda calculus. In this subsection, we introduce some features that are typical of pragmatic programming languages.
5.2.1. Let binding. To help with a proof that the call-by-need calculus can simulate callby-name, Ariola and Felleisen introduce a let-based calculus. The let-calculus adds the
construction let x = t in t to the set of terms and considers a new axiom:
(λx.t1 ) t2 = let x = t2 in t1
The let-calculus is formulated by taking this axiom as a reduction rule running from left to
right, and reformulating the original three axioms of the call-by-need calculus in terms of
let expressions. These new axioms can be justified by proving that they are derivable from
the original three axioms and the new let axiom.
One approach to producing an abstract machine that supports let is to repeat the
entire process described in this section, but focusing on the let-calculus instead of the

18

R. GARCIA, A. LUMSDAINE, AND A. SABRY

lambda calculus. However, let-binding can be retro-fitted to the current lambda calculus
much more simply by reading the new let axiom as a right-to-left reduction rule:
let x = t2 in t1 →need (λx.t1 ) t2
Essentially, this rule indicates that let bindings in the calculus can be understood as equivalent to an immediate application of an abstraction to a term.
The consequences for the naı̈ve machine are the addition of a new kind of redex:
r ::= . . . | let x = t2 in t1
and a new refocus rule:
hE, let x = t2 in t1 if 7→ hE, let x = t2 in t1 id
and a new reduce rule:
hE, let x = t2 in t1 id 7→ hE, (λx.t1 ) t2 if
Then, in the process of improving our machine, the reduce rule can be fast-forwarded to
reduce the introduced abstraction and application immediately:
hX | E, let x = t2 in t1 id 7→ X, x′ E ◦ [(λx′ .) t2 ], t1 [x′ /x]

f

This process confirms that the let expression form can be comfortably treated as a
conservative extension of the call-by-need lambda calculus. Its addition does not force a
radical reconstruction of the abstract machine. As we show in Section 5.4, adding a circular
letrec construct to the language fundamentally alters the system.
5.2.2. Constants. Plotkin (1975) augments the lambda calculus with two sets of constants,
the basic constants b and the function constants f . In that language, the basic constants
are observables and serve as placeholders for real programming language constants like
numbers, strings, and so on. The function constants serve as placeholders for real primitive
functions, generally over basic constants. The function constants are not first-class values
in the language, but instead appear as operators in primitive function expressions.
t ::= . . . | b | f t
v ::= . . . | b
Function expressions always take a single term argument.
The calculus is parametrized on a partial function δ that maps function-value pairs to
values. As is standard, the notions of reduction for the calculus are augmented to handle
function constant applications.
f v1 →need

v2 if δ(f, v1 ) = v2

Since the notions of reduction for function constants require them to be applied to values,
the calculus must account for answers. To handle this, the calculus can be extended with
a rule to commute answer bindings with function expressions, as is done for application
expressions:
f ((λx.a) t) →need (λx.f a) t
If function expressions were only defined for basic constant arguments, then answer bindings could be discarded instead of commuted. However this approach imposes an ad hoc

LAZY EVALUATION AND DELIMITED CONTROL

19

limitation on the semantics. It would be cleaner and more orthogonal to uniformly handle
garbage collection with a specific notion of reduction (Ariola and Felleisen, 1997).
Function constants must be considered in the evaluation contexts. A function constant
must force its argument in order to produce a value, so upon encountering a function
constant application, evaluation must continue in its argument:
E ::= . . . | f E
The other notions of reduction remain exactly the same, but since basic constants are
values, they are subject to rules that manipulate values and answers. For example, if the set
of basic constants includes numbers and the set of function constants includes operations
on numbers, then by the deref rule:
(λx.add1 x) 5 →need (λx.add1 5) 5
The abstract machine requires few changes to accommodate these additions. The set
of redexes is extended to include function expressions:
r ::= . . . | f a
The refocus rules are generalized to create context frames for function constant applications
and to rebuild when any value, lambda abstraction or basic constant, is encountered:
hX | E, f tif
hX | E, vif

7−→nam hX | E ◦ [f ], tif
7−→nam hX | E, vib

Furthermore, rebuild must account for function constant applications:
hX | E ◦ [f ] ◦ Eb , vif 7−→nam hX | E, f TEb , vUid
Finally, the reduce rule for f a, pushes binder frames upwards and appeals to the delta rule
δ(f, v) for its result:
hX | E, f TEb , vUid 7−→nam hX | E ◦ Eb , δ(f, v)ib
Since δ(f, v) yields only values, the reduce configuration for f a can immediately transition
to rebuild from this result.
5.3. Lazy Constructors. As pointed out by Ariola and Felleisen (1997), the call-by-need
lambda calculus can be easily extended with support for lazy constructors. The rules for
constructors and destructors can be inferred from the church encoding for pairs:
cons ≡ λx1 .λx2 .λd.d x1 x2
car ≡ λp.p (λx1 .λx2 .x1 )
cdr ≡ λp.p (λx1 .λx2 .x2 )
To add support for lazy pairs, we first extend the syntax of the language:
t ::= . . . | cons t t | car t | cdr t | hx, xi
v ::= . . . | hx, xi
E ::= . . . | car E | cdr E
The cons t1 t2 expression creates a lazy pair of its two arguments, t1 and t2 . The car t
and cdr t expressions evaluate their respective arguments and extract the first or second
element of the resulting pair. As with function constants in the previous section, the lazy
pair constructor and destructors are second-class. To express first-class constructors, these

20

R. GARCIA, A. LUMSDAINE, AND A. SABRY

may be eta-expanded into, e.g., λx1 .λx2 .cons x1 x2 . The hx1 , x2 i value is a representation
of a lazy pair. It contains variables that refer to shared computations.
According to the evaluation contexts, evaluation may focus on the argument of a car
or cdr expression. However, evaluation never directly operates on the arguments to a
constructor. This is why the evaluation contexts for the language do not examine the
arguments to cons. As a direct consequence, the standard call-by-need reduction rules will
never substitute a value for a variable inside a pair. A variable inside a pair can only be
evaluated after decomposing the pair using car or cdr.
The Church encoding of pairs motivates the following notions of reduction:
cons t1 t2 →need
car hx1 , x2 i →need
cdr hx1 , x2 i →need

(λx1 .(λx2 . hx1 , x2 i) t2 ) t1
x1
x2

These rules model cons as it is applied to two arguments. The car and cdr operations each
expose a previously inaccessible variable reference to evaluation.
To accommodate lazy pairs in the abstract machine, we extend the set of redexes:
r ::= . . . | cons t1 t2 | car a | cdr a
and we introduce several new rules. The first set of rules extends the refocus stage of the
machine to handle our extensions.
hX | E, cons t1 t2 if
hX | E, car tif
hX | E, cdr tif

7 →nam hX | E, cons t1 t2 id
−
7−→nam hX | E ◦ [car ], tif
7−→nam hX | E ◦ [cdr ], tif

A cons expression is immediately ready for reduction. The car and cdr expressions proceed
to evaluate their respective arguments. Another set of rules returns an answer to car or
cdr.
hX | E ◦ [car ] ◦ Eb , vib 7−→nam hX | E, car TEb , vUid
hX | E ◦ [cdr ] ◦ Eb , vib 7−→nam hX | E, cdr TEb , vUid
Finally, a set of rules corresponds to the notions of reduction.
hX | E, cons t1 t2 id −
7 →nam hX, x1 , x2 | E ◦ [(λx1 .) t1 ] ◦ [(λx2 .) t2 ], hx1 , x2 iib
hX | E1 , car TE2 , hx1 , x2 iUid −
7 →nam hX | E1 ◦ E2 , x1 in
hX | E2 , cdr TE2 , hx1 , x2 iUid 7−→nam hX | E1 ◦ E2 , x2 in
Lazy pair construction creates new binder frames for the two terms and produces a pair that
references them. To evaluate a destructor, the binder frames associated with the answer
are pushed upwards and the corresponding variable reference is extracted from the pair and
the value of its associated computation is demanded.
5.4. Circularity. As pointed out by Ariola et al. (1995), the presence of constructors
makes it possible to observe duplicated constructors when the Y combinator is used to
express recursion.
Consider the expression:
Y (λy.cons 1 y) ≡ (λf.(λx.f (x x)) (λx.f (x x))) (λy.cons 1 y)

LAZY EVALUATION AND DELIMITED CONTROL

21

Standard-order reduction in the calculus proceeds as follows, underlining either the
active variable reference or the current redex:
(λf.(λx.f (x x)) (λx.f (x x))) (λy.cons 1 y)
→need (λf.(λx.(λy.cons 1 y) (x x)) (λx.f (x x))) (λy.cons 1 y)
→need (λf.(λx.(λy.(λx1 .(λx2 . hx1 , x2 i) y) 1) (x x)) (λx.f (x x))) (λy.cons 1 y)
Because of the two references to f in Y, the term (λy.cons 1 y) is copied and ultimately
recomputed each time the term is needed. Ideally a recursive hx, xi value could refer to
itself and not recompute its value whenever its cdr is demanded. Duplicated computation
does not correspond to how recursion and lazy constructors interact in typical semantics for
lazy evaluation (Henderson and Morris, 1976). An implementation would create a single
self-referencing cons cell.
Because of the scoping rules for λ, there is no way to explicitly define truly circular
structures in this calculus. To address this, Ariola and Felleisen introduce a letrec-based
calculus, inspired by the circular calculus of Ariola and Klop (1994, 1997). The syntax of
the letrec-calculus follows:
t
D
v
a
E

::=
::=
::=
::=
::=
|
|
D[x, xn ] ::=

x | λx.t | t t | letrec D in t
x1 be t1 , . . . , xn be tn
λx.t
v | letrec D in a
 | E t | letrec D in E
letrec D, x be E in E[x]
letrec xn be E, D[x, xn ] in E[x]
x be E[x1 ], x1 be E[x2 ], . . . , xn−1 be E[xn ], D

The letrec-calculus is similar to the let-calculus in how it adds an explicit binding form, but
each letrec expression can contain an unordered set D of mutually recursive bindings x be t
for distinct variables.
The evaluation contexts for the letrec-calculus resemble those for the let-calculus. The
contexts letrec D, x be E in E[x] and letrec xn be E, D[x, xn ] in E[x] represent evaluation taking place in the binding position of a letrec expression. The first form expresses that a
variable has been referenced in the body of the letrec and that variable’s definition is currently under evaluation. The second form expresses that some variables bound in the letrec
form depend on each other, and a variable reference in the body of the letrec has forced
evaluation of this chain of variable references. This chain of dependencies is denoted by the
syntax D[x, xn ]. The definition of the last referenced variable in the chain of dependencies,
xn , is currently being evaluated. For evaluation to proceed, all the variables in a chain of
dependencies must be disjoint. The letrec calculus regards a cyclic dependency chain as a
diverging computation, a stuck expression that is not a valid answer.

22

R. GARCIA, A. LUMSDAINE, AND A. SABRY

The notions of reduction for the letrec calculus follow:
(1)
(2)
(3)
(4)
(5)

(λx.t1 ) t2
letrec D, x be v in E[x]
letrec xn be v, D[x, xn ] in E[x]
(letrec D in a) t
letrec xn be (letrec D in a), D[x, xn ]
in E[x]
(6) letrec D1 , x be (letrec D2 in a) in E[x]

→need
→need
→need
→need
→need

letrec x be t2 in t1
letrec D, x be v, in E[v]
letrec xn be v, D[x, v] in E[x]
letrec D in a t
letrec D, xn be a, D[x, xn ] in E[x]

→need letrec D2 , D1 , x be a in E[x]

The rules operate as follows. Rule (1) is analogous to the equivalent let-calculus rule.
Rule (2) is analogous to the basic dereference rule. Rule (3) resolves the last variable
reference in a chain of dependency. The syntax D[x, v] expresses replacing xn−1 be E[xn ]
with xn−1 be E[v] in the list of bindings. Rules (4) through (6) are associativity rules that
percolate bindings upward to ensure proper sharing. Rules (5) and (6) are important for
recursion. They lift recursive bindings from the definition of a letrec-bound variable x and
incorporate them into the same letrec expression that binds x. In essence they expand the
set of variables bound by the outer letrec expression.
Using the letrec-calculus, the corresponding example using cons is as follows:
letrec y be cons 1 y in y

→need letrec y be (letrec x1 be 1 in (letrec x2 be y in hx1 , x2 i)) in y
→need letrec x1 be 1, y be (letrec x2 be y in hx1 , x2 i) in y
→need letrec x1 be 1, x2 be y, y be hx1 , x2 i in y
→need letrec x1 be 1, x2 be y, y be hx1 , x2 i in hx1 , x2 i
In this reduction, the recursive cons cell has been computed once and for all. No reference
to the original cons lazy constructor remains.
5.4.1. The letrec machine. Now we express the call-by-need letrec-calculus as an abstract
machine. Development of this machine proceeds along the same lines as the non-circular
machine.
As described in the calculus, letrec bindings need not be ordered, but dependency chains
have a natural order imposed by the order of dependencies. Furthermore, cyclic dependency
chains are provable divergences in the letrec-calculus. In the face of such a cycle, a program
is no longer subject to reduction. We can model this by letting the machine get “stuck”.
The basic terms for the machine remain close to those of the calculus:
t ::= x | λx.t | t t | letrec D + in t
D ::= xi be ti
v ::= λx.t
As with the calculus, D refers to sets of recursive bindings. As needed, we distinguish
possibly empty sets of bindings, D ∗ , from nonempty sets D + . This precision is needed to
discuss machine behavior. The values of this machine are the lambda abstractions, but now
answers are defined as values wrapped in zero or more tiers of letrec bindings.
As we did for the prior machine, we introduce some representation changes that help
with presenting the letrec-machine. The evaluation context is once again replaced with a

LAZY EVALUATION AND DELIMITED CONTROL

23

list of context frames.
Pxx0n ::= {hxn , En i :: hxn−1 , En−1 i :: · · · :: hx0 , E0 i}
f
::=  t | LR D + in 
| LR x be , D ∗ in E
| LR xn+1 be , Pxx0n , D ∗ in E
E
::= [ ] | [f ] ◦ E | E ◦ [f ]
where E ◦ [ ] = [ ] ◦ E = E
and E1 ◦ (E2 ◦ E3 ) = (E1 ◦ E2 ) ◦ E3
The operand frame [ t] and binding frame [LR D + in ] are directly analogous to the corresponding frames in the original abstract machine. The original cont frame, on the other
hand, splits into two variants. The frame [LR xn+1 be , Pxxn0 , D ∗ in E[x0 ]] captures chain of
dependencies that is currently under evaluation. The expression D ∗ stands for the inactive
bindings in the frame, while the expression Pxxn0 indicates a chain of dependencies. While
no particular ordering is imposed on the bindings in D ∗ , the chain of dependencies represented by Pxx0n is ordered. Our machine representation separates dependencies from other
bindings. In the calculus, D[x0 , xn ] also includes any other bindings D. In the machine,
Pxx0n only captures the dependencies, and the other bindings D ∗ are explicitly indicated.
Machine dependencies Pxx0n ≡ {hxn , En i :: hxn−1 , En−1 i :: · · · :: hx0 , E0 i} correspond to calx
culus dependencies D[x0 , xn ] ≡ x be E[x1 ], x1 be E[x2 ], . . . , xn−1 be E[xn ]. We allow Px0−1
to denote an empty chain. Observe that the order of the machine dependencies is reversed.
This ordering expresses that dependencies are resolved in last-in first-out order. When the
value of xn+1 is computed, its value will be used to compute the value of xn and so on
until the value of x0 is computed and its value is returned to the body of the letrec expression. Machine dependencies form a stack of computations that reference one another. This
behavior is clarified in the behavior of the cyclic abstract machine.
The frame [LR x be , D ∗ in E] closely resembles the old cont frame [(κx.E) ], except
that the LR form may bind other variables as well. The absence of Pxx0n in this frame
explicitly indicates that it has no chain of dependencies to be evaluated before substituting
into the body of the LR .
Machine answers are still binding-value pairs, but now each binding is a recursive binding of multiple variables.
a ::= TE, vU where E = [LR Di+ in ]
The set of redexes for the abstract machine follows.
r ::= a t
| LR x be a, D ∗ in E
| LR xn+1 be a, Pxx0n , D ∗ in E
The first redex form is the same as a form from the original machine. The second form is
analogous to the (κx.E) a form from the original machine. The final redex form captures
the case where one link in the chain of dependencies is about to be resolved.
Figure 2 presents the transition rules of the cyclic abstract machine. The machine relies
on an operator F(Eb ), which given a list of binder frames [LR Di+ in ], flattens them into
a single binder frame [LR Di+ in ]. This operation captures in aggregate the treatment of
bindings by rules (5) and (6) of the calculus.

24

R. GARCIA, A. LUMSDAINE, AND A. SABRY

The first three refocus rules are the same as the lambda calculus, while the fourth rule
is analogous to the equivalent rule for the let-calculus. The rebuild rules are also analogous
to the lambda calculus, though now the binder frames have the form [LR Di+ in ].
The letrec-machine has two need rules, (N.1) for a variable reference in the body of
the corresponding letrec , and (N.2) for a variable reference that extends a (possible empty)
chain of dependencies. The need rule does not consider variable bindings that are currently
in a dependency chain, so evaluation will get stuck upon arriving at a cycle.
There are four reduce rules. The (D.1) rule, substitutes a value into the body of a
letrec after its value has been computed. The (D.2) rule resolves the most recent reference
in a chain of dependencies. Having computed the value of xn+1 , it returns to computing the
value of xn , which needed xn+1 ’s value. If the chain of dependencies has only one element
(i.e. Pxx00 ), then the chain is fully resolved. The (D.3) rule handles when an answer is
applied to an expression. It combines calculus rules (4) and (1). Finally, the (D.4) rule
handles letrec occurrences in the source program. In order to address hygiene, this rule
must simultaneously substitute for every bound variable in each binding as it focuses on
the body of the letrec expression.
The following is a machine trace of the cyclic cons example:
7→
7→
7→
7→
7→
7→
7→
7→
7→

h∅ | [ ], letrec y be cons 1 y in yif
h∅ | [ ], letrec y be cons 1 y in yid
h{ y } | [LR y be cons 1 y in ], yif
h{ y } | [LR y be cons 1 y in ], yin
h{ y } | [LR y be  in [ ]], cons 1 yif
h{ y } | [LR y be  in [ ]], cons 1 yid
h{ y, x1 , x2 } | [LR y be  in [ ]] ◦ [LR x1 be 1 in ] ◦ [LR x2 be y in ], hx1 , x2 iib
h{ y, x1 , x2 } | [ ], LR y be T[LR x1 be 1 in ] ◦ [LR x2 be y in ], hx1 , x2 iU in [ ]id
h{ y, x1 , x2 } | [LR y be hx1 , x2 i, x1 be 1, x2 be y in ], hx1 , x2 iib
h{ y, x1 , x2 } | T[LR y be hx1 , x2 i, x1 be 1, x2 be y in ], hx1 , x2 iUi
6. Simulating Call-by-need Using Control

As we allude to above, call-by-need machine evaluation is highly suggestive of delimited
control operations, but the connection is indirect and mixed with the other details of lazy
evaluation. In this section, we directly interpret this connection in the terminology of
delimited control.
Based on the operational behavior of the abstract machine from Figure 1, we derive a
simulation of call-by-need execution under call-by-value augmented with delimited control
operators. In particular, we translate call-by-need terms into the framework of Dybvig et al.
(2007). First we overview the language of delimited control operations. Then we describe
how the abstract machine performs delimited control operations. Next we present the
simulation of call-by-need using delimited control. Finally we show its correctness.

hX | E, rid
(D.1)
(D.2)
(D.3)
(D.4)

hX | E1 , (LR x be TE2 , vU, D∗ in E3 )id
X E1 , (LR xn+1 be TE2 , vU, Pxx0n , D∗ in E3 ) d
D hX | E1 , TE2 , λx.t1 U t2Eid
X E, letrec xi be ti in t

hX | E, tif

7−→nam
7−→nam
7−→nam
7−→nam

(N.1)

f

x′i ∩ X = ∅

hX | E, xin
hX | E, λx.tib
hX | E ◦ [ t2 ], t1 if
hX | E, letrec D+ in tid

(Rebuild)

(B.1)
hX | Eb , vib
(B.2)
hX | E1 ◦ [ t] ◦ Eb , vib
(B.3)
hX | E1 ◦ [(LR x be , D∗ in E2 )] ◦ Eb , vib
(B.4) X E1 ◦ [(LR xn+1 be , Pxx0n , D∗ in E2 ] ◦ Eb , v b
where Eb = [LR Di+ in ]
hX | E, xin

X, x′i E ◦ [LR x′i be ti [x′i /xi ] in ], t

7−→nam

b

(Refocus)

hX | E, xif
hX | E, λx.tif
hX | E, t1 t2 if
hX | E, letrec D+ in tif

hX | E, vib

d

hX | E1 ◦ [LR x be v, F (E2 ), D∗ in ] ◦ E3 , vib
x
X E1 ◦ [LR xn be , Px0n−1 , xn+1 be v, F (E2 ), D∗ in E3 ] ◦ En , v
′
′
′
′
hX,
/X
D x | E1 ◦ E2 ◦ [LR x be t2 in ], t1 [x
E /x]if x ∈

7−→nam
7−→nam
7−→nam

LAZY EVALUATION AND DELIMITED CONTROL

(F.1)
(F.2)
(F.3)
(F.4)

(Reduce)

7−→nam
7−→nam
7−→nam
7−→nam

hX | TEb , vUi
hX | E1 , TEb , vU tid
hX | E1 , (LR x be TEb , vU, D∗ in E2 )id
X E1 , (LR xn+1 be TEb , vU, Pxx0n , D∗ in E2 )

d

(Need)
D

E
X E1 ◦ [LR (x be t, D∗ ) in ] ◦ E2† , x

(N.2) X E1 ◦ [LR xn be
where (x be t) ∈
/ E†

x
, Px0n−1 , (x

be t, D∗ ) in E2 ] ◦ En† , x

n
n

7−→nam
7−→nam

hX | E1 ◦ [LR x be , D∗ in E2 ], tif
X E1 ◦ [LR x be , Pxx0n , D∗ in E2 ], t

f

Figure 2: Letrec Machine

25

26

R. GARCIA, A. LUMSDAINE, AND A. SABRY

6.1. Delimited Control Operators. Dybvig et al. (2007) define a language with delimited control operators. We explain these operators using a simplified variant of the defining
machine semantics.
t
v
E

M
p

::=
|
::=
::=
|
|
::=
∈

x | v | t t | newPrompt | pushPrompt t t
withSubCont t t | pushSubCont t t
λx.t | p | hM i
 | E[ t] | E[(λx.t) ] | E[pushPrompt  t]
E[withSubCont  t] | E[withSubCont p ]
E[pushSubCont  t]
[]|E:M |p:M

N

The language extends the call-by-value untyped lambda calculus with the four operators
newPrompt, pushPrompt, withSubCont, and pushSubCont as well as two new values: firstclass prompts p, and first-class delimited continuations hM i. Its control structure is defined
using evaluation contexts E, and metacontexts M , which are lists that interleave prompts
and contexts. Metacontexts use Haskell list notation. Prompts are modeled using natural
numbers.
A program state comprises an expression t, continuation E, metacontinuation M , and
fresh prompt source p. The initial state for a program t is [t], [ ], 0.
E[(λx.t) v], M, p
E[newPrompt], M, p
E[pushPrompt p1 t], M, p2
E[withSubCont p1 λx.t], M1 ++(p1 : M2 ), p2
where p1 ∈
/ M1
E[pushSubCont hM1 i t], M2 , p
[v], E : M, p
[v], p1 : M, p2

7
→
7→
7
→
7
→

E[t[v/x]], M, p
E[p], M, p + 1
[t], p1 : E : M, p2
[t[hE : M1 i /x]], M2 , p2

7
→
[t], M1 ++(E : M2 ), p
7→ E[v], M, p
7
→
[v], M, p2

The four operators manipulate delimited continuations, or subcontinuations, which are
part of an execution context. The withSubCont operator takes a prompt and a function; it
captures the smallest subcontinuation that is delimited by the prompt and passes it to the
function. The non-captured part of the continuation becomes the new continuation. The
prompt instance that delimited the captured subcontinuation is discarded: it appears in
neither the captured subcontinuation nor the current continuation. This operator generalizes F (Felleisen, 1988) and shift (Danvy and Filinski, 1990).
The pushSubCont operator takes a subcontinuation and an expression; it composes the
subcontinuation with the current continuation and proceeds to evaluate its second argument
in the newly extended continuation.
The pushPrompt operator takes a prompt and an expression; it extends the current
continuation with the prompt and evaluates the expression in the newly extended continuation. The newPrompt operator returns a distinguished fresh prompt each time it is
called. These two operators generalize the delimiting operators # (Felleisen, 1988) and

LAZY EVALUATION AND DELIMITED CONTROL

27

reset (Danvy and Filinski, 1990), which extend a continuation with a single common delimiter.
To illustrate these operators in action, we consider a program that uses arithmetic and
conditionals:
let p = newPrompt
in 2 + pushPrompt p
if (withSubCont p
(λk.(pushSubCont k False)+
(pushSubCont k True)))
then 3
else 4
A fresh prompt is bound to p and pushed onto the continuation just prior to evaluation
of the if expression. withSubCont captures the subcontinuation [if  then 3 else 4], which
was delimited by p, and binds it to k. The subcontinuation k is pushed twice, given the
value False the first time and True the second. The result of evaluation is the expression
2 + 4 + 3 which yields 9.
6.2. Delimited Control Naı̈vely Simulates the Machine. The call-by-need abstract
machine performs two different kinds of partial control capture. To review, the rebuild and
need rules of the abstract machine both capture some portion of the evaluation context.
In particular, the rebuild rules capture binder frames. If only binder frames remain, then
execution is complete. When either of the other frames is found, then a reduction is performed. On the other hand, the need rule captures the evaluation context up to the binder
that matches the variable whose value is needed.
These actions of the abstract machine can be recast in the language of delimited control
capture. First, the need rule uses the identity of its variable, which must be an active
variable, to delimit the context it captures. The well-formedness conditions from Section 4.5
guarantee that each binder frame binds a unique variable, so each active variable acts as
a unique delimiter. Second, the rebuild rule uses the nearest non-binder frame to delimit
the context it captures. This means that rebuild operates as though the operand frames,
the cont frames, and the top of the evaluation context share a common delimiter. This
guarantees that only binder frames are captured (as is stipulated in the rules).
In short, call-by-need evaluation captures partial evaluation contexts. These partial
evaluation contexts correspond to delimited continuations, and there are two different kinds
of delimitation, redex-based (for rebuild) and binder-based (for need).
It is useful to also consider how the machine manipulates these delimited continuations.
Each reduce rule in Figure 1 immediately pushes the context associated with an answer onto
the current evaluation context. In this manner, binders are consistently moved above the
point of evaluation. The reduce rule then operates on the value part of the answer and the
associated cont (for D.1) or term (for D.2).
Although each reduce rule pushes binders onto the evaluation context, only the D.2 rule
creates new binders. The variable bound by the answer’s underlying lambda abstraction
may already be a member of the set X, in which case it must be alpha-converted to a fresh
name with respect to the set X. Also note that if λx.t is alpha converted to λx′ .t[x′ /x], the
body under call-by-value satisfies the equation t[x′ /x] = (λx.t) x′ . Since we are using the
identifiers x′ as delimiters, and we never turn the binder frame [(λx′ .) t] back into a term,
we can replace fresh variables x′ with fresh prompts (Balat et al., 2004).

28

R. GARCIA, A. LUMSDAINE, AND A. SABRY

Let s be a distinguished identifier:
N P [[t]] = runCC (let s = newPrompt in pushPrompt s N [[t]])
N [[x]] = need x
N [[t1 t2 ]] = do va ⇐ N [[t1 ]]
in let xp = newPrompt
in delay N [[t2 ]] as xp in (va xp )
N [[λx.t]] = return λx.N [[t]]

return va ≡ withSubCont s λka . hka , va i
do x ⇐ t1 in t2 ≡ let hka , xi = pushPrompt s t1
in pushSubCont ka t2
delay t1 as x in t2 ≡ let fk = pushPrompt x t2
in fk λ().t1
force f ≡ f ()
need x ≡ withSubCont x λk.
λfth .do va ⇐ force fth
in delay (return va ) as x
in pushSubCont k (return va )

Figure 3: Translating CBN to CBV+Control
From these observations, we construct the simulation in Figure 3. The simulation can
be understood as a direct encoding of the abstract machine semantics for call-by-need.
To execute a program, N P [[t]], the transformation uses runCC to initiate a control-based
computation, acquires a fresh prompt, and binds it to a distinguished variable s. This
prompt is the redex prompt, which is used to delimit every continuation that denotes a
redex.
To expose the conceptual structure of the simulation, we define five syntactic macros,
do, return, delay, force, and need. We accord no formal properties to them: they merely
simplify the presentation. The return macro captures the nearest subcontinuation that is
delimited by the redex prompt s. Since the s delimiter appears before every reduction,
the captured continuation is guaranteed to contain only code equivalent to binder frames.
The translation returns a tuple containing the subcontinuation and the argument to return,
which must be a value; the tuple represents an answer. So the translation rule for lambda
abstractions, N [[λx.t]], literally simulates the rebuild rules.
The do macro executes a term t1 under the current continuation extended with the
redex prompt. If the term returns an answer hka , xi it immediately pushes the subcontinuation part and continues execution, binding the value part to the variable x. As such, the
translation rule for applications, N [[t1 t2 ]], executes [[t1 ]] and binds the resulting operator to

LAZY EVALUATION AND DELIMITED CONTROL

29

va . The answer binders are pushed by the do macro, which starts the simulation of the D.2
rule.
The remainder of the D.2 rule is subtle. In the abstract machine, binder frame variables
delimit the need rules. Since the delimited continuation framework relies on prompts to
delimit continuations, fresh prompts literally substitute for variables (Kiselyov et al., 2006).
The translation uses newPrompt to acquire a fresh prompt xp and then uses the delay macro
to simulate pushing a binder frame: the context delay t as x in  is analogous to the binder
frame [(λx.) t]. The delay macro anticipates that its body returns a function fk that
expects the delayed argument, so it applies fk to a suspension of t. As we see below, the
function fk is a cont (κx.E).
In the context of delay, the simulation executes va xp . Since alpha conversion of λx.t can
be written (λxp .t[xp /x]), the term va xp is analogous to (λx.t) xp = t[xp /x]: it substitutes
a fresh prompt for a fresh variable.
The need macro, which defines the translation rule for variables, N [[x]], captures the
continuation delimited by x (which had better be a prompt!) and returns a function λfth . . . .
that closes over both x and the captured continuation k. This function is the cont κx.E,
with x modeling the bound variable of the same name, and continuation k modeling E.
The function expects the binder frame [(λx.) t], which is now at the top of the current
continuation, to pass it the suspension λ().N [[t]]. The simulation forces the suspension, and
the do macro pushes the resulting answer binders and binds va to the underlying value.
Pushing the answer binders begins the simulation of the D.1 rule.
The simulation of D.1 delays a computation that immediately returns the result va of
evaluating the term t, pushes the continuation k associated with the cont, and returns va
to the extended continuation. Now any subsequent evaluation of x immediately returns the
memoized value va instead of recomputing t. This yields an answer hka , va i where ka is an
empty subcontinuation. The value va is delayed exactly as before and is also returned from
the properly extended continuation. This part of the translation bears close resemblance
to the paradoxical Y combinator (Curry and Feys, 1958), suggesting that the simulation
requires recursive types (Shan, 2007).
7. Correctness of the Simulation
We prove correctness of the simulation relative to the machine semantics. Since we
already proved correctness of the machine semantics relative to standard-order reduction,
the result is a proof that our simulation provides a continuation semantics for call-by-need.
The previous discussion provides an informal justification for the structure of the callby-need simulation. To prove the correctness of the simulation, we appeal to the continuation semantics for delimited control (Dybvig et al., 2007). This semantics is completely
standard for the terms of the lambda calculus. Figure 4 presents the interesting parts of
the semantics. All CPS terms take a standard continuation κ, but the control combinators
also take a metacontinuation γ, which is a list of continuations and prompts, and a global
prompt counter q. The base continuation κ0 delimits each proper continuation and directs
evaluation up the metacontinuation, discarding any intervening prompts. Given a CPS
program t, the expression t κ0 [ ] 0 runs it.
To prove correctness, we compose N [[·]] with the delimited continuation semantics to
produce a translation Λ[[·]] to the λβη calculus augmented with arithmetic, lists, and the

30

R. GARCIA, A. LUMSDAINE, AND A. SABRY

newP romptc = λκ.λγ.λq.κ q γ (q + 1)
withSubContc = λp.λf.λκ.λγ.f (κ : γ↑p ) κ0 γ↓p
pushP romptc = λp.λt.λκ.λγ.t κ0 (p : κ : γ)
pushSubContc = λγ ′ .λt.λκ.λγ.t κ0 (γ ′++(κ : γ))
κ0 = λv.λγλq.K(v, γ, q)
K(v, [ ], q) = v
K(v, p : γ, q) = K(v, γ, q)
K(v, κ : γ, q) = κ v γ q

Figure 4: Delimited Control Combinators
operator K defined in Figure 4. We also give each abstract machine configuration a denotation, defined in terms of name-indexed denotations for its constituents D[[·]]X (see Figures 5
through 8).
D[[t]]X = Λ[[t]][ι(xi , X)/xi ]
ΛP [[t]] = Λ[[t]] κ0 (0 : [ ]) 1
Λ[[x]] =
withSubContc x
λkx .λk1 .k1
λfth .λk2 .
pushPromptc 0 (fth ())
(λ hka , va i.
pushSubContc ka
(λk3 .
pushPromptc x
(pushSubContc kx
(withSubContc 0 λka .λk.k hka , va i))
(λfk .fk (λ().withSubContc 0
λka .λk.k hka , va i)
k3 ))
k2 )
Λ[[t1 t2 ]] = λk1 .pushPromptc 0 Λ[[t1 ]]
(λ hka , va i.
pushSubContc ka
(λk2 .
newPromptc
λxp .pushPromptc xp (va xp )
(λfk .fk (λ().Λ[[t2 ]]) k2 ))
k1 )
Λ[[λx.t]] = withSubContc 0 λka .λk.k hka , λx.Λ[t℄i

Figure 5: Denotations for Terms

LAZY EVALUATION AND DELIMITED CONTROL

31

ι(xi , X) = ι(xi , [x1 , x2 , . . . , xi , . . . , xn ]) = i
|X| = |[x1 , x2 , . . . , xi , . . . , xn ]| = n
Λ[[hX | E, ?ic ]] = D[[?]]X κ0 (D[[E]]X ++(0 : [ ])) (|X| + 1) c ∈ { d, f, b, n }
Λ[[hX | TE, λx.tUi]] = hD[[E]]X , λx.D[[t]]X i

Figure 6: Denotations for Names and Configurations
Denotations of machine configurations are constructed from their components: the
configuration’s focus ?, context E, and list of names X. A machine configuration denotes
the translation of its focus applied to three arguments: the base continuation κ0 as its
starting continuation, the denotation of its context, bounded by the redex delimiter 0,
as the metacontinuation, and the size |X| of X plus 1 as its initial prompt. The redex
delimiter attached to the metacontinuation handles the case when an answer subsumes
the entire context by returning the answer as the result. The denotation of the terminal
machine configuration hX | TE, vUi is treated separately to show how it corresponds directly
to a final answer.
Our semantic translation takes advantage of X being a proper list of unique names. Free
active variables denote prompts in our translation, and since 0 is the redex delimiter, we
assign to each variable its 1-based index in X. We use |X|+1 as the global prompt counter to
ensure that no future prompts conflict with the current active variable denotations, thereby
guaranteeing hygiene (see Section 4.5).
Each evaluation context frame denotes a two-element metacontinuation consisting of a
prompt and a proper continuation. The prompt for a binder frame is the prompt translation
ι(x, X) of the bound variable x. The cont and operand frames have redex prompts 0. These
prompts guarantee that answer building operations will arrive at the innermost redex. Each
continuation function specializes a subexpression of the CPS translation for terms D[[·]]X
with the denotations of the context frame’s parts. Compare, for instance, the denotation
of an application, t1 t2 , to that of an operand frame, [ t2 ]. The application term pushes
the global prompt, and executes t1 in the context of a continuation that receives an answer
hka , va i. The denotation of the operand frame is a metacontinuation containing the same
prompt and continuation.
A redex denotes a CPS’ed term that closes over the denotations of its constituents and
implements the corresponding reduction step.
To facilitate our proof of correctness, we make a slight change to the machine semantics.
In the machine, composing an empty context with the current context is an identity operation. The continuation semantics do not share this property. During execution, an empty
continuation is denoted by the base continuation κ0 . If a continuation is captured or pushed
in the context of an empty continuation, then the empty continuation will be captured as
part of the metacontinuation or pushed onto the current metacontinuation before reinstating the pushed continuation. In short, the call-by-need machine semantics guarantees that
E ◦ [ ] = E, but the continuation semantics do not prove that κ0 : γ = γ. Dybvig et al.
discuss the notion of proper tail recursion for delimited continuations. Their operational
characterization of proper tail recursion corresponds to the latter equation.

32

R. GARCIA, A. LUMSDAINE, AND A. SABRY

D[[E ◦ [f ]]]X = D[[[f ]]]X ++D[[E]]X
D[[[ ]]]X = [ ]
D[[[#]]]X = κ0 : [ ]
D[[[ t2 ]]]X = 0 : k ′ : [ ]
where k ′ = λ hka , va i.
pushSubContc ka
(λk2 .
newPromptc
λxp .pushPromptc xp (va xp )
(λfk .fk (λ().D[[t2 ]]X ) k2 ))
κ0
D[[[(λx.) t2 ]]]X = ι(x, X) : k ′ : [ ]
where k ′ = λfk .fk (λ().D[[t2 ]]X ) κ0
D[[[(κx.E) ]]]X = 0 : k ′ : [ ]
where k ′ =
λ hka , va i.
pushSubContc ka
(λk3 .
pushPromptc ι(x, X)
(pushSubContc D[[E]]X
(withSubContc 0 λka .λk.k hka , va i))
(λfk .fk (λ().withSubContc 0 λka .λk.k hka , va i)
k3 ))
κ0

Figure 7: Denotations for Evaluation Contexts
To remove this mismatch, we add a ghost frame [#] to our definition of evaluation
contexts. The ghost frame denotes the metacontinuation κ0 : [ ]. We also extend the unplug
operation on evaluation contexts such that it discards ghost frames: C[[E ◦ [#]]] = C[[E]].
Finally, we alter the right hand side of transition rules that grab and push continuations
to pair ghost frames with composed evaluation contexts in a manner consistent with the
continuation semantics. For instance, the updated D.1 rule is as follows2:
hX | E1 , (κx.E2 ) TE3 , vUid 7−→nam hX | E1 ◦ [#] ◦ E3 ◦ [(λx.) v] ◦ [#] ◦ E2 , vib

(D.1)

These modifications do not alter the observable behavior of the machine while modeling the
property that pushing empty frames has meaning in the continuation semantics.
Given these denotations, it is straightforward to prove correctness of the simulation
relative to the abstract machine.
Theorem 7.1. If t is a closed term, then ΛP [[t]] = Λ[[h∅ | [ ], tif ]].
Proof. ΛP [[t]] = D[[t]]∅ κ0 (0 : [ ]) 1 = Λ[[h∅ | [ ], tif ]].
2The exact placement of ghost frames falls right out of the correctness proof.

LAZY EVALUATION AND DELIMITED CONTROL

33

D[[(κx1 .E1 ) TE2 , λx2 .tU]]X =
pushSubContc D[[E2 ]]X
(λk3 .
pushPromptc ι(x1 , X)
(pushSubContc D[[E1 ]]X
(withSubContc 0 λka .λk.k hka , λx2 .[t℄X i))
(λfk .fk (λ().withSubContc 0 λka .λk.k hka , λx2 .[t℄X i)
k3 ))
D[[TE, λx.t1 U t2 ]]X =
pushSubContc D[[E]]X
(λk2 .
newPromptc
λxp .pushPromptc xp ((λx.D[[t1 ]]X ) xp )
(λfk .fk (λ().D[[t2 ]]X ) k2 ))

Figure 8: Denotations for Redexes
Theorem 7.2. If C1 7−→nam C2 then Λ[[C1 ]] = Λ[[C2 ]].
Proof. By cases on 7−→nam . The proof utilizes beta, eta and K equivalences to establish
correspondences.
8. Simulating Extensions
Many straightforward language extensions also have straightforward simulations under
the above model.
Simulating let bindings essentially performs the same operations as immediately applying a lambda abstraction.
N [[let x = t1 in t2 ]] = let x = newPrompt
in delay N [[t1 ]] as x
in N [[t2 ]]
In contrast to the application rule, the variable x is directly assigned a fresh prompt, rather
than binding it to an auxiliary variable xp . The body of the let can be interpreted in place
and substitution of the prompt is implicit since x is already free in t2 .
The translation for basic constants is analogous to that for lambda abstractions: the
constant must be returned to the next redex.
N [[c]] = return c
For this translation, we assume that the call-by-value language provides the same constants
as the call-by-need language.
The translation for function constants is as follows:
N [[f t]] = do va ⇐ N [[t]]
in return (f va )
Interpreting a function constant application forces its argument and then acts on the value
that is ultimately produced. Since function expressions yield values, the result is immediately returned.

34

R. GARCIA, A. LUMSDAINE, AND A. SABRY

The translation for cons acquires two fresh prompts, uses them to delay the argument
to cons, and stores them as a pair.
N [[cons t1 t2 ]] = let x1 = newPrompt in
let x2 = newPrompt in
delay N [[t1 ]] as x1 in
delay N [[t2 ]] as x2 in
cons x1 x2
The translations for car and cdr evaluate their argument, retrieve a prompt from the
resulting pair, and demand its value.
N [[car t]] = do vp ⇐ N [[t]]
in need (car vp )
N [[cdr t]] = do vp ⇐ N [[t]]
in need (cdr vp )

9. Conclusions
In this paper, we expose and examine the operational structure of lazy evaluation as
embodied in call-by-need semantics. We present this understanding in two ways: as an
abstract machine whose operational behavior involves control capture, and as a simulation
of call-by-need under call-by-value plus delimited control operations. Delimited control can
be used to simulate a global heap, but our particular simulation uses delimited control
operations to manage laziness locally, just like the calculus reduction rules.
The artifacts of this investigation provide new tools for increasing our understanding
of lazy evaluation and its connections to control. The abstract machine could be used to
establish connections to heap-based implementations of call-by-need, and possibly modern
graph-reduction based formulations (Peyton Jones and Salkild, 1989). In fact it seems that
the calculus and abstract machine may point out new structural and dynamic invariants that
are inherent to call-by-need evaluation but are hidden in the unstructured representations
of heaps.
The abstract machine and simulation might also provide new opportunities for reasoning about the correctness of transformations applied to call-by-need programs. Surely the
calculus provides the same equational reasoning powers as the abstract machine. However
the machine may enable researchers to more easily conceive transformations and justifications that are not as easy to recognize in the reduction semantics. Our simulation might be
connected to that of Okasaki et al. (1994). The simulation might suggest new mechanisms
by which to embed call-by-need evaluation within call-by-value programs.
One significant difference between the two formulations of call-by-need lambda calculi (Maraist et al., 1998; Ariola and Felleisen, 1997) is the status of variables. Maraist
et al. consider variables to be values, whereas Ariola and Felleisen do not. Ultimately,
Maraist et al. (1998) prove standardization against a standard-order relation that does not
consider variables to be values. This paper sheds no light on the inclusion of variables
among the values, however it demonstrates in stark detail the consequences of the latter
design. In the abstract machine, the transition rules for lambda terms, namely the rebuild
rules, differ significantly from the transition rules for variables, the need rules. A similar

LAZY EVALUATION AND DELIMITED CONTROL

35

distinction can be seen simply by observing the complexity of their respective translations.
In short, our semantics interpret variables as memoized computations rather than values.
Variables can be treated as values under deterministic call-by-value and call-by-name reduction; it remains an open question whether the same could be achieved for call-by-need
and if so what its operational implications would be.
Our results reveal that a proliferation of semantic frameworks—reduction semantics,
machine semantics, etc—is a boon and not a crisis. The reduction semantics of call-by-need
elegantly and mysteriously encode a rich semantics whose broad implications can be seen in
equivalent machine semantics and continuation semantics. As such, our work provides new
perspectives from which to reason about call-by-need, delimited control, and their respective
expressive powers.
10. Acknowledgements
We thank Daniel P. Friedman, Roshan James, William Byrd, Michael Adams, and
the rest of the Indiana University Programming Languages Group, as well as Jeremy Siek,
Zena Ariola, Phil Wadler, Olivier Danvy, and anonymous referees for helpful discussions
and feedback on this work.
References
Abadi, M., Cardelli, L., Curien, P.-L., and Lévy, J.-J. 1991. Explicit substitutions.
Journal of Functional Programming 1, 4, 375–416.
Ariola, Z. and Klop, J. W. 1994. Cyclic lambda graph rewriting. In Logic in Computer
Science (LICS ’94). IEEE Computer Society Press, Los Alamitos, Ca., USA, 416–425.
Ariola, Z. M. and Felleisen, M. 1997. The call-by-need lambda calculus. Journal of
Functional Programming 7, 3 (May), 265–301.
Ariola, Z. M. and Klop, J. W. 1997. Lambda calculus with explicit recursion. Information and Computation 139, 2, 154–233.
Ariola, Z. M., Maraist, J., Odersky, M., Felleisen, M., and Wadler, P. 1995. A
call-by-need lambda calculus. In POPL ’95: Proceedings of the 22nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages. ACM Press, New York,
NY, USA, 233–246.
Balat, V., Di Cosmo, R., and Fiore, M. 2004. Extensional normalisation and typedirected partial evaluation for typed lambda calculus with sums. In POPL ’04: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages. ACM, New York, NY, USA, 64–76.
Barendregt, H. P. 1981. The Lambda Calculus, its Syntax and Semantics. NorthHolland, Amsterdam, NL. Studies in Logic and the Foundations of Mathematics.
Biernacka, M. and Danvy, O. 2007. A concrete framework for environment machines.
ACM Transactions on Computational Logic 9, 1, 6.
Biernacki, D., Danvy, O., and chieh Shan, C. 2005. On the dynamic extent of
delimited continuations. Information Processing Letters 96, 1, 7 – 17.
Curry, H. B. and Feys, R. 1958. Combinatory Logic, Volume I. Studies in Logic and
the Foundations of Mathematics. North-Holland, Amsterdam. Second printing 1968.

36

R. GARCIA, A. LUMSDAINE, AND A. SABRY

Danvy, O. and Filinski, A. 1990. Abstracting control. In LFP ’90: Proceedings of the
1990 ACM Conference on LISP and Functional Programming. ACM, New York, NY,
USA, 151–160.
Danvy, O., Millikin, K., Munk, J., and Zerny, I. 2010. Defunctionalized interpreters
for call-by-need evaluation. In FLOPS ’10: Proceedings of the Tenth International Symposium on Functional and Logic Programming. Springer-Verlag, London, UK. To appear.
Danvy, O. and Nielsen, L. R. 2004. Refocusing in reduction semantics. Tech. Rep. RS04-26, BRICS, DAIMI, Department of Computer Science, University of Aarhus, Aarhus,
Denmark. November.
Dybvig, R. K., Peyton Jones, S., and Sabry, A. 2007. A monadic framework for
delimited continuations. Journal of Functional Programming 17, 6, 687–730.
Felleisen, M. 1988. The theory and practice of first-class prompts. In POPL ’88: Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages. ACM, New York, NY, USA, 180–190.
Felleisen, M., Findler, R., and Flatt, M. 2009. Semantics Engineering with PLT
Redex. MIT Press, Cambridge, MA.
Felleisen, M. and Friedman, D. P. 1986. Control operators, the SECD-machine, and
the λ-calculus. In Formal Description of Programming Concepts, M. Wirsing, Ed. NorthHolland, Netherlands, 193–217.
Felleisen, M. and Hieb, R. 1992. A revised report on the syntactic theories of sequential
control and state. Theoretical Computer Science 103, 2, 235–271.
Friedman, D. P., Ghuloum, A., Siek, J. G., and Winebarger, O. L. 2007. Improving
the lazy Krivine machine. Higher-Order and Symbolic Computation 20, 3, 271–293.
Friedman, D. P. and Wise, D. S. 1976. CONS should not evaluate its arguments. In
Automata, Languages and Programming, S. Michaelson and R. Milner, Eds. Edinburgh
University Press, Edinburgh, Scotland, 257–284.
Gibbons, J. and Wansbrough, K. 1996. Tracing lazy functional languages. In Proceedings of Conference on Computing: The Australian Theory Symposium, M. E. Houle and
P. Eades, Eds. Australian Computer Science Communications, Townsville, 11–20.
Henderson, P. and Morris, Jr., J. H. 1976. A lazy evaluator. In POPL ’76: Proceedings of the 3rd ACM SIGACT-SIGPLAN Symposium on Principles of Programming
Languages. ACM, New York, NY, USA, 95–103.
Kameyama, Y., Kiselyov, O., and Shan, C. 2008. Closing the stage: From staged code
to typed closures. In PEPM ’08: Proceedings of the 2008 ACM SIGPLAN Symposium on
Partial Evaluation and Semantics-based Program Manipulation. ACM, New York, NY,
USA, 147–157.
Kiselyov, O., Shan, C., Friedman, D. P., and Sabry, A. 2005. Backtracking, interleaving, and terminating monad transformers: (functional pearl). In ICFP ’05: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming.
ACM, New York, NY, USA, 192–203.
Kiselyov, O., Shan, C., and Sabry, A. 2006. Delimited dynamic binding. In ICFP
’06: Proceedings of the eleventh ACM SIGPLAN international conference on Functional
programming. ACM, New York, NY, USA, 26–37.
Krivine, J.-L. 2007. A call-by-name lambda-calculus machine. Higher-Order and Symbolic
Computation 20, 3, 199–207.
Launchbury, J. 1993. A natural semantics for lazy evaluation. In POPL ’93: Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming

LAZY EVALUATION AND DELIMITED CONTROL

37

Languages. ACM, New York, NY, USA, 144–154.
Maraist, J., Odersky, M., and Wadler, P. 1998. The call-by-need lambda calculus.
Journal of Functional Programming 8, 3 (May), 275–317.
Moggi, E. and Sabry, A. 2004. An abstract monadic semantics for value recursion.
Theoretical Informatics and Applications 38, 4, 375–400.
Nakata, K. and Hasegawa, M. 2009. Small-step and big-step semantics for call-by-need.
Journal of Functional Programming 19, 06, 699–722.
Okasaki, C., Lee, P., and Tarditi, D. 1994. Call-by-need and continuation-passing
style. Lisp and Symbolic Computation 7, 1 (Jan.), 57–81.
Peyton Jones, S. L. and Salkild, J. 1989. The spineless tagless G-machine. In FPCA
’89: Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture. ACM, New York, NY, USA, 184–201.
Plotkin, G. D. 1975. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science 1, 2 (Dec.), 125–159.
Sestoft, P. 1997. Deriving a lazy abstract machine. Journal of Functional Programming 7, 3, 231–264.
Shan, C. 2007. A static simulation of dynamic delimited control. Higher-Order and Symbolic Computation 20, 4, 371–401.
Sussman, G. J. and Steele Jr., G. L. 1975. Scheme: An interpreter for extended lambda
calculus. AI Memo 349, Artificial Intelligence Laboratory, Massachusetts Institute of
Technology, Cambridge, Massachusetts. Dec. Reprinted in Higher-Order and Symbolic
Computation 11(4):405–439, 1998, with a foreword (Sussman and Steele Jr., 1998).
Sussman, G. J. and Steele Jr., G. L. 1998. The first report on Scheme revisited.
Higher-Order and Symbolic Computation 11, 4, 399–404.
Wand, M. and Vaillancourt, D. 2004. Relating models of backtracking. In ICFP
’04: Proceedings of the Ninth ACM SIGPLAN International Conference on Functional
Programming. ACM, New York, NY, USA, 54–65.
Wang, C. 1990. Obtaining lazy evaluation with continuations in Scheme. Information
Processing Letters 35, 2, 93–97.
Xi, H. 1997. Evaluation under lambda abstraction. In PLILP ’97: Proceedings of the
Ninth International Symposium on Programming Languages: Implementations, Logics,
and Programs. Springer-Verlag, London, UK, 259–273.

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view
a copy of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a
letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or
Eisenacher Strasse 2, 10777 Berlin, Germany

