A Semantics For Context-Sensitive Reduction Semantics

Download as pdf or txt
Download as pdf or txt
You are on page 1of 15

A Semantics for Context-Sensitive Reduction Semantics

Casey Klein1 , Jay McCarthy2 , Steven Jaconette1 , and Robert Bruce Findler1
1
Northwestern University
2
Brigham Young University

Abstract. This paper explores the semantics of the meta-notation used in the
style of operational semantics introduced by Felleisen and Hieb. Specifically, it
defines a formal system that gives precise meanings to the notions of contexts,
decomposition, and plugging (recomposition) left implicit in most expositions.
This semantics is not naturally algorithmic, so the paper also provides an algo-
rithm and proves a correspondence with the declarative definition.
The motivation for this investigation is PLT Redex, a domain-specific program-
ming language designed to support Felleisen-Hieb-style semantics. This style of
semantics is the de-facto standard in operational semantics and, as such, is widely
used. Accordingly, our goal is that Redex programs should, as much as possible,
look and behave like those semantics. Since Redex’s first public release more than
seven years ago, its precise interpretation of contexts has changed several times,
as we repeatedly encountered reduction systems that did not behave according to
their authors’ intent. This paper describes the culimation of that experience. To
the best of our knowledge, the semantics given here accommodates even the most
complex uses of contexts available.

1 Introduction

The dominant style of operational semantics in use today has at its heart the notion of
a context that controls where evaluation occurs. These contexts allow the designer of
a reduction semantics to factor the definition of a calculus into one part that specifies
the atomic steps of computation and a second part that controls where these steps may
occur. This factoring enables concise specification, e.g., that a language is call-by-value
or call-by-name or call-by-need (Ariola and Felleisen 1997), that if expressions must
evaluate the test position before the branches, and even that exceptions, continuations,
and state (Felleisen and Hieb 1992) behave in the expected ways, all without cluttering
the rules that describe the atomic steps of computation.
Unfortunately, the precise meaning of context decomposition has not been nailed
down in a way that captures its diverse usage in the literature. Although an intuitive
definition is easy to understand from a few examples, this intuition does not cover the
full power of contexts. For example, which terms match the pattern ���� from this
language, in which values and contexts are mutually referential?

������������� ������� ��
���������������� ��
�������� ��� ���������� ��
And which terms match this bizarre, small language?
���������� ���������
To remedy this lack, we have developed a semantics for matching and reduction that
not only supports these exotic languages but also captures the intuitive meanings of
countless existing research papers. This semantics does not assume explicit language-
specific definitions of plugging and decomposition, since most expositions leave these
concepts implicit.
Our motivation for studying context-sensitive matching is its implementation in the
domain-specific programming language Redex (Felleisen et al. 2010; Matthews et al.
2004). Redex is designed to support the semantics engineer with a lightweight toolset
for operational semantics and related formalisms. Specifically, Redex supports rapid
prototyping of context-sensitive operational semantics, random testing, automatic type-
setting, and, via its embedding in Racket, access to a large palette of standard program-
ming tools. Redex is widely used, having supported several dozen research papers as
well as the latest Scheme standard (Sperber et al. 2007) and a number of larger models,
including one of the Racket virtual machine (Klein et al. 2010).
In keeping with the spirit of Redex, we augment a standard proof-based validation
of our work with testing. More concretely, in addition to proving a correspondence
between a specification of context-sensitive matching and an algorithm for that spec-
ification, we have conducted extensive testing of the semantics, using a Redex model
of Redex (there is little danger of meta-circularity causing problems, as the embedding
uses a modest subset of Redex’s functionality—notably, no contexts or reduction rela-
tions). This model allows us to test that our semantics gives the intended meanings to
interesting calculi from the literature, something that would be difficult to prove.
The remainder of this paper builds up an intuitive understanding of what contexts
are and how they are used via a series of examples, gives a semantics for Redex’s
rewriting system, and discusses an algorithm to implement the semantics.

2 Matching and Contexts


