A Syntactic Theory of Dynamic Binding.
Dynamic binding, which traditionally has always been associated with Lisp, is still semantically obscure to many. Even though most programming languages favour lexical scope, not only does dynamic binding remain an interesting and expressive programming technique in specialised circumstances, but also it is a key notion in formal semantics. This article presents a syntactic theory that enables the programmer to perform equational reasoning on programs using dynamic binding. The theory is proved to be sound and complete with respect to derivations allowed on programs in dynamic-environment passing style. From this theory, we derive a sequential evaluation function in a context-rewriting system. Then, we further refine the evaluation function in two popular implementation strategies: deep binding and shallow binding with value cells. Afterwards, following the saying that deep binding is suitable for parallel evaluation, we present the parallel evaluation function of a future-based functional language extended with constructs for dynamic binding. Finally, we exhibit the power and usefulness of dynamic binding in two different ways. First, we prove that dynamic binding adds expressiveness to a purely functional language. Second, we show that dynamic binding is an essential notion in semantics that can be used to define exceptions.
Introduction
Dynamic binding has traditionally been associated with Lisp dialects. It appeared in
McCarthy's Lisp 1.0 [24] as a bug and became a feature in all succeeding implemen-
tations, like for instance MacLisp 2 [28], Gnu Emacs Lisp [23]. Even modern dialects
of the language which favour lexical scoping provide some form of dynamic variables,
with special declarations in Common Lisp [43], or even simulate dynamic binding by
lexically-scoped variables as in MITScheme's fluid-let [18].
Lexical scope has now become the norm, not only in imperative languages, but also
in functional languages such as Scheme [39], Common Lisp [43], Standard ML [26], or
Haskell [21]. The scope of a name binding is the text where occurrences of this name refer
to the binding. Lexical scoping imposes that a variable in an expression refers to the
innermost lexically-enclosing construct declaring that variable. This rule implies that
nested declarations follow a block structure organisation. On the contrary, the scope of a
name is said to be indefinite [43] if references to it may occur anywhere in the program.
On the other hand, dynamic binding refers to a notion of dynamic extent. The
dynamic extent of an expression is the lifetime of this expression, starting and ending
when control enters and exits this expression. A dynamic binding is a binding which
exists and can only be used during the dynamic extent of an expression. A dynamic
variable refers to the latest active dynamic binding that exists for that variable [1]. The
expression dynamic scope is convenient to refer to the indefinite scope of a variable with
a dynamic extent [43].
Dynamic binding was initially defined by a meta-circular evaluator [24] and was
later formalised by a denotational semantics by Gordon [15, 16]. It is also part of the
This research was supported in part by EPSRC grant GR/K30773. Author's address: Department
of Electronics and Computer Science, University of Southampton, Southampton
SO17 1BJ. United Kingdom. E-mail: L.Moreau@ecs.soton.ac.uk.
At least, the interpreted mode.
folklore that there exists a translation, the dynamic-environment passing translation,
which translates programs using dynamic binding into programs using lexical binding
only [36, p. 180]. Like the continuation-passing transform [35], the dynamic-passing
translation adds an extra argument to each function, its dynamic environment, and
every reference to a dynamic variable is translated into a lookup in the current dynamic
environment.
The late eighties saw the apparition of "syntactic theories", a new semantic frame-work
which allows equational reasoning on programs using non-functional features like
first-class continuations and state [10, 11, 12, 44]. Those frameworks were later extended
to take into account parallel evaluation [9, 14, 29, 30]. The purpose of this paper
is to present a syntactic theory that allows the user to perform equational reasoning on
programs using dynamic binding. Our contribution is fivefold.
First, from the dynamic-environment passing translation, we construct an inverse
translation. Using Sabry and Felleisen's technique [40, 41], we derive a set of axioms
and define a calculus, which we prove to be sound and complete with respect to the
derivations accepted in dynamic-environment passing style (Section 3).
Second, we devise a sequential evaluation function, i.e. an algorithm, which we prove
to return a value whenever the calculus does so. The evaluation function, which relies
on a context-rewriting technique [11], is presented in Section 4.
Third, in order to strengthen our claim that dynamic binding is an expressive programming
technique and a useful notion in semantics, we give a formal proof of its
expressiveness and use it in the definition of exceptions. In Section 5, we define a relation
of observational equivalence using the evaluation function, and we prove that
dynamic binding adds expressiveness [8] to a purely functional programming language,
by establishing that dynamic binding cannot be macro-expressed in the call-by-value
lambda-calculus. In Section 6, we use dynamic binding as a semantic primitive to formalise
two different models of exceptions: non-resumable exceptions as in ML [26] and
resumable ones as in Common Lisp [43, 34].
Fourth, we refine our evaluation function in the strategy called deep binding , which
facilitates the creation and restoration of dynamic environments (Section 7).
Fifth, we extend our framework to parallel evaluation, based on the future construct
[14, 17, 30]. In Section 8, we define a parallel evaluation function which also relies on
the deep binding technique.
Before deriving our calculus, we further motivate our work by describing three broad
categories of use of dynamic binding: conciseness, control delimiters, and distributed
computing. Let us insist here and now that our purpose is not to denigrate the qualities
of lexical binding, which is the essence of abstraction by its block structure organisation,
but to present a syntactic theory that allows equational reasoning on dynamic binding,
to claim that dynamic binding is an expressive programming technique if used in a
sensible manner, and to show that dynamic binding can elegantly be used to define
semantics of other constructs. Let us note that dynamic binding is found not only in
Lisp but also in T E X [22], Perl [45], and Unix TM shells.
Practical Uses of Dynamic Binding
2.1 Conciseness
A typical use of dynamic binding is a printing routine print-number which requires the
basis in which the numbers should be displayed. One solution would be to pass an explicit
argument to each call to print-number. However, repeating such a programming
pattern across the whole program is the source of programming mistakes. In addition,
this solution is not scalable, because if later we require the print-number routine to
take an additional parameter indicating in which font numbers should be displayed, we
would have to modify the whole program.
Scheme I/O functions take an optional input/output port. The procedures with-
input-from-file and with-output-to-file [39] simulate dynamic binding for these
parameters.
Gnu Emacs [23] is an example of large program using dynamic variables. It contains
dynamic variables for the current buffer, the current window, the current cursor position,
which avoid to pass these parameters to all the functions that refer to them.
These examples illustrate Felleisen's conciseness conjecture [8], according to which
sensible use of expressive programming constructs can reduce programming patterns
in programs. In order to strengthen this observation, we prove that dynamic binding
actually adds expressiveness to a purely functional language in Section 5.
2.2 Control Delimiters
Even though Standard ML [26] is a lexically-scoped language, raised exceptions are
caught by the latest active handler. Usually, programmers install exception handlers for
the duration of an expression, i.e. the handler is dynamically bound during the extent
of the expression. MacLisp [28] and Common Lisp [43] catch and throw, Eulisp let/cc
[34] are other examples of exception-like control operators with a dynamic extent. More
generally, control delimiters are used to create partial continuations, whose different
semantics tolerate various degrees of dynamicness [5, 20, 31, 38, 42].
2.3 Parallelism and Distribution
Parallelism and distribution are usually considered as a possible mean of increasing the
speed of programs execution. However, another motivation for distribution, exacerbated
by the ubiquitous WWW, is the quest for new resources: a computation has to migrate
from a site s 1 to a another site s 2 , because s 2 holds a resource that is not accessible
from s 1 . For our explanatory purpose, we consider a simple resource which is the name
of a computer. There are several solutions to model the name of the running host in a
language; the last one only is entirely satisfactory.
(i) A lexical variable hostname could be bound to the name of the computer whenever
a process is created. Unfortunately, this variable, which may be closed in a closure,
will always return the same value, even though it is evaluated on a different site.
(ii) A primitive (hostname), defined as a function of its arguments only (by ffi in
[35]), cannot return different values in different contexts, unless it is defined as a non-deterministic
function, which would prevent equational reasoning.
(iii) A special form (hostname) could satisfy our goal, but it is in contradiction with
the minimalist philosophy of Scheme, which avoids adding unnecessary special forms.
Furthermore, as we would have to define such a special form for every resource, it would
be natural to abstract them into a unique special form, parameterised by the resource
name: this introduces a new name space, which is exactly what dynamic binding offers.
(iv) Our solution is to dynamically bind a variable hostname with the name of the
computer at process-creation time. Every occurrence of such a variable would refer to
the latest active binding for the variable.
Besides, control of tasks in a parallel/distributed setting usually relies on a notion of
dynamic extent: sponsors [33, 37] allow the programmer to control hierarchies of tasks.
3 A Calculus of Dynamic Binding

