A Semantics For Context-Sensitive Reduction Semantics
A Semantics For Context-Sensitive Reduction Semantics
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.
� � ���������
� � ��������� � ������������� � �
� � ���� � � ���������
� � ������� ������
� � �������������������� � � ������������
� � ������������� �� �������� � ��
� � �����������������
� � ����������������������
� � ���� � � ������������������
� � ���������������� ������
� � �������������������� � � ���������������������
� � ����������������������������� �� �������� � ��
� � ������������������
� � ������������������ � ������������� � �
��������� ��� �
� � ������������ � ����
����� �� �������� ��� ����� ���������� ��
� � �������� � �
������ � ��������� ��� ������ � �����������
� � � � � � ����
����� ����� ������ ��� �������������������� �������
����� ����� ��� ��� ����������������
����� �� ��� ��� ��������
����� ����� �� ���� �� �� ����� ��� ��������� � � ������� ������ �������
� � ����������� ��� ��� �����
��� �� � ���
�������� � ����� ��� �����
�������� � ����� ��� �����
����� �������� �� ���� ��� ��� ��������� ��� ����������� �����
��� �� � ���
�������� � ����� ��� �� ���
������� ����� � � ����� �� � ����
����� ����� � ��� ��� ��� ���������� ���� �������������� ����� � ��
������ � ����� �� ����
����� ��� ��� ��� ��� ��������� ������ � ����� �� ���� � � �����
����� �� ��� ��� ��
������ � � � � � � ����
����������� �� ��� ��� ��� ���
���������� �������� ��� ���
� ��� ������� � ����������
����������� �� ��� ���������
� ��� �������� �� ���������
����������� �������� ��� �� ������� ��� ��
� � �
������� � � � � �
����������� ��� ��� �
������������ ��������� ��� �������������
����� � � � � �
��������� ��� ��� �
��������������� ���� ��� �
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
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 �
�������
�������
� � ��������� ������������� ��� ������� ��
������� � ��
� � ����� ������ ����������� � ��
�������� � ��
� � ���
���� � � � � �
�������� ��� ��� �
����������� ��� ��� ����
���������� ��� ��� ��� ����
�������������� �� ���� ��� ��� ��������������� ���� ��������� �����
����������� �� ���� ��� ��� ��������������� ���� ��������� �����
���������� � ��� ��� ��� ������������� ����
���� � � � � �
����������� ��� ��� �
����������� �� ���� ��� ��� ����� ��������� ��� ���
����������� �� ���� ��� ��� ����� ��������� ��� ���
������������ �� ���� ��� ��� ������ �� ��������� ����
������������ �� ���� ��� ��� ����� �� ��������� ����
���� � � � � �
�������� ��� ��� ����� � �� ��������������� �
�������� ��� ��� ������ � �� ��������������� �
��������� ���� ��� ����� �� ���
� � ������� � � �
�������������������������������������������������
�������� �� �������� ��
�������� � �������� ����� �� ���
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
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.
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.