This section introduces the notion of contexts and explains through a series of examples
how matching works in their presence. Each example comes with a lesson that informs
the design of our context-sensitive reduction semantics semantics.
In its essence, a pattern of the form ����
matches an expression when the expression can �������� � �����������
be split into two parts, an outer part (the context) �������� � ������� � �������
that matches � and an inner part that matches
�. The outer part marks where the inner part ���� ������� ���������
appears with a hole, written �� . In other words,
������������� ����������
when thinking of an expression as a tree, match-
ing against ���� finds some subtree of the ex- Figure 1: Arithmetic Expressions
pression that matches �, and then replaces that
sub-term with a hole to build a new expression in such a way that the new expression
matches � .
To get warmed up, consider figure 1. In this language � matches addition expres-
sions and � matches contexts for addition expressions. More precisely, � matches an
addition expression that has exactly one hole. For example, the expression �� � ��
matches ���� three ways, as shown in figure 2. Accordingly, the reduction relation
given in figure 1 reduces addition expressions wherever they appear in an expression,
e.g., reducing �� �� � �� �� � ��� to two different expressions, �� � �� � ��� and
�� �� � �� �� . This example tells us that our context matching semantics must support
multiple decompositions for any given term.
A common use of contexts is to restrict the
places where reduction may occur in order to � = �� � = �� � ��
model a realistic programming language’s or- � = �� �� �� � = �
der of evaluation. Figure 3 gives a definition of � = �� � ��� � = �
� that enforces call-by-value left-to-right order
of evaluation. For example, consider this nested
Figure 2: Example Decomposition
set of function calls, ��� �� �� ��� , in which the
result of �� �� is passed to the result of �� �� . It decomposes into the context ��� �� ��� ,
allowing evaluation in the first position of the application. It does not, however, decom-
pose into the context ��� �� ��� , since the grammar for � allows the hole to appear in
the argument position of an application expression only when the function position is
already a value. Accordingly, the reduction system insists that the call to � happens be-
fore the call to � . This example tells us that our semantics for decomposition must be
able to support multiple different ways to decompose each expression form, depending
on the subexpressions of that form (application expressions in this case).
Contexts can also be used in clever ways to
model the call-by-need λ-calculus. Like call-by- �������� ����������
name, call-by-need evaluates the argument to a �������� ��� ����������������
function only if the value is actually needed by �������� ������� �������
the function’s body. Unlike call-by-name, each
function argument is evaluated at most once. A Figure 3: λ-calculus
typical implementation of a language with call-
by-need uses state to track if an argument has been evaluated, but it is also possible to
give a direct explanation, exploiting contexts to control where evaluation occurs.
Figure 4 shows the contexts from Ariola and
Felleisen (1997)’s model of call-by-need. The �������������� ������� ��
first three of � ’s alternatives are standard, al- ������ ��� �� ��
lowing evaluation in the argument of the �� ������ ��� ����� ��
primitive, as well as in the function position of
an application (regardless of what appears in the Figure 4: Call-by-need Contexts
argument position). The fourth alternative allows
evaluation in the body of a � -expression that is in the function position of an applica-
tion. Intuitively, this case says that once we have determined the function to be applied,
then we can begin to evaluate its body. Of course, the function may eventually need its
argument, and at that point, the final alternative comes into play. It says that when an
applied function needs its argument, then that argument may be evaluated.
As an example, the expression ��� ��� ��� ��� ��� ��� reduces by simplifying
the body of the � -expression to � , without reducing the argument, because it decom-
poses into this context ��� ��� ��� ��� ��� using the fourth alternative of � . In con-
trast, ��� ��� ��� ��� ��� ��� reduces to ��� ��� ��� ��� �� because the body of the
� -expression decomposes into the context ��� ��� with � in the hole, and thus the entire
expression decomposes into the context ��� ��� ��� ��� ��� . This use of contexts tells
us that our semantics must be able to support a sophisticated form of nesting, namely
that sometimes a decomposition must occur in one part of a term in order for a decom-
position to occur in another.
When building a model of first-class
continuations, there is an easy connec- ���������������������������� ��
tion to make, namely that an evaluation
context is itself a natural representation
���������� ��� ���� ����� ����
� �������� � �� ��� � ����
for a continuation. That is, at the point
that a continuation is grabbed, the con-
text in which it is grabbed is the con- Figure 5: Continuations
tinuation. Figure 5 extends the left-to-
right call-by-value model in figure 3 with support for continuations. It adds ������� , the
operator that grabs a continuation, and the new value form ����� �� that represents a
continuation and can be applied to invoke the continuation.
For example, the expression ��� �������� �� ��� �� ����� reduces by grabbing a
continuation. In this model that continuation is represented as ����� ��� ���� , which
is then applied to ������� ’s argument in the original context, yielding the expression
��� ��� ��� �� ��� ����� ��� ������ . The next step is to substitute for � , which yields
the expression ��� ������ ��� ���� ��� . This expression has a continuation value in
the function position of an application, making the next step invoke the continuation. So,
we can simply replace the context of the continuation invocation with the context inside
the continuation, plugging the argument passed to the continuation in the hole, yielding
��� �� . This reduction system tells us that our context decomposition semantics must
be able to support contexts that appear in a term that play no part in any decomposition
(and yet must still match a specified pattern, such as � ).
Generalizing from ordinary continuations to
delimited continuations is simply a matter of fac- ��������������� ��
toring the contexts into two parts, one that may ������������������������������ ��
contain prompts and one that may not. Figure 6 �������� ������� �������
shows one way to do this, as an extension of the �������������� ���
call-by-value lambda calculus from figure 3.
The non-terminal � matches an arbitrary eval-
���� ������������ �����
���� ���� ����� ������
uation context and � matches an evaluation con-
text that does not contain any prompt expres-
sions. Accordingly, the rule for grabbing a con- Figure 6: Delimited Continuations
tinuation exploits this factoring to record only
the portion of the context between the call to ��������� and the nearest enclosing
prompt.
The interesting aspect of this system is how � refers to � and how that makes it
difficult to support an algorithm that matches � . For all of the example systems in this
section so far, a matching algorithm can match a pattern of the form ���� by attempting
to match � against the entire term and, once a match has been found, attempting to
match what appeared at the hole against �. With � , however, this leads to an infinite
loop because � expands to a decomposition that includes � in the first position.3
A simple fix that works for the delimited
continuations example is to backtrack when en- ���������� ���������
countering such cycles; that fix, however, does �������� �������
not work for the first definition of � given in fig-
ure 7. Specifically, � would match only �� with
Figure 7: Wacky Context
an algorithm that treats that cycle as a failure to
match, but the context �� ��� should match � ,
and more generally, the two definitions of � in figure 7 should be equivalent.