Figure

1 displays the syntax of   u , the language accessible to the end user. Let us observe
that the purpose of   u is to capture the essence of dynamic variables and not to propose
a new syntax for them.The language   u is based on two disjoint sets of variables: the
dynamic and static (or lexical) variables. As a consequence, the programmer can choose
between lexical abstractions -x s :M which lexically bind their parameter when applied,
or dynamic abstractions -x d :M , which dynamically bind their parameter. The former
represent regular abstractions of the -calculus [3], while the latter model constructs
like Common Lisp abstractions with special variables [43], or dynamic-scope [6].
Fig. 1. The User Language   u
It is of paramount importance to clearly state the naming conventions that we adopt
for such a language. Following Barendregt [3], we consider terms that are equal up to
the renaming of their bound static variables as equivalent. On the contrary, two terms
that differ by their dynamic variables are not considered as equivalent.
E)
D[[(dlet
Fig. 2. Dynamic-Environment Passing Transform D
In

Figure

2, the dynamic-environment passing translation, which we call D, is a
program transformation that maps programs of   u into the target language deps(  d ), an
extended call-by-value -calculus based on lexical variables only (Figure 3). Intuitively,
each abstraction (static or dynamic) of   u is translated by D into an abstraction taking
an extra dynamic environment in argument; the target language contains a variable e
which denotes an unknown environment. As a result, the application protocol in the
target language is changed accordingly: operator values are applied to pairs. In the
translation of the application, the dynamic environment E is used in the translations
of the operator and operand, and is also passed in argument to the operator. Dynamic
abstractions are translated into abstractions which extend the dynamic environment.
Each dynamic variable is translated into a lookup for the corresponding constant in the
current dynamic environment.
The source language of D extends   u with a dlet construct, (dlet ((x d1
which stands for "dynamic let". Such a construct, inaccessible to the programmer, is
used internally by the system to model the bindings of dynamic variables x di to values
. The syntax of the input language, called   d , appears in Figure 5. Binding lists are
defined with the concatenation operator x, satisfying the following property.
Vn Vn
Evaluation in the target language is based on the set of axioms displayed in the second
part of Figure 3. Applications of binary abstractions require a double fi v -reduction
as modelled by rule (fi \Theta
environment lookup is implemented by (lk 1 ) and (lk 2 ).
Following Sabry and Felleisen, our purpose in the rest of this Section is to derive
the set of axioms that can perform on terms of   d the reductions allowed on terms of
The Language deps(  d
E) j (-y:P )P (Term)
e (Unknown Env. Variable)
Axioms:
(lookup xd (extend E xd W
(lookup xd (extend E xd1 W E) if xd1 6= xd (lk 2 )
(j \Theta
Fig. 3. Syntax and Axioms of the deps(-d )-calculus
Fig. 4. The Inverse Dynamic-Environment Passing Transform D \Gamma1
deps(  d ). More precisely, we want to define a calculus on   d that equationally corresponds
to the calculus on deps(  d ). The following definition of equational correspondence
is taken verbatim from [40].
Definition 1 (Equational Correspondence) Let R and G be two languages with
calculi -XR and -XG . Also let f G be a translation from R to G, and h
be a translation from G to R. Finally let G. Then the calculus
-XR equationally corresponds to the calculus -XG if the following four conditions hold:
1.
2. -XG '
Figure

4 contains an inverse dynamic-environment passing transform mapping terms
of deps(  d ) into terms of   d . The first case is worth explaining: a term (W 1 hE; W 2 i)
represents the application of an operator value W 1 on a pair dynamic environment E and
operand value its inverse translation is the application of the inverse translations
of W 1 and W 2 , in the scope of a dlet with the inverse translation of E. For the following
cases, the inverse translation removes the environment argument added to abstractions,
and translates any occurrence of a dynamic environment into a dlet-expression.
State Space:
(binding list)
Primary Axioms:
(dlet
(dlet
(dlet
(dlet
(dlet
Derived Axioms:
(dlet
Compatibility
(dlet
Fig. 5. Syntax and Axioms of the -d -calculus
If we apply the dynamic-environment passing transform D to a term of   d , and
immediately translate the result back to   d by D \Gamma1 , we find the first six primary
axioms of Figure 5. For explanatory purpose, we prefer to present the derived axioms
(dlet intro 0 ) and (dlet propagate 0 ). The axiom (dlet intro 0 ) is the counterpart of (fi v )
for dynamic abstraction: applying a dynamic abstraction on a value V creates a dlet-
construct that dynamically binds the parameter to the argument V and that has the
same body as the abstraction. Rule (dlet propagate 0 ), rewritten below using the syntactic
sugar let, tells us how to transform an application appearing inside the scope of a dlet.
(dlet
The operator and the operand can each separately be evaluated inside the scope of the
same dynamic environment, and the application of the operator value on the operand
value also appears inside the scope of the same dynamic environment. The interpretation
of (dlet merge), (dlet elim 1 ), (dlet
We can establish the following properties concerning the composition of D and D
Lemma 2 For any term M 2   d , any value V 2 V alue d , any list of bindings
Bind d , for any environment E 2 deps(  d ), let
For any term P 2 deps(  d ), any value W 2 deps(V alue d ), any dynamic
environments
by applying the inverse translation D \Gamma1 to each axiom of deps(- d ), we obtain
the four last primary axioms of Figure 5. Rules (lookup 1 ) and (lookup 2 ) are
the immediate correspondent of (lk 1 ) and (lk 2 ) in deps(- d ), while (fi
0\Omega ) and (j v ) were
axioms discovered by Sabry and Felleisen in applying the same technique to calculi for
continuations and assignments [40].
The intuition of the set of axioms of - d can be explained as follows. In the absence of
dynamic abstractions, - d behaves as the call-by-value -calculus. Whenever a dynamic
abstraction is applied, a dlet construct is created. Rule (dlet propagate 0 ) propagates
the dlet to the leaves of the syntax tree, and replaces each occurrence of a dynamic
variable by its value in the dynamic environment by (lookup 1 ) and (lookup 2 ). Rule
(dlet propagate 0 ) also guarantees that the dynamic binding remains accessible during
the extent of the application of the dynamic abstraction, i.e. until it is deleted by (dlet
us also observe here and now that parallel evaluation is possible because
the dynamic environment is duplicated for the operator and the operand, and both can
be reduced independently. This property will be used in Section 8 to define a parallel
evaluation function. We obtain the following soundness and completeness results:
Lemma 4 (Soundness) For any terms M
for any E 2 deps(  d ), we have that: deps(- d
Lemma 5 (Completeness) For any terms P
The following Theorem is a consequence of Lemmas 2 to 5.
Theorem 1 The calculus - d equationally corresponds to the calculus deps(- d ). 2
Within the calculus, we can define a partial evaluation relation: the value of a program
M is V if we can prove that M equals V in the calculus.
Definition 6 (eval c ) For any program M 2   0
This definition does not give us an algorithm, but it states the specification that must
be satisfied by any evaluation procedure. The purpose of the next Section is to define
such a procedure.
4 Sequential Evaluation
The sequential evaluation function is defined in Figure 6. It relies on a notion of evaluation
context [11]: an evaluation context E is a term with a "hole", [ ], in place of the
next subterm to evaluate. We use the notation E [M ] to denote the term obtained by
placing M inside the hole of the context E . Four transition rules only are necessary: (dlet
intro) and (dlet elim) are derived from the - d -calculus. Rule (lookup) is a replacement
for (dlet propagate), (dlet merge), (dlet lookup 1 ), and (dlet lookup 2 ) of the - d -calculus.
State Space:
alued ::= xs j (-xs:M) j (-xd:M) (Value)
E) j E) (Evaluation Context)
Transition Rules:
Evaluation Function:
For any program M 2   0
error if M 7!
Dynamically Bound Variables: Stuck Terms:
Fig. 6. Sequential Evaluation Function
Intuitively, the value of a dynamic variable is given by the latest active binding for this
variable. In this framework, the latest active binding corresponds to the innermost dlet
that binds this variable. The dynamic extent of a dlet construct is the period of time
between its apparition by (dlet intro) and its elimination by (dlet elim).
The evaluation algorithm introduces the concept of stuck term, which is defined by
the occurrence of a dynamic variable in an evaluation context that does not contain a
binding for it. The evaluation function is then defined as a total function returning a
value when evaluation terminates, ? when evaluation diverges, or error when a stuck
term is reached.
The correctness of the evaluation function is established by the following Theorem,
which relates eval c and eval d . Let us observe that eval c may return a value V 0 that
differs from the value V returned by eval d because the calculus can perform reductions
inside abstractions.
Theorem 2 For any program M 2   0
d , eval c
If we were to implement (lookup), we would start from the dynamic variable to
be evaluated, and search for the innermost enclosing dlet. If it contained a binding
for the variable, we would return the associated value. Otherwise, we would proceed
with the next enclosing dlet. This behaviour exactly corresponds to the search of a
value in an associative list (assoc in Scheme). Such a strategy is usually referred to
as deep binding . In Section 7, we further refine the sequential evaluation function by
making this associative list explicit. But, beforehand, we show that dynamic binding
adds expressiveness to a functional language.
5 Expressiveness
In Section 2.1, we stated that dynamic binding was an expressive programming technique
that, when used in a sensible manner, could reduce programming patterns in
programs. In this Section, we give a formal justification to this statement, by proving
that dynamic binding adds expressiveness [8] to a purely functional language. First, we
define the notion of observational equivalence.
Definition 7 (Observational Equivalence) Given a programming language L and
an evaluation function eval L , two terms are observationally equivalent ,
context C 2 L, such that C[M 1 ] and C[M 1 are both
programs of L, eval L (M 1 ) is defined and equal to V if and only if eval L (M 2 ) is defined
and equal to V . 2
We shall denote the observational equivalences for the call-by-value -calculus and
for the - d -calculus by - =v and - =d , respectively. In order to prove that dynamic binding
adds expressiveness [8] to a purely functional language, let us consider the following
lambda terms, assuming the existence of a primitive cons to construct pairs.
(cons v (f (-d:v))))
The terms are observationnally equivalent in the - v -calculus, i.e. M 1 - =v M 2 , but
we have that M 1
then
This example shows that dynamic binding enables us to distinguish terms that the
call-by-value -calculus cannot distinguish. As a result, - =v 6ae - =d , and using Felleisen's
definition of expressiveness [8, Thm 3.14], we conclude that:
Proposition 1.   v cannot macro-express dynamic binding relative to   d .
6 Semantics of Exceptions
First-class continuations and state can simulate exceptions [13]. We show here that
exceptions can be defined in terms of first-class continuations and dynamic binding.
In the semantics of ML [26], a raised exception returns an exceptional value, distinct
from a normal value, which has the effect to prune its evaluation context until
a handler is able to deal with the exception. By merging the mechanism that aborts
the computation and the mechanism that fetches the handler for the exception, the
handler can no longer be executed in the dynamic environment in which the exception
was raised. As a result, such an approach cannot be used to give a semantics to other
kinds of exceptions, like resumable ones [43].
In order to model the abortive effect, we extend the sequential evaluation function
of Figure 6 with Felleisen and Friedman's abort operator A [11]. For the sake of
simplicity, we assume that there exists only one exception type (discrimination on the
kind of exception can be performed in the handler). We also assume the existence of
a distinguished dynamic variable x ed . In Figure 7, we give the semantics of ML-style
exceptions. When an exception is raised, the latest active handler is called, escapes,
and then applies f in the same dynamic environment as handle, and not in the dynamic
environment where the exception was raised 3 .
On the other hand, there exist other kinds of exceptions, like resumable exceptions,
e.g. Common Lisp resumable errors [43], or Eulisp resumable conditions [34]. They
essentially offer the opportunity to resume the computation at the point where the
exception was raised. In the sequel, we present a variant of Queinnec's monitors [36,
3 The usage of a first-class continuation appears here as the rule for handle duplicates the
evaluation context E. Let us also observe that the continuation is only used in a downward
way, which amounts to popping frames from the stack only.
E[(-xed :M) (-v:A E[(f v)])]
Fig. 7. ML-style exceptions
p. 255], which give the essence of resumable exceptions. The primitives monitor/signal
play the role that handler/raise had for ML-style exceptions. Let us note that signal is a
binary function, which takes not only a value, but also a boolean r indicating whether
the exception should be raised as resumable.
E[(monitor f M)] 7!d E [ (-xed :M) (let (old xed
(if r x
E[(signal r V )] 7!d E[(xed r V )]
Fig. 8. Resumable exceptions
Like handle, monitor installs an exception handler for the duration of a computation.
If an exception is signalled, the latest active handler is called in the dynamic environment
of the signalled exception. If an exception is signalled by the handler itself, it will
be handled by the handler that existed before monitor was called: this is why x ed is
shadowed for the duration of the execution of the handler f , but will be again accessible
if the "normal" computation resumes. If the exception was signalled as resumable, i.e.
if the first argument of signal is true, the value returned by the handler is returned by
signal, and computation continues in exactly the same dynamic environment 4 .
This approach to define the semantics of exception has two advantages, at least.
First, as we model each effect by the appropriate primitive (abortion by A and handler
installation by dynamic binding), we have the ability to model different kinds of
semantics for exceptions. Second, defining the semantics of exceptions with assignments
weakens the theory [12] because assignments break some equivalences that would hold
in the presence of exceptions: so, our definition provides a more precise characterisation
of a theory of exceptions.
Refinement
We refine the evaluation function by representing the dynamic environment explicitly by
an associative list. By separating the evaluation context from the dynamic environment,
we facilitate the design of a parallel evaluation function of Section 8.

Figure

9 displays the state space and transition rules of the deep binding strategy.
The dynamic environment is represented in a new dlet construct which can only appear
at the outermost level of a configuration, called state. The list of bindings ffi can be
regarded as a global stack, initially empty when evaluation starts. A binding is pushed
on the binding list, every time a dynamic abstraction is applied, and popped at the
end of the dynamic extent of the application. In Section 4, the dlet construct was also
modelling the dynamic extent of a dynamic-abstraction application; now that the dlet
construct no longer appears inside terms, we introduce a (pop M) term playing the
same role: it is created when a dynamic abstraction is applied and is destroyed at the
end of the dynamic extent, after popping the top binding of the binding list. Theorem
3 establishes the correctness of the deep binding strategy.
4 Such a semantics assumes that there exists an initial handler in which evaluation can proceed.
State Space:
(Binding list)
E) j E) (Evaluation Context)
Transition Rules:
(dlet
(dlet
(dlet
(dlet ffix((x d V
Evaluation Function:
db (dlet
error if (dlet () M) 7!
Stuck State: S 2 Stuck(  db
Fig. 9. Deep Binding
Theorem 3 eval
The deep binding technique is simple to implement: bindings are pushed on the
binding list ffi at application time of dynamic abstractions and popped at the end of
their extent. However, the lookup operation is inefficient because it requires searching
the dynamic list, which is an operation linear in its length.
There exist some techniques to improve the lookup operation. The shallow binding
technique consists in indexing the dynamic environment by the variable names [1]. A
further optimisation, called shallow binding with value cell is to associate each dynamic
variable with a fixed location which contains the correct binding for that variable: the
lookup operation then simply requires to read the content of that location.
8 Parallel Evaluation
In Section 3, we observed that the axiom (dlet propagate 0 ) was particularly suitable for
parallel evaluation because it allowed the independent evaluation of the operator and
operand by duplicating the dynamic environment. It is well-known that the deep binding
strategy is adapted to parallel evaluation because the associative list representing the
dynamic environment can be shared between different tasks.
As in our previous work [30], we follow the "parallelism by annotation" approach,
where the programmer uses an annotation future [17] to indicate which expressions may
be evaluated in parallel. The semantics of future has been described in the purely functional
framework [14] and in the presence of first-class continuations and assignments
[30]. In

Figure

10, we present the semantics of future in the presence of dynamic binding.
As in [14, 30], the set of terms is augmented with a future construct, and we add to
the set of values a placeholder variable, "which represents the result of a computation
that is in progress". In addition, a new construct (f-let (p M) S) has a double goal: first
as a let, it binds p to the value of M in S; second, it models the potential evaluation of
S in parallel with M . The component M is the mandatory term because it is the first
that would be evaluated if evaluation was sequential, while S is speculative because its
value is not known to be needed before M terminates.
State Space:
Transition Rules:
(dlet
ae
(dlet
(dlet
(dlet
(dlet
ae
(dlet
(dlet
(dlet ffix((x d V
(dlet
error (error)
(dlet
(dlet
(dlet
(dlet
(dlet
Evaluation Function: For any program M 2   0
(dlet
IN such that
(dlet
error if (dlet () M) 7!
error
Fig. 10. Parallel Evaluation (differences with Figure
It is important to observe that (future [ ]) is not a valid evaluation context. Otherwise,
if evaluation was allowed to proceed inside the future body, it could possibly change the
dynamic environment, which would make (fork) unsound. Instead, rule (ltc), which
stands for lazy task creation [27, 7], replaces a (future M) expression by (fmark
which should be interpreted as a mark indicating that a task may be created.
If the runtime elects to create a new task, (fork) creates a f-let expression, whose
mandatory component is the argument of fmark, i.e. the future argument, and whose
speculative component is a new state evaluating the context of fmark filled with the
placeholder variable, in the scope of the duplicated dynamic environment ffi 1 . If the run-time
does not elect to spawn a new task, evaluation can proceed in the fmark argument.
Rules (ltc) and (future id) specify the sequential behaviour of future: the value of
future is the value of fmark, which is the value of its argument.
When the evaluation of the mandatory component terminates, rule (join) substitutes
the value of the placeholder in the speculative state. Rule (speculative) indicates that
speculative transitions are allowed in the f-let body.
Following [14], Figure 10 defines a relation S 1 7! n;m
meaning that n steps are
involved in the reduction from S 1 to S 2 , among which m are mandatory.
The correctness of the evaluation function follows from a modified diamond property
and by the observation that the number of pop terms in a state is always smaller or
equal to the length of the dynamic environment.
Theorem 4 eval
As far as implementation is concerned, rule (ltc) seems to indicate that the dynamic
environment should be duplicated. A further refinement of the system indicates that it
suffices to duplicate a pointer to the associative list, as long as the list remains accessible
in a shared store.
Rule (ltc) adds an overhead to every use of future, by duplicating the dynamic environment
even if dynamic variables are not used. Feeley [7] describes an implementation
that avoids this cost by lazily recreating a dynamic environment when a task is stolen.
Due to the orthogonality between assignments and dynamic binding, our previous
results [30] with assignments can be merged within this framework. Adding assignments
permits the definition of mutable dynamic variables (with a construct like dynamic-set!
[34]). Due to the purely dynamic nature of the semantics, the presence of mutable
dynamic variables offers less parallelism as observed in [30]. The interaction of dynamic
binding and continuations is however beyond the scope of this paper [19].
9 Related Work
In the conference on the History of Programming Languages, McCarthy [25] relates
that they observed the behaviour of dynamic binding on a program with higher-order
functions. The bug was fixed by introducing the funarg device and the function con-
struct[32].
Cartwright [4] presents an equational theory of dynamic binding, but his language
is extended with explicit substitutions and assumes a call-by-name parameter passing
technique. The motivation of his work fundamentally differs from ours: his goal is to
derive a homomorphic model of functional languages by considering - as a combinator.
His axioms are derived from the -oe-calculus axioms, while ours are constructed during
the proof of equational correspondence of the calculus.
The authors of [6] discuss the issue of tail-recursion in the presence of dynamic
binding. They observe that simple implementations of fluid-let [18] are not tail-recursive
because they restore the previous dynamic environment after evaluating the
fluid-let body. Therefore, they propose an implementation strategy, which in essence
is a dynamic-environment passing style solution. Programs in dynamic-environment
passing style are characterised by the fact that they do not require a growth of the
control state for dynamic binding; however, they require a growth of the heap space.
An analogy is the continuation-passing translation, which generates a program where all
function calls are in terminal position although it does not mean that all cps-programs
are iterative. Feeley [7] and Queinnec [36] observe that programs in dynamic-environ-
ment passing style reserve a special register for the current dynamic environment. Since
every non-terminal call saves and then restores this register, such a strategy penalises
programs that do not use dynamic binding, especially in byte-code interpreters where
the marginal cost of an extra register is very high. Both of them prefer a solution that
does not penalise all programs, at the price of a growth of the control state for every
dynamic binding. Consequently, we believe that implementors have to decide whether
dynamic binding should or not increase the control state; in any case, it will result in a
non-iterative behaviour.
In the tradition of the syntactic theories for continuations and assignments, we present
a syntactic theory of dynamic binding. This theory helps us in deriving a sequential
evaluation function and a refined implementation like deep binding. We also integrate
dynamic-binding constructs into our framework for parallel evaluation of future-based
programs.
Besides, we prove that dynamic binding adds expressiveness to purely functional
language and we show that dynamic binding is a suitable tool to define the semantics
of exceptions-like notions. Furthermore, we believe that a single framework integrating
continuations, side-effects, and dynamic binding would help us in proving implementation
strategies of fluid-let in the presence of continuations [19].

Acknowledgement

Many thanks to Daniel Ribbens, Christian Queinnec, and the anonymous referees for
their helpful comments.



--R

Anatomy of Lisp.
Shallow binding in lisp 1.5.
The Lambda Calculus: Its Syntax and Semantics
Lambda: the Ultimate Combinator.
Abstracting Control.
Dynamic Identifiers Can Be Neat.
An Efficient and General Implementation of Futures on Large Scale Shared-Memory Multiprocessors
On the Expressive Power of Programming Languages.
A Reduction Semantics for Imperative Higher-Order Languages
A Syntactic Theory of Sequential State.
A Syntactic Theory of Sequential Control.
The Revised Report on the Syntactic Theories of Sequential Control and State.
Controlling Effects.
The Semantics of Future and Its Use in Program Optimization.
Operational Reasoning and Denotational Semantics.
Towards a Semantic Theory of Dynamic Binding.

MIT Scheme Reference Manual.
Embedding Continuations in Procedural Objects.
Continuations and Concurrency.
Report on the Programming Language Haskell.
The
GNU Emacs Lisp Reference Manual
Recursive Functions of Symbolic Expressions and Their Computation by Machine
History of Lisp.
The Definition of Standard ML.
Lazy Task Creation
Maclisp reference manual.
Sound Evaluation of Parallel Functional Programs with First-Class Contin- uations
The Semantics of Scheme with Future.
Partial Continuations as the Difference of Continu- ations
The function of function in lisp or why the funarg problem should be called the environment problem.
Speculative Computation in Multilisp.
The Eulisp Definition

Lisp in Small Pieces.
Design of a Concurrent and Distributed Lan- guage
A Dynamic Extent Control Operator for Partial Continuations.
Revised 4 Report on the Algorithmic Language Scheme.
The Formal Relationship between Direct and Continuation-Passing Style Optimizing Compilers: a Synthesis of Two Paradigms
Reasoning about Programs in Continuation-Passing Style
Control Delimiters and Their Hierarchies.
The Language.
Rum : an Intensional Theory of Function and Control Abstractions.
Programming Perl.
--TR

--CTR
Christian Queinnec, The influence of browsers on evaluators or, continuations to program web servers, ACM SIGPLAN Notices, v.35 n.9, p.23-33, Sept. 2000
Matthias Neubauer , Michael Sperber, Down with Emacs Lisp: dynamic scope analysis, ACM SIGPLAN Notices, v.36 n.10, October 2001
Gavin Bierman , Michael Hicks , Peter Sewell , Gareth Stoyle , Keith Wansbrough, Dynamic rebinding for marshalling and update, with destruct-time ?, ACM SIGPLAN Notices, v.38 n.9, p.99-110, September
Zena M. Ariola , Hugo Herbelin , Amr Sabry, A type-theoretic foundation of continuations and prompts, ACM SIGPLAN Notices, v.39 n.9, September 2004
Oleg Kiselyov , Chung-chieh Shan , Amr Sabry, Delimited dynamic binding, ACM SIGPLAN Notices, v.41 n.9, September 2006
Magorzata Biernacka , Olivier Danvy, A syntactic correspondence between context-sensitive calculi and abstract machines, Theoretical Computer Science, v.375 n.1-3, p.76-108, May, 2007
dynamic binding and extent;parallelism;functional programming;syntactic theories