3 A Semantics for Matching


This section formalizes the notion of matching ����������� � ��
used in the definitions of the example reduction sys- ����
tems in section 2. For ease of presentation, we stick ����
to the core language of patterns and terms in figure 8. ����������
Redex supports a richer language of patterns (notably �������� � ��
including a notion of Kleene star), but this core cap- ��������� � ��
tures an essence suitable for explaining the semantics �������
of matching. �������� � ��
Ignoring embedded contexts, a term � is simply ������ ��
a binary tree where leaf nodes are atoms � and inte- ����������� � ��
rior nodes are constructed with ���� . A context � is �������� � ��
similarly a binary tree, but with a distinguished path �������
(marked with ���� and �����) from the root of the con- � � ��������
text to its ����.
� � ���������
Contexts are generated by decomposition and rep-
� � �������������
resent single-holed contexts. Although the ���� can
appear multiple times in a single term, such terms Figure 8: Patterns and Terms
represent expressions that contain multiple, indepen-
dently pluggable contexts.
Patterns � take one of six forms. Atomic patterns � and the ���� pattern match only
themselves. A pattern ����� � �� binds the pattern variable � to the term matched
by � . Repeated pattern variables force the corresponding sub-terms to be identical. A
pattern ��� �� matches terms that match any of the alternatives of the non-terminal �
(defined outside the pattern). We write decomposition patterns p1 [p2 ] using a separate
keyword for clarity: �������� �� ��� . Finally, interior nodes are matched by the pattern
����� �� ���, where �� and �� match the corresponding sub-terms.
3
Some find the equivalent, non-problematic grammar �������������� ��� clearer. At least
one author of the present paper (who has spent a considerable amount of time hacking on
Redex’s implementation, no less), however, does not and was surprised when Redex failed to
terminate on a similar example. We have also received comments from Redex users who were
surprised by similar examples, suggesting that Redex should support such definitions.
For example, the left-hand side of the reduction rule in figure 1 corresponds to the
following pattern, where the literal ����� is used for the empty sequence and the
pattern ������ matches literal numbers:
�������� ����� � ��� ���
����� �
����� ����� ������� �������
����� ����� ������� �������
���������
Figure 9 gives a semantics for patterns via the judgment form � � ��������� , which
defines when the pattern � matches the term � . The grammar � is a finite map from
non-terminals to sets of patterns. The bindings � is a finite map from pattern variables
to terms showing how the pattern variables of � can be instantiated to yield � . The
� � ��������� judgment relies on an auxiliary judgment � � ����������������� that per-
forms decompositions. Specifically, it holds when � can be decomposed into a context
� that matches � and contains the sub-term �� at its hole.
Many of the rules for these two judgment forms rely on the operator � . It combines
two mappings into a single one by taking the union of their bindings, as long as the
domains do not overlap. If the domains do overlap, then the corresponding ranges must
be the same; otherwise � is not defined. Accordingly, rules that use � apply only when
� is well-defined.
The � � ��������� rules are organized by the structure of � . The atom and hole rules
produce an empty binding map because those pattern contain no pattern variables. The
���� rule matches � with � and produces a map extended with the binding ������ .
The �� rule applies if any of the non-terminal’s alternatives match. The scope of an
alternative’s pattern variables is limited to that alternative, and consequently, the �� rule
produces an empty binding map. The ���� rule matches the sub-terms and combines
the resulting sets of bindings. The ������� rule uses the decomposition judgment form
to find a decomposition and checks that the term in the hole matches ��.
The rules for the � � �������� ��������� form are also organized around the pattern.
The ���� decomposition rule decomposes any term � into the empty context and �
itself. The first of two ���� decomposition rules applies when a decomposition’s focus
may be placed within a pair’s left sub-term. This decomposition highlights the same
sub-term ��� as the decomposition of �� does, but places it within the larger context
����� � ��� . The second of the ���� decomposition rules does the same for the pair’s
right sub-term. The �� decomposition rule propagates decompositions but, as in the
corresponding matching rule, ignores binding maps.
The ������� decomposition rule performs a nested decomposition. Nested decom-
position occurs, for example, when decomposing according to call-by-need evaluation
contexts (see the last production in figure 4). The ������� rule decomposes � into a
composed context �������� and a sub-term �� , where �� and �� match �� and �� re-
spectively. The definition of context composition (figure 9, bottom-right) follows the
path in �� . The ���� decomposition rule is similar to the corresponding matching
rule, but it introduces a binding to the context that is matched, not the entire term.
� � ��������� � � ��������� � � ���������������

� � ���������
� � ��������� � ������������� � �

� � ���� � � ���������
� � ������� ������

� � ������������ � � ������������ � ���������������������


� � �� �� ����������� �� �������� � ��

� � �������������������� � � ������������
� � ������������� �� �������� � ��
� � �����������������

� � ����������������������

� � ��������������������� � � ������������ � ���������������������


� � �� �� ����������� � ���������������� �� �������� � ��

� � ������������ � � ��������������������� � ���������������������


� � �� �� ������������ �� ��������������� �� �������� � ��

� � ���� � � ������������������
� � ���������������� ������

� � �������������������� � � ���������������������
� � ����������������������������� �� �������� � ��

� � ������������������
� � ������������������ � ������������� � �

��������� ��� �
� � ������������ � ����
����� �� �������� ��� ����� ���������� ��
� � �������� � �
������ � ��������� ��� ������ � �����������

Figure 9: Matching and Decomposition


4 An Algorithm for Matching

The rules in figure 9 provide a declarative definition of context-sensitive matching, but


they do not lead directly to a tractable matching algorithm. There are two problems.
First, as reflected in the two ���� decomposition rules, an algorithm cannot know a
priori whether to match on the left and decompose on the right or to decompose on the
left and match on the right. An implementation that tries both possibilities scales ex-
ponentially in the number of nested ���� patterns matched (counting indirect nesting
through non-terminals). Second, the rules provide no answer to the question of whether
to proceed in expanding a non-terminal if none of the input term has been consumed
since last encountering that non-terminal. This question arises, for example, when de-
composing by the non-terminal � from the grammar in figure 6, since � ’s second
alternative causes the ������� rule to decompose the same term by � . This second
problem is the manifestation of left recursion in the form of grammars we consider.
The first problem can be solved by matching and decomposing simultaneously.
Since these tasks differ only in their treatment of ���� patterns, much work can be
saved by sharing intermediate results between the tasks. Figure 10 demonstrates this
approach with a function � that returns a set of pairs ������ representing possible ways
to match or decompose the input term. In a pair representing a match, � is the marker
�; in a pair representing a decomposition, � is a pair ������ such that the input term can
be decomposed into a context � and a sub-term � occurring in � ’s hole.
The first two � cases handle the pattern ����. If the term in question is also ����,
then it may be considered either to match ���� or to decompose into ���� in the empty
context. If the term is not ����, then only decomposition is possible. The third case
handles atomic patterns by producing a match result only if the given term is identical
to the atom.
The (meta) context in which a call to � appears may eventually discard some or
all of the results it receives. For example, consider the fourth clause, which handles
���� patterns. If the term is also a pair (constructed with any of ���� , ���� , or �����),
then this case makes two recursive calls and examines the cross product of the results
using the ������ helper function. For each result pair, the case merges their bindings
and checks that the results are not both decompositions. If neither is a decomposition,
������ combines the pair into a match result; if exactly one is a decomposition, it
extends the decomposition with the term matched by the non-decomposition. If both
are decompositions, then the match fails.
The next case, for patterns �������� �� ��� , recurs with �� and the input term, ex-
pecting to receive decompositions. For each one, it makes another recursive call, this
time with �� and the sub-term in the decomposition’s focus. Each of the latter call’s
results � is combined with the decomposition’s context, yielding a match result if � is
a match and a larger context if � is a decomposition.
The remaining three cases are straightforward. The ���� case recurs on the sub-
pattern and extends the bindings of each of the results with either the matched term
or the context carved out by the decomposition. The �� case tries each alternative,
discarding the binding component of each result. The final case, a catch-all, applies
when the pattern does not match or decompose the input term.
������� � � � � � ���� ������������
����������� �� ��� ��� ���� ������ � ����� �� ���� ����������������

� � � � � � ����
����� ����� ������ ��� �������������������� �������
����� ����� ��� ��� ����������������
����� �� ��� ��� ��������
����� ����� �� ���� �� �� ����� ��� ��������� � � ������� ������ �������
� � ����������� ��� ��� �����
��� �� � ���
�������� � ����� ��� �����
�������� � ����� ��� �����
����� �������� �� ���� ��� ��� ��������� ��� ����������� �����
��� �� � ���
�������� � ����� ��� �� ���
������� ����� � � ����� �� � ����
����� ����� � ��� ��� ��� ���������� ���� �������������� ����� � ��
������ � ����� �� ����
����� ��� ��� ��� ��� ��������� ������ � ����� �� ���� � � �����
����� �� ��� ��� ��

������ � � � � � � ����
����������� �� ��� ��� ��� ���
���������� �������� ��� ���
� ��� ������� � ����������
����������� �� ��� ���������
� ��� �������� �� ���������
����������� �������� ��� �� ������� ��� ��
� � �

������� � � � � �
����������� ��� ��� �
������������ ��������� ��� �������������
����� � � � � �
��������� ��� ��� �
��������������� ���� ��� �

Figure 10: Core matching algorithm (cases apply in order)


Putting aside the problem of left recursion, the call ����� �� ��� computes the set
of � such that � � ��������� or � � �������� ��������� for some � and �� , and the top-
level wrapper function ������� restricts this set to the bindings associated with match
derivations.
To make this precise, we first give a definition of left-recursion. Intuitively, a gram-
mar is left-recursive if there is a way, in a straight-forward recursive parser, to get from
some non-terminal back to that same non-terminal without consuming any input. So,
our definition of left-recursion builds a graph from the grammar by connecting each
pattern to the other patterns that might reached without consuming any input, and then
checks for a cycle in the graph. The most interesting case is the last one, where an
������� pattern is connected to its second argument when the first argument can gen-
erate ����.

Definition. A grammar G is left recursive if p →∗G p for some p, where →∗G is the
transitive (but not reflexive) closure of →G ⊆ p × p, the least relation satisfying the
following conditions:

1. (nt n) →G p if p ∈ G(n),
2. (name n p) →G p.
3. (in-hole p p0 ) →G p,
4. (in-hole p p0 ) →G p0 if G ` hole : p | b, and

Theorem. For all G, p, and t, if G is not left recursive, then b ∈ matchesJG, p, tK ⇔


G ` t : p | b.

The complete proof is available at eecs.northwestern.edu/~robby/plug/.


Parsing algorithms that support left recursive context-free grammars go back nearly
fifty years (Kuno 1965). We refer the reader to Frost et al. (2007, section 3) for a sum-
mary. We have implemented an extension of the packrat parsing algorithm (Warth et
al. 2008) that dynamically detects left recursion and treats the choice leading to it as
a failure. If the other choices for the same portion of the input make any progress at
all, the algorithm repeats the parse attempt, in hopes that the entries added to the memo
table during the failed attempt will cause a second attempt to succeed. This process con-
tinues as long as repeated attempts make additional progress. Extending the algorithm
in figure 10 with a similar iterative phase allows matching of terms from left recursive
grammars, such the ones in figure 6 and figure 7.

5 A Semantics for Reduction

We now put the notion of matching from section 3 to work in a formalization of the
standard notation for context-sensitive reduction rules. As with patterns, we consider
a core specification language that lacks many of the conveniences of a language like
Redex but nevertheless highlights the principal ideas.
Figure 11 shows our definition. A user of Redex specifies a grammar and rules of
the shape � �, each consisting of a pattern � and a term template �. Redex uses the
judgment form in the upper-left corner of the figure to determine if a particular term �
�������
�������
� � ��������� ������������� ��� ������� ��
������� � ��
� � ����� ������ ����������� � ��
�������� � ��
� � ���

���� � � � � �
�������� ��� ��� �
����������� ��� ��� ����
���������� ��� ��� ��� ����
�������������� �� ���� ��� ��� ��������������� ���� ��������� �����
����������� �� ���� ��� ��� ��������������� ���� ��������� �����
���������� � ��� ��� ��� ������������� ����

���� � � � � �
����������� ��� ��� �
����������� �� ���� ��� ��� ����� ��������� ��� ���
����������� �� ���� ��� ��� ����� ��������� ��� ���
������������ �� ���� ��� ��� ������ �� ��������� ����
������������ �� ���� ��� ��� ����� �� ��������� ����

���� � � � � �
�������� ��� ��� ����� � �� ��������������� �
�������� ��� ��� ������ � �� ��������������� �
��������� ���� ��� ����� �� ���

� � ������� � � �
�������������������������������������������������

�������� �� �������� ��
�������� � �������� ����� �� ���

Figure 11: A semantics for reduction (function cases apply in order)


reduces to �� by the given rule. The grammar in the figure’s top-right gives the syntax for
term templates, which include atoms, the context ����, references to variables bound by
the left-hand side, applications of meta-level functions (e.g., substitution), hole-filling
operations, and pairing operations.
The rest of the figure defines template instantiation. Atoms and ���� instantiate to
themselves, variables instantiate to their values, and meta-applications instantiate to the
result of applying the meta-function to the instantiated argument template.
The instantiation of ������� templates makes use of a generic ���� function that
accepts a context and a term and returns the result of plugging the context with the term.
When ����’s second argument is a context, it constructs a larger context by concatenat-
ing the two contexts, preserving the path to the hole. The path extension is necessary,
for example, to support the following rule for an unusual control operator:
����������� ��� ���� ����� �������

When ����’s second argument is some non-context term, it replaces the ���� or �����
constructor with ���� , producing a non-context term.
Insistence that ����’s first argument be a context creates a potential problem for
rules which extend contexts, like this one for another unusual control operator:
����������� ��� ���� ����� ��� �����

Although the rule does not explicitly define a path for the extended context ��� �� ,
one can be safely inferred, since the term paired with � has no pluggable sub-terms.
The case of the ���� function for ���� templates performs this inference via the
function ���� . When given a context and a term containing no contexts, ���� extends
the context’s path through the extra layer. When both arguments contain contexts, ����
combines the terms with ���� , preventing possible ambiguity in a subsequent plugging
operation.
Note, however, that the embedded contexts themselves remain pluggable by reduc-
tion rules and meta-functions that later pick apart the result term. For example, consider
the rule for yet another unusual control operator:
����������� ��� ���� ������ ����� �� ����� ��������

This rule calls � with a pair of continuation values. The term denoting this pair is not
itself pluggable, but the embedded contexts can be plugged by subsequent reduction
steps, after they are extracted by the reduction rules for projecting ����� components.
In addition to these contrived reduction rules, the semantics in figure 11 supports all
of the systems in section 2, as well as the most sophisticated uses of contexts we have
encountered in the literature, specifically:
– Ariola and Felleisen (1997)’s core call-by-need calculus. Their extension of this
calculus to letrec uses decomposition in fundamentally the same way, but the
particular formulation they choose makes use of pattern-matching constructs or-
thogonal to the ones we describe here, namely associative-commutative matching
and a Kleene star-like construct that enforces dependencies between adjacent terms.
The examples directory distributed with Redex shows one way to define their le-
trec evaluation contexts without these constructs, which Redex does not currently
support.
– Flatt et al. (2007)’s semantics for delimited control in the presence of dynamic
binding, exception handling, and Scheme’s dynamic-wind form.
– Chang and Felleisen (2011)’s call-by-need calculus, which defines evaluation con-
texts using a heavily left-recursive grammar.

6 Related Work

Barendregt (1984) makes frequent use of a notion of contexts specialized to λ-terms.


Like ours, these contexts may contain multiple holes, but plug’s behavior differs in that
it fills all of the context’s holes. Felleisen and Hieb (1992) exploit the power of a selec-
tive notion of context to give equational semantics for many aspects of programming
languages, notably continuations and state. The meaning of multi-holed grammars does
not arise in their work, since the grammar for contexts restricts them to exactly one
hole.
Lucas (1995) later explored an alternative formulation of selective contexts. This
formulation defines contexts not by grammars but by specifying, for each function sym-
bol, which sub-term positions may be reduced. Because the specification depends only
on the function symbol’s identity (i.e., and not on its sub-terms), this formulation can-
not express common evaluation strategies, such as left-to-right, call-by-value evalua-
tion. Follow-up work on this form of context-sensitive rewriting focuses on tools for
proving termination, generally a topic of limited interest when studying reduction sys-
tems designed to model a programming language since these systems are not expected
to terminate.
As part of their work on SL, a meta-language similar to Redex, Xiao et al. (2001)
define a semantics for Felleisen-Hieb contexts by translating grammars into their own
formalism, an extension of finite tree automata. This indirect approach allows SL to
prove decomposition lemmas automatically using existing automata algorithms, but it
is considerably more complicated than our approach and does not allow for multi-holed
grammars like the ones in figure 5 and figure 6.
Dubois (2000) develops the first formulation of a Felleisen-Hieb reduction seman-
tics in a proof assistant, as part of a mechanized proof of the soundness of ML’s type
system. Her formulation encodes single-hole contexts as meta-level term-to-term func-
tions (restricted to coincide with the usual grammar defining call-by-value evaluation)
and therefore models plug as meta-application. The formulation does not use an explicit
notion of decomposition; instead, the contextual closure reduction rule applies to terms
that may be formed using the plug operation.
Berghofer’s, Leroy’s, and Xi’s solutions to the POPLmark Challenge (Aydemir et
al. 2005) use Dubois’s encoding for the challenge’s reduction semantics. Vouillon’s
solution uses a first-order encoding of contexts and therefore provides an explicit defi-
nition of plugging. The other submitted solutions use structural operational semantics,
do not address dynamic semantics at all, or are no longer available online.
Danvy and Nielsen (2004) and Sieczkowski et al. (2010) provide an axiomatization
of the various components of a Felleisen-Hieb reduction semantics, such as a decom-
position relation, that together define the semantics. This axiomatization is not an ap-
propriate basis for Redex for two reasons. First, it requires users to specify plugging
and decomposition explicitly. Common practice leaves these definitions implicit, and
one of our design goals for Redex is to support conventional definitions. Second, the
axiomatization requires decomposition to be a (single-valued) function, ruling out the
semantics in figure 1 and, more problematically, reduction semantics for multi-threaded
programs and programs in languages like C and Scheme, which do not specify an order
of evaluation for application expressions.
More broadly speaking, there are hundreds4 of papers that use evaluation context
semantics to model programming languages for just as many different purposes. Al-
though we have not implemented anywhere near all of them in Redex, we have sought
out interesting and non-standard ones over the years to try them out and to build our
intuition about how a semantics should behave.

Acknowledgments Thanks to Stephen Chang for his many interesting examples of con-
texts that challenged our understanding of context-sensitive matching. Thanks also to
Matthias Felleisen and Matthew Flatt for helpful discussions of the work.

A version of this paper can be found online at:

http://www.eecs.northwestern.edu/~robby/plug/

That web page contains the final version of the paper as it appears in the proceedings
and the Redex models for all of the figures in this paper.

Bibliography
Zena M. Ariola and Matthias Felleisen. The Call-by-Need Lambda-Calculus. J. Functional Pro-
gramming 7(3), pp. 265–301, 1997.
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce,
Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve
Zdancewic. Mechanized Metatheory for the Masses: The POPLmark Challenge. In Proc.
Intl. Conf. Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science
volume 3603, pp. 50–65, 2005.
H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North Holland, 1984.

4
There are more than 400 citations to the original Felleisen-Hieb paper; while evaluation-
context based semantics are still widely used, the paper is now rarely cited as it has become a
standard part of the programming languages landscape.
Stephen Chang and Matthias Felleisen. The Call-by-need Lambda Calculus. Unpublished
Manuscript, 2011.
Olivier Danvy and Lasse R. Nielsen. Refocusing in Reduction Semantics. Aarhus University,
BRICS RS-04-26, 2004.
Catherine Dubois. Proving ML Type Soundness within Coq. In Proc. Intl. Conf. Theorem Proving
in Higher Order Logics, Lecture Notes in Computer Science volume 1869, pp. 126–144,
2000.
Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. Semantics Engineering with PLT
Redex. MIT Press, 2010.
Matthias Felleisen and Robert Hieb. The Revised Report on the Syntactic Theories of Squential
Control and State. Theoretical Computer Science 103(2), pp. 235–271, 1992.
Matthew Flatt, Gang Yu, Robert Bruce Findler, and Matthias Felleisen. Adding Delimited and
Composable Control to a Production Programming Environment. In Proc. ACM Intl. Conf.
Functional Programming, pp. 165–176, 2007.
Richard A. Frost, Rahmatullah Hafiz, and Paul C. Callaghan. Modular and Efficient Top-Down
Parsing for Ambiguous Left-Recursive Grammars. In Proc. International Conference on
Parsing Technology, pp. 109–120, 2007.
Casey Klein, Matthew Flatt, and Robert Bruce Findler. The Racket Virtual Machine and Ran-
domized Testing. 2010. http://plt.eecs.northwestern.edu/racket-machine/
Susumu Kuno. The Predictive Analyzer and a Path Elimination Technique. Communications of
the ACM 8(7), pp. 453–462, 1965.
Salvador Lucas. Fundamentals of Context-Sensitive Rewriting. In Proc. Seminar on Current
Trends in Theory and Practice of Informatics, Lecture Notes in Computer Science volume
1012, pp. 405–412, 1995.
Jacob Matthews, Robert Bruce Findler, Matthew Flatt, and Matthias Felleisen. A Visual En-
vironment for Developing Context-Sensitive Term Rewriting Systems. In Proc. Intl. Conf.
Rewriting Techniques and Applications, Lecture Notes in Computer Science volume 3091,
pp. 301–311, 2004.
Filip Sieczkowski, Malgorzata Biernacka, and Dariusz Biernacki. Automating Derivations of
Abstract Machines from Reduction Semantics: A Generic Formalization of Refocusing in
Coq. In Proc. Symp. Implementation and Application of Functional Languages, To appear
in Lecture Notes in Computer Science, 2010.
Michael Sperber, R. Kent Dybvig, Matthew Flatt, Anton van Straaten, Richard Kelsey, William
Clinger, Jonathan Rees, Robert Bruce Findler, and Jacob Matthews. Revised [6] Report on
the Algorithmic Language Scheme. Cambridge University Press, 2007.
Alessandro Warth, James R. Douglass, and Todd Millstein. Packrat Parsers Can Support Left
Recursion. In Proc. ACM SIGPLAN Wksp. Partial Evaluation and Program Manipulation,
pp. 103–110, 2008.
Yong Xiao, Amr Sabry, and Zena M. Ariola. From Syntactic Theories to Interpreters: Automating
the Proof of Unique Decomposition. Higher-Order and Symbolic Computation 14(4), pp.
387–409, 2001.

You might also like